[sledge sem] Implement and verify cast expressions

Summary:
This commit adds truncation, sign extension and zero extension to LLVM
and the Convert instruction to LLAIR.

The LLVM instructions use HOL's build-in word/int and word/num
conversions. Sanity-checking theorems prove that zero-extending leaves
the value of the word unchanged when considered as an unsigned value,
and that sign-extending leaves the value unchanged when considered as a
signed value.

The llair semantics for Convert uses the truncate_2comp function which
converts an integer to another integer as though they were represented
in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp
255 8 = -1, truncate_2comp -3 2 = 1

Reviewed By: jberdine

Differential Revision: D18058833

fbshipit-source-id: df9de480c

sledge/semantics/llairScript.sml

@@ -57,6 +57,8 @@ Datatype:
   | Select exp exp
   (* Args: Record, index, value *)
   | Update exp exp exp
+  (* Args: signed?, to-type, from-type, value *)
+  | Convert bool typ typ exp
 End
 
 Datatype:
@@ -166,6 +168,18 @@ Termination
   first_x_assum drule >> decide_tac
 End
 
+(* The size of a type in bits *)
+Definition sizeof_bits_def:
+  (sizeof_bits (IntegerT n) = n) ∧
+  (sizeof_bits (PointerT t) = pointer_size) ∧
+  (sizeof_bits (ArrayT t n) = n * sizeof_bits t) ∧
+  (sizeof_bits (TupleT ts) = sum (map sizeof_bits ts))
+Termination
+  WF_REL_TAC `measure typ_size` >> simp [] >>
+  Induct >> rw [definition "typ_size_def"] >> simp [] >>
+  first_x_assum drule >> decide_tac
+End
+
 Definition first_class_type_def:
   (first_class_type (IntegerT _) ⇔ T) ∧
   (first_class_type (PointerT _) ⇔ T) ∧
@@ -195,12 +209,6 @@ Definition bool2v_def:
   bool2v b = FlatV (IntV (if b then 1 else 0) 1)
 End
 
-(* The integer, interpreted as 2's complement, fits in the given number of bits *)
-Definition ifits_def:
-  ifits (i:int) size ⇔
-    0 < size ∧ -(2 ** (size - 1)) ≤ i ∧ i < 2 ** (size - 1)
-End
-
 (* The natural number, interpreted as unsigned, fits in the given number of bits *)
 Definition nfits_def:
   nfits (n:num) size ⇔
@@ -208,7 +216,8 @@ Definition nfits_def:
 End
 
 (* Convert an integer to an unsigned number, following the 2's complement,
- * assuming (ifits i size) *)
+ * assuming (ifits i size). This looks like what OCaml's Z.extract does, which
+ * is used in LLAIR for Convert expressions *)
 Definition i2n_def:
   i2n (IntV i size) : num =
     if i < 0 then
@@ -307,7 +316,19 @@ Inductive eval_exp:
    eval_exp s e3 r ∧
    idx < length vals
    ⇒
-   eval_exp s (Update e1 e2 e3) (AggV (list_update r idx vals)))
+   eval_exp s (Update e1 e2 e3) (AggV (list_update r idx vals))) ∧
+
+  (∀s to_t from_t e v size.
+   eval_exp s e (FlatV v) ∧
+   size = sizeof_bits to_t
+   ⇒
+   eval_exp s (Convert F to_t from_t e) (FlatV (IntV (truncate_2comp (&i2n v) size) size))) ∧
+
+  (∀s to_t from_t e size size1 i.
+   eval_exp s e (FlatV (IntV i size1)) ∧
+   size = sizeof_bits to_t
+   ⇒
+   eval_exp s (Convert T to_t from_t e) (FlatV (IntV (truncate_2comp i size) size)))
 
 End
 

sledge/semantics/llair_propScript.sml

@@ -16,56 +16,6 @@ new_theory "llair_prop";
 
 numLib.prefer_num ();
 
-Theorem ifits_w2i:
-  ∀(w : 'a word). ifits (w2i w) (dimindex (:'a))
-Proof
-  rw [ifits_def, GSYM INT_MIN_def] >>
-  metis_tac [INT_MIN, w2i_ge, integer_wordTheory.INT_MAX_def, w2i_le,
-             intLib.COOPER_PROVE ``!(x:int) y. x ≤ y - 1 ⇔ x < y``]
-QED
-
-Theorem truncate_2comp_fits:
-  ∀i size. 0 < size ⇒ ifits (truncate_2comp i size) size
-Proof
-  rw [truncate_2comp_def, ifits_def] >>
-  qmatch_goalsub_abbrev_tac `(i + s1) % s2` >>
-  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`]
-  >- (
-    `0 ≤ (i + s1) % s2` suffices_by intLib.COOPER_TAC >>
-    drule INT_MOD_BOUNDS >>
-    rw [])
-  >- (
-    `(i + s1) % s2 < 2 * s1` suffices_by intLib.COOPER_TAC >>
-    `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
-    drule INT_MOD_BOUNDS >>
-    rw [Abbr `s1`, Abbr `s2`])
-QED
-
-Theorem fits_ident:
-  ∀i size. 0 < size ⇒ (ifits i size ⇔ truncate_2comp i size = i)
-Proof
-  rw [ifits_def, truncate_2comp_def] >>
-  rw [intLib.COOPER_PROVE ``!(x:int) y z. x - y = z <=> x = y + z``] >>
-  qmatch_goalsub_abbrev_tac `(_ + s1) % s2` >>
-  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`] >>
-  `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
-  eq_tac >>
-  rw []
-  >- (
-    simp [Once INT_ADD_COMM] >>
-    irule INT_LESS_MOD >>
-    rw [] >>
-    intLib.COOPER_TAC)
-  >- (
-   `0 ≤ (i + s1) % (2 * s1)` suffices_by intLib.COOPER_TAC >>
-    drule INT_MOD_BOUNDS >>
-    simp [])
-  >- (
-   `(i + s1) % (2 * s1) < 2 * s1` suffices_by intLib.COOPER_TAC >>
-    drule INT_MOD_BOUNDS >>
-    simp [])
-QED
-
 Theorem i2n_n2i:
   !n size. 0 < size ⇒ (nfits n size ⇔ (i2n (n2i n size) = n))
 Proof
