diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index 69e64cf4a..e6f15ced2 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -57,7 +57,7 @@ Datatype:
   | Select exp exp
   (* Args: Record, index, value *)
   | Update exp exp exp
-  (* Args: signed?, to-type, from-type, value *)
+  (* Args: unsigned?, to-type, from-type, value *)
   | Convert bool typ typ exp
 End
 
@@ -322,13 +322,13 @@ Inductive eval_exp:
    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))) ∧
+   eval_exp s (Convert T 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)))
+   eval_exp s (Convert F to_t from_t e) (FlatV (IntV (truncate_2comp i size) size)))
 
 End
 
diff --git a/sledge/semantics/llair_propScript.sml b/sledge/semantics/llair_propScript.sml
index d1754d6a0..7d6c32f13 100644
--- a/sledge/semantics/llair_propScript.sml
+++ b/sledge/semantics/llair_propScript.sml
@@ -179,4 +179,182 @@ Proof
   metis_tac [eval_exp_ignores_unused_lem]
 QED
 
+(* Relate the semantics of Convert to something more closely following the
+ * implementation *)
+
+Definition Zextract_def:
+  Zextract (:'a) z off len = &w2n ((len+off-1 -- off) (i2w z : 'a word))
+End
+
+Definition Zsigned_extract_def:
+  Zsigned_extract (:'a) z off len = w2i ((len+off-1 --- off) (i2w z : 'a word))
+End
+
+(*
+ * Some tests of extract and signed_extract in both HOL and OCaml to check that
+ * we are defining the same thing *)
+
+(*
+ EVAL ``
+   let bp1 = 0b11001100w : word8 in
+   let bp2 = 0b01011011w : word8 in
+   let i1 = &(w2n bp1) in
+   let i2 = w2i bp1 in
+   let i3 = &(w2n bp2) in
+     Zextract (:128) i1 0 8 = i1 ∧
+     Zextract (:128) i2 0 8 = i1 ∧
+     Zextract (:128) i3 0 8 = i3 ∧
+     Zsigned_extract (:128) i1 0 8 = i2 ∧
+     Zsigned_extract (:128) i2 0 8 = i2 ∧
+     Zsigned_extract (:128) i3 0 8 = i3 ∧
+
+     Zextract (:128) i1 2 4 = 3 ∧
+     Zextract (:128) i2 2 4 = 3 ∧
+     Zextract (:128) i1 2 5 = 19 ∧
+     Zextract (:128) i2 2 5 = 19 ∧
+     Zextract (:128) i3 1 2 = 1 ∧
+     Zextract (:128) i3 1 3 = 5 ∧
+
+     Zsigned_extract (:128) i1 2 4 = 3 ∧
+     Zsigned_extract (:128) i2 2 4 = 3 ∧
+     Zsigned_extract (:128) i1 2 5 = -13 ∧
+     Zsigned_extract (:128) i2 2 5 = -13 ∧
+     Zsigned_extract (:128) i3 1 2 = 1 ∧
+     Zsigned_extract (:128) i3 1 3 = -3``
+
+   let i1 = Z.of_int 0b11001100 in
+   let i2 = Z.of_int (-52) in
+   let i3 = Z.of_int 0b01011011 in
+     Z.extract i1 0 8 = i1 &&
+     Z.extract i2 0 8 = i1 &&
+     Z.extract i3 0 8 = i3 &&
+     Z.signed_extract i1 0 8 = i2 &&
+     Z.signed_extract i2 0 8 = i2 &&
+     Z.signed_extract i3 0 8 = i3 &&
+
+     Z.extract i1 2 4 = Z.of_int 3 &&
+     Z.extract i2 2 4 = Z.of_int 3 &&
+     Z.extract i1 2 5 = Z.of_int 19 &&
+     Z.extract i2 2 5 = Z.of_int 19 &&
+     Z.extract i3 1 2 = Z.of_int 1 &&
+     Z.extract i3 1 3 = Z.of_int 5 &&
+
+     Z.signed_extract i1 2 4 = Z.of_int 3 &&
+     Z.signed_extract i2 2 4 = Z.of_int 3 &&
+     Z.signed_extract i1 2 5 = Z.of_int (-13) &&
+     Z.signed_extract i2 2 5 = Z.of_int (-13) &&
+     Z.signed_extract i3 1 2 = Z.of_int 1 &&
+     Z.signed_extract i3 1 3 = Z.of_int (-3);;
+     *)
+
+Definition extract_def:
+  extract (:'a) unsigned bits z =
+    if unsigned then Zextract (:'a) z 0 bits else Zsigned_extract (:'a) z 0 bits
+End
+
+Definition simp_convert_def:
+  simp_convert (:'a) unsigned dst src arg =
+    case (dst, src, arg) of
+    | (IntegerT m, IntegerT n, Integer data _) =>
+      if ¬unsigned ∧ m ≥ n then (Integer data dst)
+      else Integer (extract (:'a) unsigned (MIN m n) data) dst
+    | _ =>
+      arg
+End
+
+Theorem Zextract0:
+  dimindex (:'b) ≤ dimindex (:'a)
+  ⇒
+  Zextract (:'a) i 0 (dimindex (:'b)) = &w2n (i2w i : 'b word)
+Proof
+  rw [Zextract_def] >>
+  `w2n ((dimindex (:β) − 1 -- 0) (i2w i : 'a word)) =
+   w2n (w2w (i2w i : 'a word) : 'b word)`
+  by (
+    rw [w2n_w2w] >>
+    `dimindex (:'b) = dimindex (:'a)` by decide_tac >>
+    fs [WORD_ALL_BITS]) >>
+  rw [w2w_i2w]
+QED
+
+Theorem Zsigned_extract0:
+  dimindex (:'b) ≤ dimindex (:'a)
+  ⇒
+  Zsigned_extract (:'a) i 0 (dimindex (:'b)) = w2i (i2w i : 'b word)
+Proof
+  rw [Zsigned_extract_def] >>
+  rw [word_sign_extend_bits, word_sign_extend_def, ADD1] >>
+  `0 < dimindex (:'b) ⇒ dimindex (:'b) - 1 + 1 = dimindex (:'b)` by decide_tac >>
+  `min (dimindex (:β)) (dimindex (:α)) = dimindex (:β)` by fs [MIN_DEF] >>
+  rw [] >>
+  `w2n ((dimindex (:β) − 1 -- 0) (i2w i : 'a word)) =
+   w2n (w2w (i2w i : 'a word) : 'b word)`
+  by (
+    rw [w2n_w2w] >>
+    `dimindex (:'b) = dimindex (:'a)` by decide_tac >>
+    fs [WORD_ALL_BITS]) >>
+  rw [GSYM sw2sw_def, w2w_i2w] >>
+  rw [w21_sw2sw_extend]
+QED
+
+Theorem convert_implementation:
+  ∀h unsigned dst src const i m n.
+    const = Integer i src ∧
+    src = IntegerT n ∧ 0 < n ∧
+    dst = IntegerT m ∧
+    ifits i (sizeof_bits src) ∧
+    dimindex (:'b) = min m n ∧
+    dimindex (:'b) ≤ dimindex (:'a)
+    ⇒
+    eval_exp h (Convert unsigned dst src const) =
+    eval_exp h (simp_convert (:'a) unsigned dst src const)
+Proof
+  rw [EXTENSION, IN_DEF] >>
+  simp [simp_convert_def] >>
+  CASE_TAC >>
+  fs [METIS_PROVE [] ``¬(¬unsigned ∧ m ≥ n) ⇔ (m ≥ n ⇒ unsigned)``] >>
+  ONCE_REWRITE_TAC [eval_exp_cases] >>
+  fs [sizeof_bits_def] >>
+  ONCE_REWRITE_TAC [eval_exp_cases] >> rw [] >>
+  `truncate_2comp i n = i` by metis_tac [fits_ident] >>
+  rw [] >>
+  Cases_on `unsigned` >> fs [extract_def] >>
+  irule (METIS_PROVE [] ``y = z ⇒ (x = y ⇔ x = z)``) >> rw []
+  >- ( (* unsigned *)
+    drule Zextract0 >> rw [] >>
+    `min m n = n ∨ min m n = m` by rw [MIN_DEF]
+    >- ( (* zero extending *)
+      `truncate_2comp i n = w2i (i2w i : 'b word)` by metis_tac [truncate_2comp_i2w_w2i] >>
+      fs [] >>
+      qpat_x_assum `w2i (i2w _) = _` (fn th => ONCE_REWRITE_TAC [GSYM th]) >>
+      rw [GSYM w2n_i2n])
+    >- ( (* truncating *)
+      fs [] >> rw [] >>
+      `∀i. truncate_2comp i (dimindex (:β)) = w2i (i2w i : 'b word)`
+      by rw [GSYM truncate_2comp_i2w_w2i] >>
+      rw [i2w_pos, i2n_def, i2w_def] >>
+      `?j. 0 ≤ j ∧ -i = j` by rw [] >>
+      `i = -j` by intLib.COOPER_TAC >>
+      simp [] >>
+      simp [GSYM int_sub] >>
+      `?k. j = &k` by metis_tac [NUM_POSINT_EXISTS] >>
+      simp [] >>
+      `k < 2 ** n`
+      by (fs [ifits_def] >> Cases_on `n` >> fs [ADD1, EXP_ADD]) >>
+      simp [INT_SUB, word_2comp_n2w, dimword_def] >>
+      qabbrev_tac `d = dimindex (:'b)` >>
+      `∃x. (2:num) ** n = 2 ** x * 2 ** d`
+      by (
+        `?x. n = x + d` by (qexists_tac `n - d` >> fs [MIN_DEF]) >>
+        metis_tac [EXP_ADD]) >>
+      metis_tac [MOD_COMPLEMENT, bitTheory.ZERO_LT_TWOEXP, MULT_COMM]))
+  >- (
+    `min m n = m` by rw [MIN_DEF] >>
+    drule Zsigned_extract0 >> rw [] >> fs [] >>
+    `w2i (i2w i : 'b word) = truncate_2comp i m` by metis_tac [truncate_2comp_i2w_w2i] >>
+    rw [] >>
+    `0 < dimindex (:'b)` by rw [] >>
+    metis_tac [fits_ident, truncate_2comp_fits])
+QED
+
 export_theory ();
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index 35cd922fe..0271ba353 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -131,7 +131,7 @@ Definition translate_instr_to_exp_def:
   (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_instr_to_exp gmap emap (Cast _ cop (t1, a1) t) =
-    Convert (cop = Sext) (translate_ty t) (translate_ty t1) (translate_arg gmap emap a1))
+    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
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 517785475..a616fb456 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -644,7 +644,7 @@ Theorem translate_cast_correct:
     (cop = Inttoptr ⇒ ∃t. ty = PtrT t)
     ⇒
     ∃v3'.
-      eval_exp s1' (Convert (cop = Sext) (translate_ty ty) t2 e1') 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] >>
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index 034b395ba..cf00a1cea 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -219,6 +219,13 @@ Proof
   >- (fs [optionTheory.IS_SOME_EXISTS] >> metis_tac [MAP])
 QED
 
+Theorem list_rel_flat:
+  ∀r ls l. list_rel r (flat ls) l ⇔ ∃ls2. list_rel (list_rel r) ls ls2 ∧ l = flat ls2
+Proof
+  Induct_on `ls` >> rw [LIST_REL_SPLIT1] >> eq_tac >> rw [PULL_EXISTS] >>
+  metis_tac []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound:
@@ -456,6 +463,28 @@ Proof
   full_simp_tac std_ss [w2w_def]
 QED
 
+Theorem w21_sw2sw_extend:
+  dimindex (:'b) ≤ dimindex (:'a)
+  ⇒
+  w2i (sw2sw (w :'b word) :'a word) = w2i (w : 'b word)
+Proof
+  rw [] >>
+  `∃j. INT_MIN (:'b) ≤ j ∧ j ≤ INT_MAX (:'b) ∧ w = i2w j` by metis_tac [ranged_int_word_nchotomy] >>
+  rw [sw2sw_i2w] >>
+  `INT_MIN (:'a) ≤ j ∧ j ≤ INT_MAX (:'a)`
+  by (
+    fs [INT_MIN_def, INT_MAX_def] >>
+    `2 ** (dimindex (:'b) - 1) ≤ 2 ** (dimindex (:'a) - 1)`
+    by rw [EXP_BASE_LE_IFF] >>
+    qmatch_assum_abbrev_tac `b ≤ a` >>
+    rw []
+    >- intLib.COOPER_TAC >>
+    `&(b - 1) ≤ &(a - 1)` by intLib.COOPER_TAC >>
+    full_simp_tac bool_ss [GSYM INT_LE] >>
+    intLib.COOPER_TAC) >>
+  rw [w2i_i2w]
+QED
+
 (* ----- Theorems about lazy lists ----- *)
 
 Theorem toList_some: