Commit ae1207f9 by Raphael Rieu-Helft

### Remove the need for the new assertions in reflection example

parent 95d5a31f
 ... ... @@ -30,7 +30,7 @@ val add (a b: t) : t val mul (a b: t) : t ensures { forall v: cvars. interp result v = interp a v * interp b v } raises { Unknown -> true } (* removing this is ok ??? *) raises { Unknown -> true } val opp (a:t) : t ensures { forall v: cvars. interp result v = - (interp a v) } ... ... @@ -687,7 +687,7 @@ use import real.RealInfix use import real.FromInt use import int.Abs meta coercion function from_int (*meta coercion function from_int*) type t = (int, int) type rvars = int -> real ... ... @@ -941,11 +941,11 @@ end module MP64Coeffs use mach.int.UInt64 as M use import int.Int use import real.RealInfix use import real.FromInt use import real.PowerReal use RationalCoeffs as Q use import int.Int type evars = int -> int ... ... @@ -1173,9 +1173,7 @@ use LinearDecisionRationalMP as R use import real.FromInt use import real.PowerReal use import real.RealInfix axiom pow_from_int: forall x y: int. 0 <= x -> 0 <= y -> pow (from_int x) (from_int y) = from_int (power x y) use import int.Int use import list.List ... ... @@ -1281,7 +1279,19 @@ goal g: forall i x c r: int. goal g': forall a b i j: int. 0 <= i -> 0 <= j -> (power radix i) * a = b -> i = j -> (power radix j) * a = b i+1 = j -> (power radix j) * a = radix*b end module TI use import real.RealInfix use import int.Int (*constant y : real = 0.0 + 0.0*) constant x : int = 0 + 0 goal g: True end \ No newline at end of file
 ... ... @@ -150,10 +150,10 @@ ... ... @@ -1164,7 +1164,7 @@ ... ... @@ -1174,24 +1174,24 @@ ... ... @@ -1222,10 +1222,10 @@ ... ... @@ -1262,10 +1262,10 @@ ... ... @@ -1357,25 +1357,25 @@ ... ... @@ -1650,7 +1650,7 @@ ... ... @@ -1735,7 +1735,7 @@ ... ... @@ -1833,7 +1833,7 @@ ... ... @@ -1866,7 +1866,7 @@ ... ... @@ -1895,7 +1895,7 @@ ... ... @@ -1943,13 +1943,13 @@ ... ... @@ -1973,13 +1973,13 @@ ... ... @@ -2103,7 +2103,7 @@ ... ... @@ -2190,10 +2190,10 @@ ... ... @@ -2211,7 +2211,7 @@ ... ... @@ -2285,7 +2285,7 @@ ... ... @@ -2388,7 +2388,7 @@ ... ... @@ -2438,7 +2438,7 @@ ... ... @@ -2480,7 +2480,43 @@ ... ...
