Updates for change to Loc values

Author: myreen

semantics/alt_semantics/proofs/itree_semanticsEquivScript.sml

@@ -459,10 +459,10 @@ QED
 
 Theorem estep_to_Effi:
   estep ea = Effi (ExtCall s) conf ws lnum env st cs ⇔
-  ∃env' conf' fp'.
+  ∃env' conf' fp' b.
     conf = MAP (λc. n2w (ORD c)) (EXPLODE conf') ∧
     ea = (env',st,fp',Val (Litv (StrLit conf')),
-            (Capp (FFI s) [Loc lnum] [],env)::cs) ∧
+            (Capp (FFI s) [Loc b lnum] [],env)::cs) ∧
     store_lookup lnum st = SOME (W8array ws) ∧ s ≠ ""
 Proof
   PairCases_on `ea` >> Cases_on `ea3` >> gvs[SF itree_ss]
@@ -487,10 +487,10 @@ QED
 Theorem dstep_to_Dffi:
   dstep env dst dev dcs =
   Dffi dst' (ExtCall s,ws1,ws2,lnum,env',cs) locs pat dcs' ⇔
-  ∃env'' conf.
+  ∃env'' conf b.
     dst = dst' ∧ dcs = dcs' ∧
     dev = ExpVal env'' (Val (Litv (StrLit conf)))
-            ((Capp (FFI s) [Loc lnum] [],env')::cs) locs pat ∧
+            ((Capp (FFI s) [Loc b lnum] [],env')::cs) locs pat ∧
     ws1 = MAP (λc. n2w (ORD c)) (EXPLODE conf) ∧
     store_lookup lnum dst.refs = SOME (W8array ws2) ∧ s ≠ ""
 Proof
@@ -513,9 +513,9 @@ Theorem decl_step_ffi_changed_dstep_to_Dffi:
   decl_step env (dst2, dev2, dcs) = Dstep (dst2', dev2', dcs') ∧
   dst2.ffi ≠ dst2'.ffi ∧
   dstate_rel dst1 dst2 ∧ deval_rel dev1 dev2 ⇒
-  ∃env' env'' conf s lnum ccs locs pat ws.
+  ∃env' env'' conf s lnum ccs locs pat ws b.
     dev1 = ExpVal env' (Val $ Litv $ StrLit conf)
-            ((Capp (FFI s) [Loc lnum] [], env'') :: ccs) locs pat ∧
+            ((Capp (FFI s) [Loc b lnum] [], env'') :: ccs) locs pat ∧
     store_lookup lnum dst1.refs = SOME (W8array ws) ∧
     dstep env dst1 dev1 dcs = Dffi dst1
       (ExtCall s,MAP (λc. n2w $ ORD c) (EXPLODE conf),ws,lnum,env'',ccs)
@@ -578,12 +578,12 @@ Theorem dstep_result_rel_single_FFI_strong:
     dstep_result_rel (Dstep dsta deva dcsa) (Dstep (dstb, devb, dcsb)) ∧
     dstep env dsta deva dcsa =
     Dffi dsta' (ExtCall s,conf,ws,lnum,eenv,cs1) locs pat dcsa'
-  ⇒ ∃env' ffi conf' cs2 fp.
+  ⇒ ∃env' ffi conf' cs2 fp b.
       conf = MAP (λc. n2w (ORD c)) (EXPLODE conf') ∧
       deva = ExpVal env' (Val (Litv $ StrLit conf'))
-              ((Capp (FFI s) [Loc lnum] [], eenv)::cs1) locs pat ∧
+              ((Capp (FFI s) [Loc b lnum] [], eenv)::cs1) locs pat ∧
       devb = ExpVal env' (Val (Litv $ StrLit conf'))
-              ((Capp (FFI s) [Loc lnum] () [], eenv)::cs2) locs pat ∧
+              ((Capp (FFI s) [Loc b lnum] () [], eenv)::cs2) locs pat ∧
       store_lookup lnum dsta.refs = SOME (W8array ws) ∧ s ≠ "" ∧
       dget_ffi (Dstep (dstb, devb, dcsb)) = SOME ffi ∧
       decl_step env (dstb, devb, dcsb) =

semantics/alt_semantics/proofs/itree_semanticsPropsScript.sml

@@ -532,7 +532,7 @@ Theorem application_thm:
     else if ∃n. op = FFI n then (
       case op of FFI n => (
         case vs of
-          [Litv (StrLit conf); Loc lnum] => (
+          [Litv (StrLit conf); Loc b lnum] => (
             case store_lookup lnum s of
               SOME (W8array ws) =>
                 if n = "" then Estep (env, s, fp, Val $ Conv NONE [], c)
@@ -604,8 +604,8 @@ QED
 Theorem application_eq_Effi_fields:
   application op env st fp vs cs = Effi (ExtCall s) conf ws lnum env' st' cs' ⇒
   op = FFI s ∧ env = env' ∧ st = st' ∧ cs' = cs ∧
-  ∃conf'.
-    vs = [Litv $ StrLit conf'; Loc lnum] ∧
+  ∃conf' b.
+    vs = [Litv $ StrLit conf'; Loc b lnum] ∧
     conf = MAP (λc. n2w $ ORD c) (EXPLODE conf')
 Proof
   Cases_on `op` >> simp[application_def, SF itree_ss] >>

semantics/alt_semantics/proofs/smallStepPropsScript.sml

@@ -1730,9 +1730,9 @@ Theorem e_step_ffi_changed:
   ∀env st ffi fp ev cs ffi' env' st' fp' ev' cs'.
   e_step (env, (st, ffi), fp, ev, cs) = Estep (env', (st', ffi'), fp', ev', cs') ∧
   ffi ≠ ffi' ⇒
-  ∃ s conf lnum ccs ws ffi_st ws'.
+  ∃ s conf lnum ccs ws ffi_st ws' b.
     ev = Val (Litv (StrLit conf)) ∧
-    cs = (Capp (FFI s) [Loc lnum] () [], env') :: ccs ∧
+    cs = (Capp (FFI s) [Loc b lnum] () [], env') :: ccs ∧
     store_lookup lnum st = SOME (W8array ws) ∧
     s ≠ "" ∧
     ffi.oracle
@@ -1771,9 +1771,9 @@ QED
 
 Theorem decl_step_ffi_changed:
   decl_step benv (st, dev, dcs) = Dstep (st', dev', dcs') ∧ st.ffi ≠ st'.ffi ⇒
-  ∃env conf s lnum env' ccs locs pat ws ffi_st ws'.
+  ∃env conf s lnum env' ccs locs pat ws ffi_st ws' b.
     dev = ExpVal env (Val (Litv (StrLit conf)))
-            ((Capp (FFI s) [Loc lnum] () [], env')::ccs) locs pat ∧
+            ((Capp (FFI s) [Loc b lnum] () [], env')::ccs) locs pat ∧
     store_lookup lnum st.refs = SOME (W8array ws) ∧
     s ≠ "" ∧
     st.ffi.oracle (ExtCall s) st.ffi.ffi_state