From 9f0fdd3bfeedf456ab652539b9b45b12bb9d42fd Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Thu, 24 Oct 2019 05:55:58 -0700
Subject: [PATCH] [sledge sem] Add proof of bit cast implementation

Summary:
Add some theorems establishing the correspondence between the
implementation of the Convert operation in OCaml and the definition of
Convert in the semantics. Essentially, the OCaml version is in terms of
extracting certain ranges of bits, whereas the semantics is in terms of
integer arithmetic (addition, modulus, and exponentiation)

Reviewed By: jberdine

Differential Revision: D18113878

fbshipit-source-id: c318596d0
---
 sledge/semantics/llairScript.sml              |   6 +-
 sledge/semantics/llair_propScript.sml         | 178 ++++++++++++++++++
 sledge/semantics/llvm_to_llairScript.sml      |   2 +-
 sledge/semantics/llvm_to_llair_propScript.sml |   2 +-
 sledge/semantics/miscScript.sml               |  29 +++
 5 files changed, 212 insertions(+), 5 deletions(-)

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: