dependent types and modular arithmetics

[cmp xchg]

today i read the blog post about dependent types and ats [1]

the following function was given:

fun add_int {m,n:int} (a: int m, b: int n): int (m + n) = a + b

however, i assume that the sort (n:int) uses infinite precision integers whereas

the type of a uses 32bit ints. then the dependent type int(m+n) only holds if

the addition does not wrap. i tried the following example which should not compile,

but it does. that is bad because accessing an array in (gtz) would lead to crashes.

#include "share/atspre_define.hats"

#include "share/atspre_staload.hats"

fun gtz {n:int| n>0 } ( a: int(n) ) : int(n) = a where {

    val () = println!("a=", a)

}

fun add {m,n:int} ( a: int(m), b: int(n) ) : int(m+n) = a+b

implmnt main0 ( ) = {

    val () = println!("1+2=", add(1,2))

    val () = println!("=", add(0x80000000, 0x80000000))

    val n = add(0x80000000, 0x7fffffff)

    val n = gtz(n)

    //val m = add(1,~1)

    //val m = gtz(m)

}

$ ./test

1+2=3

=0

a=-1

or did i misunderstood something?

[1](https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html)

[gmhwxi]

There was some discussion on arithmetic overflow in the following
archive:

https://sourceforge.net/p/ats-lang/mailman/ats-lang-users/?viewmonth=201304

Try to search 'overflow' to find those messages.

Your observation is correct: static '+' and dynamic '+' do not agree.
So the type-soundness of ATS needs to assume that no arithmetic overflow
happens at run-time (if you use '+'). However, this is not a fundamental limitation of ATS.

######

Here is an example that shows a way to address the arith overflow issue:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/arith_overflow.dats

When doing binary search, the middle point can be computed using
(l+r)/2, where l and r are left and right indices, respectively.
But (l+r) may overflow. The above example shows a way to capture
this potential overflow. To address this issue, one can use l+(r-l)/2 
instead of (l+r)/2, and the example verifies it.

[cmp xchg]

hmm. but why didn't you choose the technique presented in your example

for implementing at least array access in the main library? it seems to me

that the current situation is even worse than in plain c. at least the current

design decisions should be mentioned in the tutorial/introduction sections? 

[gmhwxi]

The technique for addressing integer overflow in a general setting
seems too costly. ATS is already very complex at this point.

The mismatch between the statics and the dynamics is explicitly mentioned.
For instance, it is mentioned in the last paragraph of the following article:

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2403.html

I want re-emphasize that this mismatch is primarily for the purpose of
making ATS more accessible. One can and probably should build his or her own
arithmetic API in ATS when using ATS for critical low-level programming. It is even better if one
is willing to share as well.

[cmp xchg]

ok. i missed that. however the claim "...constraint-solver that uses machine-level arithmetic can 

be incorrect (but I have so far not knowingly encountered such a situation in practice)..." seems 

a bit too optimistic. there are and were many remote-code-execution vulnerabilities related to

this. and i would like to use ats to absolutely make this impossible. (which is doable but not

using the standard library)

i understand that the internal (custom) constraint solver is of limited expressiveness. would it be

possible to map modular arithmetic onto SMT+QF_BV (quantifier free bitvector-arithmetic)? 

z3, boolector and many others have support for this. ideally an external solver could be avoided. 

is it possible to teach QF_BV to the internal solver in finite time and effort?

http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

example:

fun {m,n:bv32} bvadd ( a:bv32(m), b:bv32(n) ) : bv32(bvadd(m,n))

anyway, thanks for the great work on ats. especially the template system is something not

seen in other languages. (however reminding me a bit of lisp's dynamic-bind)

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/PREd1G9K0Aw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/bcb8969a-29a8-4fa4-b196-1180de54ade5%40googlegroups.com.

[Chris Double]

On Fri, Jan 5, 2018 at 11:07 AM, cmp xchg <c0mp...@gmail.com> wrote:
>
> example:
>
> fun {m,n:bv32} bvadd ( a:bv32(m), b:bv32(n) ) : bv32(bvadd(m,n))

IIRC, William Blair did some work on an experimental prelude that used
bv32 with the original work on using Z3 as an external solver. You can
see some of it in 'contrib':

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/wdblair/prelude/SATS/integer.sats

I'm not sure if the current Z3 solver work exposes bv32, etc.

--
http://bluishcoder.co.nz

[gmhwxi]

Right now, I feel that the best way to do this is using the following
package to turn ATS typechecking constraints into smt-lib2 format:

https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-smt2

Then use a solver like Z3 or CVC4 to solve these constraints externally.

The current implementation of ATS2 is not very modular. It is difficult to
write a plug-in solver for it (even if I myself want to do it). If there would ever
be ATS3, we should have further discussion on this issue :)

On Thursday, January 4, 2018 at 5:07:55 PM UTC-5, cmp xchg wrote:

ok. i missed that. however the claim "...constraint-solver that uses machine-level arithmetic can 

be incorrect (but I have so far not knowingly encountered such a situation in practice)..." seems 

a bit too optimistic. there are and were many remote-code-execution vulnerabilities related to

this. and i would like to use ats to absolutely make this impossible. (which is doable but not

using the standard library)

i understand that the internal (custom) constraint solver is of limited expressiveness. would it be

possible to map modular arithmetic onto SMT+QF_BV (quantifier free bitvector-arithmetic)? 

z3, boolector and many others have support for this. ideally an external solver could be avoided. 

is it possible to teach QF_BV to the internal solver in finite time and effort?

http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

example:

fun {m,n:bv32} bvadd ( a:bv32(m), b:bv32(n) ) : bv32(bvadd(m,n))

anyway, thanks for the great work on ats. especially the template system is something not

seen in other languages. (however reminding me a bit of lisp's dynamic-bind)