Revert test updates

Author: febyeji

ArchSemArm/tests/VMPromisingTest.v

@@ -90,33 +90,6 @@ Definition table_desc (next_pa : Z) : Z :=
 Definition page_desc (out_pa : Z) : Z :=
   Z.lor (Z.lor (Z.land out_pa (Z.lnot 0xFFF%Z)) 0x400%Z) 0x3%Z.  (* Valid=1, Page=1, AF=1 *)
 
-Definition init_empty_table(mem : memoryMap) (baddr : bv addr_size) : memoryMap :=
-  let reserved_addrs := dom mem in
-  foldl (λ mem index,
-    let addr := baddr `+Z` (index * 8) in
-    if decide (addr ∈ reserved_addrs)
-    then mem
-    else mem_insert addr 8 0 mem) mem (seqZ 0 512).
-
-Definition clear_offset (addr : bv addr_size) : bv addr_size :=
-  let ones : bv 9 := (-1)%bv in
-  bv_and addr (bv_not (bv_zero_extend addr_size ones)).
-
-Definition init_mem_trans (instrs : list (bv addr_size * bv 32))
-      (data : list (bv addr_size * bv 64))
-      (pgt : list (bv addr_size * bv 64))
-      (mem_strict : bool) : memoryMap :=
-  let mem_instrs :=
-    foldl (λ mem '(addr, val), mem_insert addr 4 val mem) ∅ instrs in
-  let mem :=
-    foldl (λ mem '(addr, val), mem_insert addr 8 val mem) mem_instrs (data ++ pgt) in
-
-  (* WARNING: filling out 512 entries for whole page table level *)
-  if mem_strict then
-    let baddrs := remove_dups $ map clear_offset pgt.*1 in
-    foldl init_empty_table mem baddrs
-  else mem.
-
 (** We test against the sail-tiny-arm semantic, with non-determinism enabled *)
 Definition arm_sem := sail_tiny_arm_sem true.