diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-23 15:32:22 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-23 15:32:22 -0400 |
commit | b0c64e3f384f30ab6515574a23ae85d8ad0e9ae2 (patch) | |
tree | 7356fd21f96036bd8f276ac5f1b9cc9a8ec9d60a /src/Util | |
parent | bbd4cc11aa335eb4e831c75755effca8c5782e40 (diff) |
Prove more things in WordUtil
The proofs should be automated eventually...
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/WordUtil.v | 79 |
1 files changed, 77 insertions, 2 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index f73d9fccc..9aa529383 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -128,13 +128,88 @@ Proof. rewrite wordToNat_cast_word, wordToNat_combine, wordToNat_wzero; nia. Qed. +Lemma bitwp_combine {a b} f (x x' : word a) (y y' : word b) + : bitwp f x x' ++ bitwp f y y' = bitwp f (x ++ y) (x' ++ y'). +Proof. + revert x' y y'. + induction x as [|b' n x IHx]; simpl. + { intro x'; intros. + refine match x' with + | WO => _ + | _ => I + end. + reflexivity. } + { intros; rewrite IHx; clear IHx; revert x. + refine match x' in word Sn return match Sn return word Sn -> _ with + | 0 => fun _ => True + | S _ => fun x' => forall x, WS (f b' (whd x')) (bitwp f (x ++ y) (wtl x' ++ y')) = WS (f b' (whd (x' ++ y'))) (bitwp f (x ++ y) (wtl (x' ++ y'))) + end x' + with + | WO => I + | WS _ _ _ => fun _ => Logic.eq_refl + end. } +Qed. + +Lemma wand_combine {a b} (x : word a) (y : word b) (z : word (a + b)) + : (x ++ y) ^& z = ((x ^& split1 _ _ z) ++ (y ^& split2 _ _ z)). +Proof. + rewrite <- (combine_split _ _ z) at 1. + unfold wand. + rewrite bitwp_combine. + reflexivity. +Qed. + Lemma wordToNat_clearlow {b} (c : nat) (x : Word.word b) : wordToNat (clearlow c x) = wordToNat x - (wordToNat x) mod (2^c). -Admitted. +Proof. + assert (2^c <> 0) by auto with arith. + unfold clearlow. + match goal with + | [ |- context[@cast_word _ _ ?pf ?w] ] + => generalize pf + end. + intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl. + rewrite <- (combine_split _ _ x) at 2 3. + rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero. + generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl. + apply Min.min_case_strong; intros Hbc x0 x1; + pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1); + rewrite pow2_id in *. + { assert (b - c = 0) by omega. + assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. + generalize dependent (b - c); intros; destruct x0; try omega. + simpl; rewrite mul_0_r, add_0_r. + rewrite mod_small by omega. + omega. } + { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega. + lia. } +Qed. Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) : wordToNat (keeplow c x) = (wordToNat x) mod (2^c). -Admitted. +Proof. + assert (2^c <> 0) by auto with arith. + unfold keeplow. + match goal with + | [ |- context[@cast_word _ _ ?pf ?w] ] + => generalize pf + end. + intro H'; revert x; destruct H'; intro x; rewrite cast_word_refl. + rewrite <- (combine_split _ _ x) at 2 3. + rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero. + generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl. + apply Min.min_case_strong; intros Hbc x0 x1; + pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1); + rewrite pow2_id in *. + { assert (b - c = 0) by omega. + assert (2^b <= 2^c) by auto using pow_le_mono_r with arith. + generalize dependent (b - c); intros; destruct x0; try omega. + simpl; rewrite mul_0_r, add_0_r. + rewrite mod_small by omega. + omega. } + { rewrite !(mul_comm (2^c)), mod_add, mod_small by omega. + lia. } +Qed. Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a). Proof. |