@@ -179,7 +129,8 @@ Definition exp_uses_def:
   (exp_uses (Sub _ e1 e2) = exp_uses e1 ∪ exp_uses e2) ∧
   (exp_uses (Record es) = bigunion (set (map exp_uses es))) ∧
   (exp_uses (Select e1 e2) = exp_uses e1 ∪ exp_uses e2) ∧
-  (exp_uses (Update e1 e2 e3) = exp_uses e1 ∪ exp_uses e2 ∪ exp_uses e3)
+  (exp_uses (Update e1 e2 e3) = exp_uses e1 ∪ exp_uses e2 ∪ exp_uses e3) ∧
+  (exp_uses (Convert _ _ _ e) = exp_uses e)
 Termination
   WF_REL_TAC `measure exp_size` >> rw [] >>
   Induct_on `es` >> rw [exp_size_def] >> res_tac >> rw []
@@ -218,6 +169,8 @@ Proof
     Induct_on `es` >> rw [] >> fs [drestrict_union_eq])
   >- metis_tac []
   >- metis_tac []
+  >- metis_tac []
+  >- metis_tac []
 QED
 
 Theorem eval_exp_ignores_unused:

sledge/semantics/llvmScript.sml

@@ -72,6 +72,10 @@ Datatype:
   phi = Phi reg ty ((label option, arg) alist)
 End
 
+Datatype:
+  cast_op = Trunc | Zext | Sext | Ptrtoint | Inttoptr
+End
+
 (*
  * The Exit instruction below models a system/libc call to exit the program. The
  * semantics needs some way to tell the difference between normally terminated
@@ -99,8 +103,7 @@ Datatype:
   | Load reg ty targ
   | Store targ targ
   | Gep reg ty targ (targ list)
-  | Ptrtoint reg targ ty
-  | Inttoptr reg targ ty
+  | Cast reg cast_op targ ty
   | Icmp reg cond ty arg arg
   | Call reg ty fun_name (targ list)
   (* C++ runtime functions *)
@@ -440,6 +443,34 @@ Definition get_comp_def:
   (get_comp Ult = $<+)
 End
 
+Definition do_cast_def:
+  (do_cast Trunc v t =
+    option_join (option_map (λw. w64_cast (n2w w) t) (unsigned_v_to_num v))) ∧
+  (do_cast Zext v t =
+    option_join (option_map (λw. w64_cast (n2w w) t) (unsigned_v_to_num v))) ∧
+  (do_cast Sext v t =
+    option_join (option_map (λi. w64_cast (i2w i) t) (signed_v_to_int v))) ∧
+  (do_cast Ptrtoint v t =
+    case v of
+    | FlatV (PtrV w) => w64_cast w t
+    | _ => None) ∧
+  (do_cast Inttoptr v t =
+    option_join (option_map mk_ptr (unsigned_v_to_num v)))
+End
+
+(*
+  EVAL ``do_cast Trunc (FlatV (W32V 4294967295w)) (IntT W8) = Some (FlatV (W8V 255w))``
+  EVAL ``do_cast Trunc (FlatV (W32V 511w)) (IntT W8) = Some (FlatV (W8V 255w))``
+  EVAL ``do_cast Trunc (FlatV (W32V 255w)) (IntT W8) = Some (FlatV (W8V 255w))``
+  EVAL ``do_cast Trunc (FlatV (W32V 4294967166w)) (IntT W8) = Some (FlatV (W8V 126w))``
+  EVAL ``do_cast Trunc (FlatV (W32V 257w)) (IntT W8) = Some (FlatV (W8V 1w))``
+  EVAL ``do_cast Zext (FlatV (W8V 127w)) (IntT W32) = Some (FlatV (W32V 127w))``
+  EVAL ``do_cast Zext (FlatV (W8V 129w)) (IntT W32) = Some (FlatV (W32V 129w))``
+  EVAL ``do_cast Sext (FlatV (W8V 127w)) (IntT W32) = Some (FlatV (W32V 127w))``
+  EVAL ``do_cast Sext (FlatV (W8V 129w)) (IntT W32) = Some (FlatV (W32V (n2w (2 ** 32 - 1 - 255 + 129))))``
+  *)
+
+
 Definition do_icmp_def:
   do_icmp c v1 v2 =
     option_map (\b. <| poison := (v1.poison ∨ v2.poison); value := bool_to_v b |>)
@@ -625,26 +656,16 @@ Inductive step_instr:
                   value := ptr |>
                s))) ∧
 