No preview for this file type
 ... ... @@ -432,14 +432,11 @@ module N variant { sz - !i } label StartLoop in lx := get_ofs x !i; assert { (pelts x)[offset x + !i] = !lx }; let (res, carry) = add_with_carry !lx !c limb_zero in set_ofs r !i res; assert { value r !i + (power radix !i) * !c = value x !i + y }; assert { res + radix * carry = !lx + !c }; (* add_with_carry post *) c := carry; assert { (pelts r)[offset r + !i] = res }; value_tail r !i; value_tail x !i; assert { value r (!i+1) + (power radix (!i+1)) * !c ... ...
This diff is collapsed.
No preview for this file type
 ... ... @@ -2,7 +2,7 @@ module TestInt32 use import int.Int use import mach.int.Int32 use import mach.int.Int32BV let mask_111 (x: int32) : int32 ensures { 0 <= to_int result < 8 } ... ...
 ... ... @@ -151,7 +151,19 @@ let rec reify_term renv t rt = | Papp (cs, _) -> t_app cs [trv] rty | Pvar _ -> trv | _ -> assert false in let t = t_label ?loc:t.t_loc Slab.empty t in let rec rm t = let t = match t.t_node with | Tapp (f,tl) -> t_app f (List.map rm tl) t.t_ty | Tvar _ | Tconst _ -> t | Tif (f,t1,t2) -> t_if (rm f) (rm t1) (rm t2) | Tbinop (op,f1,f2) -> t_binary op (rm f1) (rm f2) | Tnot f1 -> t_not (rm f1) | Ttrue | Tfalse -> t | _ -> t (* FIXME some cases missing *) in t_label ?loc:t.t_loc Slab.empty t in let t = rm t in (* remove labels to identify terms that are equal modulo labels *) if Mterm.mem t renv.store then ... ... @@ -274,22 +286,24 @@ let rec reify_term renv t rt = let (renv, rg) = invert_interp renv leq t in let renv = { renv with subst = Mvs.add g rg renv.subst } in if debug then Format.printf "filling context@."; let rec add_to_ctx (renv, ctx) e = try match e.t_node with | Tquant _ | Teps _ -> (renv, ctx) | Tbinop (Tand,e1,e2) -> add_to_ctx (add_to_ctx (renv, ctx) e1) e2 | _ -> let (renv,req) = invert_interp renv leq e in (renv,(t_app cons [req; ctx] (Some ty_list_g))) with | NoReification -> renv,ctx in let renv, ctx = task_fold (fun (renv,ctx) td -> match td.td_node with | Decl {d_node = Dprop (Paxiom, _, e)} -> begin try (match e.t_node with | Tquant _ | Teps _ | Tbinop _ -> renv, ctx | _ -> let (renv,req) = invert_interp renv leq e in (renv,(t_app cons [req; ctx] (Some ty_list_g)))) with | NoReification -> renv,ctx (* | TypeMismatch _ -> raise NoReification*) end -> add_to_ctx (renv, ctx) e | _-> renv,ctx) (renv, (t_app nil [] (Some ty_list_g))) renv.task in { renv with subst = Mvs.add l ctx renv.subst } ... ...
 ... ... @@ -37,7 +37,7 @@ module C val incr (p:ptr 'a) (ofs:int32) : ptr 'a requires { p.offset + ofs <= plength p } ensures { result.offset = p.offset + Int32.to_int ofs } ensures { result.offset = p.offset + ofs } ensures { plength result = plength p } ensures { pelts result = pelts p } ensures { result.data = p.data } ... ... @@ -48,8 +48,8 @@ module C ensures { result = (pelts p)[p.offset] } let get_ofs (p:ptr 'a) (ofs:int32) : 'a requires { 0 <= p.offset + Int32.to_int ofs < plength p } ensures { result = (pelts p)[p.offset + Int32.to_int ofs] } requires { 0 <= p.offset + ofs < plength p } ensures { result = (pelts p)[p.offset + ofs] } = get (incr p ofs) val set (p:ptr 'a) (v:'a) : unit ... ... @@ -58,9 +58,10 @@ module C writes { p.data.elts } let set_ofs (p:ptr 'a) (ofs:int32) (v:'a) : unit requires { 0 <= p.offset + Int32.to_int ofs < plength p } requires { 0 <= p.offset + ofs < plength p } ensures { pelts p = Map.set (pelts (old p)) (p.offset + Int32.to_int ofs) v } (p.offset + ofs) v } ensures { (pelts p)[p.offset + ofs] = v } writes { p.data.elts } = set (incr p ofs) v ... ... @@ -78,7 +79,7 @@ module C val malloc (sz:uint32) : ptr 'a requires { sz > 0 } ensures { plength result = UInt32.to_int sz \/ plength result = 0 } ensures { plength result = sz \/ plength result = 0 } ensures { result.offset = 0 } val free (p:ptr 'a) : unit ... ... @@ -87,16 +88,16 @@ module C ensures { plength p = 0 } val realloc (p:ptr 'a) (sz:int32) : ptr 'a requires { Int32.to_int sz > 0 } (* for simplicity, though 0 is legal in C *) requires { sz > 0 } (* for simplicity, though 0 is legal in C *) requires { p.offset = 0 } requires { plength p > 0 } writes { p.data } ensures { plength result = Int32.to_int sz \/ plength result = 0 } ensures { plength result = Int32.to_int sz -> plength p = 0 } ensures { plength result = Int32.to_int sz -> forall i:int. 0 <= i < plength (old p) /\ i < Int32.to_int sz -> ensures { plength result = sz \/ plength result = 0 } ensures { plength result = sz -> plength p = 0 } ensures { plength result = sz -> forall i:int. 0 <= i < plength (old p) /\ i < sz -> (pelts result)[i] = (pelts (old p))[i] } ensures { plength result <> Int32.to_int sz -> p = old p } ensures { plength result <> sz -> p = old p } val predicate is_not_null (p:ptr 'a) : bool ensures { result <-> plength p <> 0 } ... ...