Commit da67461f authored by Andrei Paskevich's avatar Andrei Paskevich

examples: use pure { .. } or {..} for lsymbols

parent 12340a86
......@@ -46,14 +46,14 @@ module MonoidSumDef
let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t
variant { length s }
= if length s = 0 then zero else op (f s[0]) (agg f s[1 ..])
= if pure { length s = 0 } then {zero} else {op} (f s[0]) (agg f s[1 ..])
lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty
let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a)
ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) }
variant { length s1 }
= if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2
= if pure { length s1 <> 0 } then let s3 = s1[1 ..] in agg_cat f s3 s2
clone MonoidSum as MS with type M.t = M.t,
constant M.zero = M.zero,
......
......@@ -216,7 +216,7 @@ module PQueue
use import seq.Occ
let ghost function to_bag (s:seq 'a) : 'a -> int =
fun x -> occ x s 0 (length s)
fun x -> pure { occ x s 0 (length s) }
let lemma to_bag_mem (x:'a) (s:seq 'a)
ensures { s.to_bag x > 0 <-> exists i. 0 <= i < length s /\ s[i] = x}
......@@ -278,7 +278,7 @@ module PQueue
ensures { forall d. 0 <= t.bag d <= t.card }
ensures { t.card >= 0 /\ (t.card > 0 -> t.bag t.minimum > 0) }
ensures { forall d. 0 < t.bag d -> CO.le t.minimum.key d.key }
= if t.m.card > 0
= if pure { t.m.card > 0 }
then let r0 = Sel.default_split () in
let _ = Sel.split r0 () t in
()
......
......@@ -135,7 +135,7 @@ module MapBase
requires { selection_possible () s /\ domain s k }
ensures { forall i. 0 <= i < length s /\ CO.eq s[i].key k -> result = s[i] }
= let j = ref 0 in
while not CO.eq s[!j].key k do
while not {CO.eq} s[!j].key k do
invariant { 0 <= !j < length s }
invariant { CO.le s[!j].key k }
variant { length s - !j }
......
......@@ -34,7 +34,7 @@ module Compile_aexpr
| Asub a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 -- $ isubf ()
| Amul a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 -- $ imulf ()
end in
hoare trivial_pre c (aexpr_post a c.wcode.length)
hoare {trivial_pre} c ({aexpr_post} a c.wcode.length)
(* Check that the above specification indeed implies the
natural one. *)
......@@ -83,7 +83,7 @@ module Compile_bexpr
| Bfalse -> $ if cond then inil () else ibranchf ofs
| Bnot b1 -> $ compile_bexpr b1 (not cond) ofs
| Band b1 b2 ->
let c2 = $ compile_bexpr b2 cond ofs % exec_cond b1 true in
let c2 = $ compile_bexpr b2 cond ofs % {exec_cond} b1 true in
let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
$ compile_bexpr b1 false ofs -- c2
| Beq a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
......@@ -91,8 +91,9 @@ module Compile_bexpr
| Ble a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
$ if cond then iblef ofs else ibgtf ofs
end in
let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length in
hoare trivial_pre c post
let ghost post =
{bexpr_post} b cond (c.wcode.length + ofs) c.wcode.length in
hoare {trivial_pre} c post
(* Check that the above specification implies the natural one. *)
let compile_bexpr_natural (b:bexpr) (cond:bool) (ofs:ofs) : code
......@@ -146,11 +147,11 @@ module Compile_com
meta rewrite_def function loop_invariant
function loop_variant (c:com) (test:bexpr) : post 'a =
fun _ _ msj msi -> let VMS pj sj mj = msj in let VMS pi si mi = msi in
fun _ _ msj msi -> let VMS _pj _sj mj = msj in let VMS _pi _si mi = msi in
ceval mi c mj /\ beval mi test
lemma loop_variant_lemma : forall c test,x:'a,p msj msi.
loop_variant c test x p msj msi =
let VMS pj sj mj = msj in let VMS pi si mi = msi in
let VMS _pj _sj mj = msj in let VMS _pi _si mi = msi in
ceval mi c mj /\ beval mi test
meta rewrite lemma loop_variant_lemma
......@@ -174,20 +175,20 @@ module Compile_com
| Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
let code_true = $ compile_com cmd1 -- $ ibranchf code_false.code.length in
$ compile_bexpr cond false code_true.wcode.length --
(code_true % exec_cond cond true) --
($ code_false % exec_cond_old cond false)
(code_true % {exec_cond} cond true) --
($ code_false % {exec_cond_old} cond false)
| Cwhile test body ->
let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test false body_length in
let ofs = length code_test.code + body_length in
let wp_while = $ code_test --
($ code_body -- $ ibranchf (- ofs)) % exec_cond test true in
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
$ inil () -- make_loop wp_while inv (exec_cond test true) var
($ code_body -- $ ibranchf (- ofs)) % {exec_cond} test true in
let ghost inv = {loop_invariant} cmd in
let ghost var = {loop_variant} body test in
$ inil () -- make_loop wp_while inv ({exec_cond} test true) var
end in
hoare (com_pre cmd) res (com_post cmd res.wcode.length)
hoare ({com_pre} cmd) res ({com_post} cmd res.wcode.length)
(* Get back to natural specification for the compiler. *)
let compile_com_natural (com: com) : code
......
......@@ -69,7 +69,7 @@ module Compiler_logic
ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length }
ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
let res = { wcode = code; wp = {seq_wp} s1.wcode.length s1.wp s2.wp } in
assert { forall x: 'a, p post ms. res.wp x p post ms ->
not (exists ms'. post ms' /\ contextual_irrelevance res.wcode p ms ms') ->
(forall ms'. s2.wp (x,ms) (p + s1.wcode.length) post ms' /\
......@@ -91,7 +91,7 @@ module Compiler_logic
let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a
ensures { result.wp --> fork_wp s.wp cond }
ensures { result.wcode.length --> s.wcode.length }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
= { wcode = s.wcode; wp = {fork_wp} s.wp cond }
(* WP transformer for hoare triples. *)
function towp_wp (pr:pre 'a) (ps:post 'a) : wp_trans 'a =
......@@ -107,7 +107,7 @@ module Compiler_logic
let ($_) (c:hl 'a) : wp 'a
ensures { result.wcode.length --> c.code.length }
ensures { result.wp --> towp_wp c.pre c.post }
= { wcode = c.code; wp = towp_wp c.pre c.post }
= { wcode = c.code; wp = {towp_wp} c.pre c.post }
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
......@@ -156,7 +156,7 @@ module Compiler_logic
(ghost var:post {'a}) : wp 'a
ensures { result.wp --> loop_wp c.wp inv cont var }
ensures { result.wcode.length --> c.wcode.length }
= let wpt = loop_wp c.wp inv cont var in
= let wpt = pure { loop_wp c.wp inv cont var } in
assert { forall x p q ms0. wpt x p q ms0 ->
forall ms. inv x p ms -> acc (var x p) ms ->
exists ms'. contextual_irrelevance c.wcode p ms ms' /\ q ms'
......
......@@ -23,7 +23,7 @@ module VM_instr_spec
ensures { result.pre --> pre }
ensures { result.post --> ifun_post f }
ensures { result.code --> code_f }
= let res = { pre = pre; code = code_f; post = ifun_post f } in
= let res = { pre = pre; code = code_f; post = {ifun_post} f } in
assert { forall x p ms. res.pre x p ms ->
not (exists ms' : machine_state. res.post x p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
......@@ -43,7 +43,9 @@ module VM_instr_spec
ensures { result.pre --> trivial_pre }
ensures { result.post --> iconst_post n }
ensures { result.code.length --> 1 }
= hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post
= hoare {trivial_pre}
($ ifunf {trivial_pre} n.iconst n.{iconst_fun})
n.{iconst_post}
(* Ivar spec *)
function ivar_post (x:id) : post 'a =
......@@ -58,7 +60,9 @@ module VM_instr_spec
ensures { result.pre --> trivial_pre }
ensures { result.post --> ivar_post x }
ensures { result.code.length --> 1 }
= hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
= hoare {trivial_pre}
($ ifunf {trivial_pre} x.ivar x.{ivar_fun})
x.{ivar_post}
(* Binary arithmetic operators specification (Iadd, Isub, Imul)
via a generic builder. *)
......@@ -87,7 +91,9 @@ module VM_instr_spec
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post op }
ensures { result.code.length --> code_b.length }
= hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post
= hoare {ibinop_pre}
($ ifunf {ibinop_pre} code_b op.{ibinop_fun})
op.{ibinop_post}
constant plus : binop = fun x y -> x + y
meta rewrite_def function plus
......@@ -102,19 +108,19 @@ module VM_instr_spec
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post plus }
ensures { result.code.length --> 1 }
= create_binop iadd plus
= create_binop iadd {plus}
let isubf () : hl 'a
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post sub }
ensures { result.code.length --> 1 }
= create_binop isub sub
= create_binop isub {sub}
let imulf () : hl 'a
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post mul }
ensures { result.code.length --> 1 }
= create_binop imul mul
= create_binop imul {mul}
(* Inil spec *)
function inil_post : post 'a =
......@@ -125,7 +131,7 @@ module VM_instr_spec
ensures { result.pre --> trivial_pre }
ensures { result.post --> inil_post }
ensures { result.code.length --> 0 }
= { pre = trivial_pre; code = Nil; post = inil_post }
= { pre = {trivial_pre}; code = Nil; post = {inil_post} }
(* Ibranch specification *)
function ibranch_post (ofs: ofs) : post 'a =
......@@ -140,8 +146,8 @@ module VM_instr_spec
ensures { result.pre --> trivial_pre }
ensures { result.post --> ibranch_post ofs }
ensures { result.code.length --> 1 }
= let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
hoare trivial_pre cf (ibranch_post ofs)
= let cf = $ ifunf {trivial_pre} ofs.ibranch ofs.{ibranch_fun} in
hoare {trivial_pre} cf ofs.{ibranch_post}
(* Conditional jump specification via a generic builder. *)
type cond = int -> int -> bool
......@@ -167,8 +173,8 @@ module VM_instr_spec
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post cond ofs }
ensures { result.code.length --> code_cd.length }
= let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
hoare ibinop_pre c (icjump_post cond ofs)
= let c = $ ifunf {ibinop_pre} code_cd ({icjump_fun} cond ofs) in
hoare {ibinop_pre} c ({icjump_post} cond ofs)
(* binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
constant beq : cond = fun x y -> x = y
......@@ -187,25 +193,25 @@ module VM_instr_spec
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post beq ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibeq ofs) beq ofs
= create_cjump (ibeq ofs) {beq} ofs
let ibnef (ofs:ofs) : hl 'a
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post bne ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibne ofs) bne ofs
= create_cjump (ibne ofs) {bne} ofs
let iblef (ofs:ofs) : hl 'a
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post ble ofs }
ensures { result.code.length --> 1 }
= create_cjump (ible ofs) ble ofs
= create_cjump (ible ofs) {ble} ofs
let ibgtf (ofs:ofs) : hl 'a
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post bgt ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibgt ofs) bgt ofs
= create_cjump (ibgt ofs) {bgt} ofs
(* Isetvar specification *)
constant isetvar_pre : pre 'a =
......@@ -228,7 +234,7 @@ module VM_instr_spec
ensures { result.pre --> isetvar_pre }
ensures { result.post --> isetvar_post x }
ensures { result.code.length --> 1 }
= let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
hoare isetvar_pre c (isetvar_post x)
= let c = $ ifunf {isetvar_pre} x.isetvar x.{isetvar_fun} in
hoare {isetvar_pre} c x.{isetvar_post}
end
......@@ -57,8 +57,7 @@ module Esterel
let res = bw_or a.bv (neg a.bv) in
assert { eq_sub_bv res zeros zeros p_bv };
assert { eq_sub_bv res ones p_bv (sub size_bv p_bv) };
{ bv = res;
mdl = interval p size }
{ bv = res; mdl = pure {interval p size} }
let maxUnion (a b : s) : s (* operator [(a|b)&(a|-a)&(b|-b)] *)
......
......@@ -13,15 +13,17 @@ module Tarski
use import set.Fset
clone export relations.PartialOrder
constant a : set t
val constant a : set t
constant e : t
val constant e : t
axiom minimality: mem e a /\ forall x. mem x a -> rel e x
function f t : t
val function f t : t
axiom range: forall x. mem x a -> mem (f x) a
axiom monotone: forall x y. mem x a -> mem y a -> rel x y -> rel (f x) (f y)
val (=) (a b: t) : bool ensures { result <-> a = b }
predicate fixpoint (x:t) = mem x a /\ f x = x
end
......
......@@ -222,7 +222,7 @@ module N
res := one;
raise Break
end;
acc := !acc + power base (to_int !i) * to_int x[!i];
acc := !acc + power {base} (to_int !i) * to_int x[!i];
done;
raise Break
with Break -> !res
......
......@@ -79,7 +79,7 @@ let lemma ground_app (t1 t2 : term)
requires { ground (App t1 t2) }
ensures { ground t1 }
ensures { ground t2 }
= ground_rec_app t1 t2 no_bound
= ground_rec_app t1 t2 {no_bound}
(* substitution of [x] by [s] in [t].
......
......@@ -199,7 +199,7 @@ module Lemmas
= match st with
| Nil -> ()
| Cons E st' -> inverse_inverse st' c1 c2 c3
| Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
| Cons f st' -> if {even_forest} f then () else inverse_inverse st' c1 c2 c3
end
inductive sub stack (forest int) coloring =
......
This diff is collapsed.
......@@ -38,7 +38,7 @@ module SimplePrioriyQueue
let create (n: int) (dummy: elt) : t
requires { 0 <= n }
ensures {result. size = 0 }
= { elems = Array.make n dummy; size = 0; h = 0; bag = empty_bag }
= { elems = Array.make n dummy; size = 0; h = 0; bag = {empty_bag} }
predicate is_empty (q: t) = q.size = 0
......@@ -54,7 +54,7 @@ module SimplePrioriyQueue
else if priority x > priority q.elems[q.h] then
q.h <- q.size;
q.size <- q.size + 1;
q.bag <- add x q.bag
q.bag <- {add} x q.bag
let highest (q: t) : elt
requires { not (is_empty q) }
......@@ -82,7 +82,7 @@ module SimplePrioriyQueue
if p > !m then begin q.h <- i; m := p end
done
end;
q.bag <- diff q.bag (singleton r);
q.bag <- pure { diff q.bag (singleton r) };
r
end
......
......@@ -96,7 +96,7 @@ module PigeonHole
if f j = m-1 then return
done;
(* we know that for all k <> i, f k <> m-1 *)
let g = shift f i in
let g = pure { shift f i } in
assert { range g (n-1) (m-1) };
pigeon_hole (n-1) (m-1) g;
return
......
......@@ -181,19 +181,19 @@ module Bits "the 1-bits of an integer, as a set of integers"
ensures { result.mdl = remove size (succ a.mdl) }
=
{ bv = lsl_bv a.bv (1:BV32.t);
mdl = ghost remove size (succ a.mdl) }
mdl = pure { remove size (succ a.mdl) } }
let div2 (a: t) : t
ensures { result.mdl = pred a.mdl }
=
{ bv = lsr_bv a.bv (1:BV32.t);
mdl = ghost pred a.mdl }
mdl = pure { pred a.mdl } }
let diff (a b: t) : t
ensures { result.mdl = diff a.mdl b.mdl }
=
{ bv = bw_and a.bv (bw_not b.bv);
mdl = ghost diff a.mdl b.mdl }
mdl = pure { diff a.mdl b.mdl } }
predicate bits_interval_is_zeros_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
eq_sub_bv a zeros i n
......@@ -221,14 +221,14 @@ module Bits "the 1-bits of an integer, as a set of integers"
assert {bits_interval_is_zeros_bv res (add n_bv (1:BV32.t)) (sub (31:BV32.t) n_bv )};
assert {bits_interval_is_zeros res (n + 1) (31 - n)};
{ bv = res;
mdl = singleton n }
mdl = pure { singleton n } }
let below (n: BV32.t) : t
requires { BV32.ule n (32:BV32.t) }
ensures { result.mdl = interval 0 (t'int n) }
=
{ bv = bw_not (lsl_bv ones n);
mdl = ghost interval 0 (t'int n) }
mdl = pure { interval 0 (t'int n) } }
end
......
......@@ -77,7 +77,7 @@ module Spec
variant { c1 }
= match c1 with
| Nil -> ()
| Cons i1 l1 -> exec_append l1 c2 (exec i1 s)
| Cons i1 l1 -> exec_append l1 c2 ({exec} i1 s)
end
(** specification of the forthcoming compilation:
......@@ -138,7 +138,7 @@ module DWP
requires { hcode_ok hc }
ensures { wcode_ok result }
ensures { result.trans --> to_wp hc.post }
= { wcode = hc.hcode; trans = to_wp hc.post }
= { wcode = hc.hcode; trans = {to_wp} hc.post }
let wrap (wc: wcode) (ghost pst: post) : hcode
requires { wcode_ok wc }
......@@ -151,19 +151,19 @@ module DWP
requires { wcode_ok w1 /\ wcode_ok w2 }
ensures { wcode_ok result }
ensures { result.trans --> rcompose w2.trans w1.trans }
= { wcode = w1.wcode ++ w2.wcode; trans = rcompose w2.trans w1.trans }
= { wcode = w1.wcode ++ w2.wcode; trans = {rcompose} w2.trans w1.trans }
let cons (i: instr) (w: wcode) : wcode
requires { wcode_ok w }
ensures { wcode_ok result }
ensures { result.trans --> rcompose w.trans (rcompose (exec i)) }
= { wcode = Cons i w.wcode;
trans = rcompose w.trans (rcompose (exec_closure i)) }
trans = pure { rcompose w.trans (rcompose (exec_closure i)) } }
let nil () : wcode
ensures { wcode_ok result }
ensures { result.trans --> fun q -> q }
= { wcode = Nil; trans = id }
= { wcode = Nil; trans = {id} }
end
......@@ -188,7 +188,7 @@ module InfinityOfRegisters
| Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
| Eadd e1 e2 ->
$ compile e1 r -- $ compile e2 (r + 1) -- cons (Iadd (r+1) r) (nil ())
end) (expr_post e r)
end) ({expr_post} e r)
(* To recover usual specification. *)
let ghost recover (e: expr) (r: register) (h: hcode) : unit
......@@ -236,7 +236,7 @@ module FiniteNumberOfRegisters
$ compile e1 (k - 2) -- $ compile e2 (k - 1) --
cons (Iadd (k - 2) (k - 1)) (
cons (Ipop (k - 2)) (nil ())))
end) (expr_post e r)
end) ({expr_post} e r)
end
......@@ -304,6 +304,6 @@ module OptimalNumberOfRegisters
cons (Ipop (k - 2)) (nil ())))
else
$ compile (Eadd e2 e1) r (* compile e2 first *)
end) (expr_post e r)
end) ({expr_post} e r)
end
......@@ -28,8 +28,8 @@ module Rmbt
ensures { nth result !p }
=
let ghost p_bv = rightmost_position_set x in
ghost p := t'int p_bv;
ghost p := pure { t'int p_bv };
assert { nth_bv (neg x) p_bv };
bw_and x (neg x)
end
\ No newline at end of file
end
......@@ -25,7 +25,7 @@ module M603_018
requires { roundToIntegral RTN z = x }
requires { roundToIntegral RTP z = y }
=
let t = (x .+ y) ./ (2.0:t) in
let t = pure {(x .+ y) ./ (2.0:t)} in
assert { roundToIntegral RTN x .= x };
assert { roundToIntegral RTN y .= y };
assert { roundToIntegral RTN z .= x };
......@@ -86,7 +86,7 @@ module M121_039_nonlinear
assert { x .+ y .* a .>= x .+ y };
assert { x .+ y .>= zeroF };
assert { x .+ y .* a .>= zeroF };
x .+ y .* a
pure { x .+ y .* a }
end
......@@ -101,6 +101,6 @@ module LB09_025_conversion
ensures { of_int RNE result .<= x .+ (of_int RNE 1) }
ensures { result = to_int RNE x }
=
to_int RNE x
{to_int} RNE x
end
......@@ -210,7 +210,7 @@ module BellmanFord
while not (S.is_empty es) do
invariant { subset es.S.contents edges /\ inv1 m i (diff edges es.S.contents) }
variant { S.cardinal es }
let ghost via = diff edges es.S.contents in
let ghost via = pure { diff edges es.S.contents } in
let (u, v) = S.choose_and_remove es in
relax m u v i via
done;
......
......@@ -215,7 +215,7 @@ module Lemmas
= match st with
| Nil -> ()
| Cons E st' -> inverse_inverse st' c1 c2 c3
| Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
| Cons f st' -> if {even_forest} f then () else inverse_inverse st' c1 c2 c3
end
inductive sub stack forest coloring =
......
......@@ -196,7 +196,7 @@ module LinearProbing
assert { eq a[j] dummy };
a[j] <- x;
assert { numofd a 0 (j+1) = numofd (a at L) 0 (j+1) - 1 };
l := Map.set !l (keym x) j
l := Map.set !l x.{keym} j
end
done;
h.loc <- !l;
......@@ -219,8 +219,8 @@ module LinearProbing
assert { numofd h.data 0 (i+1) =
numofd (h.data at L) 0 (i+1) - 1 }
end;
ghost h.view <- Map.set h.view (keym x) True;
ghost h.loc <- Map.set h.loc (keym x) i
ghost h.view <- Map.set h.view x.{keym} True;
ghost h.loc <- Map.set h.loc x.{keym} i
let copy (h: t) : t
ensures { result.view = h.view }
......@@ -295,7 +295,7 @@ module LinearProbing
ghost numof_update a1 a 0 j n;
let ghost a2 = Array.copy a in
ghost NumOfDummy.numof_eq a a2 0 n;
ghost loc := Map.set !loc (keym xi) j;
ghost loc := Map.set !loc xi.{keym} j;
a[i] <- dummy;
ghost numof_update a a2 0 i n;
delete a loc view f0 i i
......@@ -313,7 +313,7 @@ module LinearProbing
h.data[j] <- dummy;
assert { numofd h.data 0 (j+1) =
numofd (h.data at L) 0 (j+1) + 1 };
ghost h.view <- Map.set h.view (keym x) False;
ghost h.view <- Map.set h.view x.{keym} False;
let l = ref h.loc in
let f0 = find_dummy h.data j (next n j) in
delete h.data l h.view f0 j j;
......
......@@ -328,7 +328,7 @@ module InPlaceRevSeq
= if length pM > 0 then begin
let h = pM[0] in
let t = pM[1 .. ] in
if mem h t then
if {mem} h t then
(* absurd case *)
let (l1,l2) = mem_decomp h t in
list_seg_sublistl next (cons h l1) l2 p h;
......
......@@ -72,8 +72,8 @@ module PrefixSumRec
variant { right-left }
ensures { phase1 left right a0 a' } =
if right > left + 1 then begin
phase1_frame (go_left left right) left a0 a a';
phase1_frame (go_right left right) right a0 a a'
phase1_frame ({go_left} left right) left a0 a a';
phase1_frame ({go_right} left right) right a0 a a'
end
(** frame lemma for "phase1" on third argument.
......@@ -86,8 +86,8 @@ module PrefixSumRec
variant { right-left }
ensures { phase1 left right a0' a } =
if right > left + 1 then begin
phase1_frame2 (go_left left right) left a0 a0' a;
phase1_frame2 (go_right left right) right a0 a0' a
phase1_frame2 ({go_left} left right) left a0 a0' a;
phase1_frame2 ({go_right} left right) right a0 a0' a
end
......
......@@ -40,11 +40,11 @@ end
module Compiler
use export list.Append
use import Expr
use import StackMachine
function compile (e:expr) : list asm =
match e with
| Cte n -> Cons (Push n) Nil
......@@ -57,19 +57,19 @@ module Compiler
variant { e }
ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r }
= match e with
| Cte n ->
| Cte n ->
assert { compile e ++ r = Cons (Push n) r }
| Plus e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Add r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r)
soundness_gen e1 s ({compile} e2 ++ Cons Add r);
soundness_gen e2 (Cons ({eval_expr} e1) s) (Cons Add r)
| Minus e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Sub r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r)
soundness_gen e1 s ({compile} e2 ++ Cons Sub r);
soundness_gen e2 (Cons ({eval_expr} e1) s) (Cons Sub r)
| Mult e1 e2 ->
soundness_gen e1 s (compile e2 ++ Cons Mul r);
soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r)
soundness_gen e1 s ({compile} e2 ++ Cons Mul r);
soundness_gen e2 (Cons ({eval_expr} e1) s) (Cons Mul r)
end
let lemma soundness (e:expr)
ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) }
=
......
......@@ -236,7 +236,7 @@ module Interleaving
(* shared variables *)
let a = ref a0 in
let b = ref b0 in
let ghost d = gcd a0 b0 in
let ghost d = {gcd} a0 b0 in
(* two threads *)
let th1 = create_thread () in
let th2 = create_thread () in
......
......@@ -50,7 +50,6 @@ end
theory Matrix
use import int.Int
use HighOrd
type mat 'a
......@@ -113,8 +112,6 @@ theory FixedMatrix
function cols = cols,
goal rows_and_cols_nonnegative
use HighOrd
function create (f: int -> int -> 'a) : mat 'a
axiom create_get:
......@@ -159,14 +156,14 @@ module MatrixArithmetic
fun x y -> get a x y + get b x y
function add (a b: mat int) : mat int =
create (rows a) (cols a) (add2f a b)
create (rows a) a.cols (add2f a b)
(* Matrix additive inverse *)
function opp2f (a: mat int) : int -> int -> int =
fun x y -> - get a x y
function opp (a: mat int) : mat int =
create (rows a) (cols a) (opp2f a)
create (rows a) a.cols (opp2f a)
function sub (a b: mat int) : mat int =
add a (opp b)
......@@ -176,10 +173,10 @@ module MatrixArithmetic
fun k -> get a i k * get b k j
function mul_cell (a b: mat int): int -> int -> int =
fun i j -> sum (mul_atom a b i j) 0 (cols a)
fun i j -> sum (mul_atom a b i j) 0 a.cols
function mul (a b: mat int) : mat int =
create (rows a) (cols b) (mul_cell a b)
create (rows a) b.cols (mul_cell a b)
lemma zero_neutral:
forall a. add a (zero a.rows a.cols) = a
......@@ -214,15 +211,15 @@ module MatrixArithmetic
let lemma mul_assoc_get (a b c: mat int) (i j: int)
requires { cols a = rows b }
requires { cols b = rows c }
requires { 0 <= i < (rows a) /\ 0 <= j < (cols c) }
requires { 0 <= i < rows a /\ 0 <= j < cols c }
ensures { get (mul (mul a b) c) i j = get (mul a (mul b c)) i j }
= let ft1 = ft1 a b c i j in
let ft2 = ft2 a b c i j in
fubini ft1 ft2 0 (cols b) 0 (cols a);
sum_ext (mul_atom (mul a b) c i j) (sumf ft1 0 (cols a)) 0 (cols b);
assert { get (mul (mul a b) c) i j = sum (sumf ft1 0 (cols a)) 0 (cols b) };
sum_ext (mul_atom a (mul b c) i j) (sumf ft2 0 (cols b)) 0 (cols a);
assert { get (mul a (mul b c)) i j = sum (sumf ft2 0 (cols b)) 0 (cols a) }
= let ft1 = pure { ft1 a b c i j } in
let ft2 = pure { ft2 a b c i j } in
fubini ft1 ft2 0 b.{cols} 0 a.{cols};
sum_ext ({mul_atom} ({mul} a b) c i j) ({sumf} ft1 0 a.{cols}) 0 b.{cols};
assert { get (mul (mul a b) c) i j = sum (sumf ft1 0 a.cols) 0 b.cols };
sum_ext ({mul_atom} a ({mul} b c) i j) ({sumf} ft2 0 b.{cols}) 0 a.{cols};
assert { get (mul a (mul b c)) i j = sum (sumf ft2 0 b.cols) 0 a.cols }
lemma mul_assoc:
forall a b c. cols a = rows b -> cols b = rows c ->
......@@ -238,12 +235,12 @@ module MatrixArithmetic
requires { cols b = rows c}
requires { a === b }
ensures { get (mul (add a b) c) i j = get (add (mul a c) (mul b c)) i j }
= let mac = mul_atom a c i j in
let mbc = mul_atom b c i j in
= let mac = pure { mul_atom a c i j } in
let mbc = pure { mul_atom b c i j } in
assert { get (add (mul a c) (mul b c)) i j =
get (mul a c) i j + get (mul b c) i j =
sum (addf mac mbc) 0 (cols b) };
sum_ext (addf mac mbc) (mul_atom (add a b) c i j) 0 (cols b)
sum (addf mac mbc) 0 b.cols };
sum_ext ({addf} mac mbc) ({mul_atom} ({add} a b) c i j) 0 b.{cols}
lemma mul_distr_right:
forall a b c. a === b -> cols b = rows c ->
......@@ -255,12 +252,12 @@ module MatrixArithmetic
requires { cols a = rows b }
requires { b === c }