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)}
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.
--
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.
ok. i missed that. however the claim "...constraint-solver that uses machine-level arithmetic canbe incorrect (but I have so far not knowingly encountered such a situation in practice)..." seemsa bit too optimistic. there are and were many remote-code-execution vulnerabilities related tothis. and i would like to use ats to absolutely make this impossible. (which is doable but notusing the standard library)i understand that the internal (custom) constraint solver is of limited expressiveness. would it bepossible 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?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 notseen in other languages. (however reminding me a bit of lisp's dynamic-bind)