Remove unused arg from closLang's ByteArray

compiler/backend/proofs/clos_fvsProofScript.sml

@@ -91,7 +91,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [
 (* state relation *)
 
 Inductive ref_rel:
-  (!b bs. ref_rel (ByteArray b bs) (ByteArray b bs)) /\
+  (!bs. ref_rel (ByteArray bs) (ByteArray bs)) /\
   (!xs ys.
     LIST_REL v_rel xs ys ==>
     ref_rel (ValueArray xs) (ValueArray ys))

compiler/backend/proofs/clos_knownProofScript.sml

@@ -825,7 +825,8 @@ Proof
       >- (fs[ssgc_free_def,FLOOKUP_UPDATE, bool_case_eq] >> metis_tac[])
       >- (last_x_assum match_mp_tac >> fs[])
       >- (first_x_assum match_mp_tac >> fs[] >> metis_tac[])
-      >- (first_x_assum match_mp_tac >> fs[] >> metis_tac[]))
+      >- (first_x_assum match_mp_tac >> fs[] >> metis_tac[])
+      \\ dsimp[ssgc_free_def, FLOOKUP_UPDATE, bool_case_eq])
   >- (rename [‘EqualConst’]
       \\ rw [] \\ fs [Boolv_def])
   >- (rename [‘Constant c’]
@@ -2567,15 +2568,15 @@ val v_rel_IMP_v_to_words = prove(
 (* state relation *)
 
 Inductive ref_rel:
-  (!b bs. ref_rel c g (ByteArray b bs) (ByteArray b bs)) /\
+  (!bs. ref_rel c g (ByteArray bs) (ByteArray bs)) /\
   (!xs ys.
     LIST_REL (v_rel c g) xs ys ==>
     ref_rel c g (ValueArray xs) (ValueArray ys))
 End
 
 val ref_rel_simps = save_thm("ref_rel_simps[simp]",LIST_CONJ [
   SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ValueArray vs) x``,
-  SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ByteArray b bs) x``])
+  SIMP_CONV (srw_ss()) [ref_rel_cases] ``ref_rel c g (ByteArray bs) x``])
 
 Theorem ref_rel_upd_inline_factor:
    ref_rel (c with inline_factor := k) = ref_rel c

compiler/backend/proofs/clos_letopProofScript.sml

