diff options
Diffstat (limited to 'tests/lexers/fstar/example.txt')
| -rw-r--r-- | tests/lexers/fstar/example.txt | 15930 |
1 files changed, 15930 insertions, 0 deletions
diff --git a/tests/lexers/fstar/example.txt b/tests/lexers/fstar/example.txt new file mode 100644 index 00000000..0e26dcfa --- /dev/null +++ b/tests/lexers/fstar/example.txt @@ -0,0 +1,15930 @@ +---input--- +(* + Copyright 2020 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + +module Steel.Semantics.Hoare.MST + +module P = FStar.Preorder + +open FStar.Tactics + +open NMST + + +(* + * This module provides a semantic model for a combined effect of + * divergence, state, and parallel composition of atomic actions. + * + * It is built over a monotonic state effect -- so that we can give + * lock semantics using monotonicity + * + * It also builds a generic separation-logic-style program logic + * for this effect, in a partial correctness setting. + + * It is also be possible to give a variant of this semantics for + * total correctness. However, we specifically focus on partial correctness + * here so that this semantics can be instantiated with lock operations, + * which may deadlock. See ParTot.fst for a total-correctness variant of + * these semantics. + * + * The program logic is specified in the Hoare-style pre- and postconditions +*) + + +/// Disabling projectors because we don't use them and they increase the typechecking time + +#push-options "--fuel 0 --ifuel 2 --z3rlimit 20 --print_implicits --print_universes \ + --using_facts_from 'Prims FStar.Pervasives FStar.Preorder MST NMST Steel.Semantics.Hoare.MST'" + +(**** Begin state defn ****) + + +/// We start by defining some basic notions for a commutative monoid. +/// +/// We could reuse FStar.Algebra.CommMonoid, but this style with +/// quanitifers was more convenient for the proof done here. + + +let symmetry #a (equals: a -> a -> prop) = + forall x y. {:pattern (x `equals` y)} + x `equals` y ==> y `equals` x + +let transitive #a (equals:a -> a -> prop) = + forall x y z. x `equals` y /\ y `equals` z ==> x `equals` z + +let associative #a (equals: a -> a -> prop) (f: a -> a -> a)= + forall x y z. + f x (f y z) `equals` f (f x y) z + +let commutative #a (equals: a -> a -> prop) (f: a -> a -> a) = + forall x y.{:pattern f x y} + f x y `equals` f y x + +let is_unit #a (x:a) (equals: a -> a -> prop) (f:a -> a -> a) = + forall y. {:pattern f x y \/ f y x} + f x y `equals` y /\ + f y x `equals` y + +let equals_ext #a (equals:a -> a -> prop) (f:a -> a -> a) = + forall x1 x2 y. x1 `equals` x2 ==> f x1 y `equals` f x2 y + +let fp_heap_0 + (#heap:Type) + (#hprop:Type) + (interp:hprop -> heap -> prop) + (pre:hprop) + = + h:heap{interp pre h} + +let depends_only_on_0 + (#heap:Type) + (#hprop:Type) + (interp:hprop -> heap -> prop) + (disjoint: heap -> heap -> prop) + (join: (h0:heap -> h1:heap{disjoint h0 h1} -> heap)) + (q:heap -> prop) (fp: hprop) + = + forall (h0:fp_heap_0 interp fp) (h1:heap{disjoint h0 h1}). q h0 <==> q (join h0 h1) + +let fp_prop_0 + (#heap:Type) + (#hprop:Type) + (interp:hprop -> heap -> prop) + (disjoint: heap -> heap -> prop) + (join: (h0:heap -> h1:heap{disjoint h0 h1} -> heap)) + (fp:hprop) + = + p:(heap -> prop){p `(depends_only_on_0 interp disjoint join)` fp} + +noeq +type st0 = { + mem:Type u#2; + core:mem -> mem; + + locks_preorder:P.preorder mem; + hprop:Type u#2; + locks_invariant: mem -> hprop; + + disjoint: mem -> mem -> prop; + join: h0:mem -> h1:mem{disjoint h0 h1} -> mem; + + interp: hprop -> mem -> prop; + + emp:hprop; + star: hprop -> hprop -> hprop; + + equals: hprop -> hprop -> prop; +} + + +/// disjointness is symmetric + +let disjoint_sym (st:st0) = + forall h0 h1. st.disjoint h0 h1 <==> st.disjoint h1 h0 + +let disjoint_join (st:st0) = + forall m0 m1 m2. + st.disjoint m1 m2 /\ + st.disjoint m0 (st.join m1 m2) ==> + st.disjoint m0 m1 /\ + st.disjoint m0 m2 /\ + st.disjoint (st.join m0 m1) m2 /\ + st.disjoint (st.join m0 m2) m1 + +let join_commutative (st:st0 { disjoint_sym st }) = + forall m0 m1. + st.disjoint m0 m1 ==> + st.join m0 m1 == st.join m1 m0 + +let join_associative (st:st0{disjoint_join st})= + forall m0 m1 m2. + st.disjoint m1 m2 /\ + st.disjoint m0 (st.join m1 m2) ==> + st.join m0 (st.join m1 m2) == st.join (st.join m0 m1) m2 + +//////////////////////////////////////////////////////////////////////////////// + +let interp_extensionality #r #s (equals:r -> r -> prop) (f:r -> s -> prop) = + forall x y h. {:pattern equals x y; f x h} equals x y /\ f x h ==> f y h + +let affine (st:st0) = + forall r0 r1 s. {:pattern (st.interp (r0 `st.star` r1) s) } + st.interp (r0 `st.star` r1) s ==> st.interp r0 s + +//////////////////////////////////////////////////////////////////////////////// + +let depends_only_on (#st:st0) (q:st.mem -> prop) (fp: st.hprop) = + depends_only_on_0 st.interp st.disjoint st.join q fp + +let fp_prop (#st:st0) (fp:st.hprop) = + fp_prop_0 st.interp st.disjoint st.join fp + +let lemma_weaken_depends_only_on + (#st:st0{affine st}) + (fp0 fp1:st.hprop) + (q:fp_prop fp0) + : Lemma (q `depends_only_on` (fp0 `st.star` fp1)) + = + () + +let st_laws (st:st0) = + (* standard laws about the equality relation *) + symmetry st.equals /\ + transitive st.equals /\ + interp_extensionality st.equals st.interp /\ + (* standard laws for star forming a CM *) + associative st.equals st.star /\ + commutative st.equals st.star /\ + is_unit st.emp st.equals st.star /\ + equals_ext st.equals st.star /\ + (* We're working in an affine interpretation of SL *) + affine st /\ + (* laws about disjoint and join *) + disjoint_sym st /\ + disjoint_join st /\ + join_commutative st /\ + join_associative st + +let st = s:st0 { st_laws s } + +(**** End state defn ****) + + +(**** Begin expects, provides, requires, and ensures defns ****) + + +/// expects (the heap assertion expected by a computation) is simply an st.hprop +/// +/// provides, or the post heap assertion, is a st.hprop on [a]-typed result + +type post_t (st:st) (a:Type) = a -> st.hprop + + +/// requires is a heap predicate that depends only on a pre heap assertion +/// (where the notion of `depends only on` is defined above as part of the state definition) +/// +/// we call the type l_pre for logical precondition + +let l_pre (#st:st) (pre:st.hprop) = fp_prop pre + + +/// ensures is a 2-state postcondition of type heap -> a -> heap -> prop +/// +/// To define ensures, we need a notion of depends_only_on_2 +/// +/// Essentially, in the first heap argument, postconditions depend only on the expects hprop +/// and in the second heap argument, postconditions depend only on the provides hprop +/// +/// Also note that the support for depends_only_on_2 is not required from the underlying memory model + + +let depends_only_on_0_2 + (#a:Type) + (#heap:Type) + (#hprop:Type) + (interp:hprop -> heap -> prop) + (disjoint:heap -> heap -> prop) + (join:(h0:heap -> h1:heap{disjoint h0 h1} -> heap)) + (q:heap -> a -> heap -> prop) (fp_pre:hprop) (fp_post:a -> hprop) + + = //can join any disjoint heap to the pre-heap and q is still valid + (forall x (h_pre:fp_heap_0 interp fp_pre) h_post (h:heap{disjoint h_pre h}). + q h_pre x h_post <==> q (join h_pre h) x h_post) /\ + //can join any disjoint heap to the post-heap and q is still valid + (forall x h_pre (h_post:fp_heap_0 interp (fp_post x)) (h:heap{disjoint h_post h}). + q h_pre x h_post <==> q h_pre x (join h_post h)) + +/// Abbreviations for two-state depends + +let fp_prop_0_2 + (#a:Type) + (#heap #hprop:Type) + (interp:hprop -> heap -> prop) + (disjoint:heap -> heap -> prop) + (join:(h0:heap -> h1:heap{disjoint h0 h1} -> heap)) + (fp_pre:hprop) + (fp_post:a -> hprop) + = + q:(heap -> a -> heap -> prop){depends_only_on_0_2 interp disjoint join q fp_pre fp_post} + +let depends_only_on2 + (#st:st0) + (#a:Type) + (q:st.mem -> a -> st.mem -> prop) + (fp_pre:st.hprop) + (fp_post:a -> st.hprop) + = + depends_only_on_0_2 st.interp st.disjoint st.join q fp_pre fp_post + +let fp_prop2 (#st:st0) (#a:Type) (fp_pre:st.hprop) (fp_post:a -> st.hprop) = + q:(st.mem -> a -> st.mem -> prop){depends_only_on2 q fp_pre fp_post} + +/// Finally the type of 2-state postconditions + +let l_post (#st:st) (#a:Type) (pre:st.hprop) (post:post_t st a) = fp_prop2 pre post + + +(**** End expects, provides, requires, + and ensures defns ****) + +effect Mst (a:Type) (#st:st) (req:st.mem -> Type0) (ens:st.mem -> a -> st.mem -> Type0) = + NMSTATE a st.mem st.locks_preorder req ens + + +(**** Begin interface of actions ****) + +/// Actions are essentially state transformers that preserve frames + +let preserves_frame (#st:st) (pre post:st.hprop) (m0 m1:st.mem) = + forall (frame:st.hprop). + st.interp ((pre `st.star` frame) `st.star` (st.locks_invariant m0)) m0 ==> + (st.interp ((post `st.star` frame) `st.star` (st.locks_invariant m1)) m1 /\ + (forall (f_frame:fp_prop frame). f_frame (st.core m0) == f_frame (st.core m1))) + +let action_t + (#st:st) + (#a:Type) + (pre:st.hprop) + (post:post_t st a) + (lpre:l_pre pre) + (lpost:l_post pre post) + = + unit -> + Mst a + (requires fun m0 -> + st.interp (pre `st.star` st.locks_invariant m0) m0 /\ + lpre (st.core m0)) + (ensures fun m0 x m1 -> + st.interp ((post x) `st.star` st.locks_invariant m1) m1 /\ + lpost (st.core m0) x (st.core m1) /\ + preserves_frame pre (post x) m0 m1) + +(**** End interface of actions ****) + + +(**** Begin definition of the computation AST ****) + + +/// Gadgets for building lpre- and lpostconditions for various nodes + + +/// Return node is parametric in provides and ensures + +let return_lpre (#st:st) (#a:Type) (#post:post_t st a) (x:a) (lpost:l_post (post x) post) + : l_pre (post x) + = + fun h -> lpost h x h + +let frame_lpre (#st:st) (#pre:st.hprop) (lpre:l_pre pre) (#frame:st.hprop) (f_frame:fp_prop frame) + : l_pre (pre `st.star` frame) + = + fun h -> lpre h /\ f_frame h + +let frame_lpost + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (lpre:l_pre pre) + (lpost:l_post pre post) + (#frame:st.hprop) + (f_frame:fp_prop frame) + : l_post (pre `st.star` frame) (fun x -> post x `st.star` frame) + = + fun h0 x h1 -> lpre h0 /\ lpost h0 x h1 /\ f_frame h1 + +/// The bind rule bakes in weakening of requires / ensures + +let bind_lpre + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post_a:post_t st a) + (lpre_a:l_pre pre) + (lpost_a:l_post pre post_a) + (lpre_b:(x:a -> l_pre (post_a x))) + : l_pre pre + = + fun h -> lpre_a h /\ (forall (x:a) h1. lpost_a h x h1 ==> lpre_b x h1) + +let bind_lpost + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post_a:post_t st a) + (lpre_a:l_pre pre) + (lpost_a:l_post pre post_a) + (#b:Type) + (#post_b:post_t st b) + (lpost_b:(x:a -> l_post (post_a x) post_b)) + : l_post pre post_b + = + fun h0 y h2 -> lpre_a h0 /\ (exists x h1. lpost_a h0 x h1 /\ (lpost_b x) h1 y h2) + +/// Parallel composition is pointwise + +let par_lpre + (#st:st) + (#preL:st.hprop) + (lpreL:l_pre preL) + (#preR:st.hprop) + (lpreR:l_pre preR) + : l_pre (preL `st.star` preR) + = + fun h -> lpreL h /\ lpreR h + +let par_lpost + (#st:st) + (#aL:Type) + (#preL:st.hprop) + (#postL:post_t st aL) + (lpreL:l_pre preL) + (lpostL:l_post preL postL) + (#aR:Type) + (#preR:st.hprop) + (#postR:post_t st aR) + (lpreR:l_pre preR) + (lpostR:l_post preR postR) + : l_post (preL `st.star` preR) (fun (xL, xR) -> postL xL `st.star` postR xR) + = + fun h0 (xL, xR) h1 -> lpreL h0 /\ lpreR h0 /\ lpostL h0 xL h1 /\ lpostR h0 xR h1 + +let weaker_pre (#st:st) (pre:st.hprop) (next_pre:st.hprop) = + forall (h:st.mem) (frame:st.hprop). + st.interp (pre `st.star` frame) h ==> + st.interp (next_pre `st.star` frame) h + +let stronger_post (#st:st) (#a:Type u#a) (post next_post:post_t st a) = + forall (x:a) (h:st.mem) (frame:st.hprop). + st.interp (next_post x `st.star` frame) h ==> + st.interp (post x `st.star` frame) h + +let weakening_ok + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (lpre:l_pre pre) + (lpost:l_post pre post) + (#wpre:st.hprop) + (#wpost:post_t st a) + (wlpre:l_pre wpre) + (wlpost:l_post wpre wpost) + = + weaker_pre wpre pre /\ + stronger_post wpost post /\ + (forall h. wlpre h ==> lpre h) /\ + (forall h0 x h1. lpost h0 x h1 ==> wlpost h0 x h1) + + +/// Setting the flag just to reduce the time to typecheck the type m + +#push-options "--__temp_no_proj Steel.Semantics.Hoare.MST" +noeq +type m (st:st) : + a:Type u#a -> + pre:st.hprop -> + post:post_t st a -> + l_pre pre -> + l_post pre post -> Type + = + | Ret: + #a:Type u#a -> + post:post_t st a -> + x:a -> + lpost:l_post (post x) post -> + m st a (post x) post (return_lpre #_ #_ #post x lpost) lpost + + | Bind: + #a:Type u#a -> + #pre:st.hprop -> + #post_a:post_t st a -> + #lpre_a:l_pre pre -> + #lpost_a:l_post pre post_a -> + #b:Type u#a -> + #post_b:post_t st b -> + #lpre_b:(x:a -> l_pre (post_a x)) -> + #lpost_b:(x:a -> l_post (post_a x) post_b) -> + f:m st a pre post_a lpre_a lpost_a -> + g:(x:a -> Dv (m st b (post_a x) post_b (lpre_b x) (lpost_b x))) -> + m st b pre post_b + (bind_lpre lpre_a lpost_a lpre_b) + (bind_lpost lpre_a lpost_a lpost_b) + + | Act: + #a:Type u#a -> + #pre:st.hprop -> + #post:post_t st a -> + #lpre:l_pre pre -> + #lpost:l_post pre post -> + f:action_t #st #a pre post lpre lpost -> + m st a pre post lpre lpost + + | Frame: + #a:Type -> + #pre:st.hprop -> + #post:post_t st a -> + #lpre:l_pre pre -> + #lpost:l_post pre post -> + f:m st a pre post lpre lpost -> + frame:st.hprop -> + f_frame:fp_prop frame -> + m st a (pre `st.star` frame) (fun x -> post x `st.star` frame) + (frame_lpre lpre f_frame) + (frame_lpost lpre lpost f_frame) + + | Par: + #aL:Type u#a -> + #preL:st.hprop -> + #postL:post_t st aL -> + #lpreL:l_pre preL -> + #lpostL:l_post preL postL -> + mL:m st aL preL postL lpreL lpostL -> + #aR:Type u#a -> + #preR:st.hprop -> + #postR:post_t st aR -> + #lpreR:l_pre preR -> + #lpostR:l_post preR postR -> + mR:m st aR preR postR lpreR lpostR -> + m st (aL & aR) (preL `st.star` preR) (fun (xL, xR) -> postL xL `st.star` postR xR) + (par_lpre lpreL lpreR) + (par_lpost lpreL lpostL lpreR lpostR) + + | Weaken: + #a:Type u#a -> + #pre:st.hprop -> + #post:post_t st a -> + #lpre:l_pre pre -> + #lpost:l_post pre post -> + #wpre:st.hprop -> + #wpost:post_t st a -> + wlpre:l_pre wpre -> + wlpost:l_post wpre wpost -> + _:squash (weakening_ok lpre lpost wlpre wlpost) -> + m st a pre post lpre lpost -> + m st a wpre wpost wlpre wlpost +#pop-options + +(**** End definition of the computation AST ****) + + +(**** Stepping relation ****) + +/// All steps preserve frames + +noeq +type step_result (st:st) (a:Type u#a) = + | Step: + next_pre:st.hprop -> + next_post:post_t st a -> + lpre:l_pre next_pre -> + lpost:l_post next_pre next_post -> + m st a next_pre next_post lpre lpost -> + step_result st a + + +(**** Type of the single-step interpreter ****) + + +/// Interpreter is setup as a Div function from computation trees to computation trees +/// +/// While the requires for the Div is standard (that the expects hprop holds and requires is valid), +/// the ensures is interesting +/// +/// As the computation evolves, the requires and ensures associated with the computation graph nodes +/// also evolve +/// But they evolve systematically: preconditions become weaker and postconditions become stronger +/// +/// Consider { req } c | st { ens } ~~> { req1 } c1 | st1 { ens1 } +/// +/// Then, req st ==> req1 st1 /\ +/// (forall x st_final. ens1 st1 x st_final ==> ens st x st_final) + + +unfold +let step_req + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost) + : st.mem -> Type0 + = + fun m0 -> + st.interp (pre `st.star` st.locks_invariant m0) m0 /\ + lpre (st.core m0) + +let weaker_lpre + (#st:st) + (#pre:st.hprop) + (lpre:l_pre pre) + (#next_pre:st.hprop) + (next_lpre:l_pre next_pre) + (m0 m1:st.mem) + = + lpre (st.core m0) ==> next_lpre (st.core m1) + +let stronger_lpost + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (lpost:l_post pre post) + (#next_pre:st.hprop) + #next_post + (next_lpost:l_post next_pre next_post) + (m0 m1:st.mem) + = + forall (x:a) (h_final:st.mem). + next_lpost (st.core m1) x h_final ==> + lpost (st.core m0) x h_final + +unfold +let step_ens + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost) + : st.mem -> step_result st a -> st.mem -> Type0 + = + fun m0 r m1 -> + let Step next_pre next_post next_lpre next_lpost _ = r in + st.interp (next_pre `st.star` st.locks_invariant m1) m1 /\ + stronger_post post next_post /\ + next_lpre (st.core m1) /\ + preserves_frame pre next_pre m0 m1 /\ + weaker_lpre lpre next_lpre m0 m1 /\ + stronger_lpost lpost next_lpost m0 m1 + + +/// The type of the stepping function + +type step_t = + #st:st -> + #a:Type u#a -> + #pre:st.hprop -> + #post:post_t st a -> + #lpre:l_pre pre -> + #lpost:l_post pre post -> + f:m st a pre post lpre lpost -> + Mst (step_result st a) (step_req f) (step_ens f) + + +(**** Auxiliary lemmas ****) + +/// Some AC lemmas on `st.star` + +let apply_assoc (#st:st) (p q r:st.hprop) + : Lemma (st.equals (p `st.star` (q `st.star` r)) ((p `st.star` q) `st.star` r)) + = + () + +let equals_ext_left (#st:st) (p q r:st.hprop) + : Lemma + (requires p `st.equals` q) + (ensures (p `st.star` r) `st.equals` (q `st.star` r)) + = + () + +let equals_ext_right (#st:st) (p q r:st.hprop) + : Lemma + (requires q `st.equals` r) + (ensures (p `st.star` q) `st.equals` (p `st.star` r)) + = + calc (st.equals) { + p `st.star` q; + (st.equals) { } + q `st.star` p; + (st.equals) { } + r `st.star` p; + (st.equals) { } + p `st.star` r; + } + +let commute_star_right (#st:st) (p q r:st.hprop) + : Lemma + ((p `st.star` (q `st.star` r)) `st.equals` + (p `st.star` (r `st.star` q))) + = + calc (st.equals) { + p `st.star` (q `st.star` r); + (st.equals) { equals_ext_right p (q `st.star` r) (r `st.star` q) } + p `st.star` (r `st.star` q); + } + +let assoc_star_right (#st:st) (p q r s:st.hprop) + : Lemma + ((p `st.star` ((q `st.star` r) `st.star` s)) `st.equals` + (p `st.star` (q `st.star` (r `st.star` s)))) + = + calc (st.equals) { + p `st.star` ((q `st.star` r) `st.star` s); + (st.equals) { equals_ext_right p ((q `st.star` r) `st.star` s) + (q `st.star` (r `st.star` s)) } + p `st.star` (q `st.star` (r `st.star` s)); + } + +let commute_assoc_star_right (#st:st) (p q r s:st.hprop) + : Lemma + ((p `st.star` ((q `st.star` r) `st.star` s)) `st.equals` + (p `st.star` (r `st.star` (q `st.star` s)))) + = + calc (st.equals) { + p `st.star` ((q `st.star` r) `st.star` s); + (st.equals) { equals_ext_right p + ((q `st.star` r) `st.star` s) + ((r `st.star` q) `st.star` s) } + p `st.star` ((r `st.star` q) `st.star` s); + (st.equals) { assoc_star_right p r q s } + p `st.star` (r `st.star` (q `st.star` s)); + } + + +/// Apply extensionality manually, control proofs + +let apply_interp_ext (#st:st) (p q:st.hprop) (m:st.mem) + : Lemma + (requires (st.interp p m /\ p `st.equals` q)) + (ensures st.interp q m) + = + () + +let weaken_fp_prop (#st:st) (frame frame':st.hprop) (m0 m1:st.mem) + : Lemma + (requires + forall (f_frame:fp_prop (frame `st.star` frame')). + f_frame (st.core m0) == f_frame (st.core m1)) + (ensures + forall (f_frame:fp_prop frame'). + f_frame (st.core m0) == f_frame (st.core m1)) + = + () + +let depends_only_on_commutes_with_weaker + (#st:st) + (q:st.mem -> prop) + (fp:st.hprop) + (fp_next:st.hprop) + : Lemma + (requires depends_only_on q fp /\ weaker_pre fp_next fp) + (ensures depends_only_on q fp_next) + = + assert (forall (h0:fp_heap_0 st.interp fp_next). st.interp (fp_next `st.star` st.emp) h0) + +let depends_only_on2_commutes_with_weaker + (#st:st) + (#a:Type) + (q:st.mem -> a -> st.mem -> prop) + (fp:st.hprop) + (fp_next:st.hprop) + (fp_post:a -> st.hprop) + : Lemma + (requires depends_only_on2 q fp fp_post /\ weaker_pre fp_next fp) + (ensures depends_only_on2 q fp_next fp_post) + = + assert (forall (h0:fp_heap_0 st.interp fp_next). st.interp (fp_next `st.star` st.emp) h0) + +/// Lemmas about preserves_frame + +let preserves_frame_trans + (#st:st) + (hp1 hp2 hp3:st.hprop) + (m1 m2 m3:st.mem) + : Lemma + (requires preserves_frame hp1 hp2 m1 m2 /\ preserves_frame hp2 hp3 m2 m3) + (ensures preserves_frame hp1 hp3 m1 m3) + = + () + +#push-options "--warn_error -271" +let preserves_frame_stronger_post + (#st:st) + (#a:Type) + (pre:st.hprop) + (post post_s:post_t st a) + (x:a) + (m1 m2:st.mem) + : Lemma + (requires preserves_frame pre (post_s x) m1 m2 /\ stronger_post post post_s) + (ensures preserves_frame pre (post x) m1 m2) + = + let aux (frame:st.hprop) + : Lemma + (requires st.interp (st.locks_invariant m1 `st.star` (pre `st.star` frame)) m1) + (ensures + st.interp (st.locks_invariant m2 `st.star` (post x `st.star` frame)) m2 /\ + (forall (f_frame:fp_prop frame). f_frame (st.core m1) == f_frame (st.core m2))) + [SMTPat ()] + = + assert (st.interp (st.locks_invariant m2 `st.star` (post_s x `st.star` frame)) m2); + calc (st.equals) { + st.locks_invariant m2 `st.star` (post_s x `st.star` frame); + (st.equals) { } + (st.locks_invariant m2 `st.star` post_s x) `st.star` frame; + (st.equals) { } + (post_s x `st.star` st.locks_invariant m2) `st.star` frame; + (st.equals) { } + post_s x `st.star` (st.locks_invariant m2 `st.star` frame); + }; + assert (st.interp (post_s x `st.star` (st.locks_invariant m2 `st.star` frame)) m2); + assert (st.interp (post x `st.star` (st.locks_invariant m2 `st.star` frame)) m2); + calc (st.equals) { + post x `st.star` (st.locks_invariant m2 `st.star` frame); + (st.equals) { } + (post x `st.star` st.locks_invariant m2) `st.star` frame; + (st.equals) { } + (st.locks_invariant m2 `st.star` post x) `st.star` frame; + (st.equals) { apply_assoc (st.locks_invariant m2) (post x) frame } + st.locks_invariant m2 `st.star` (post x `st.star` frame); + }; + assert (st.interp (st.locks_invariant m2 `st.star` (post x `st.star` frame)) m2) + in + () +#pop-options + +#push-options "--z3rlimit 40 --warn_error -271" +let preserves_frame_star (#st:st) (pre post:st.hprop) (m0 m1:st.mem) (frame:st.hprop) + : Lemma + (requires preserves_frame pre post m0 m1) + (ensures preserves_frame (pre `st.star` frame) (post `st.star` frame) m0 m1) + = + let aux (frame':st.hprop) + : Lemma + (requires + st.interp (st.locks_invariant m0 `st.star` ((pre `st.star` frame) `st.star` frame')) m0) + (ensures + st.interp (st.locks_invariant m1 `st.star` + ((post `st.star` frame) `st.star` frame')) m1 /\ + (forall (f_frame:fp_prop frame'). f_frame (st.core m0) == f_frame (st.core m1))) + [SMTPat ()] + = + assoc_star_right (st.locks_invariant m0) pre frame frame'; + apply_interp_ext + (st.locks_invariant m0 `st.star` ((pre `st.star` frame) `st.star` frame')) + (st.locks_invariant m0 `st.star` (pre `st.star` (frame `st.star` frame'))) + m0; + assoc_star_right (st.locks_invariant m1) post frame frame'; + apply_interp_ext + (st.locks_invariant m1 `st.star` (post `st.star` (frame `st.star` frame'))) + (st.locks_invariant m1 `st.star` ((post `st.star` frame) `st.star` frame')) + m1; + weaken_fp_prop frame frame' m0 m1 + in + () + +let preserves_frame_star_left (#st:st) (pre post:st.hprop) (m0 m1:st.mem) (frame:st.hprop) + : Lemma + (requires preserves_frame pre post m0 m1) + (ensures preserves_frame (frame `st.star` pre) (frame `st.star` post) m0 m1) + = + let aux (frame':st.hprop) + : Lemma + (requires + st.interp (st.locks_invariant m0 `st.star` ((frame `st.star` pre) `st.star` frame')) m0) + (ensures + st.interp (st.locks_invariant m1 `st.star` + ((frame `st.star` post) `st.star` frame')) m1 /\ + (forall (f_frame:fp_prop frame'). f_frame (st.core m0) == f_frame (st.core m1))) + [SMTPat ()] + = + commute_assoc_star_right (st.locks_invariant m0) frame pre frame'; + apply_interp_ext + (st.locks_invariant m0 `st.star` ((frame `st.star` pre) `st.star` frame')) + (st.locks_invariant m0 `st.star` (pre `st.star` (frame `st.star` frame'))) + m0; + commute_assoc_star_right (st.locks_invariant m1) frame post frame'; + apply_interp_ext + (st.locks_invariant m1 `st.star` (post `st.star` (frame `st.star` frame'))) + (st.locks_invariant m1 `st.star` ((frame `st.star` post) `st.star` frame')) + m1; + weaken_fp_prop frame frame' m0 m1 + in + () +#pop-options + + +/// Lemma frame_post_for_par is used in the par proof +/// +/// E.g. in the par rule, when L takes a step, we can frame the requires of R +/// by using the preserves_frame property of the stepping relation +/// +/// However we also need to frame the ensures of R, for establishing stronger_post +/// +/// Basically, we need: +/// +/// forall x h_final. postR prev_state x h_final <==> postR next_state x h_final +/// +/// (the proof only requires the reverse implication, but we can prove iff) +/// +/// To prove this, we rely on the framing of all frame fp props provides by the stepping relation +/// +/// To use it, we instantiate the fp prop with inst_heap_prop_for_par + +let inst_heap_prop_for_par + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (lpost:l_post pre post) + (state:st.mem) + : fp_prop pre + = + fun h -> + forall x final_state. + lpost h x final_state <==> + lpost (st.core state) x final_state + +let frame_post_for_par_tautology + (#st:st) + (#a:Type) + (#pre_f:st.hprop) + (#post_f:post_t st a) + (lpost_f:l_post pre_f post_f) + (m0:st.mem) + : Lemma (inst_heap_prop_for_par lpost_f m0 (st.core m0)) + = + () + +let frame_post_for_par_aux + (#st:st) + (pre_s post_s:st.hprop) (m0 m1:st.mem) + (#a:Type) (#pre_f:st.hprop) (#post_f:post_t st a) (lpost_f:l_post pre_f post_f) + : Lemma + (requires + preserves_frame pre_s post_s m0 m1 /\ + st.interp ((pre_s `st.star` pre_f) `st.star` st.locks_invariant m0) m0) + (ensures + inst_heap_prop_for_par lpost_f m0 (st.core m0) <==> + inst_heap_prop_for_par lpost_f m0 (st.core m1)) + = + () + +let frame_post_for_par + (#st:st) + (pre_s post_s:st.hprop) + (m0 m1:st.mem) + (#a:Type) + (#pre_f:st.hprop) + (#post_f:post_t st a) + (lpre_f:l_pre pre_f) + (lpost_f:l_post pre_f post_f) + : Lemma + (requires + preserves_frame pre_s post_s m0 m1 /\ + st.interp ((pre_s `st.star` pre_f) `st.star` st.locks_invariant m0) m0) + (ensures + (lpre_f (st.core m0) <==> lpre_f (st.core m1)) /\ + (forall (x:a) (final_state:st.mem). + lpost_f (st.core m0) x final_state <==> + lpost_f (st.core m1) x final_state)) + = + frame_post_for_par_tautology lpost_f m0; + frame_post_for_par_aux pre_s post_s m0 m1 lpost_f + +/// Finally lemmas for proving that in the par rules preconditions get weaker +/// and postconditions get stronger + +let par_weaker_lpre_and_stronger_lpost_l + (#st:st) + (#preL:st.hprop) + (lpreL:l_pre preL) + (#aL:Type) + (#postL:post_t st aL) + (lpostL:l_post preL postL) + (#next_preL:st.hprop) + (#next_postL:post_t st aL) + (next_lpreL:l_pre next_preL) + (next_lpostL:l_post next_preL next_postL) + (#preR:st.hprop) + (lpreR:l_pre preR) + (#aR:Type) + (#postR:post_t st aR) + (lpostR:l_post preR postR) + (state next_state:st.mem) + : Lemma + (requires + weaker_lpre lpreL next_lpreL state next_state /\ + stronger_lpost lpostL next_lpostL state next_state /\ + preserves_frame preL next_preL state next_state /\ + lpreL (st.core state) /\ + lpreR (st.core state) /\ + st.interp ((preL `st.star` preR) `st.star` st.locks_invariant state) state) + (ensures + weaker_lpre + (par_lpre lpreL lpreR) + (par_lpre next_lpreL lpreR) + state next_state /\ + stronger_lpost + (par_lpost lpreL lpostL lpreR lpostR) + (par_lpost next_lpreL next_lpostL lpreR lpostR) + state next_state) + = + frame_post_for_par preL next_preL state next_state lpreR lpostR; + assert (weaker_lpre (par_lpre lpreL lpreR) (par_lpre next_lpreL lpreR) state next_state) by + (norm [delta_only [`%weaker_lpre; `%par_lpre] ]) + +let par_weaker_lpre_and_stronger_lpost_r + (#st:st) + (#preL:st.hprop) + (lpreL:l_pre preL) + (#aL:Type) + (#postL:post_t st aL) + (lpostL:l_post preL postL) + (#preR:st.hprop) + (lpreR:l_pre preR) + (#aR:Type) + (#postR:post_t st aR) + (lpostR:l_post preR postR) + (#next_preR:st.hprop) + (#next_postR:post_t st aR) + (next_lpreR:l_pre next_preR) + (next_lpostR:l_post next_preR next_postR) + (state next_state:st.mem) + : Lemma + (requires + weaker_lpre lpreR next_lpreR state next_state /\ + stronger_lpost lpostR next_lpostR state next_state /\ + preserves_frame preR next_preR state next_state /\ + lpreR (st.core state) /\ + lpreL (st.core state) /\ + st.interp ((preL `st.star` preR) `st.star` st.locks_invariant state) state) + (ensures + st.interp ((preL `st.star` next_preR) `st.star` st.locks_invariant next_state) next_state /\ + weaker_lpre + (par_lpre lpreL lpreR) + (par_lpre lpreL next_lpreR) + state next_state /\ + stronger_lpost + (par_lpost lpreL lpostL lpreR lpostR) + (par_lpost lpreL lpostL next_lpreR next_lpostR) + state next_state) + = + commute_star_right (st.locks_invariant state) preL preR; + apply_interp_ext + (st.locks_invariant state `st.star` (preL `st.star` preR)) + (st.locks_invariant state `st.star` (preR `st.star` preL)) + state; + frame_post_for_par preR next_preR state next_state lpreL lpostL; + assert (weaker_lpre (par_lpre lpreL lpreR) (par_lpre lpreL next_lpreR) state next_state) by + (norm [delta_only [`%weaker_lpre; `%par_lpre] ]); + commute_star_right (st.locks_invariant next_state) next_preR preL; + apply_interp_ext + (st.locks_invariant next_state `st.star` (next_preR `st.star` preL)) + (st.locks_invariant next_state `st.star` (preL `st.star` next_preR)) + next_state + +#push-options "--warn_error -271" +let stronger_post_par_r + (#st:st) + (#aL #aR:Type u#a) + (postL:post_t st aL) + (postR:post_t st aR) + (next_postR:post_t st aR) + : Lemma + (requires stronger_post postR next_postR) + (ensures + forall xL xR frame h. + st.interp ((postL xL `st.star` next_postR xR) `st.star` frame) h ==> + st.interp ((postL xL `st.star` postR xR) `st.star` frame) h) + = + let aux xL xR frame h + : Lemma + (requires st.interp ((postL xL `st.star` next_postR xR) `st.star` frame) h) + (ensures st.interp ((postL xL `st.star` postR xR) `st.star` frame) h) + [SMTPat ()] + = + calc (st.equals) { + (postL xL `st.star` next_postR xR) `st.star` frame; + (st.equals) { } + (next_postR xR `st.star` postL xL) `st.star` frame; + (st.equals) { } + next_postR xR `st.star` (postL xL `st.star` frame); + }; + assert (st.interp (next_postR xR `st.star` (postL xL `st.star` frame)) h); + assert (st.interp (postR xR `st.star` (postL xL `st.star` frame)) h); + calc (st.equals) { + postR xR `st.star` (postL xL `st.star` frame); + (st.equals) { } + (postR xR `st.star` postL xL) `st.star` frame; + (st.equals) { } + (postL xL `st.star` postR xR) `st.star` frame; + } + in + () +#pop-options + + +(**** Begin stepping functions ****) + +let step_ret + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Ret? f}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + NMSTATE?.reflect (fun (_, n) -> + let Ret p x lp = f in + Step (p x) p lpre lpost f, n) + +let lpost_ret_act + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (lpost:l_post pre post) + (x:a) + (state:st.mem) + : l_post (post x) post + = + fun _ x h1 -> lpost (st.core state) x h1 + +let step_act + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Act? f}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + let m0 = get () in + + let Act #_ #_ #_ #_ #_ #_ f = f in + + let x = f () in + + let lpost : l_post (post x) post = lpost_ret_act lpost x m0 in + + Step (post x) post (fun h -> lpost h x h) lpost (Ret post x lpost) + +module M = MST + +let step_bind_ret_aux + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Bind? f /\ Ret? (Bind?.f f)}) + : M.MSTATE (step_result st a) st.mem st.locks_preorder (step_req f) (step_ens f) + = + M.MSTATE?.reflect (fun m0 -> + match f with + | Bind #_ #_ #_ #_ #_ #_ #_ #post_b #lpre_b #lpost_b (Ret p x _) g -> + Step (p x) post_b (lpre_b x) (lpost_b x) (g x), m0) + +let step_bind_ret + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Bind? f /\ Ret? (Bind?.f f)}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + NMSTATE?.reflect (fun (_, n) -> step_bind_ret_aux f, n) + + +#push-options "--z3rlimit 40" +let step_bind + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Bind? f}) + (step:step_t) + : Mst (step_result st a) (step_req f) (step_ens f) + = + match f with + | Bind (Ret _ _ _) _ -> step_bind_ret f + + | Bind #_ #b #_ #post_a #_ #_ #_ #post_b #lpre_b #lpost_b f g -> + let Step next_pre next_post next_lpre next_lpost f = step f in + + let lpre_b : (x:b -> l_pre (next_post x)) = + fun x -> + depends_only_on_commutes_with_weaker (lpre_b x) (post_a x) (next_post x); + lpre_b x in + + let lpost_b : (x:b -> l_post (next_post x) post_b) = + fun x -> + depends_only_on2_commutes_with_weaker (lpost_b x) (post_a x) (next_post x) post_b; + lpost_b x in + + let g : (x:b -> Dv (m st _ (next_post x) post_b (lpre_b x) (lpost_b x))) = + fun x -> + Weaken (lpre_b x) (lpost_b x) () (g x) in + + let m1 = get () in + + assert ((bind_lpre next_lpre next_lpost lpre_b) (st.core m1)) + by norm ([delta_only [`%bind_lpre]]); + + Step next_pre post_b + (bind_lpre next_lpre next_lpost lpre_b) + (bind_lpost next_lpre next_lpost lpost_b) + (Bind f g) +#pop-options + +let step_frame_ret_aux + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#p:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre p) + (f:m st a pre p lpre lpost{Frame? f /\ Ret? (Frame?.f f)}) + : M.MSTATE (step_result st a) st.mem st.locks_preorder (step_req f) (step_ens f) + = + M.MSTATE?.reflect (fun m0 -> + match f with + | Frame (Ret p x lp) frame f_frame -> + Step (p x `st.star` frame) (fun x -> p x `st.star` frame) + (fun h -> lpost h x h) + lpost + (Ret (fun x -> p x `st.star` frame) x lpost), m0) + +let step_frame_ret + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#p:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre p) + (f:m st a pre p lpre lpost{Frame? f /\ Ret? (Frame?.f f)}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + NMSTATE?.reflect (fun (_, n) -> step_frame_ret_aux f, n) + +let step_frame + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#p:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre p) + (f:m st a pre p lpre lpost{Frame? f}) + (step:step_t) + : Mst (step_result st a) (step_req f) (step_ens f) + = + match f with + | Frame (Ret p x lp) frame f_frame -> step_frame_ret f + + | Frame #_ #_ #f_pre #_ #_ #_ f frame f_frame -> + let m0 = get () in + + let Step next_fpre next_fpost next_flpre next_flpost f = step f in + + let m1 = get () in + + preserves_frame_star f_pre next_fpre m0 m1 frame; + + assert ((frame_lpre next_flpre f_frame) (st.core m1)) + by (norm [delta_only [`%frame_lpre]]); + + Step (next_fpre `st.star` frame) (fun x -> next_fpost x `st.star` frame) + (frame_lpre next_flpre f_frame) + (frame_lpost next_flpre next_flpost f_frame) + (Frame f frame f_frame) + +let step_par_ret_aux + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Par? f /\ Ret? (Par?.mL f) /\ Ret? (Par?.mR f)}) + : M.MSTATE (step_result st a) st.mem st.locks_preorder (step_req f) (step_ens f) + = + M.MSTATE?.reflect (fun m0 -> + match f with + | Par #_ #aL #_ #_ #_ #_ (Ret pL xL lpL) #aR #_ #_ #_ #_ (Ret pR xR lpR) -> + let lpost : l_post + #st #(aL & aR) + (pL xL `st.star` pR xR) + (fun (xL, xR) -> pL xL `st.star` pR xR) + = + fun h0 (xL, xR) h1 -> lpL h0 xL h1 /\ lpR h0 xR h1 + in + Step (pL xL `st.star` pR xR) (fun (xL, xR) -> pL xL `st.star` pR xR) + (fun h -> lpL h xL h /\ lpR h xR h) + lpost + (Ret (fun (xL, xR) -> pL xL `st.star` pR xR) (xL, xR) lpost), m0) + +let step_par_ret + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Par? f /\ Ret? (Par?.mL f) /\ Ret? (Par?.mR f)}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + NMSTATE?.reflect (fun (_, n) -> step_par_ret_aux f, n) + +let step_par + (#st:st) + (#a:Type) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Par? f}) + (step:step_t) + : Mst (step_result st a) (step_req f) (step_ens f) + = + match f with + | Par (Ret _ _ _) (Ret _ _ _) -> step_par_ret f + + | Par #_ #aL #preL #postL #lpreL #lpostL mL #aR #preR #postR #lpreR #lpostR mR -> + let b = sample () in + + if b then begin + let m0 = get () in + + let Step next_preL next_postL next_lpreL next_lpostL mL = step mL in + + let m1 = get () in + + preserves_frame_star preL next_preL m0 m1 preR; + par_weaker_lpre_and_stronger_lpost_l lpreL lpostL next_lpreL next_lpostL lpreR lpostR m0 m1; + + let next_post = (fun (xL, xR) -> next_postL xL `st.star` postR xR) in + + assert (stronger_post post next_post) by (norm [delta_only [`%stronger_post]]); + + Step (next_preL `st.star` preR) next_post + (par_lpre next_lpreL lpreR) + (par_lpost next_lpreL next_lpostL lpreR lpostR) + (Par mL mR) + + end + else begin + let m0 = get () in + + let Step next_preR next_postR next_lpreR next_lpostR mR = step mR in + + let m1 = get () in + + preserves_frame_star_left preR next_preR m0 m1 preL; + par_weaker_lpre_and_stronger_lpost_r lpreL lpostL lpreR lpostR next_lpreR next_lpostR m0 m1; + + let next_post = (fun (xL, xR) -> postL xL `st.star` next_postR xR) in + + stronger_post_par_r postL postR next_postR; + + Step (preL `st.star` next_preR) next_post + (par_lpre lpreL next_lpreR) + (par_lpost lpreL lpostL next_lpreR next_lpostR) + (Par mL mR) + end + +let step_weaken + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost{Weaken? f}) + : Mst (step_result st a) (step_req f) (step_ens f) + = + NMSTATE?.reflect (fun (_, n) -> + let Weaken #_ #_ #pre #post #lpre #lpost #_ #_ #_ #_ #_ f = f in + + Step pre post lpre lpost f, n) + +/// Step function + +let rec step + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost) + : Mst (step_result st a) + (step_req f) + (step_ens f) + = + match f with + | Ret _ _ _ -> step_ret f + | Bind _ _ -> step_bind f step + | Act _ -> step_act f + | Frame _ _ _ -> step_frame f step + | Par _ _ -> step_par f step + | Weaken _ _ _ _ -> step_weaken f + +let rec run + (#st:st) + (#a:Type u#a) + (#pre:st.hprop) + (#post:post_t st a) + (#lpre:l_pre pre) + (#lpost:l_post pre post) + (f:m st a pre post lpre lpost) + : Mst a + (requires fun m0 -> + st.interp (pre `st.star` st.locks_invariant m0) m0 /\ + lpre (st.core m0)) + (ensures fun m0 x m1 -> + st.interp (post x `st.star` st.locks_invariant m1) m1 /\ + lpost (st.core m0) x (st.core m1) /\ + preserves_frame pre (post x) m0 m1) + = + match f with + | Ret _ x _ -> x + + | _ -> + let m0 = get () in + let Step new_pre new_post _ _ f = step f in + let m1 = get () in + let x = run f in + let m2 = get () in + + preserves_frame_trans pre new_pre (new_post x) m0 m1 m2; + preserves_frame_stronger_post pre post new_post x m0 m2; + x + +---tokens--- +'(*' Comment +'\n Copyright 2020 Microsoft Research\n\n Licensed under the Apache License, Version 2.0 ' Comment +'(' Comment +'the "License"' Comment +')' Comment +';\n you may not use this file except in compliance with the License.\n You may obtain a copy of the License at\n\n http://www.apache.org/licenses/LICENSE-2.0\n\n Unless required by applicable law or agreed to in writing, software\n distributed under the License is distributed on an "AS IS" BASIS,\n WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n See the License for the specific language governing permissions and\n limitations under the License.\n' Comment + +'*)' Comment +'\n\n' Text + +'module' Keyword +' ' Text +'Steel' Name.Namespace +'.' Punctuation +'Semantics' Name.Namespace +'.' Punctuation +'Hoare' Name.Namespace +'.' Punctuation +'MST' Name.Class +'\n\n' Text + +'module' Keyword +' ' Text +'P' Name.Class +' ' Text +'=' Operator +' ' Text +'FStar' Name.Namespace +'.' Punctuation +'Preorder' Name.Class +'\n\n' Text + +'open' Keyword +' ' Text +'FStar' Name.Namespace +'.' Punctuation +'Tactics' Name.Class +'\n\n' Text + +'open' Keyword +' ' Text +'NMST' Name.Class +'\n\n\n' Text + +'(*' Comment +'\n ' Comment +'*' Comment +' This module provides a semantic model for a combined effect of\n ' Comment +'*' Comment +' divergence, state, and parallel composition of atomic actions.\n ' Comment +'*' Comment +'\n ' Comment +'*' Comment +' It is built over a monotonic state effect -- so that we can give\n ' Comment +'*' Comment +' lock semantics using monotonicity\n ' Comment +'*' Comment +'\n ' Comment +'*' Comment +' It also builds a generic separation-logic-style program logic\n ' Comment +'*' Comment +' for this effect, in a partial correctness setting.\n\n ' Comment +'*' Comment +' It is also be possible to give a variant of this semantics for\n ' Comment +'*' Comment +' total correctness. However, we specifically focus on partial correctness\n ' Comment +'*' Comment +' here so that this semantics can be instantiated with lock operations,\n ' Comment +'*' Comment +' which may deadlock. See ParTot.fst for a total-correctness variant of\n ' Comment +'*' Comment +' these semantics.\n ' Comment +'*' Comment +'\n ' Comment +'*' Comment +' The program logic is specified in the Hoare-style pre- and postconditions\n' Comment + +'*)' Comment +'\n\n\n' Text + +"/// Disabling projectors because we don't use them and they increase the typechecking time" Comment +'\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--fuel 0 --ifuel 2 --z3rlimit 20 --print_implicits --print_universes ' Literal.String.Double +'\\\n' Literal.String.Double + +" --using_facts_from 'Prims FStar.Pervasives FStar.Preorder MST NMST Steel.Semantics.Hoare.MST'" Literal.String.Double +'"' Literal.String.Double +'\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Begin state defn ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'/// We start by defining some basic notions for a commutative monoid.' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// We could reuse FStar.Algebra.CommMonoid, but this style with' Comment +'\n' Text + +'/// quanitifers was more convenient for the proof done here.' Comment +'\n\n\n' Text + +'let' Keyword.Declaration +' ' Text +'symmetry' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +'.' Operator +' ' Text +'{' Operator +':' Operator +'pattern' Name +' ' Text +'(' Operator +'x' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'y' Name +')' Operator +'}' Operator +'\n ' Text +'x' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'y' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'y' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'x' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'transitive' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'z' Name +'.' Operator +' ' Text +'x' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'y' Name +' ' Text +'/\\' Operator +' ' Text +'y' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'z' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'x' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'z' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'associative' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'f' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +')' Operator +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'z' Name +'.' Operator +'\n ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'(' Operator +'f' Name +' ' Text +'y' Name +' ' Text +'z' Name +')' Operator +' ' Text +'`equals`' Operator.Word +' ' Text +'f' Name +' ' Text +'(' Operator +'f' Name +' ' Text +'x' Name +' ' Text +'y' Name +')' Operator +' ' Text +'z' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'commutative' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'f' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +'.' Operator +'{' Operator +':' Operator +'pattern' Name +' ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'y' Name +'}' Operator +'\n ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'f' Name +' ' Text +'y' Name +' ' Text +'x' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'is_unit' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'equals' Name +':' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'f' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'y' Name +'.' Operator +' ' Text +'{' Operator +':' Operator +'pattern' Name +' ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'\\/' Operator +' ' Text +'f' Name +' ' Text +'y' Name +' ' Text +'x' Name +'}' Operator +'\n ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'y' Name +' ' Text +'/\\' Operator +'\n ' Text +'f' Name +' ' Text +'y' Name +' ' Text +'x' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'y' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'equals_ext' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'f' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'a' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x1' Name +' ' Text +'x2' Name +' ' Text +'y' Name +'.' Operator +' ' Text +'x1' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'x2' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'f' Name +' ' Text +'x1' Name +' ' Text +'y' Name +' ' Text +'`equals`' Operator.Word +' ' Text +'f' Name +' ' Text +'x2' Name +' ' Text +'y' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'fp_heap_0' Name +'\n ' Text +'(' Operator +'#' Operator +'heap' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'hprop' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'interp' Name +':' Operator +'hprop' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'pre' Name +':' Operator +'hprop' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'h' Name +':' Operator +'heap' Name +'{' Operator +'interp' Name +' ' Text +'pre' Name +' ' Text +'h' Name +'}' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on_0' Name +'\n ' Text +'(' Operator +'#' Operator +'heap' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'hprop' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'interp' Name +':' Operator +'hprop' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'disjoint' Name +':' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'join' Name +':' Operator +' ' Text +'(' Operator +'h0' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'h1' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +' ' Text +'->' Operator +' ' Text +'heap' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'fp' Name +':' Operator +' ' Text +'hprop' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'h0' Name +':' Operator +'fp_heap_0' Name +' ' Text +'interp' Name +' ' Text +'fp' Name +')' Operator +' ' Text +'(' Operator +'h1' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +')' Operator +'.' Operator +' ' Text +'q' Name +' ' Text +'h0' Name +' ' Text +'<==>' Operator +' ' Text +'q' Name +' ' Text +'(' Operator +'join' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'fp_prop_0' Name +'\n ' Text +'(' Operator +'#' Operator +'heap' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'hprop' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'interp' Name +':' Operator +'hprop' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'disjoint' Name +':' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'join' Name +':' Operator +' ' Text +'(' Operator +'h0' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'h1' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +' ' Text +'->' Operator +' ' Text +'heap' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'fp' Name +':' Operator +'hprop' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'p' Name +':' Operator +'(' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'{' Operator +'p' Name +' ' Text +'`' Keyword +'(' Operator +'depends_only_on_0' Name +' ' Text +'interp' Name +' ' Text +'disjoint' Name +' ' Text +'join' Name +')' Operator +'`' Keyword +' ' Text +'fp' Name +'}' Operator +'\n\n' Text + +'noeq' Keyword +'\n' Text + +'type' Keyword +' ' Text +'st0' Name +' ' Text +'=' Operator +' ' Text +'{' Operator +'\n ' Text +'mem' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'2' Literal.Number.Integer +';' Operator +'\n ' Text +'core' Name +':' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'mem' Name +';' Operator +'\n\n ' Text +'locks_preorder' Name +':' Operator +'P' Name.Namespace +'.' Punctuation +'preorder' Name +' ' Text +'mem' Name +';' Operator +'\n ' Text +'hprop' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'2' Literal.Number.Integer +';' Operator +'\n ' Text +'locks_invariant' Name +':' Operator +' ' Text +'mem' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +';' Operator +'\n\n ' Text +'disjoint' Name +':' Operator +' ' Text +'mem' Name +' ' Text +'->' Operator +' ' Text +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +';' Operator +'\n ' Text +'join' Name +':' Operator +' ' Text +'h0' Name +':' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'h1' Name +':' Operator +'mem' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +' ' Text +'->' Operator +' ' Text +'mem' Name +';' Operator +'\n\n ' Text +'interp' Name +':' Operator +' ' Text +'hprop' Name +' ' Text +'->' Operator +' ' Text +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +';' Operator +'\n\n ' Text +'emp' Name +':' Operator +'hprop' Name +';' Operator +'\n ' Text +'star' Name +':' Operator +' ' Text +'hprop' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +';' Operator +'\n\n ' Text +'equals' Name +':' Operator +' ' Text +'hprop' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +';' Operator +'\n' Text + +'}' Operator +'\n\n\n' Text + +'/// disjointness is symmetric' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'disjoint_sym' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'h0' Name +' ' Text +'h1' Name +'.' Operator +' ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +' ' Text +'<==>' Operator +' ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'h1' Name +' ' Text +'h0' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'disjoint_join' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m0' Name +' ' Text +'m2' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'m2' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m0' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'m1' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'join_commutative' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +' ' Text +'{' Operator +' ' Text +'disjoint_sym' Name +' ' Text +'st' Name +' ' Text +'}' Operator +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'m0' Name +' ' Text +'m1' Name +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'=' Operator +'=' Operator +' ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'m1' Name +' ' Text +'m0' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'join_associative' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +'{' Operator +'disjoint_join' Name +' ' Text +'st' Name +'}' Operator +')' Operator +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'join' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'m2' Name +'\n\n' Text + +'////////////////////////////////////////////////////////////////////////////////' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'interp_extensionality' Name +' ' Text +'#' Operator +'r' Name +' ' Text +'#' Operator +'s' Name +' ' Text +'(' Operator +'equals' Name +':' Operator +'r' Name +' ' Text +'->' Operator +' ' Text +'r' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'f' Name +':' Operator +'r' Name +' ' Text +'->' Operator +' ' Text +'s' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'h' Name +'.' Operator +' ' Text +'{' Operator +':' Operator +'pattern' Name +' ' Text +'equals' Name +' ' Text +'x' Name +' ' Text +'y' Name +';' Operator +' ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'h' Name +'}' Operator +' ' Text +'equals' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'/\\' Operator +' ' Text +'f' Name +' ' Text +'x' Name +' ' Text +'h' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'f' Name +' ' Text +'y' Name +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'affine' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'r0' Name +' ' Text +'r1' Name +' ' Text +'s' Name +'.' Operator +' ' Text +'{' Operator +':' Operator +'pattern' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'r0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r1' Name +')' Operator +' ' Text +'s' Name +')' Operator +' ' Text +'}' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'r0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r1' Name +')' Operator +' ' Text +'s' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'r0' Name +' ' Text +'s' Name +'\n\n' Text + +'////////////////////////////////////////////////////////////////////////////////' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'(' Operator +'q' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'fp' Name +':' Operator +' ' Text +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'depends_only_on_0' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'q' Name +' ' Text +'fp' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'fp_prop' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'(' Operator +'fp' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'fp_prop_0' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'fp' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'lemma_weaken_depends_only_on' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st0' Name +'{' Operator +'affine' Name +' ' Text +'st' Name +'}' Operator +')' Operator +'\n ' Text +'(' Operator +'fp0' Name +' ' Text +'fp1' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'fp_prop' Name +' ' Text +'fp0' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +' ' Text +'(' Operator +'q' Name +' ' Text +'`depends_only_on`' Operator.Word +' ' Text +'(' Operator +'fp0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'fp1' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'st_laws' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'(*' Comment +' standard laws about the equality relation ' Comment +'*)' Comment +'\n ' Text +'symmetry' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'/\\' Operator +'\n ' Text +'transitive' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'/\\' Operator +'\n ' Text +'interp_extensionality' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'/\\' Operator +'\n ' Text +'(*' Comment +' standard laws for star forming a CM ' Comment +'*)' Comment +'\n ' Text +'associative' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'st' Name +'.' Operator +'star' Name +' ' Text +'/\\' Operator +'\n ' Text +'commutative' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'st' Name +'.' Operator +'star' Name +' ' Text +'/\\' Operator +'\n ' Text +'is_unit' Name +' ' Text +'st' Name +'.' Operator +'emp' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'st' Name +'.' Operator +'star' Name +' ' Text +'/\\' Operator +'\n ' Text +'equals_ext' Name +' ' Text +'st' Name +'.' Operator +'equals' Name +' ' Text +'st' Name +'.' Operator +'star' Name +' ' Text +'/\\' Operator +'\n ' Text +'(*' Comment +" We're working in an affine interpretation of SL " Comment +'*)' Comment +'\n ' Text +'affine' Name +' ' Text +'st' Name +' ' Text +'/\\' Operator +'\n ' Text +'(*' Comment +' laws about disjoint and join ' Comment +'*)' Comment +'\n ' Text +'disjoint_sym' Name +' ' Text +'st' Name +' ' Text +'/\\' Operator +'\n ' Text +'disjoint_join' Name +' ' Text +'st' Name +' ' Text +'/\\' Operator +'\n ' Text +'join_commutative' Name +' ' Text +'st' Name +' ' Text +'/\\' Operator +'\n ' Text +'join_associative' Name +' ' Text +'st' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'st' Name +' ' Text +'=' Operator +' ' Text +'s' Name +':' Operator +'st0' Name +' ' Text +'{' Operator +' ' Text +'st_laws' Name +' ' Text +'s' Name +' ' Text +'}' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' End state defn ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Begin expects, provides, requires, and ensures defns ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'/// expects (the heap assertion expected by a computation) is simply an st.hprop' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// provides, or the post heap assertion, is a st.hprop on [a]-typed result' Comment +'\n\n' Text + +'type' Keyword +' ' Text +'post_t' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'=' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'hprop' Name +'\n\n\n' Text + +'/// requires is a heap predicate that depends only on a pre heap assertion' Comment +'\n' Text + +'/// (where the notion of `depends only on` is defined above as part of the state definition)' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// we call the type l_pre for logical precondition' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'=' Operator +' ' Text +'fp_prop' Name +' ' Text +'pre' Name +'\n\n\n' Text + +'/// ensures is a 2-state postcondition of type heap -> a -> heap -> prop' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// To define ensures, we need a notion of depends_only_on_2' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// Essentially, in the first heap argument, postconditions depend only on the expects hprop' Comment +'\n' Text + +'/// and in the second heap argument, postconditions depend only on the provides hprop' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// Also note that the support for depends_only_on_2 is not required from the underlying memory model' Comment +'\n\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on_0_2' Name +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'heap' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'hprop' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'interp' Name +':' Operator +'hprop' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'disjoint' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'join' Name +':' Operator +'(' Operator +'h0' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'h1' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +' ' Text +'->' Operator +' ' Text +'heap' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +' ' Text +'(' Operator +'fp_pre' Name +':' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'fp_post' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +')' Operator +'\n\n ' Text +'=' Operator +' ' Text +'//' Operator +'can' Name +' ' Text +'join' Name +' ' Text +'any' Name +' ' Text +'disjoint' Name +' ' Text +'heap' Name +' ' Text +'to' Name +' ' Text +'the' Name +' ' Text +'pre' Name +'-' Operator +'heap' Name +' ' Text +'and' Name +' ' Text +'q' Name +' ' Text +'is' Name +' ' Text +'still' Name +' ' Text +'valid' Name +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'x' Name +' ' Text +'(' Operator +'h_pre' Name +':' Operator +'fp_heap_0' Name +' ' Text +'interp' Name +' ' Text +'fp_pre' Name +')' Operator +' ' Text +'h_post' Name +' ' Text +'(' Operator +'h' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h_pre' Name +' ' Text +'h' Name +'}' Operator +')' Operator +'.' Operator +'\n ' Text +'q' Name +' ' Text +'h_pre' Name +' ' Text +'x' Name +' ' Text +'h_post' Name +' ' Text +'<==>' Operator +' ' Text +'q' Name +' ' Text +'(' Operator +'join' Name +' ' Text +'h_pre' Name +' ' Text +'h' Name +')' Operator +' ' Text +'x' Name +' ' Text +'h_post' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'//' Operator +'can' Name +' ' Text +'join' Name +' ' Text +'any' Name +' ' Text +'disjoint' Name +' ' Text +'heap' Name +' ' Text +'to' Name +' ' Text +'the' Name +' ' Text +'post' Name +'-' Operator +'heap' Name +' ' Text +'and' Name +' ' Text +'q' Name +' ' Text +'is' Name +' ' Text +'still' Name +' ' Text +'valid' Name +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'x' Name +' ' Text +'h_pre' Name +' ' Text +'(' Operator +'h_post' Name +':' Operator +'fp_heap_0' Name +' ' Text +'interp' Name +' ' Text +'(' Operator +'fp_post' Name +' ' Text +'x' Name +')' Operator +')' Operator +' ' Text +'(' Operator +'h' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h_post' Name +' ' Text +'h' Name +'}' Operator +')' Operator +'.' Operator +'\n ' Text +'q' Name +' ' Text +'h_pre' Name +' ' Text +'x' Name +' ' Text +'h_post' Name +' ' Text +'<==>' Operator +' ' Text +'q' Name +' ' Text +'h_pre' Name +' ' Text +'x' Name +' ' Text +'(' Operator +'join' Name +' ' Text +'h_post' Name +' ' Text +'h' Name +')' Operator +')' Operator +'\n\n' Text + +'/// Abbreviations for two-state depends' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'fp_prop_0_2' Name +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'heap' Name +' ' Text +'#' Operator +'hprop' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'interp' Name +':' Operator +'hprop' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'disjoint' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'join' Name +':' Operator +'(' Operator +'h0' Name +':' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'h1' Name +':' Operator +'heap' Name +'{' Operator +'disjoint' Name +' ' Text +'h0' Name +' ' Text +'h1' Name +'}' Operator +' ' Text +'->' Operator +' ' Text +'heap' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'fp_pre' Name +':' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_post' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'hprop' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'q' Name +':' Operator +'(' Operator +'heap' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'heap' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'{' Operator +'depends_only_on_0_2' Name +' ' Text +'interp' Name +' ' Text +'disjoint' Name +' ' Text +'join' Name +' ' Text +'q' Name +' ' Text +'fp_pre' Name +' ' Text +'fp_post' Name +'}' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on2' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_post' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'depends_only_on_0_2' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'st' Name +'.' Operator +'disjoint' Name +' ' Text +'st' Name +'.' Operator +'join' Name +' ' Text +'q' Name +' ' Text +'fp_pre' Name +' ' Text +'fp_post' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'fp_prop2' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st0' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'(' Operator +'fp_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'fp_post' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'q' Name +':' Operator +'(' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'{' Operator +'depends_only_on2' Name +' ' Text +'q' Name +' ' Text +'fp_pre' Name +' ' Text +'fp_post' Name +'}' Operator +'\n\n' Text + +'/// Finally the type of 2-state postconditions' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'l_post' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'(' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'=' Operator +' ' Text +'fp_prop2' Name +' ' Text +'pre' Name +' ' Text +'post' Name +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' End expects, provides, requires,\n and ensures defns ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'effect' Keyword +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'req' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'Type0' Name.Class +')' Operator +' ' Text +'(' Operator +'ens' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'Type0' Name.Class +')' Operator +' ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +' ' Text +'a' Name +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'st' Name +'.' Operator +'locks_preorder' Name +' ' Text +'req' Name +' ' Text +'ens' Name +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Begin interface of actions ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'/// Actions are essentially state transformers that preserve frames' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'preserves_frame' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'pre' Name +' ' Text +'post' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +')' Operator +' ' Text +'m0' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'frame' Name +')' Operator +'.' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'action_t' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'unit' Keyword.Type +' ' Text +'->' Operator +'\n ' Text +'Mst' Name.Class +' ' Text +'a' Name +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'x' Name +' ' Text +'m1' Name +' ' Text +'->' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'x' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' End interface of actions ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Begin definition of the computation AST ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'/// Gadgets for building lpre- and lpostconditions for various nodes' Comment +'\n\n\n' Text + +'/// Return node is parametric in provides and ensures' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'return_lpre' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpost' Name +' ' Text +'h' Name +' ' Text +'x' Name +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'frame_lpre' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'frame' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpre' Name +' ' Text +'h' Name +' ' Text +'/\\' Operator +' ' Text +'f_frame' Name +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'frame_lpost' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'frame' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'->' Operator +' ' Text +'lpre' Name +' ' Text +'h0' Name +' ' Text +'/\\' Operator +' ' Text +'lpost' Name +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'/\\' Operator +' ' Text +'f_frame' Name +' ' Text +'h1' Name +'\n\n' Text + +'/// The bind rule bakes in weakening of requires / ensures' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'bind_lpre' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post_a' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre_a' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'lpost_a' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post_a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre_b' Name +':' Operator +'(' Operator +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +')' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_pre' Name +' ' Text +'pre' Name +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpre_a' Name +' ' Text +'h' Name +' ' Text +'/\\' Operator +' ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'h1' Name +'.' Operator +' ' Text +'lpost_a' Name +' ' Text +'h' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'lpre_b' Name +' ' Text +'x' Name +' ' Text +'h1' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'bind_lpost' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post_a' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre_a' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'lpost_a' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post_a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'b' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post_b' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'b' Name +')' Operator +'\n ' Text +'(' Operator +'lpost_b' Name +':' Operator +'(' Operator +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +')' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post_b' Name +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h0' Name +' ' Text +'y' Name +' ' Text +'h2' Name +' ' Text +'->' Operator +' ' Text +'lpre_a' Name +' ' Text +'h0' Name +' ' Text +'/\\' Operator +' ' Text +'(' Operator +'exists' Keyword +' ' Text +'x' Name +' ' Text +'h1' Name +'.' Operator +' ' Text +'lpost_a' Name +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'/\\' Operator +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'h1' Name +' ' Text +'y' Name +' ' Text +'h2' Name +')' Operator +'\n\n' Text + +'/// Parallel composition is pointwise' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'par_lpre' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'preL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'preR' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpreL' Name +' ' Text +'h' Name +' ' Text +'/\\' Operator +' ' Text +'lpreR' Name +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'par_lpost' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aL' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +')' Operator +'\n ' Text +'(' Operator +'lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'preL' Name +')' Operator +'\n ' Text +'(' Operator +'lpostL' Name +':' Operator +'l_post' Name +' ' Text +'preL' Name +' ' Text +'postL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aR' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'preR' Name +')' Operator +'\n ' Text +'(' Operator +'lpostR' Name +':' Operator +'l_post' Name +' ' Text +'preR' Name +' ' Text +'postR' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h0' Name +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'h1' Name +' ' Text +'->' Operator +' ' Text +'lpreL' Name +' ' Text +'h0' Name +' ' Text +'/\\' Operator +' ' Text +'lpreR' Name +' ' Text +'h0' Name +' ' Text +'/\\' Operator +' ' Text +'lpostL' Name +' ' Text +'h0' Name +' ' Text +'xL' Name +' ' Text +'h1' Name +' ' Text +'/\\' Operator +' ' Text +'lpostR' Name +' ' Text +'h0' Name +' ' Text +'xR' Name +' ' Text +'h1' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'weaker_pre' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'next_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'h' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'next_pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'stronger_post' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'post' Name +' ' Text +'next_post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'h' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'weakening_ok' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'wpre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'wpost' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'wlpre' Name +':' Operator +'l_pre' Name +' ' Text +'wpre' Name +')' Operator +'\n ' Text +'(' Operator +'wlpost' Name +':' Operator +'l_post' Name +' ' Text +'wpre' Name +' ' Text +'wpost' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'weaker_pre' Name +' ' Text +'wpre' Name +' ' Text +'pre' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_post' Name +' ' Text +'wpost' Name +' ' Text +'post' Name +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'h' Name +'.' Operator +' ' Text +'wlpre' Name +' ' Text +'h' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'lpre' Name +' ' Text +'h' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +'.' Operator +' ' Text +'lpost' Name +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'wlpost' Name +' ' Text +'h0' Name +' ' Text +'x' Name +' ' Text +'h1' Name +')' Operator +'\n\n\n' Text + +'/// Setting the flag just to reduce the time to typecheck the type m' Comment +'\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--__temp_no_proj Steel.Semantics.Hoare.MST' Literal.String.Double +'"' Literal.String.Double +'\n' Text + +'noeq' Keyword +'\n' Text + +'type' Keyword +' ' Text +'m' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +':' Operator +'\n ' Text +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'->' Operator +' ' Text +'Type' Name.Class +'\n ' Text +'=' Operator +'\n ' Text +'|' Operator +' ' Text +'Ret' Name.Class +':' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +' ' Text +'(' Operator +'return_lpre' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'lpost' Name +')' Operator +' ' Text +'lpost' Name +'\n\n ' Text +'|' Operator +' ' Text +'Bind' Name.Class +':' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post_a' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre_a' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost_a' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post_a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'b' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post_b' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'b' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre_b' Name +':' Operator +'(' Operator +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +')' Operator +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost_b' Name +':' Operator +'(' Operator +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +')' Operator +' ' Text +'->' Operator +'\n ' Text +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post_a' Name +' ' Text +'lpre_a' Name +' ' Text +'lpost_a' Name +' ' Text +'->' Operator +'\n ' Text +'g' Name +':' Operator +'(' Operator +'x' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'Dv' Name.Class +' ' Text +'(' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'b' Name +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +' ' Text +'(' Operator +'lpre_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +')' Operator +')' Operator +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'b' Name +' ' Text +'pre' Name +' ' Text +'post_b' Name +'\n ' Text +'(' Operator +'bind_lpre' Name +' ' Text +'lpre_a' Name +' ' Text +'lpost_a' Name +' ' Text +'lpre_b' Name +')' Operator +'\n ' Text +'(' Operator +'bind_lpost' Name +' ' Text +'lpre_a' Name +' ' Text +'lpost_a' Name +' ' Text +'lpost_b' Name +')' Operator +'\n\n ' Text +'|' Operator +' ' Text +'Act' Name.Class +':' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'->' Operator +'\n ' Text +'f' Name +':' Operator +'action_t' Name +' ' Text +'#' Operator +'st' Name +' ' Text +'#' Operator +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'\n\n ' Text +'|' Operator +' ' Text +'Frame' Name.Class +':' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'->' Operator +'\n ' Text +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'->' Operator +'\n ' Text +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'frame' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +'\n ' Text +'(' Operator +'frame_lpre' Name +' ' Text +'lpre' Name +' ' Text +'f_frame' Name +')' Operator +'\n ' Text +'(' Operator +'frame_lpost' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'f_frame' Name +')' Operator +'\n\n ' Text +'|' Operator +' ' Text +'Par' Name.Class +':' Operator +'\n ' Text +'#' Operator +'aL' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'preL' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpostL' Name +':' Operator +'l_post' Name +' ' Text +'preL' Name +' ' Text +'postL' Name +' ' Text +'->' Operator +'\n ' Text +'mL' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'aL' Name +' ' Text +'preL' Name +' ' Text +'postL' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'aR' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'preR' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpostR' Name +':' Operator +'l_post' Name +' ' Text +'preR' Name +' ' Text +'postR' Name +' ' Text +'->' Operator +'\n ' Text +'mR' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'aR' Name +' ' Text +'preR' Name +' ' Text +'postR' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'(' Operator +'aL' Name +' ' Text +'&' Operator +' ' Text +'aR' Name +')' Operator +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'lpreR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +')' Operator +'\n\n ' Text +'|' Operator +' ' Text +'Weaken' Name.Class +':' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'wpre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'wpost' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'wlpre' Name +':' Operator +'l_pre' Name +' ' Text +'wpre' Name +' ' Text +'->' Operator +'\n ' Text +'wlpost' Name +':' Operator +'l_post' Name +' ' Text +'wpre' Name +' ' Text +'wpost' Name +' ' Text +'->' Operator +'\n ' Text +'_' Name +':' Operator +'squash' Name +' ' Text +'(' Operator +'weakening_ok' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'wlpre' Name +' ' Text +'wlpost' Name +')' Operator +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'wpre' Name +' ' Text +'wpost' Name +' ' Text +'wlpre' Name +' ' Text +'wlpost' Name +'\n' Text + +'#' Operator +'pop' Name +'-' Operator +'options' Name +'\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' End definition of the computation AST ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Stepping relation ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'/// All steps preserve frames' Comment +'\n\n' Text + +'noeq' Keyword +'\n' Text + +'type' Keyword +' ' Text +'step_result' Name +' ' Text +'(' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'|' Operator +' ' Text +'Step' Name.Class +':' Operator +'\n ' Text +'next_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'next_post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'next_pre' Name +' ' Text +'->' Operator +'\n ' Text +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'next_pre' Name +' ' Text +'next_post' Name +' ' Text +'->' Operator +'\n ' Text +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'next_pre' Name +' ' Text +'next_post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'->' Operator +'\n ' Text +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Type of the single-step interpreter ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n\n' Text + +'/// Interpreter is setup as a Div function from computation trees to computation trees' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// While the requires for the Div is standard (that the expects hprop holds and requires is valid),' Comment +'\n' Text + +'/// the ensures is interesting' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// As the computation evolves, the requires and ensures associated with the computation graph nodes' Comment +'\n' Text + +'/// also evolve' Comment +'\n' Text + +'/// But they evolve systematically: preconditions become weaker and postconditions become stronger' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// Consider { req } c | st { ens } ~~> { req1 } c1 | st1 { ens1 }' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// Then, req st ==> req1 st1 /\\' Comment +'\n' Text + +'/// (forall x st_final. ens1 st1 x st_final ==> ens st x st_final)' Comment +'\n\n\n' Text + +'unfold' Keyword +'\n' Text + +'let' Keyword.Declaration +' ' Text +'step_req' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'Type0' Name.Class +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'weaker_lpre' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'next_lpre' Name +':' Operator +'l_pre' Name +' ' Text +'next_pre' Name +')' Operator +'\n ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +'>' Operator +' ' Text +'next_lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'stronger_lpost' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'#' Operator +'next_post' Name +'\n ' Text +'(' Operator +'next_lpost' Name +':' Operator +'l_post' Name +' ' Text +'next_pre' Name +' ' Text +'next_post' Name +')' Operator +'\n ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'h_final' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'.' Operator +'\n ' Text +'next_lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'x' Name +' ' Text +'h_final' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'x' Name +' ' Text +'h_final' Name +'\n\n' Text + +'unfold' Keyword +'\n' Text + +'let' Keyword.Declaration +' ' Text +'step_ens' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'Type0' Name.Class +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'r' Name +' ' Text +'m1' Name +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'next_pre' Name +' ' Text +'next_post' Name +' ' Text +'next_lpre' Name +' ' Text +'next_lpost' Name +' ' Text +'_' Name +' ' Text +'=' Operator +' ' Text +'r' Name +' ' Text +'in' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'next_pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_post' Name +' ' Text +'post' Name +' ' Text +'next_post' Name +' ' Text +'/\\' Operator +'\n ' Text +'next_lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'next_pre' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'weaker_lpre' Name +' ' Text +'lpre' Name +' ' Text +'next_lpre' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_lpost' Name +' ' Text +'lpost' Name +' ' Text +'next_lpost' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +'\n\n\n' Text + +'/// The type of the stepping function' Comment +'\n\n' Text + +'type' Keyword +' ' Text +'step_t' Name +' ' Text +'=' Operator +'\n ' Text +'#' Operator +'st' Name +':' Operator +'st' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +' ' Text +'->' Operator +'\n ' Text +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'->' Operator +'\n ' Text +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'->' Operator +'\n ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Auxiliary lemmas ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'/// Some AC lemmas on `st.star`' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'apply_assoc' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +' ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +')' Operator +' ' Text +'(' Operator +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'equals_ext_left' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'p' Name +' ' Text +'`st.equals`' Operator.Word +' ' Text +'q' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.equals`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'equals_ext_right' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'q' Name +' ' Text +'`st.equals`' Operator.Word +' ' Text +'r' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +' ' Text +'`st.equals`' Operator.Word +' ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'p' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'p' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +';' Operator +'\n ' Text +'}' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'commute_star_right' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +')' Operator +' ' Text +'`st.equals`' Operator.Word +'\n ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'equals_ext_right' Name +' ' Text +'p' Name +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +' ' Text +'}' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +';' Operator +'\n ' Text +'}' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'assoc_star_right' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +' ' Text +'s' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +' ' Text +'`st.equals`' Operator.Word +'\n ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'equals_ext_right' Name +' ' Text +'p' Name +' ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +'\n ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +' ' Text +'}' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +';' Operator +'\n ' Text +'}' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'commute_assoc_star_right' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +' ' Text +'r' Name +' ' Text +'s' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +' ' Text +'`st.equals`' Operator.Word +'\n ' Text +'(' Operator +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'equals_ext_right' Name +' ' Text +'p' Name +'\n ' Text +'(' Operator +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'r' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +'\n ' Text +'(' Operator +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +' ' Text +'}' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'q' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'assoc_star_right' Name +' ' Text +'p' Name +' ' Text +'r' Name +' ' Text +'q' Name +' ' Text +'s' Name +' ' Text +'}' Operator +'\n ' Text +'p' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'r' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'q' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'s' Name +')' Operator +')' Operator +';' Operator +'\n ' Text +'}' Operator +'\n\n\n' Text + +'/// Apply extensionality manually, control proofs' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'apply_interp_ext' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'p' Name +' ' Text +'q' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'p' Name +' ' Text +'m' Name +' ' Text +'/\\' Operator +' ' Text +'p' Name +' ' Text +'`st.equals`' Operator.Word +' ' Text +'q' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'q' Name +' ' Text +'m' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'weaken_fp_prop' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +' ' Text +"frame'" Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +'.' Operator +'\n ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +"frame'" Name +')' Operator +'.' Operator +'\n ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on_commutes_with_weaker' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'fp' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_next' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'depends_only_on' Name +' ' Text +'q' Name +' ' Text +'fp' Name +' ' Text +'/\\' Operator +' ' Text +'weaker_pre' Name +' ' Text +'fp_next' Name +' ' Text +'fp' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'depends_only_on' Name +' ' Text +'q' Name +' ' Text +'fp_next' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'h0' Name +':' Operator +'fp_heap_0' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'fp_next' Name +')' Operator +'.' Operator +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'fp_next' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'emp' Name +')' Operator +' ' Text +'h0' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'depends_only_on2_commutes_with_weaker' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'q' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'->' Operator +' ' Text +'prop' Name +')' Operator +'\n ' Text +'(' Operator +'fp' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_next' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'fp_post' Name +':' Operator +'a' Name +' ' Text +'->' Operator +' ' Text +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'depends_only_on2' Name +' ' Text +'q' Name +' ' Text +'fp' Name +' ' Text +'fp_post' Name +' ' Text +'/\\' Operator +' ' Text +'weaker_pre' Name +' ' Text +'fp_next' Name +' ' Text +'fp' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'depends_only_on2' Name +' ' Text +'q' Name +' ' Text +'fp_next' Name +' ' Text +'fp_post' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'h0' Name +':' Operator +'fp_heap_0' Name +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'fp_next' Name +')' Operator +'.' Operator +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'fp_next' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'emp' Name +')' Operator +' ' Text +'h0' Name +')' Operator +'\n\n' Text + +'/// Lemmas about preserves_frame' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'preserves_frame_trans' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'hp1' Name +' ' Text +'hp2' Name +' ' Text +'hp3' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'m1' Name +' ' Text +'m2' Name +' ' Text +'m3' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'hp1' Name +' ' Text +'hp2' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +' ' Text +'/\\' Operator +' ' Text +'preserves_frame' Name +' ' Text +'hp2' Name +' ' Text +'hp3' Name +' ' Text +'m2' Name +' ' Text +'m3' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'hp1' Name +' ' Text +'hp3' Name +' ' Text +'m1' Name +' ' Text +'m3' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--warn_error -271' Literal.String.Double +'"' Literal.String.Double +'\n' Text + +'let' Keyword.Declaration +' ' Text +'preserves_frame_stronger_post' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'post' Name +' ' Text +'post_s' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'m1' Name +' ' Text +'m2' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'(' Operator +'post_s' Name +' ' Text +'x' Name +')' Operator +' ' Text +'m1' Name +' ' Text +'m2' Name +' ' Text +'/\\' Operator +' ' Text +'stronger_post' Name +' ' Text +'post' Name +' ' Text +'post_s' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'m1' Name +' ' Text +'m2' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'aux' Name +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m1' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m2' Name +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +'frame' Name +')' Operator +'.' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m2' Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'[' Operator +'SMTPat' Name.Class +' ' Text +'()' Name.Builtin.Pseudo +']' Operator +'\n ' Text +'=' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post_s' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m2' Name +')' Operator +';' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post_s' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'post_s' Name +' ' Text +'x' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'post_s' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'post_s' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'}' Operator +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'post_s' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m2' Name +')' Operator +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m2' Name +')' Operator +';' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'apply_assoc' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +')' Operator +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'frame' Name +' ' Text +'}' Operator +'\n ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'}' Operator +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m2' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'m2' Name +')' Operator +'\n ' Text +'in' Keyword +'\n ' Text +'()' Name.Builtin.Pseudo +'\n' Text + +'#' Operator +'pop' Name +'-' Operator +'options' Name +'\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--z3rlimit 40 --warn_error -271' Literal.String.Double +'"' Literal.String.Double +'\n' Text + +'let' Keyword.Declaration +' ' Text +'preserves_frame_star' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'pre' Name +' ' Text +'post' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'aux' Name +' ' Text +'(' Operator +"frame'" Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +' ' Text +'m0' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +'\n ' Text +'(' Operator +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +"frame'" Name +')' Operator +'.' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'[' Operator +'SMTPat' Name.Class +' ' Text +'()' Name.Builtin.Pseudo +']' Operator +'\n ' Text +'=' Operator +'\n ' Text +'assoc_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'pre' Name +' ' Text +'frame' Name +' ' Text +"frame'" Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'m0' Name +';' Operator +'\n ' Text +'assoc_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'post' Name +' ' Text +'frame' Name +' ' Text +"frame'" Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +'\n ' Text +'m1' Name +';' Operator +'\n ' Text +'weaken_fp_prop' Name +' ' Text +'frame' Name +' ' Text +"frame'" Name +' ' Text +'m0' Name +' ' Text +'m1' Name +'\n ' Text +'in' Keyword +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'preserves_frame_star_left' Name +' ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +' ' Text +'(' Operator +'pre' Name +' ' Text +'post' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'preserves_frame' Name +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pre' Name +')' Operator +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'post' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'aux' Name +' ' Text +'(' Operator +"frame'" Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pre' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +' ' Text +'m0' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +'\n ' Text +'(' Operator +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'post' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'f_frame' Name +':' Operator +'fp_prop' Name +' ' Text +"frame'" Name +')' Operator +'.' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'=' Operator +'=' Operator +' ' Text +'f_frame' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'[' Operator +'SMTPat' Name.Class +' ' Text +'()' Name.Builtin.Pseudo +']' Operator +'\n ' Text +'=' Operator +'\n ' Text +'commute_assoc_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'frame' Name +' ' Text +'pre' Name +' ' Text +"frame'" Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pre' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'m0' Name +';' Operator +'\n ' Text +'commute_assoc_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'frame' Name +' ' Text +'post' Name +' ' Text +"frame'" Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'post' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'(' Operator +'frame' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'post' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +"frame'" Name +')' Operator +')' Operator +'\n ' Text +'m1' Name +';' Operator +'\n ' Text +'weaken_fp_prop' Name +' ' Text +'frame' Name +' ' Text +"frame'" Name +' ' Text +'m0' Name +' ' Text +'m1' Name +'\n ' Text +'in' Keyword +'\n ' Text +'()' Name.Builtin.Pseudo +'\n' Text + +'#' Operator +'pop' Name +'-' Operator +'options' Name +'\n\n\n' Text + +'/// Lemma frame_post_for_par is used in the par proof' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// E.g. in the par rule, when L takes a step, we can frame the requires of R' Comment +'\n' Text + +'/// by using the preserves_frame property of the stepping relation' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// However we also need to frame the ensures of R, for establishing stronger_post' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// Basically, we need:' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// forall x h_final. postR prev_state x h_final <==> postR next_state x h_final' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// (the proof only requires the reverse implication, but we can prove iff)' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// To prove this, we rely on the framing of all frame fp props provides by the stepping relation' Comment +'\n' Text + +'///' Comment +'\n' Text + +'/// To use it, we instantiate the fp prop with inst_heap_prop_for_par' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'inst_heap_prop_for_par' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'state' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'fp_prop' Name +' ' Text +'pre' Name +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'final_state' Name +'.' Operator +'\n ' Text +'lpost' Name +' ' Text +'h' Name +' ' Text +'x' Name +' ' Text +'final_state' Name +' ' Text +'<==>' Operator +'\n ' Text +'lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'x' Name +' ' Text +'final_state' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'frame_post_for_par_tautology' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre_f' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post_f' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpost_f' Name +':' Operator +'l_post' Name +' ' Text +'pre_f' Name +' ' Text +'post_f' Name +')' Operator +'\n ' Text +'(' Operator +'m0' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +' ' Text +'(' Operator +'inst_heap_prop_for_par' Name +' ' Text +'lpost_f' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'frame_post_for_par_aux' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'pre_s' Name +' ' Text +'post_s' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +' ' Text +'(' Operator +'#' Operator +'pre_f' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +' ' Text +'(' Operator +'#' Operator +'post_f' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'lpost_f' Name +':' Operator +'l_post' Name +' ' Text +'pre_f' Name +' ' Text +'post_f' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'preserves_frame' Name +' ' Text +'pre_s' Name +' ' Text +'post_s' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'pre_s' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pre_f' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'m0' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'inst_heap_prop_for_par' Name +' ' Text +'lpost_f' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'<==>' Operator +'\n ' Text +'inst_heap_prop_for_par' Name +' ' Text +'lpost_f' Name +' ' Text +'m0' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'()' Name.Builtin.Pseudo +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'frame_post_for_par' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'pre_s' Name +' ' Text +'post_s' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'m0' Name +' ' Text +'m1' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre_f' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post_f' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpre_f' Name +':' Operator +'l_pre' Name +' ' Text +'pre_f' Name +')' Operator +'\n ' Text +'(' Operator +'lpost_f' Name +':' Operator +'l_post' Name +' ' Text +'pre_f' Name +' ' Text +'post_f' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'preserves_frame' Name +' ' Text +'pre_s' Name +' ' Text +'post_s' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'pre_s' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pre_f' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'m0' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'(' Operator +'lpre_f' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'<==>' Operator +' ' Text +'lpre_f' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'(' Operator +'forall' Keyword +' ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +' ' Text +'(' Operator +'final_state' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'.' Operator +'\n ' Text +'lpost_f' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'x' Name +' ' Text +'final_state' Name +' ' Text +'<==>' Operator +'\n ' Text +'lpost_f' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'x' Name +' ' Text +'final_state' Name +')' Operator +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'frame_post_for_par_tautology' Name +' ' Text +'lpost_f' Name +' ' Text +'m0' Name +';' Operator +'\n ' Text +'frame_post_for_par_aux' Name +' ' Text +'pre_s' Name +' ' Text +'post_s' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'lpost_f' Name +'\n\n' Text + +'/// Finally lemmas for proving that in the par rules preconditions get weaker' Comment +'\n' Text + +'/// and postconditions get stronger' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'par_weaker_lpre_and_stronger_lpost_l' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'preL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aL' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +')' Operator +'\n ' Text +'(' Operator +'lpostL' Name +':' Operator +'l_post' Name +' ' Text +'preL' Name +' ' Text +'postL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +')' Operator +'\n ' Text +'(' Operator +'next_lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'next_preL' Name +')' Operator +'\n ' Text +'(' Operator +'next_lpostL' Name +':' Operator +'l_post' Name +' ' Text +'next_preL' Name +' ' Text +'next_postL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'preR' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aR' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'lpostR' Name +':' Operator +'l_post' Name +' ' Text +'preR' Name +' ' Text +'postR' Name +')' Operator +'\n ' Text +'(' Operator +'state' Name +' ' Text +'next_state' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'weaker_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'next_lpreL' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_lpost' Name +' ' Text +'lpostL' Name +' ' Text +'next_lpostL' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'preserves_frame' Name +' ' Text +'preL' Name +' ' Text +'next_preL' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpreL' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'lpreR' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'state' Name +')' Operator +' ' Text +'state' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'weaker_lpre' Name +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'lpreR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'next_lpreL' Name +' ' Text +'lpreR' Name +')' Operator +'\n ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_lpost' Name +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'next_lpreL' Name +' ' Text +'next_lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +')' Operator +'\n ' Text +'state' Name +' ' Text +'next_state' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'frame_post_for_par' Name +' ' Text +'preL' Name +' ' Text +'next_preL' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'weaker_lpre' Name +' ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'lpreR' Name +')' Operator +' ' Text +'(' Operator +'par_lpre' Name +' ' Text +'next_lpreL' Name +' ' Text +'lpreR' Name +')' Operator +' ' Text +'state' Name +' ' Text +'next_state' Name +')' Operator +' ' Text +'by' Keyword +'\n ' Text +'(' Operator +'norm' Name +' ' Text +'[' Operator +'delta_only' Name +' ' Text +'[' Operator +'`' Keyword +'%' Operator +'weaker_lpre' Name +';' Operator +' ' Text +'`' Keyword +'%' Operator +'par_lpre' Name +']' Operator +' ' Text +']' Operator +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'par_weaker_lpre_and_stronger_lpost_r' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preL' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreL' Name +':' Operator +'l_pre' Name +' ' Text +'preL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aL' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +')' Operator +'\n ' Text +'(' Operator +'lpostL' Name +':' Operator +'l_post' Name +' ' Text +'preL' Name +' ' Text +'postL' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'preR' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aR' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'lpostR' Name +':' Operator +'l_post' Name +' ' Text +'preR' Name +' ' Text +'postR' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_preR' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'next_postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'next_lpreR' Name +':' Operator +'l_pre' Name +' ' Text +'next_preR' Name +')' Operator +'\n ' Text +'(' Operator +'next_lpostR' Name +':' Operator +'l_post' Name +' ' Text +'next_preR' Name +' ' Text +'next_postR' Name +')' Operator +'\n ' Text +'(' Operator +'state' Name +' ' Text +'next_state' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +'\n ' Text +'weaker_lpre' Name +' ' Text +'lpreR' Name +' ' Text +'next_lpreR' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_lpost' Name +' ' Text +'lpostR' Name +' ' Text +'next_lpostR' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'preserves_frame' Name +' ' Text +'preR' Name +' ' Text +'next_preR' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpreR' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'lpreL' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'state' Name +')' Operator +' ' Text +'state' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_preR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'next_state' Name +')' Operator +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'weaker_lpre' Name +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'lpreR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'next_lpreR' Name +')' Operator +'\n ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'/\\' Operator +'\n ' Text +'stronger_lpost' Name +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'next_lpreR' Name +' ' Text +'next_lpostR' Name +')' Operator +'\n ' Text +'state' Name +' ' Text +'next_state' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'commute_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'state' Name +')' Operator +' ' Text +'preL' Name +' ' Text +'preR' Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'state' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'state' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'preR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preL' Name +')' Operator +')' Operator +'\n ' Text +'state' Name +';' Operator +'\n ' Text +'frame_post_for_par' Name +' ' Text +'preR' Name +' ' Text +'next_preR' Name +' ' Text +'state' Name +' ' Text +'next_state' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'weaker_lpre' Name +' ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'lpreR' Name +')' Operator +' ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'next_lpreR' Name +')' Operator +' ' Text +'state' Name +' ' Text +'next_state' Name +')' Operator +' ' Text +'by' Keyword +'\n ' Text +'(' Operator +'norm' Name +' ' Text +'[' Operator +'delta_only' Name +' ' Text +'[' Operator +'`' Keyword +'%' Operator +'weaker_lpre' Name +';' Operator +' ' Text +'`' Keyword +'%' Operator +'par_lpre' Name +']' Operator +' ' Text +']' Operator +')' Operator +';' Operator +'\n ' Text +'commute_star_right' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'next_state' Name +')' Operator +' ' Text +'next_preR' Name +' ' Text +'preL' Name +';' Operator +'\n ' Text +'apply_interp_ext' Name +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'next_state' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'next_preR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preL' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'next_state' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_preR' Name +')' Operator +')' Operator +'\n ' Text +'next_state' Name +'\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--warn_error -271' Literal.String.Double +'"' Literal.String.Double +'\n' Text + +'let' Keyword.Declaration +' ' Text +'stronger_post_par_r' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'aL' Name +' ' Text +'#' Operator +'aR' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'postL' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aL' Name +')' Operator +'\n ' Text +'(' Operator +'postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'next_postR' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'aR' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'stronger_post' Name +' ' Text +'postR' Name +' ' Text +'next_postR' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +'\n ' Text +'forall' Keyword +' ' Text +'xL' Name +' ' Text +'xR' Name +' ' Text +'frame' Name +' ' Text +'h' Name +'.' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +' ' Text +'=' Operator +'=' Operator +'>' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'aux' Name +' ' Text +'xL' Name +' ' Text +'xR' Name +' ' Text +'frame' Name +' ' Text +'h' Name +'\n ' Text +':' Operator +' ' Text +'Lemma' Name.Class +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'h' Name +')' Operator +'\n ' Text +'[' Operator +'SMTPat' Name.Class +' ' Text +'()' Name.Builtin.Pseudo +']' Operator +'\n ' Text +'=' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'next_postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postL' Name +' ' Text +'xL' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'next_postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'}' Operator +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'next_postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'h' Name +')' Operator +';' Operator +'\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +')' Operator +' ' Text +'h' Name +')' Operator +';' Operator +'\n ' Text +'calc' Name.Exception +' ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +'\n ' Text +'postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'postR' Name +' ' Text +'xR' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postL' Name +' ' Text +'xL' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'(' Operator +'st' Name +'.' Operator +'equals' Name +')' Operator +' ' Text +'{' Operator +' ' Text +'}' Operator +'\n ' Text +'(' Operator +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +';' Operator +'\n ' Text +'}' Operator +'\n ' Text +'in' Keyword +'\n ' Text +'()' Name.Builtin.Pseudo +'\n' Text + +'#' Operator +'pop' Name +'-' Operator +'options' Name +'\n\n\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +' Begin stepping functions ' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_ret' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Ret' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'_' Name +',' Operator +' ' Text +'n' Name +')' Operator +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'Ret' Name.Class +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'lp' Name +' ' Text +'=' Operator +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'p' Name +' ' Text +'x' Name +')' Operator +' ' Text +'p' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'f' Name +',' Operator +' ' Text +'n' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'lpost_ret_act' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'x' Name +':' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'state' Name +':' Operator +'st' Name +'.' Operator +'mem' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'_' Name +' ' Text +'x' Name +' ' Text +'h1' Name +' ' Text +'->' Operator +' ' Text +'lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'state' Name +')' Operator +' ' Text +'x' Name +' ' Text +'h1' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_act' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Act' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m0' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'Act' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'f' Name +' ' Text +'=' Operator +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'x' Name +' ' Text +'=' Operator +' ' Text +'f' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'lpost' Name +' ' Text +':' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +' ' Text +'=' Operator +' ' Text +'lpost_ret_act' Name +' ' Text +'lpost' Name +' ' Text +'x' Name +' ' Text +'m0' Name +' ' Text +'in' Keyword +'\n\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpost' Name +' ' Text +'h' Name +' ' Text +'x' Name +' ' Text +'h' Name +')' Operator +' ' Text +'lpost' Name +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'post' Name +' ' Text +'x' Name +' ' Text +'lpost' Name +')' Operator +'\n\n' Text + +'module' Keyword +' ' Text +'M' Name.Class +' ' Text +'=' Operator +' ' Text +'MST' Name.Class +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_bind_ret_aux' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Bind' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Bind' Name.Class +'?.' Operator +'f' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'st' Name +'.' Operator +'locks_preorder' Name +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Bind' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'post_b' Name +' ' Text +'#' Operator +'lpre_b' Name +' ' Text +'#' Operator +'lpost_b' Name +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'_' Name +')' Operator +' ' Text +'g' Name +' ' Text +'->' Operator +'\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'p' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +' ' Text +'(' Operator +'lpre_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'g' Name +' ' Text +'x' Name +')' Operator +',' Operator +' ' Text +'m0' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_bind_ret' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Bind' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Bind' Name.Class +'?.' Operator +'f' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'_' Name +',' Operator +' ' Text +'n' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'step_bind_ret_aux' Name +' ' Text +'f' Name +',' Operator +' ' Text +'n' Name +')' Operator +'\n\n\n' Text + +'#' Operator +'push' Name +'-' Operator +'options' Name +' ' Text +'"' Literal.String.Double +'--z3rlimit 40' Literal.String.Double +'"' Literal.String.Double +'\n' Text + +'let' Keyword.Declaration +' ' Text +'step_bind' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Bind' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +'(' Operator +'step' Name +':' Operator +'step_t' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Bind' Name.Class +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +')' Operator +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_bind_ret' Name +' ' Text +'f' Name +'\n\n ' Text +'|' Operator +' ' Text +'Bind' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'b' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'post_a' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'post_b' Name +' ' Text +'#' Operator +'lpre_b' Name +' ' Text +'#' Operator +'lpost_b' Name +' ' Text +'f' Name +' ' Text +'g' Name +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'next_pre' Name +' ' Text +'next_post' Name +' ' Text +'next_lpre' Name +' ' Text +'next_lpost' Name +' ' Text +'f' Name +' ' Text +'=' Operator +' ' Text +'step' Name +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'lpre_b' Name +' ' Text +':' Operator +' ' Text +'(' Operator +'x' Name +':' Operator +'b' Name +' ' Text +'->' Operator +' ' Text +'l_pre' Name +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +')' Operator +')' Operator +' ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +'\n ' Text +'depends_only_on_commutes_with_weaker' Name +' ' Text +'(' Operator +'lpre_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +')' Operator +';' Operator +'\n ' Text +'lpre_b' Name +' ' Text +'x' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'lpost_b' Name +' ' Text +':' Operator +' ' Text +'(' Operator +'x' Name +':' Operator +'b' Name +' ' Text +'->' Operator +' ' Text +'l_post' Name +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +')' Operator +' ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +'\n ' Text +'depends_only_on2_commutes_with_weaker' Name +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'post_a' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +';' Operator +'\n ' Text +'lpost_b' Name +' ' Text +'x' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'g' Name +' ' Text +':' Operator +' ' Text +'(' Operator +'x' Name +':' Operator +'b' Name +' ' Text +'->' Operator +' ' Text +'Dv' Name.Class +' ' Text +'(' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'_' Name +' ' Text +'(' Operator +'next_post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'post_b' Name +' ' Text +'(' Operator +'lpre_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +')' Operator +')' Operator +' ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +'\n ' Text +'Weaken' Name.Class +' ' Text +'(' Operator +'lpre_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +'lpost_b' Name +' ' Text +'x' Name +')' Operator +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'(' Operator +'g' Name +' ' Text +'x' Name +')' Operator +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'m1' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'(' Operator +'bind_lpre' Name +' ' Text +'next_lpre' Name +' ' Text +'next_lpost' Name +' ' Text +'lpre_b' Name +')' Operator +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +'\n ' Text +'by' Keyword +' ' Text +'norm' Name +' ' Text +'(' Operator +'[' Operator +'delta_only' Name +' ' Text +'[' Operator +'`' Keyword +'%' Operator +'bind_lpre' Name +']' Operator +']' Operator +')' Operator +';' Operator +'\n\n ' Text +'Step' Name.Class +' ' Text +'next_pre' Name +' ' Text +'post_b' Name +'\n ' Text +'(' Operator +'bind_lpre' Name +' ' Text +'next_lpre' Name +' ' Text +'next_lpost' Name +' ' Text +'lpre_b' Name +')' Operator +'\n ' Text +'(' Operator +'bind_lpost' Name +' ' Text +'next_lpre' Name +' ' Text +'next_lpost' Name +' ' Text +'lpost_b' Name +')' Operator +'\n ' Text +'(' Operator +'Bind' Name.Class +' ' Text +'f' Name +' ' Text +'g' Name +')' Operator +'\n' Text + +'#' Operator +'pop' Name +'-' Operator +'options' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_frame_ret_aux' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'p' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'p' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'p' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Frame' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Frame' Name.Class +'?.' Operator +'f' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'st' Name +'.' Operator +'locks_preorder' Name +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Frame' Name.Class +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'lp' Name +')' Operator +' ' Text +'frame' Name +' ' Text +'f_frame' Name +' ' Text +'->' Operator +'\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'p' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +'\n ' Text +'(' Operator +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpost' Name +' ' Text +'h' Name +' ' Text +'x' Name +' ' Text +'h' Name +')' Operator +'\n ' Text +'lpost' Name +'\n ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'x' Name +' ' Text +'lpost' Name +')' Operator +',' Operator +' ' Text +'m0' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_frame_ret' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'p' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'p' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'p' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Frame' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Frame' Name.Class +'?.' Operator +'f' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'_' Name +',' Operator +' ' Text +'n' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'step_frame_ret_aux' Name +' ' Text +'f' Name +',' Operator +' ' Text +'n' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_frame' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'p' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'p' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'p' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Frame' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +'(' Operator +'step' Name +':' Operator +'step_t' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Frame' Name.Class +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'p' Name +' ' Text +'x' Name +' ' Text +'lp' Name +')' Operator +' ' Text +'frame' Name +' ' Text +'f_frame' Name +' ' Text +'->' Operator +' ' Text +'step_frame_ret' Name +' ' Text +'f' Name +'\n\n ' Text +'|' Operator +' ' Text +'Frame' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'f_pre' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'f' Name +' ' Text +'frame' Name +' ' Text +'f_frame' Name +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m0' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'next_fpre' Name +' ' Text +'next_fpost' Name +' ' Text +'next_flpre' Name +' ' Text +'next_flpost' Name +' ' Text +'f' Name +' ' Text +'=' Operator +' ' Text +'step' Name +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'m1' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'preserves_frame_star' Name +' ' Text +'f_pre' Name +' ' Text +'next_fpre' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'frame' Name +';' Operator +'\n\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'(' Operator +'frame_lpre' Name +' ' Text +'next_flpre' Name +' ' Text +'f_frame' Name +')' Operator +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +')' Operator +'\n ' Text +'by' Keyword +' ' Text +'(' Operator +'norm' Name +' ' Text +'[' Operator +'delta_only' Name +' ' Text +'[' Operator +'`' Keyword +'%' Operator +'frame_lpre' Name +']' Operator +']' Operator +')' Operator +';' Operator +'\n\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'next_fpre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'next_fpost' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'frame' Name +')' Operator +'\n ' Text +'(' Operator +'frame_lpre' Name +' ' Text +'next_flpre' Name +' ' Text +'f_frame' Name +')' Operator +'\n ' Text +'(' Operator +'frame_lpost' Name +' ' Text +'next_flpre' Name +' ' Text +'next_flpost' Name +' ' Text +'f_frame' Name +')' Operator +'\n ' Text +'(' Operator +'Frame' Name.Class +' ' Text +'f' Name +' ' Text +'frame' Name +' ' Text +'f_frame' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_par_ret_aux' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Par' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Par' Name.Class +'?.' Operator +'mL' Name +' ' Text +'f' Name +')' Operator +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Par' Name.Class +'?.' Operator +'mR' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'st' Name +'.' Operator +'mem' Name +' ' Text +'st' Name +'.' Operator +'locks_preorder' Name +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'M' Name.Namespace +'.' Punctuation +'MSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Par' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'aL' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'pL' Name +' ' Text +'xL' Name +' ' Text +'lpL' Name +')' Operator +' ' Text +'#' Operator +'aR' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'pR' Name +' ' Text +'xR' Name +' ' Text +'lpR' Name +')' Operator +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'lpost' Name +' ' Text +':' Operator +' ' Text +'l_post' Name +'\n ' Text +'#' Operator +'st' Name +' ' Text +'#' Operator +'(' Operator +'aL' Name +' ' Text +'&' Operator +' ' Text +'aR' Name +')' Operator +'\n ' Text +'(' Operator +'pL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pR' Name +' ' Text +'xR' Name +')' Operator +'\n ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'pL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pR' Name +' ' Text +'xR' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'h0' Name +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'h1' Name +' ' Text +'->' Operator +' ' Text +'lpL' Name +' ' Text +'h0' Name +' ' Text +'xL' Name +' ' Text +'h1' Name +' ' Text +'/\\' Operator +' ' Text +'lpR' Name +' ' Text +'h0' Name +' ' Text +'xR' Name +' ' Text +'h1' Name +'\n ' Text +'in' Keyword +'\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'pL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'pL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pR' Name +' ' Text +'xR' Name +')' Operator +'\n ' Text +'(' Operator +'fun' Keyword +' ' Text +'h' Name +' ' Text +'->' Operator +' ' Text +'lpL' Name +' ' Text +'h' Name +' ' Text +'xL' Name +' ' Text +'h' Name +' ' Text +'/\\' Operator +' ' Text +'lpR' Name +' ' Text +'h' Name +' ' Text +'xR' Name +' ' Text +'h' Name +')' Operator +'\n ' Text +'lpost' Name +'\n ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'pL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'pR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'lpost' Name +')' Operator +',' Operator +' ' Text +'m0' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_par_ret' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Par' Name.Class +'?' Operator +' ' Text +'f' Name +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Par' Name.Class +'?.' Operator +'mL' Name +' ' Text +'f' Name +')' Operator +' ' Text +'/\\' Operator +' ' Text +'Ret' Name.Class +'?' Operator +' ' Text +'(' Operator +'Par' Name.Class +'?.' Operator +'mR' Name +' ' Text +'f' Name +')' Operator +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'_' Name +',' Operator +' ' Text +'n' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'step_par_ret_aux' Name +' ' Text +'f' Name +',' Operator +' ' Text +'n' Name +')' Operator +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_par' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Par' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +'(' Operator +'step' Name +':' Operator +'step_t' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Par' Name.Class +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +')' Operator +' ' Text +'(' Operator +'Ret' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'step_par_ret' Name +' ' Text +'f' Name +'\n\n ' Text +'|' Operator +' ' Text +'Par' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'aL' Name +' ' Text +'#' Operator +'preL' Name +' ' Text +'#' Operator +'postL' Name +' ' Text +'#' Operator +'lpreL' Name +' ' Text +'#' Operator +'lpostL' Name +' ' Text +'mL' Name +' ' Text +'#' Operator +'aR' Name +' ' Text +'#' Operator +'preR' Name +' ' Text +'#' Operator +'postR' Name +' ' Text +'#' Operator +'lpreR' Name +' ' Text +'#' Operator +'lpostR' Name +' ' Text +'mR' Name +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'b' Name +' ' Text +'=' Operator +' ' Text +'sample' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'if' Keyword +' ' Text +'b' Name +' ' Text +'then' Keyword +' ' Text +'begin' Name +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m0' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'next_preL' Name +' ' Text +'next_postL' Name +' ' Text +'next_lpreL' Name +' ' Text +'next_lpostL' Name +' ' Text +'mL' Name +' ' Text +'=' Operator +' ' Text +'step' Name +' ' Text +'mL' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'m1' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'preserves_frame_star' Name +' ' Text +'preL' Name +' ' Text +'next_preL' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'preR' Name +';' Operator +'\n ' Text +'par_weaker_lpre_and_stronger_lpost_l' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'next_lpreL' Name +' ' Text +'next_lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +';' Operator +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'next_post' Name +' ' Text +'=' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'next_postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'in' Keyword +'\n\n ' Text +'assert' Name.Exception +' ' Text +'(' Operator +'stronger_post' Name +' ' Text +'post' Name +' ' Text +'next_post' Name +')' Operator +' ' Text +'by' Keyword +' ' Text +'(' Operator +'norm' Name +' ' Text +'[' Operator +'delta_only' Name +' ' Text +'[' Operator +'`' Keyword +'%' Operator +'stronger_post' Name +']' Operator +']' Operator +')' Operator +';' Operator +'\n\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'next_preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'preR' Name +')' Operator +' ' Text +'next_post' Name +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'next_lpreL' Name +' ' Text +'lpreR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'next_lpreL' Name +' ' Text +'next_lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +')' Operator +'\n ' Text +'(' Operator +'Par' Name.Class +' ' Text +'mL' Name +' ' Text +'mR' Name +')' Operator +'\n\n ' Text +'end' Keyword +'\n ' Text +'else' Keyword +' ' Text +'begin' Name +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m0' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'next_preR' Name +' ' Text +'next_postR' Name +' ' Text +'next_lpreR' Name +' ' Text +'next_lpostR' Name +' ' Text +'mR' Name +' ' Text +'=' Operator +' ' Text +'step' Name +' ' Text +'mR' Name +' ' Text +'in' Keyword +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'m1' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'preserves_frame_star_left' Name +' ' Text +'preR' Name +' ' Text +'next_preR' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'preL' Name +';' Operator +'\n ' Text +'par_weaker_lpre_and_stronger_lpost_r' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'lpreR' Name +' ' Text +'lpostR' Name +' ' Text +'next_lpreR' Name +' ' Text +'next_lpostR' Name +' ' Text +'m0' Name +' ' Text +'m1' Name +';' Operator +'\n\n ' Text +'let' Keyword.Declaration +' ' Text +'next_post' Name +' ' Text +'=' Operator +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'xL' Name +',' Operator +' ' Text +'xR' Name +')' Operator +' ' Text +'->' Operator +' ' Text +'postL' Name +' ' Text +'xL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_postR' Name +' ' Text +'xR' Name +')' Operator +' ' Text +'in' Keyword +'\n\n ' Text +'stronger_post_par_r' Name +' ' Text +'postL' Name +' ' Text +'postR' Name +' ' Text +'next_postR' Name +';' Operator +'\n\n ' Text +'Step' Name.Class +' ' Text +'(' Operator +'preL' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'next_preR' Name +')' Operator +' ' Text +'next_post' Name +'\n ' Text +'(' Operator +'par_lpre' Name +' ' Text +'lpreL' Name +' ' Text +'next_lpreR' Name +')' Operator +'\n ' Text +'(' Operator +'par_lpost' Name +' ' Text +'lpreL' Name +' ' Text +'lpostL' Name +' ' Text +'next_lpreR' Name +' ' Text +'next_lpostR' Name +')' Operator +'\n ' Text +'(' Operator +'Par' Name.Class +' ' Text +'mL' Name +' ' Text +'mR' Name +')' Operator +'\n ' Text +'end' Keyword +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'step_weaken' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +'{' Operator +'Weaken' Name.Class +'?' Operator +' ' Text +'f' Name +'}' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +' ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +' ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'NMSTATE' Name.Class +'?.' Operator +'reflect' Name +' ' Text +'(' Operator +'fun' Keyword +' ' Text +'(' Operator +'_' Name +',' Operator +' ' Text +'n' Name +')' Operator +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'Weaken' Name.Class +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'pre' Name +' ' Text +'#' Operator +'post' Name +' ' Text +'#' Operator +'lpre' Name +' ' Text +'#' Operator +'lpost' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'#' Operator +'_' Name +' ' Text +'f' Name +' ' Text +'=' Operator +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n\n ' Text +'Step' Name.Class +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +' ' Text +'f' Name +',' Operator +' ' Text +'n' Name +')' Operator +'\n\n' Text + +'/// Step function' Comment +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'rec' Keyword.Declaration +' ' Text +'step' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'(' Operator +'step_result' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'step_req' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'(' Operator +'step_ens' Name +' ' Text +'f' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Ret' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_ret' Name +' ' Text +'f' Name +'\n ' Text +'|' Operator +' ' Text +'Bind' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_bind' Name +' ' Text +'f' Name +' ' Text +'step' Name +'\n ' Text +'|' Operator +' ' Text +'Act' Name.Class +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_act' Name +' ' Text +'f' Name +'\n ' Text +'|' Operator +' ' Text +'Frame' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_frame' Name +' ' Text +'f' Name +' ' Text +'step' Name +'\n ' Text +'|' Operator +' ' Text +'Par' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_par' Name +' ' Text +'f' Name +' ' Text +'step' Name +'\n ' Text +'|' Operator +' ' Text +'Weaken' Name.Class +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'step_weaken' Name +' ' Text +'f' Name +'\n\n' Text + +'let' Keyword.Declaration +' ' Text +'rec' Keyword.Declaration +' ' Text +'run' Name +'\n ' Text +'(' Operator +'#' Operator +'st' Name +':' Operator +'st' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'a' Name +':' Operator +'Type' Name.Class +' ' Text +'u#' Operator +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'pre' Name +':' Operator +'st' Name +'.' Operator +'hprop' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'post' Name +':' Operator +'post_t' Name +' ' Text +'st' Name +' ' Text +'a' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpre' Name +':' Operator +'l_pre' Name +' ' Text +'pre' Name +')' Operator +'\n ' Text +'(' Operator +'#' Operator +'lpost' Name +':' Operator +'l_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +')' Operator +'\n ' Text +'(' Operator +'f' Name +':' Operator +'m' Name +' ' Text +'st' Name +' ' Text +'a' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'lpre' Name +' ' Text +'lpost' Name +')' Operator +'\n ' Text +':' Operator +' ' Text +'Mst' Name.Class +' ' Text +'a' Name +'\n ' Text +'(' Operator +'requires' Keyword +' ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'->' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'pre' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpre' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +')' Operator +'\n ' Text +'(' Operator +'ensures' Keyword +' ' Text +'fun' Keyword +' ' Text +'m0' Name +' ' Text +'x' Name +' ' Text +'m1' Name +' ' Text +'->' Operator +'\n ' Text +'st' Name +'.' Operator +'interp' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +' ' Text +'`st.star`' Operator.Word +' ' Text +'st' Name +'.' Operator +'locks_invariant' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'m1' Name +' ' Text +'/\\' Operator +'\n ' Text +'lpost' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m0' Name +')' Operator +' ' Text +'x' Name +' ' Text +'(' Operator +'st' Name +'.' Operator +'core' Name +' ' Text +'m1' Name +')' Operator +' ' Text +'/\\' Operator +'\n ' Text +'preserves_frame' Name +' ' Text +'pre' Name +' ' Text +'(' Operator +'post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'m1' Name +')' Operator +'\n ' Text +'=' Operator +'\n ' Text +'match' Keyword +' ' Text +'f' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'Ret' Name.Class +' ' Text +'_' Name +' ' Text +'x' Name +' ' Text +'_' Name +' ' Text +'->' Operator +' ' Text +'x' Name +'\n\n ' Text +'|' Operator +' ' Text +'_' Name +' ' Text +'->' Operator +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m0' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n ' Text +'let' Keyword.Declaration +' ' Text +'Step' Name.Class +' ' Text +'new_pre' Name +' ' Text +'new_post' Name +' ' Text +'_' Name +' ' Text +'_' Name +' ' Text +'f' Name +' ' Text +'=' Operator +' ' Text +'step' Name +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m1' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n ' Text +'let' Keyword.Declaration +' ' Text +'x' Name +' ' Text +'=' Operator +' ' Text +'run' Name +' ' Text +'f' Name +' ' Text +'in' Keyword +'\n ' Text +'let' Keyword.Declaration +' ' Text +'m2' Name +' ' Text +'=' Operator +' ' Text +'get' Name +' ' Text +'()' Name.Builtin.Pseudo +' ' Text +'in' Keyword +'\n\n ' Text +'preserves_frame_trans' Name +' ' Text +'pre' Name +' ' Text +'new_pre' Name +' ' Text +'(' Operator +'new_post' Name +' ' Text +'x' Name +')' Operator +' ' Text +'m0' Name +' ' Text +'m1' Name +' ' Text +'m2' Name +';' Operator +'\n ' Text +'preserves_frame_stronger_post' Name +' ' Text +'pre' Name +' ' Text +'post' Name +' ' Text +'new_post' Name +' ' Text +'x' Name +' ' Text +'m0' Name +' ' Text +'m2' Name +';' Operator +'\n ' Text +'x' Name +'\n' Text |