-  (∀prog s r t1 a1 t v1 int_v w.
+  (∀prog s cop r t1 a1 t v1 v2.
    eval s a1 = Some v1 ∧
-   v1.value = FlatV (PtrV w) ∧
-   w64_cast w t = Some int_v
+   do_cast cop v1.value t = Some v2
    ⇒
    step_instr prog s
-    (Ptrtoint r (t1, a1) t) Tau
-    (inc_pc (update_result r <| poison := v1.poison; value := int_v |> s))) ∧
-
-  (∀prog s r t1 a1 t ptr v1 n.
-   eval s a1 = Some v1 ∧
-   unsigned_v_to_num v1.value = Some n ∧
-   mk_ptr n = Some ptr
-   ⇒
-   step_instr prog s
-    (Inttoptr r (t1, a1) t) Tau
-    (inc_pc (update_result r <| poison := v1.poison; value := ptr |> s))) ∧
+    (Cast r cop (t1, a1) t) Tau
+    (inc_pc (update_result r <| poison := v1.poison; value := v2 |> s))) ∧
 
   (∀prog s r c t a1 a2 v3 v1 v2.
-  eval s a1 = Some v1 ∧
+   eval s a1 = Some v1 ∧
    eval s a2 = Some v2 ∧
    do_icmp c v1 v2 = Some v3
    ⇒

sledge/semantics/llvm_propScript.sml

@@ -10,6 +10,7 @@
 open HolKernel boolLib bossLib Parse;
 open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
 open pred_setTheory finite_mapTheory relationTheory llistTheory pathTheory;
+open optionTheory;
 open logrootTheory numposrepTheory;
 open settingsTheory miscTheory memory_modelTheory llvmTheory;
 
@@ -290,6 +291,132 @@ QED
 
 (* ----- Theorems about the step function ----- *)
 
+Theorem w64_cast_some:
+  ∀w t.
+    (w64_cast w t = Some v)
+    ⇔
+    v = FlatV (W1V (w2w w)) ∧ t = IntT W1 ∨
+    v = FlatV (W8V (w2w w)) ∧ t = IntT W8 ∨
+    v = FlatV (W32V (w2w w)) ∧ t = IntT W32 ∨
+    v = FlatV (W64V (w2w w)) ∧ t = IntT W64
+Proof
+  Cases_on `t` >> rw [w64_cast_def] >> Cases_on `s` >> rw [w64_cast_def] >>
+  metis_tac []
+QED
+
+Theorem unsigned_v_to_num_some:
+  ∀v n.
+    (unsigned_v_to_num v = Some n)
+    ⇔
+    (∃w. v = FlatV (W1V w) ∧ n = w2n w) ∨
+    (∃w. v = FlatV (W8V w) ∧ n = w2n w) ∨
+    (∃w. v = FlatV (W32V w) ∧ n = w2n w) ∨
+    (∃w. v = FlatV (W64V w) ∧ n = w2n w)
+Proof
+  Cases_on `v` >> rw [unsigned_v_to_num_def] >>
+  Cases_on `a` >> rw [unsigned_v_to_num_def]
+QED
+
+Theorem signed_v_to_int_some:
+  ∀v n.
+    (signed_v_to_int v = Some n)
+    ⇔
+    (∃w. v = FlatV (W1V w) ∧ n = w2i w) ∨
+    (∃w. v = FlatV (W8V w) ∧ n = w2i w) ∨
+    (∃w. v = FlatV (W32V w) ∧ n = w2i w) ∨
+    (∃w. v = FlatV (W64V w) ∧ n = w2i w)
+Proof
+  Cases_on `v` >> rw [signed_v_to_int_def] >>
+  Cases_on `a` >> rw [signed_v_to_int_def] >>
+  metis_tac []
+QED
+
+Theorem signed_v_to_num_some:
+  ∀v n.
+    (signed_v_to_num v = Some n)
+    ⇔
+    ∃m. 0 ≤ m ∧ n = Num m ∧
+      ((∃w. v = FlatV (W1V w) ∧ m = w2i w) ∨
+       (∃w. v = FlatV (W8V w) ∧ m = w2i w) ∨
+       (∃w. v = FlatV (W32V w) ∧ m = w2i w) ∨
+       (∃w. v = FlatV (W64V w) ∧ m = w2i w))
+Proof
+  rw [signed_v_to_num_def, OPTION_JOIN_EQ_SOME, signed_v_to_int_some] >>
+  metis_tac [intLib.COOPER_PROVE ``!x:int. 0 ≤ x ⇔ ¬(x < 0)``]
+QED
+
+Theorem mk_ptr_some:
+  ∀n p. mk_ptr n = Some p ⇔ n < 256 ** pointer_size ∧ p = FlatV (PtrV (n2w n))
+Proof
+  rw [mk_ptr_def] >> metis_tac []
+QED
+
+(* How many bytes a value of the given type occupies *)
+Definition sizeof_bits_def:
+  (sizeof_bits (IntT W1) = 1) ∧
+  (sizeof_bits (IntT W8) = 8) ∧
+  (sizeof_bits (IntT W32) = 32) ∧
+  (sizeof_bits (IntT W64) = 64) ∧
+  (sizeof_bits (PtrT _) = pointer_size) ∧
+  (sizeof_bits (ArrT n t) = n * sizeof_bits t) ∧
+  (sizeof_bits (StrT ts) = sum (map sizeof_bits ts))
+Termination
+  WF_REL_TAC `measure ty_size` >> simp [] >>
+  Induct >> rw [ty_size_def] >> simp [] >>
+  first_x_assum drule >> decide_tac
+End
+
+Theorem do_cast_zext:
+  (∃t'. sizeof_bits t' < sizeof_bits t ∧ value_type t' v) ∧ do_cast Zext v t = Some v'
+  ⇒
+  unsigned_v_to_num v = unsigned_v_to_num v'
+Proof
+  rw [do_cast_def, OPTION_JOIN_EQ_SOME, w64_cast_some] >>
+  fs [unsigned_v_to_num_def, unsigned_v_to_num_some, sizeof_bits_def, value_type_cases] >>
+  rw [w2n_11, w2w_n2w]  >>
+  fs [sizeof_bits_def]
+  >- (
+    `w2n w' < dimword (:1)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+  >- (
+    `w2n w' < dimword (:1)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+  >- (
+    `w2n w' < dimword (:8)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+  >- (
+    `w2n w' < dimword (:1)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+  >- (
+    `w2n w' < dimword (:8)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+  >- (
+    `w2n w' < dimword (:32)` by metis_tac [w2n_lt] >>
+    fs [dimword_1])
+QED
+
+val trunc_thms =
+  LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] (GSYM truncate_2comp_i2w_w2i)))
+                 [``:1``, ``:8``, ``:32``, ``:64``]);
+
+val ifits_thms =
+  LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] (ifits_w2i )))
+                 [``:1``, ``:8``, ``:32``, ``:64``]);
+
+Theorem do_cast_sext:
+  (∃t'. sizeof_bits t' < sizeof_bits t ∧ value_type t' v) ∧ do_cast Sext v t = Some v'
+  ⇒
+  signed_v_to_int v = signed_v_to_int v'
+Proof
+  rw [do_cast_def, OPTION_JOIN_EQ_SOME, w64_cast_some] >>
+  fs [signed_v_to_int_def, signed_v_to_num_some, sizeof_bits_def, value_type_cases] >>
+  rw [] >>
+  fs [sizeof_bits_def, signed_v_to_int_def] >> rw [integer_wordTheory.w2w_i2w] >>
+  rw [trunc_thms, GSYM fits_ident] >>
+  rw [ifits_thms] >>
+  metis_tac [ifits_thms, ifits_mono, DECIDE ``1 ≤ 8 ∧ 1 ≤ 32 ∧ 8 ≤ 32 ∧ 1 ≤ 64 ∧ 8 ≤ 64 ∧ 32 ≤ 64``]
+QED
+
 Theorem get_instr_func:
   ∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2
 Proof
@@ -350,7 +477,7 @@ Proof
 QED
 
 Triviality not_none_eq:
-  !x. x ≠ None ⇔ ?y. x = Some y
+  !x. x ≠ None ⇔ ∃y. x = Some y
 Proof
   Cases >> rw []
 QED
@@ -373,8 +500,8 @@ Proof
       >- metis_tac [] >>
       fs [deallocate_def, heap_ok_def] >> rw [flookup_fdiff] >>
       eq_tac >> rw []
-      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE]
-      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE] >>
+      >- metis_tac [NOT_IS_SOME_EQ_NONE]
+      >- metis_tac [NOT_IS_SOME_EQ_NONE] >>
       fs [allocations_ok_def, stack_ok_def, EXTENSION] >> metis_tac [])
     >- (
       fs [globals_ok_def, deallocate_def] >> rw [] >>
@@ -461,9 +588,6 @@ Proof
   >- (
     irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
-  >- (
-    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
-    metis_tac [terminator_def])
   >- ( (* Call *)
     rw [state_invariant_def]
     >- (fs [prog_ok_def, ip_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
@@ -701,10 +825,10 @@ QED
 Triviality some_lemma:
   ∀P a b. (some (x, y). P x y) = Some (a, b) ⇒ P a b
 Proof
-  rw [optionTheory.some_def] >>
+  rw [some_def] >>
   qmatch_assum_abbrev_tac `(@x. Q x) = _` >>
   `Q (@x. Q x)` suffices_by (rw [Abbr `Q`]) >>
-  `?x. Q x` suffices_by rw [SELECT_THM] >>
+  `∃x. Q x` suffices_by rw [SELECT_THM] >>
   unabbrev_all_tac >> rw [] >>
   pairarg_tac >> fs [] >> rw [EXISTS_PROD] >>
   metis_tac []
@@ -724,7 +848,7 @@ Proof
   rw [] >>
   Cases_on `get_next_step p (last path) = None ∧ ∀s. path ≠ stopped_at s`
   >- (
-    fs [get_next_step_def, optionTheory.some_def, FORALL_PROD, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
+    fs [get_next_step_def, some_def, FORALL_PROD, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
     Cases_on `∃l2 s2. sem_step p (last path) l2 s2` >> fs []
     >- ( (* Can take a last step from the end of the path *)
       first_x_assum drule >> rw [] >>
@@ -747,7 +871,7 @@ Proof
       fs [finite_length] >>
       qexists_tac `n` >> rw [] >>
       `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
-      by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
+      by metis_tac [length_plink, alt_length_thm, OPTION_MAP_DEF] >>
       rw []
       >- fs [sem_step_cases]
       >- metis_tac [sem_step_not_last]
@@ -777,8 +901,8 @@ Proof
     drule sem_step_not_last >> simp [] >> strip_tac >>
     qpat_x_assum `sem_step p s2 l s3` mp_tac >> rw [Once sem_step_cases]
     >- (
-      `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
-      `?x. i = Inl x` by (fs [last_step_cases] >> metis_tac [sumTheory.sum_CASES]) >>
+      `∃i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
+      `∃x. i = Inl x` by (fs [last_step_cases] >> metis_tac [sumTheory.sum_CASES]) >>
       drule step_same_block >> disch_then drule >> simp [] >>
       impl_tac
       >- (fs [last_step_cases] >> metis_tac []) >>
@@ -798,7 +922,7 @@ Proof
     qabbrev_tac `P = (\s2 l. sem_step p s l s2 ∧ ¬last_step p s l s2)` >>
     `P s' l` by (irule some_lemma >> simp [Abbr `P`]) >>
     pop_assum mp_tac >> simp [Abbr `P`]) >>
-  `?n. length path1 = Some n` by fs [finite_length] >>
+  `∃n. length path1 = Some n` by fs [finite_length] >>
   `n ≠ 0` by metis_tac [length_never_zero] >>
   `length (plink path path1) = Some (Suc m + n - 1)` by metis_tac [length_plink] >>
   simp [take_pconcat, PL_def, finite_pconcat, length_plink] >>
@@ -807,7 +931,7 @@ Proof
   simp [GSYM PULL_EXISTS] >>
   unabbrev_all_tac >> drule unfold_last >>
   qmatch_goalsub_abbrev_tac `last_step _ (last path1) _ _` >>
-  simp [Once get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+  simp [Once get_next_step_def, some_def, FORALL_PROD] >>
   strip_tac >>
   simp [CONJ_ASSOC, Once CONJ_SYM] >>
   simp [GSYM CONJ_ASSOC] >>
@@ -834,7 +958,7 @@ Proof
       unabbrev_all_tac >> simp [] >>
       fs [] >> fs [Once unfold_thm] >>
       Cases_on `get_next_step p (last path)` >> simp [] >> fs [] >> rw [] >>
-      fs [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+      fs [get_next_step_def, some_def, FORALL_PROD] >>
       TRY split_pair_case_tac >> fs [sem_step_cases] >>
       metis_tac [])
     >- fs [alt_length_thm, length_never_zero])
@@ -852,7 +976,7 @@ Theorem find_path_prefix:
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw [toList_THM]
   >- fs [observation_prefixes_cases, IN_DEF] >>
-  `?s ls. obs = (s, ls)` by metis_tac [pairTheory.pair_CASES] >>
+  `∃s ls. obs = (s, ls)` by metis_tac [pairTheory.pair_CASES] >>
   fs [] >>
   `∃l. length path = Some l ∧ l ≠ 0` by metis_tac [finite_length, length_never_zero] >>
   `take (l-1) path = path` by metis_tac [take_all] >>
@@ -894,7 +1018,7 @@ Proof
   >- (
     drule expand_multi_step_path >> rw [] >>
     rename [`toList (labels m_path) = Some m_l`, `toList (labels s_path) = Some (flat m_l)`] >>
-    `?n short_l.
+    `∃n short_l.
       n ∈ PL s_path ∧
       toList (labels (take n s_path)) = Some short_l ∧
       x = ((last (take n s_path)).status, filter ($≠ Tau) short_l)`
@@ -911,7 +1035,7 @@ Proof
     impl_tac >> rw []
     >- metis_tac [] >>
     rename1 `last_step _ (last s_ext_path) last_l last_s` >>
-    `?s_ext_l. toList (labels s_ext_path) = Some s_ext_l` by metis_tac [LFINITE_toList, finite_labels] >>
+    `∃s_ext_l. toList (labels s_ext_path) = Some s_ext_l` by metis_tac [LFINITE_toList, finite_labels] >>
     qabbrev_tac `orig_path = take n (pconcat s_ext_path last_l (stopped_at last_s))` >>
     drule contract_step_path >> simp [] >> disch_then drule >> rw [] >>
     rename [`toList (labels m_path) = Some m_l`,
@@ -930,7 +1054,7 @@ Proof
       Cases_on `(last m_path).status` >> simp [] >>
       qexists_tac `s_ext_l ++ [last_l]` >> rw []) >>
     fs [PL_def, finite_pconcat] >> rfs [] >>
-    `?m. length s_ext_path = Some m` by metis_tac [finite_length] >>
+    `∃m. length s_ext_path = Some m` by metis_tac [finite_length] >>
     `length s_ext_path = Some m` by metis_tac [finite_length] >>
     `length (pconcat s_ext_path last_l (stopped_at (last m_path))) = Some (m + 1)`
     by metis_tac [length_pconcat, alt_length_thm] >>

sledge/semantics/llvm_ssaScript.sml

@@ -39,8 +39,7 @@ Definition instr_next_ips_def:
   (instr_next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
   (instr_next_ips (Store _ _) ip = { inc_pc ip }) ∧
   (instr_next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
-  (instr_next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
-  (instr_next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cast _ _ _ _) ip = { inc_pc ip }) ∧
   (instr_next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
   (instr_next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
   (instr_next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
@@ -163,8 +162,7 @@ Definition instr_uses_def:
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
   (instr_uses (Gep _ _ (_, a) targs) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (instr_uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
-  (instr_uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Cast _ _ (_, a) _) = arg_to_regs a) ∧
   (instr_uses (Icmp _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
   (instr_uses (Call _ _ _ targs) =
@@ -206,8 +204,7 @@ Definition instr_assigns_def:
   (instr_assigns (Alloca r _ _) = {r}) ∧
   (instr_assigns (Load r _ _) = {r}) ∧
   (instr_assigns (Gep r _ _ _) = {r}) ∧
-  (instr_assigns (Ptrtoint r _ _) = {r}) ∧
-  (instr_assigns (Inttoptr r _ _) = {r}) ∧
+  (instr_assigns (Cast r _ _ _) = {r}) ∧
   (instr_assigns (Icmp r _ _ _ _) = {r}) ∧
   (instr_assigns (Call r _ _ _) = {r}) ∧
   (instr_assigns (Cxa_allocate_exn r _) = {r}) ∧

sledge/semantics/llvm_to_llairScript.sml

@@ -129,7 +129,9 @@ Definition translate_instr_to_exp_def:
   (translate_instr_to_exp gmap emap (Extractvalue _ (t, a) cs) =
     foldl (λe c. Select e (translate_const gmap c)) (translate_arg gmap emap a) cs) ∧
   (translate_instr_to_exp gmap emap (Insertvalue _ (t1, a1) (t2, a2) cs) =
-    translate_updatevalue gmap (translate_arg gmap emap a1) (translate_arg gmap emap a2) cs)
+    translate_updatevalue gmap (translate_arg gmap emap a1) (translate_arg gmap emap a2) cs) ∧
+  (translate_instr_to_exp gmap emap (Cast _ cop (t1, a1) t) =
+    Convert (cop = Sext) (translate_ty t) (translate_ty t1) (translate_arg gmap emap a1))
 End
 
 (* This translation of insertvalue to update and select is quadratic in the
@@ -236,8 +238,7 @@ Definition classify_instr_def:
   (classify_instr (Alloca r t _) = Exp r (PtrT t)) ∧
   (classify_instr (Gep r t _ idx) =
     Exp r (PtrT (THE (extract_type t (map idx_to_num idx))))) ∧
-  (classify_instr (Ptrtoint r _ t) = Exp r t) ∧
-  (classify_instr (Inttoptr r _ t) = Exp r t) ∧
+  (classify_instr (Cast r _ _ t) = Exp r t) ∧
   (classify_instr (Icmp r _ _ _ _) = Exp r (IntT W1)) ∧
   (* TODO *)
   (classify_instr (Cxa_allocate_exn r _) = Exp r ARB) ∧

sledge/semantics/llvm_to_llair_propScript.sml

@@ -9,7 +9,7 @@
 
 open HolKernel boolLib bossLib Parse lcsymtacs;
 open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
-open rich_listTheory pathTheory;
+open optionTheory rich_listTheory pathTheory;
 open settingsTheory miscTheory memory_modelTheory;
 open llvmTheory llvm_propTheory llvm_ssaTheory llairTheory llair_propTheory llvm_to_llairTheory;
 
@@ -421,7 +421,7 @@ Proof
   >- (
     fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP] >>
     CASE_TAC >> fs [] >> first_x_assum (qspec_then `g` mp_tac) >> rw [] >>
-    rename1 `option_rel _ _ opt` >> Cases_on `opt` >> fs [optionTheory.OPTREL_def] >>
+    rename1 `option_rel _ _ opt` >> Cases_on `opt` >> fs [OPTREL_def] >>
     (* TODO: false at the moment, need to work out the llair story on globals *)
     cheat)
   (* TODO: unimplemented stuff *)
@@ -503,7 +503,6 @@ QED
 
 Theorem translate_sub_correct:
   ∀prog gmap emap s1 s1' nsw nuw ty v1 v1' v2 v2' e2' e1' result.
-    mem_state_rel prog gmap emap s1 s1' ∧
     do_sub nuw nsw v1 v2 ty = Some result ∧
     eval_exp s1' e1' v1' ∧
     v_rel v1.value v1' ∧
@@ -629,6 +628,49 @@ Proof
   metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
 QED
 
+val trunc_thms =
+  LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] truncate_2comp_i2w_w2i))
+                 [``:1``, ``:8``, ``:32``, ``:64``]);
+
+val i2n_thms =
+  LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] (GSYM w2n_i2n)))
+                 [``:1``, ``:8``, ``:32``, ``:64``]);
+
+Theorem translate_cast_correct:
+  ∀prog gmap emap s1' cop ty v1 v1' e1' result t2.
+    do_cast cop v1.value ty = Some result ∧
+    eval_exp s1' e1' v1' ∧
+    v_rel v1.value v1' ∧
+    (cop = Inttoptr ⇒ ∃t. ty = PtrT t)
+    ⇒
+    ∃v3'.
+      eval_exp s1' (Convert (cop = Sext) (translate_ty ty) t2 e1') v3' ∧
+      v_rel result v3'
+Proof
+  rw [] >> simp [Once eval_exp_cases, PULL_EXISTS, Once v_rel_cases] >>
+  Cases_on `cop ≠ Sext`
+  >- (
+    Cases_on `cop` >> fs [do_cast_def] >> rw [] >>
+    BasicProvers.EVERY_CASE_TAC >> fs [] >>
+    fs [OPTION_JOIN_EQ_SOME, w64_cast_some, signed_v_to_int_some,
+        unsigned_v_to_num_some, mk_ptr_some] >>
+    rw [sizeof_bits_def, translate_ty_def, translate_size_def] >>
+    rfs [] >> fs [v_rel_cases] >>
+    HINT_EXISTS_TAC >>
+    rw [w2w_n2w, trunc_thms, i2n_thms, w2w_def, pointer_size_def]) >>
+  fs [do_cast_def, OPTION_JOIN_EQ_SOME, PULL_EXISTS, w64_cast_some,
+      translate_ty_def, sizeof_bits_def, signed_v_to_int_some,
+      translate_size_def] >>
+  rfs [v_rel_cases, w2w_i2w] >> rw [trunc_thms] >>
+  qmatch_assum_abbrev_tac `eval_exp _ _ (FlatV (IntV i s))` >>
+  qexists_tac `s` >> qexists_tac `i` >> rw [] >>
+  unabbrev_all_tac >> rw [] >>
+  rw [i2w_w2i_extend, WORD_w2w_OVER_MUL, WORD_ALL_BITS] >>
+  Cases_on `w2w w : word1` >> rw [] >> fs [dimword_1] >>
+  Cases_on `n` >> rw [] >> fs [] >>
+  Cases_on `n'` >> rw [] >> fs []
+QED
+
 Theorem prog_ok_nonterm:
   ∀prog i ip.
     prog_ok prog ∧ get_instr prog ip (Inl i) ∧ ¬terminator i ⇒ inc_pc ip ∈ next_ips prog ip
@@ -644,6 +686,25 @@ Proof
   rw [EXISTS_OR_THM, inc_pc_def, inc_bip_def]
 QED
 
+Theorem const_idx_uses[simp]:
+  ∀cs gmap e.
+    exp_uses (foldl (λe c. Select e (translate_const gmap c)) e cs) = exp_uses e
+Proof
+  Induct_on `cs` >> rw [exp_uses_def] >>
+  rw [translate_const_no_reg, EXTENSION]
+QED
+
+Theorem exp_uses_trans_upd_val[simp]:
+  ∀cs gmap e1 e2. exp_uses (translate_updatevalue gmap e1 e2 cs) =
+    (if cs = [] then {} else exp_uses e1) ∪ exp_uses e2
+Proof
+  Induct_on `cs` >> rw [exp_uses_def, translate_updatevalue_def] >>
+  rw [translate_const_no_reg, EXTENSION] >>
+  metis_tac []
+QED
+
+(* TODO: identify some lemmas to cut down on the duplicated proof in the very
+ * similar cases *)
 Theorem translate_instr_to_exp_correct:
   ∀gmap emap instr r t s1 s1' s2 prog l.
     is_ssa prog ∧ prog_ok prog ∧
@@ -676,30 +737,29 @@ Proof
     disch_then drule >> disch_then drule >>
     first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
     disch_then drule >> disch_then drule >> rw [] >>
-    drule translate_sub_correct >> disch_then drule >>
-    disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
+    drule translate_sub_correct >>
+    simp [] >>
+    disch_then (qspecl_then [`s1'`, `v'`, `v''`] mp_tac) >> simp [] >>
     disch_then drule >> disch_then drule >> rw [] >>
     rename1 `eval_exp _ (Sub _ _ _) res_v` >>
     rename1 `r ∈ _` >>
+    simp [inc_pc_def, llvmTheory.inc_pc_def] >>
+    `assigns prog s1.ip = {r}`
+    by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
+    `reachable prog s1.ip` by fs [mem_state_rel_def] >>
+    `s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
+    by (
+      drule prog_ok_nonterm >>
+      simp [get_instr_cases, PULL_EXISTS] >>
+      ntac 3 (disch_then drule) >>
+      simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
     Cases_on `r ∈ regs_to_keep` >> rw []
     >- (
       simp [step_inst_cases, PULL_EXISTS] >>
-      qexists_tac `res_v` >> rw []
-      >- simp [inc_pc_def, llvmTheory.inc_pc_def]
-      >- (
-        rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
-        simp [llvmTheory.inc_pc_def] >>
-        irule mem_state_rel_update_keep >> rw []
-        >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
-        >- (
-          drule prog_ok_nonterm >>
-          simp [get_instr_cases, PULL_EXISTS] >>
-          ntac 3 (disch_then drule) >>
-          simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def])
-        >- fs [mem_state_rel_def]))
-    >- rw [inc_pc_def, llvmTheory.inc_pc_def]
+      qexists_tac `res_v` >> rw [] >>
+      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+      irule mem_state_rel_update_keep >> rw [])
     >- (
-      simp [llvmTheory.inc_pc_def] >>
       irule mem_state_rel_update >> rw []
       >- (
         fs [exp_uses_def]
@@ -708,72 +768,142 @@ Proof
         rename1 `flookup _ r_tmp` >>
         qexists_tac `r_tmp` >> rw [] >>
         simp [Once live_gen_kill] >> disj2_tac >>
-        simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def])
-      >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
-      >- (
-        drule prog_ok_nonterm >>
-        simp [get_instr_cases, PULL_EXISTS] >>
-        ntac 3 (disch_then drule) >>
-        simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
+        simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
       metis_tac [])) >>
   conj_tac
   >- ( (* Extractvalue *)
-    rw [step_instr_cases] >>
-    simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
-    drule translate_extract_correct >> rpt (disch_then drule) >>
-    drule translate_arg_correct >> disch_then drule >>
+    rw [step_instr_cases, get_instr_cases, update_result_def] >>
+    qpat_x_assum `Extractvalue _ _ _ = el _ _` (assume_tac o GSYM) >>
     `arg_to_regs a ⊆ live prog s1.ip`
     by (
-      fs [get_instr_cases] >>
-      qpat_x_assum `Extractvalue _ _ _ = el _ _` (mp_tac o GSYM) >>
       simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
             instr_uses_def]) >>
+    drule translate_extract_correct >> rpt (disch_then drule) >>
+    drule translate_arg_correct >> disch_then drule >>
     simp [] >> strip_tac >>
     disch_then drule >> simp [] >> rw [] >>
     rename1 `eval_exp _ (foldl _ _ _) res_v` >>
-    rw [inc_bip_def, inc_pc_def] >>
+    rw [inc_pc_def, llvmTheory.inc_pc_def] >>
     rename1 `r ∈ _` >>
+    `assigns prog s1.ip = {r}`
+    by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
+    `reachable prog s1.ip` by fs [mem_state_rel_def] >>
+    `s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
+    by (
+      drule prog_ok_nonterm >>
+      simp [get_instr_cases, PULL_EXISTS] >>
+      ntac 3 (disch_then drule) >>
+      simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
     Cases_on `r ∈ regs_to_keep` >> rw []
     >- (
       simp [step_inst_cases, PULL_EXISTS] >>
       qexists_tac `res_v` >> rw [] >>
-      rw [update_results_def] >>
-      (* TODO: unfinished *)
-      cheat)
-    >- cheat) >>
+      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+      irule mem_state_rel_update_keep >> rw [])
+    >- (
+      irule mem_state_rel_update >> rw []
+      >- (
+        Cases_on `a` >>
+        fs [translate_arg_def] >>
+        rename1 `flookup _ r_tmp` >>
+        qexists_tac `r_tmp` >> rw [] >>
+        simp [Once live_gen_kill] >> disj2_tac >>
+        simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
+      metis_tac [])) >>
   conj_tac
   >- ( (* Updatevalue *)
-    rw [step_instr_cases] >>
-    simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
-    drule translate_update_correct >> rpt (disch_then drule) >>
-    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
-    disch_then drule >>
-    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
-    disch_then drule >>
+    rw [step_instr_cases, get_instr_cases, update_result_def] >>
+    qpat_x_assum `Insertvalue _ _ _ _ = el _ _` (assume_tac o GSYM) >>
     `arg_to_regs a1 ⊆ live prog s1.ip ∧
      arg_to_regs a2 ⊆ live prog s1.ip`
     by (
-      fs [get_instr_cases] >>
-      qpat_x_assum `Insertvalue _ _ _ _ = el _ _` (mp_tac o GSYM) >>
       ONCE_REWRITE_TAC [live_gen_kill] >>
       simp [SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
             instr_uses_def]) >>
-   simp [] >> strip_tac >> strip_tac >>
-   disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
-   disch_then drule >> disch_then drule >>
-   rw [] >>
-   rename1 `eval_exp _ (translate_updatevalue _ _ _ _) res_v` >>
-   rw [inc_pc_def, inc_bip_def] >>
-   rename1 `r ∈ _` >>
-   Cases_on `r ∈ regs_to_keep` >> rw []
+    drule translate_update_correct >> rpt (disch_then drule) >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >>
+    simp [] >> strip_tac >> strip_tac >>
+    disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
+    disch_then drule >> disch_then drule >>
+    rw [] >>
+    rename1 `eval_exp _ (translate_updatevalue _ _ _ _) res_v` >>
+    rw [inc_pc_def, llvmTheory.inc_pc_def] >>
+    rename1 `r ∈ _` >>
+    `assigns prog s1.ip = {r}`
+    by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
+    `reachable prog s1.ip` by fs [mem_state_rel_def] >>
+    `s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
+    by (
+      drule prog_ok_nonterm >>
+      simp [get_instr_cases, PULL_EXISTS] >>
+      ntac 3 (disch_then drule) >>
+      simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
+    Cases_on `r ∈ regs_to_keep` >> rw []
     >- (
       simp [step_inst_cases, PULL_EXISTS] >>
       qexists_tac `res_v` >> rw [] >>
-      rw [update_results_def] >>
-      (* TODO: unfinished *)
-      cheat)
-    >- cheat) >>
-  (* Other expressions, Icmp, Inttoptr, Ptrtoint, Gep, Alloca *)
+      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+      irule mem_state_rel_update_keep >> rw [])
+    >- (
+      irule mem_state_rel_update >> strip_tac
+      >- (
+        Cases_on `a1` >> Cases_on `a2` >>
+        rw [translate_arg_def] >>
+        rename1 `flookup _ r_tmp` >>
+        qexists_tac `r_tmp` >> rw [] >>
+        simp [Once live_gen_kill] >> disj2_tac >>
+        simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
+      rw [] >> metis_tac [] ))>>
+  conj_tac
+  >- ( (* Cast *)
+    rw [step_instr_cases, get_instr_cases, update_result_def] >>
+    qpat_x_assum `Cast _ _ _ _ = el _ _` (assume_tac o GSYM) >>
+    `arg_to_regs a1 ⊆ live prog s1.ip`
+    by (
+      simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
+            instr_uses_def] >>
+      metis_tac []) >>
+    fs [] >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >> disch_then drule >> rw [] >>
+    drule translate_cast_correct >> ntac 2 (disch_then drule) >>
+    simp [] >>
+    disch_then (qspec_then `translate_ty t1` mp_tac) >>
+    impl_tac
+    (* TODO: prog_ok should enforce that the type is consistent *)
+    >- cheat >>
+    rw [] >>
+    rename1 `eval_exp _ (Convert _ _ _ _) res_v` >>
+    rw [inc_pc_def, llvmTheory.inc_pc_def] >>
+    rename1 `r ∈ _` >>
+    `assigns prog s1.ip = {r}`
+    by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
+    `reachable prog s1.ip` by fs [mem_state_rel_def] >>
+    `s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
+    by (
+      drule prog_ok_nonterm >>
+      simp [get_instr_cases, PULL_EXISTS] >>
+      ntac 3 (disch_then drule) >>
+      simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
+    Cases_on `r ∈ regs_to_keep` >> rw []
+    >- (
+      simp [step_inst_cases, PULL_EXISTS] >>
+      qexists_tac `res_v` >> rw [] >>
+      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+      irule mem_state_rel_update_keep >> rw [])
+    >- (
+      irule mem_state_rel_update >> rw []
+      >- (
+        fs [exp_uses_def] >> Cases_on `a1` >> fs [translate_arg_def] >>
+        rename1 `flookup _ r_tmp` >>
+        qexists_tac `r_tmp` >> rw [] >>
+        simp [Once live_gen_kill] >> disj2_tac >>
+        simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
+      metis_tac [])) >>
+  (* TODO: unimplemented instruction translations *)
   cheat
 QED
 
@@ -877,7 +1007,7 @@ Proof
       >- (
         first_x_assum (qspec_then `x` mp_tac) >> rw [] >>
         rename1 `option_rel _ _ opt` >> Cases_on `opt` >>
-        fs [optionTheory.OPTREL_def] >>
+        fs [OPTREL_def] >>
         cheat) >>
       cheat))
 QED

sledge/semantics/miscScript.sml

@@ -375,6 +375,87 @@ Proof
     simp [INT_MOD_PLUS])
 QED
 
+(* The integer, interpreted as 2's complement, fits in the given number of bits *)
+Definition ifits_def:
+  ifits (i:int) size ⇔
+    0 < size ∧ -(2 ** (size - 1)) ≤ i ∧ i < 2 ** (size - 1)
+End
+Theorem ifits_w2i:
+  ∀(w : 'a word). ifits (w2i w) (dimindex (:'a))
+Proof
+  rw [ifits_def, GSYM INT_MIN_def] >>
+  metis_tac [INT_MIN, w2i_ge, integer_wordTheory.INT_MAX_def, w2i_le,
+             intLib.COOPER_PROVE ``!(x:int) y. x ≤ y - 1 ⇔ x < y``]
+QED
+
+Theorem truncate_2comp_fits:
+  ∀i size. 0 < size ⇒ ifits (truncate_2comp i size) size
+Proof
+  rw [truncate_2comp_def, ifits_def] >>
+  qmatch_goalsub_abbrev_tac `(i + s1) % s2` >>
+  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`]
+  >- (
+    `0 ≤ (i + s1) % s2` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    rw [])
+  >- (
+    `(i + s1) % s2 < 2 * s1` suffices_by intLib.COOPER_TAC >>
+    `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
+    drule INT_MOD_BOUNDS >>
+    rw [Abbr `s1`, Abbr `s2`])
+QED
+
+Theorem ifits_mono:
+  ∀i s1 s2. s1 ≤ s2 ∧ ifits i s1 ⇒ ifits i s2
+Proof
+  rw [ifits_def]
+  >- (
+    `&(2 ** (s1 − 1)) ≤ &(2 ** (s2 − 1))` suffices_by intLib.COOPER_TAC >>
+    rw [])
+  >- (
+    `&(2 ** (s1 − 1)) ≤ &(2 ** (s2 − 1))` suffices_by intLib.COOPER_TAC >>
+    rw [])
+QED
+
+Theorem fits_ident:
+  ∀i size. 0 < size ⇒ (ifits i size ⇔ truncate_2comp i size = i)
+Proof
+  rw [ifits_def, truncate_2comp_def] >>
+  rw [intLib.COOPER_PROVE ``!(x:int) y z. x - y = z <=> x = y + z``] >>
+  qmatch_goalsub_abbrev_tac `(_ + s1) % s2` >>
+  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`] >>
+  `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
+  eq_tac >>
+  rw []
+  >- (
+    simp [Once INT_ADD_COMM] >>
+    irule INT_LESS_MOD >>
+    rw [] >>
+    intLib.COOPER_TAC)
+  >- (
+   `0 ≤ (i + s1) % (2 * s1)` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    simp [])
+  >- (
+   `(i + s1) % (2 * s1) < 2 * s1` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    simp [])
+QED
+
+Theorem i2w_w2i_extend:
+  i2w (w2i (w : 'a word)) : 'b word =
+    if ¬word_msb w then
+      w2w w
+    else
+      -w2w (-w)
+Proof
+  rw [i2w_def, w2i_def] >>
+  BasicProvers.FULL_CASE_TAC >> fs [] >>
+  fs [] >>
+  full_simp_tac std_ss [GSYM WORD_NEG_MUL] >>
+  full_simp_tac std_ss [w2w_def]
+QED
+
 (* ----- Theorems about lazy lists ----- *)
 
 Theorem toList_some: