'(*' 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 ' ' Text '// Test' Comment '\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 '//can join any disjoint heap to the pre-heap and q is still valid' Comment '\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 '//can join any disjoint heap to the post-heap and q is still valid' Comment '\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