@@ -86,7 +86,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [
 (* state relation *)
 
 Inductive ref_rel:
-  (!b bs. ref_rel (ByteArray b bs) (ByteArray b bs)) /\
+  (!bs. ref_rel (ByteArray bs) (ByteArray bs)) /\
   (!xs ys.
     LIST_REL v_rel xs ys ==>
     ref_rel (ValueArray xs) (ValueArray ys))

compiler/backend/proofs/clos_mtiProofScript.sml

@@ -110,7 +110,7 @@ val v_rel_opt_def = Define `
   (v_rel_opt max_app _ _ = F)`;
 
 Inductive ref_rel:
-  (!b bs. ref_rel max_app (ByteArray b bs) (ByteArray b bs)) /\
+  (!bs. ref_rel max_app (ByteArray bs) (ByteArray bs)) /\
   (!xs ys.
     LIST_REL (v_rel max_app) xs ys ==>
     ref_rel max_app (ValueArray xs) (ValueArray ys))

compiler/backend/proofs/clos_ticksProofScript.sml

@@ -104,7 +104,7 @@ val v_rel_simps = save_thm("v_rel_simps[simp]",LIST_CONJ [
 (* state relation *)
 
 Inductive ref_rel:
-  (!b bs. ref_rel (ByteArray b bs) (ByteArray b bs)) /\
+  (!bs. ref_rel (ByteArray bs) (ByteArray bs)) /\
   (!xs ys.
     LIST_REL v_rel xs ys ==>
     ref_rel (ValueArray xs) (ValueArray ys))

compiler/backend/proofs/clos_to_bvlProofScript.sml

@@ -1024,13 +1024,13 @@ val compile_oracle_inv_def = Define`
 
 val ref_rel_def = Define`
   (ref_rel R (closSem$ValueArray vs) (bvlSem$ValueArray ws) ⇔ LIST_REL R vs ws) ∧
-  (ref_rel R (ByteArray f as) (ByteArray g bs) ⇔ f = g ∧ as = bs) ∧
+  (ref_rel R (ByteArray as) (ByteArray g bs) ⇔ ~g ∧ as = bs) ∧
   (ref_rel _ _ _ = F)`
 val _ = export_rewrites["ref_rel_def"];
 
 Theorem ref_rel_simp[simp]:
    (ref_rel R (ValueArray vs) y ⇔ ∃ws. y = ValueArray ws ∧ LIST_REL R vs ws) ∧
-   (ref_rel R (ByteArray f bs) y ⇔ y = ByteArray f bs)
+   (ref_rel R (ByteArray bs) y ⇔ y = ByteArray F bs)
 Proof
   Cases_on`y`>>simp[ref_rel_def] >> srw_tac[][EQ_IMP_THM]
 QED
@@ -4090,10 +4090,10 @@ Proof
       \\ rw[] \\ fs[SWAP_REVERSE_SYM] \\ rw[]
       \\ fs[v_rel_SIMP] \\ rw[]
       \\ imp_res_tac evaluate_const
-      \\ qmatch_assum_rename_tac`FLOOKUP _ n = SOME (ByteArray b l)`
+      \\ qmatch_assum_rename_tac`FLOOKUP _ n = SOME (ByteArray l)`
       \\ `?y m.
             FLOOKUP f2 n = SOME m /\ FLOOKUP t2.refs m = SOME y /\
-            ref_rel (v_rel s.max_app f2 t2.refs t2.code) (ByteArray b l) y` by
+            ref_rel (v_rel s.max_app f2 t2.refs t2.code) (ByteArray l) y` by
               METIS_TAC [state_rel_def]
       \\ full_simp_tac(srw_ss())[] \\ rpt var_eq_tac
       \\ Q.EXISTS_TAC `f2` \\ fsrw_tac[][]
@@ -4152,7 +4152,7 @@ Proof
       >- (fs[state_rel_def] >> res_tac >> fs[] >> rfs[] >> rveq)
       \\ `?y m.
             FLOOKUP f2 k = SOME m /\ FLOOKUP t2.refs m = SOME y /\
-            ref_rel (v_rel s.max_app f2 t2.refs t2.code) (ByteArray b' l'') y` by
+            ref_rel (v_rel s.max_app f2 t2.refs t2.code) (ByteArray l'') y` by
               METIS_TAC [state_rel_def]
       \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
       \\ rfs[]

compiler/backend/proofs/flat_to_closProofScript.sml

@@ -83,7 +83,7 @@ Definition store_rel_def:
           | Refv v => (?x. FLOOKUP t_refs i = SOME (ValueArray [x]) /\ v_rel v x)
           | Varray vs => (?xs. FLOOKUP t_refs i = SOME (ValueArray xs) /\
                                LIST_REL v_rel vs xs)
-          | W8array bs => FLOOKUP t_refs i = SOME (ByteArray F bs)
+          | W8array bs => FLOOKUP t_refs i = SOME (ByteArray bs)
 End
 
 Definition inc_compile_decs'_def:
@@ -131,7 +131,7 @@ QED
 
 Theorem lookup_byte_array:
   state_rel s1 t1 /\ store_lookup i s1.refs = SOME (W8array bytes) ==>
-  FLOOKUP t1.refs i = SOME (ByteArray F bytes)
+  FLOOKUP t1.refs i = SOME (ByteArray bytes)
 Proof
   fs [state_rel_def,store_rel_def] \\ rw []
   \\ fs [store_lookup_def]

compiler/backend/semantics/closPropsScript.sml

@@ -99,13 +99,13 @@ QED
 
 val ref_rel_def = Define`
   (ref_rel R (ValueArray vs) (ValueArray ws) ⇔ LIST_REL R vs ws) ∧
-  (ref_rel R (ByteArray f as) (ByteArray g bs) ⇔ f = g ∧ as = bs) ∧
+  (ref_rel R (ByteArray as) (ByteArray bs) ⇔ as = bs) ∧
   (ref_rel _ _ _ = F)`
 val _ = export_rewrites["ref_rel_def"];
 
 Theorem ref_rel_simp[simp]:
    (ref_rel R (ValueArray vs) y ⇔ ∃ws. y = ValueArray ws ∧ LIST_REL R vs ws) ∧
-   (ref_rel R (ByteArray f bs) y ⇔ y = ByteArray f bs)
+   (ref_rel R (ByteArray bs) y ⇔ y = ByteArray bs)
 Proof
   Cases_on`y`>>simp[ref_rel_def] >> srw_tac[][EQ_IMP_THM]
 QED
@@ -2000,9 +2000,9 @@ val simple_state_rel_def = Define `
   simple_state_rel vr sr <=>
     (!s t ptr. FLOOKUP t.refs ptr = NONE /\ sr s t ==>
                FLOOKUP s.refs ptr = NONE) /\
-    (∀w t s ptr b.
-      FLOOKUP t.refs ptr = SOME (ByteArray b w) ∧ sr s t ⇒
-      FLOOKUP s.refs ptr = SOME (ByteArray b w)) /\
+    (∀w t s ptr.
+      FLOOKUP t.refs ptr = SOME (ByteArray w) ∧ sr s t ⇒
+      FLOOKUP s.refs ptr = SOME (ByteArray w)) /\
     (∀w (t:('c,'ffi) closSem$state) (s:('d,'ffi) closSem$state) ptr.
       FLOOKUP t.refs ptr = SOME (ValueArray w) ∧ sr s t ⇒
       ∃w1.
@@ -2013,9 +2013,9 @@ val simple_state_rel_def = Define `
     (!f s t.
       sr s t ==> sr (s with ffi := f)
                     (t with ffi := f)) /\
-    (!f bs s t p.
-      sr s t ==> sr (s with refs := s.refs |+ (p,ByteArray f bs))
-                    (t with refs := t.refs |+ (p,ByteArray f bs))) /\
+    (!bs s t p.
+      sr s t ==> sr (s with refs := s.refs |+ (p,ByteArray bs))
+                    (t with refs := t.refs |+ (p,ByteArray bs))) /\
     (!s t p xs ys.
       sr s t /\ LIST_REL vr xs ys ==>
       sr (s with refs := s.refs |+ (p,ValueArray xs))
@@ -2043,8 +2043,8 @@ val simple_state_rel_update_ffi = prove(
 
 val simple_state_rel_update_bytes = prove(
   ``simple_state_rel vr sr /\ sr s t ==>
-    sr (s with refs := s.refs |+ (p,ByteArray f bs))
-       (t with refs := t.refs |+ (p,ByteArray f bs))``,
+    sr (s with refs := s.refs |+ (p,ByteArray bs))
+       (t with refs := t.refs |+ (p,ByteArray bs))``,
   fs [simple_state_rel_def]);
 
 val simple_state_rel_update = prove(
@@ -2171,7 +2171,7 @@ Theorem simple_state_rel_FLOOKUP_refs_IMP:
     FLOOKUP t.refs p = x ==>
     case x of
     | NONE => FLOOKUP s.refs p = NONE
-    | SOME (ByteArray f bs) => FLOOKUP s.refs p = SOME (ByteArray f bs)
+    | SOME (ByteArray bs) => FLOOKUP s.refs p = SOME (ByteArray bs)
     | SOME (ValueArray vs) =>
         ?xs. FLOOKUP s.refs p = SOME (ValueArray xs) /\ LIST_REL vr xs vs
 Proof

compiler/backend/semantics/closSemScript.sml

@@ -8,30 +8,27 @@ val _ = new_theory"closSem"
 
 (* differs from store_v by removing the single value Refv,
    also, adds flag to ByteArray for equality semantics *)
-val _ = Datatype `
+Datatype:
   ref = ValueArray ('a list)
-      | ByteArray bool (word8 list)`
-               (* T = compare-by-contents, immutable
-                  F = compare-by-pointer, mutable *)
-(* in closLang all are ByteArray F,
-   ByteArray T introduced in BVL to implement ByteVector *)
-
+      | ByteArray (word8 list)
+End
 
 (* --- Semantics of ClosLang --- *)
 
-val _ = Datatype `
+Datatype:
   v =
     Number int
   | Word64 word64
   | Block num (v list)
   | ByteVector (word8 list)
   | RefPtr num
   | Closure (num option) (v list) (v list) num closLang$exp
-  | Recclosure (num option) (v list) (v list) ((num # closLang$exp) list) num`
+  | Recclosure (num option) (v list) (v list) ((num # closLang$exp) list) num
+End
 
 Type clos_co = ``:num -> 'c # clos_prog``
 
-val _ = Datatype `
+Datatype:
   state =
     <| globals : (closSem$v option) list
      ; refs    : num |-> closSem$v ref
@@ -41,7 +38,8 @@ val _ = Datatype `
      ; compile_oracle : 'c clos_co
      ; code    : num |-> (num # closLang$exp)
      ; max_app : num
-    |> `
+    |>
+End
 
 (* helper functions *)
 
@@ -222,14 +220,14 @@ Definition do_app_def:
           | _ => Error)
     | (LengthByte,[RefPtr ptr]) =>
         (case FLOOKUP s.refs ptr of
-          | SOME (ByteArray _ xs) =>
+          | SOME (ByteArray xs) =>
               Rval (Number (&LENGTH xs), s)
           | _ => Error)
     | (RefByte F,[Number i;Number b]) =>
          if 0 ≤ i ∧ (∃w:word8. b = & (w2n w)) then
            let ptr = (LEAST ptr. ¬(ptr IN FDOM s.refs)) in
              Rval (RefPtr ptr, s with refs := s.refs |+
-               (ptr,ByteArray F (REPLICATE (Num i) (i2w b))))
+               (ptr,ByteArray (REPLICATE (Num i) (i2w b))))
          else Error
     | (RefArray,[Number i;v]) =>
         if 0 ≤ i then
@@ -239,18 +237,18 @@ Definition do_app_def:
          else Error
     | (DerefByte,[RefPtr ptr; Number i]) =>
         (case FLOOKUP s.refs ptr of
-         | SOME (ByteArray _ ws) =>
+         | SOME (ByteArray ws) =>
             (if 0 ≤ i ∧ i < &LENGTH ws
              then Rval (Number (& (w2n (EL (Num i) ws))),s)
              else Error)
          | _ => Error)
     | (UpdateByte,[RefPtr ptr; Number i; Number b]) =>
         (case FLOOKUP s.refs ptr of
-         | SOME (ByteArray f bs) =>
+         | SOME (ByteArray bs) =>
             (if 0 ≤ i ∧ i < &LENGTH bs ∧ (∃w:word8. b = & (w2n w))
              then
                Rval (Unit, s with refs := s.refs |+
-                 (ptr, ByteArray f (LUPDATE (i2w b) (Num i) bs)))
+                 (ptr, ByteArray (LUPDATE (i2w b) (Num i) bs)))
              else Error)
          | _ => Error)
     | (ConcatByteVec,[lv]) =>
@@ -275,16 +273,16 @@ Definition do_app_def:
          else Error)
     | (CopyByte F,[ByteVector ws; Number srcoff; Number len; RefPtr dst; Number dstoff]) =>
         (case FLOOKUP s.refs dst of
-         | SOME (ByteArray F ds) =>
+         | SOME (ByteArray ds) =>
            (case copy_array (ws,srcoff) len (SOME(ds,dstoff)) of
-            | SOME ds => Rval (Unit, s with refs := s.refs |+ (dst, ByteArray F ds))
+            | SOME ds => Rval (Unit, s with refs := s.refs |+ (dst, ByteArray ds))
             | NONE => Error)
          | _ => Error)
     | (CopyByte F,[RefPtr src; Number srcoff; Number len; RefPtr dst; Number dstoff]) =>
         (case (FLOOKUP s.refs src, FLOOKUP s.refs dst) of
-         | (SOME (ByteArray _ ws), SOME (ByteArray F ds)) =>
+         | (SOME (ByteArray ws), SOME (ByteArray ds)) =>
            (case copy_array (ws,srcoff) len (SOME(ds,dstoff)) of
-            | SOME ds => Rval (Unit, s with refs := s.refs |+ (dst, ByteArray F ds))
+            | SOME ds => Rval (Unit, s with refs := s.refs |+ (dst, ByteArray ds))
             | NONE => Error)
          | _ => Error)
     | (CopyByte T,[ByteVector ws; Number srcoff; Number len]) =>
@@ -293,7 +291,7 @@ Definition do_app_def:
         | _ => Error)
     | (CopyByte T,[RefPtr src; Number srcoff; Number len]) =>
        (case FLOOKUP s.refs src of
-        | SOME (ByteArray _ ws) =>
+        | SOME (ByteArray ws) =>
           (case copy_array (ws,srcoff) len NONE of
            | SOME ds => Rval (ByteVector ds, s)
            | _ => Error)
@@ -366,11 +364,11 @@ Definition do_app_def:
         | SOME w => Rval (Word64 (w2w w),s))
     | (FFI n, [ByteVector conf; RefPtr ptr]) =>
         (case FLOOKUP s.refs ptr of
-         | SOME (ByteArray F ws) =>
+         | SOME (ByteArray ws) =>
            (case call_FFI s.ffi (ExtCall n) conf ws of
             | FFI_return ffi' ws' =>
                 Rval (Unit,
-                      s with <| refs := s.refs |+ (ptr,ByteArray F ws')
+                      s with <| refs := s.refs |+ (ptr,ByteArray ws')
                               ; ffi   := ffi'|>)
             | FFI_final outcome =>
                 Rerr (Rabort (Rffi_error outcome)))
@@ -398,7 +396,7 @@ Definition do_app_def:
         Rval (Boolv (0 <= i /\ (if loose then $<= else $<) i (& LENGTH bs)),s)
     | (BoundsCheckByte loose,[RefPtr ptr; Number i]) =>
         (case FLOOKUP s.refs ptr of
-         | SOME (ByteArray _ ws) =>
+         | SOME (ByteArray ws) =>
              Rval (Boolv (0 <= i /\ (if loose then $<= else $<) i (& LENGTH ws)),s)
          | _ => Error)
     | (BoundsCheckArray,[RefPtr ptr; Number i]) =>