diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 12:04:38 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 12:04:38 -0400 |
| commit | ddf6a123256be3a97831a4cc83f846a82d227a5a (patch) | |
| tree | 0f441af77065f104869e068d4256b8fd188c0ab0 | |
| parent | ef6b158b511abfe004d23e0b7faab074e281f4da (diff) | |
git rm -rf src/Assembly
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | _CoqProject | 16 | ||||
| -rw-r--r-- | src/Assembly/Bounds.v | 515 | ||||
| -rw-r--r-- | src/Assembly/Compile.v | 299 | ||||
| -rw-r--r-- | src/Assembly/Conversions.v | 458 | ||||
| -rw-r--r-- | src/Assembly/Evaluables.v | 782 | ||||
| -rw-r--r-- | src/Assembly/GF25519.v | 313 | ||||
| -rw-r--r-- | src/Assembly/HL.v | 212 | ||||
| -rw-r--r-- | src/Assembly/LL.v | 180 | ||||
| -rw-r--r-- | src/Assembly/Output.ml | 14 | ||||
| -rw-r--r-- | src/Assembly/PhoasCommon.v | 42 | ||||
| -rw-r--r-- | src/Assembly/Pipeline.v | 140 | ||||
| -rw-r--r-- | src/Assembly/Qhasm.v | 81 | ||||
| -rw-r--r-- | src/Assembly/QhasmCommon.v | 149 | ||||
| -rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 299 | ||||
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 91 | ||||
| -rw-r--r-- | src/Assembly/State.v | 331 | ||||
| -rw-r--r-- | src/Assembly/StringConversion.v | 367 | ||||
| -rw-r--r-- | src/Assembly/WordizeUtil.v | 996 |
19 files changed, 1 insertions, 5286 deletions
@@ -1,6 +1,6 @@ [](https://travis-ci.org/mit-plv/fiat-crypto) -Fiat-Crypto: Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives +Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives ----- NOTE: The github.com repo is only intermittently synced with diff --git a/_CoqProject b/_CoqProject index 694f80648..cc1272093 100644 --- a/_CoqProject +++ b/_CoqProject @@ -22,22 +22,6 @@ src/Algebra/IntegralDomain.v src/Algebra/Monoid.v src/Algebra/Ring.v src/Algebra/ScalarMult.v -src/Assembly/Bounds.v -src/Assembly/Compile.v -src/Assembly/Conversions.v -src/Assembly/Evaluables.v -src/Assembly/GF25519.v -src/Assembly/HL.v -src/Assembly/LL.v -src/Assembly/PhoasCommon.v -src/Assembly/Pipeline.v -src/Assembly/Qhasm.v -src/Assembly/QhasmCommon.v -src/Assembly/QhasmEvalCommon.v -src/Assembly/QhasmUtil.v -src/Assembly/State.v -src/Assembly/StringConversion.v -src/Assembly/WordizeUtil.v src/BoundedArithmetic/ArchitectureToZLike.v src/BoundedArithmetic/ArchitectureToZLikeProofs.v src/BoundedArithmetic/Eta.v diff --git a/src/Assembly/Bounds.v b/src/Assembly/Bounds.v deleted file mode 100644 index 3064f840c..000000000 --- a/src/Assembly/Bounds.v +++ /dev/null @@ -1,515 +0,0 @@ -Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec Ndigits. -Require Import Compare_dec Omega. -Require Import FunctionalExtensionality ProofIrrelevance. -Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.WordizeUtil. - -Import EvalUtil. - -Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add - Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N. - -Open Scope nword_scope. - -Section Bounds. - Lemma wordize_plus': forall {n} (x y: word n) (b: N), - (&x < b)%N - -> (&y < (Npow2 n - b))%N - -> (b <= Npow2 n)%N - -> (&x + &y)%N = & (x ^+ y). - Proof. - intros. - unfold wplus, wordBin. - rewrite wordToN_NToWord; intuition. - apply (N.lt_le_trans _ (b + &y)%N _). - - - apply N.add_lt_le_mono; try assumption. - apply N.eq_le_incl; reflexivity. - - - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega; - replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by ( - replace (b + (Npow2 n - b))%N with ((Npow2 n - b) + b)%N by nomega; - rewrite (N.sub_add b (Npow2 n)) by assumption; - nomega). - - apply N.add_le_mono_l; try nomega. - apply N.lt_le_incl; assumption. - Qed. - - Lemma wordize_mult': forall {n} (x y: word n) (b: N), - (1 < n)%nat -> (0 < b)%N - -> (&x < b)%N - -> (&y < (Npow2 n) / b)%N - -> (&x * &y)%N = & (x ^* y). - Proof. - intros; unfold wmult, wordBin. - rewrite wordToN_NToWord; intuition. - apply (N.lt_le_trans _ (b * ((Npow2 n) / b))%N _). - - - apply N.mul_lt_mono; assumption. - - - apply N.mul_div_le; nomega. - Qed. - - Lemma constant_bound_N : forall {n} (k: word n), - (& k < & k + 1)%N. - Proof. intros; nomega. Qed. - - Lemma constant_bound_nat : forall (n k: nat), - (N.of_nat k < Npow2 n)%N - -> (& (@natToWord n k) < (N.of_nat k) + 1)%N. - Proof. - intros. - rewrite wordToN_nat. - rewrite wordToNat_natToWord_idempotent; - try assumption; nomega. - Qed. - - Lemma let_bound : forall {n} (x: word n) (f: word n -> word n) xb fb, - (& x < xb)%N - -> (forall x', & x' < xb -> & (f x') < fb)%N - -> ((let k := x in &(f k)) < fb)%N. - Proof. intros; eauto. Qed. - - Definition Nlt_dec (x y: N): {(x < y)%N} + {(x >= y)%N}. - refine ( - let c := N.compare x y in - match c as c' return c = c' -> _ with - | Lt => fun _ => left _ - | _ => fun _ => right _ - end eq_refl); - abstract ( - unfold c, N.ge, N.lt in *; intuition; subst; - match goal with - | [H0: ?x = _, H1: ?x = _ |- _] => - rewrite H0 in H1; inversion H1 - end). - Defined. - - Lemma wplus_bound : forall {n} (w1 w2 : word n) b1 b2, - (&w1 < b1)%N - -> (&w2 < b2)%N - -> (&(w1 ^+ w2) < b1 + b2)%N. - Proof. - intros. - - destruct (Nlt_dec (b1 + b2)%N (Npow2 n)) as [g|g]. - - - rewrite <- wordize_plus' with (b := b1); - try apply N.add_lt_mono; - try assumption. - - + apply (N.lt_le_trans _ b2 _); try assumption. - apply N.lt_le_incl. - apply N.lt_add_lt_sub_l. - assumption. - - + apply N.lt_le_incl; nomega. - - - apply (N.lt_le_trans _ (Npow2 n) _). - - + apply word_size_bound. - - + unfold N.le, N.ge in *. - intro Hg. - contradict g. - rewrite N.compare_antisym. - rewrite Hg. - simpl; intuition. - Qed. - - Theorem wmult_bound : forall {n} (w1 w2 : word n) b1 b2, - (1 < n)%nat - -> (&w1 < b1)%N - -> (&w2 < b2)%N - -> (&(w1 ^* w2) < b1 * b2)%N. - Proof. - intros. - destruct (Nlt_dec (b1 * b2)%N (Npow2 n)) as [g|g]. - - - rewrite <- wordize_mult' with (b := b1); - try apply N.mul_lt_mono; - try assumption; - try nomega. - - apply (N.lt_le_trans _ b2 _); try assumption. - apply N.div_le_lower_bound. - - + induction (& w1); nomega. - - + apply N.lt_le_incl. - assumption. - - - apply (N.lt_le_trans _ (Npow2 n) _). - - + apply word_size_bound. - - + unfold N.le, N.ge in *. - intro Hg. - contradict g. - rewrite N.compare_antisym. - rewrite Hg. - simpl; intuition. - Qed. - - Lemma wminus_bound: forall {n} (x y: word n) low0 high0 low1 high1, - (low0 <= wordToN x)%N -> (wordToN x <= high0)%N - -> (low1 <= wordToN y)%N -> (wordToN y <= high1)%N - -> (&x >= &y)%N -> (& (x ^- y) <= high0 - low1)%N. - Proof. - intros. - - destruct (Nge_dec 0%N (&y)). { - unfold wminus, wneg. - replace (& y) with 0%N in * by nomega. - replace low1 with 0%N by (symmetry; apply N.le_0_r; assumption). - replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N - by (rewrite wordToN_zero; nomega). - rewrite <- Npow2_ignore. - rewrite wplus_comm. - rewrite wplus_unit. - replace (high0 - 0)%N with high0 by nomega; assumption. - } - - assert (& x - & y < Npow2 n)%N. { - transitivity (wordToN x); - try apply word_size_bound; - apply N.sub_lt; - [apply N.ge_le|]; assumption. - } - - assert (& x - & y + & y < Npow2 n)%N. { - replace (& x - & y + & y)%N - with (wordToN x) by nomega; - apply word_size_bound. - } - - assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. { - apply NToWord_equal. - rewrite <- wordize_plus; rewrite wordToN_NToWord; try assumption. - nomega. - } - - rewrite Hv. - unfold wminus. - rewrite <- wplus_assoc. - rewrite wminus_inv. - rewrite wplus_comm. - rewrite wplus_unit. - rewrite wordToN_NToWord; try assumption. - - transitivity (high0 - & y)%N; - [apply N.sub_le_mono_r | apply N.sub_le_mono_l]; - assumption. - Qed. - - Lemma shiftr_bound : forall {n} (w : word n) b bits, - (&w < b)%N - -> (&(shiftr w bits) < N.succ (N.shiftr_nat b bits))%N. - Proof. - intros. - apply (N.le_lt_trans _ (N.shiftr_nat b bits) _). - - - unfold shiftr, extend, high. - destruct (le_dec bits n); try omega. - - + rewrite wordToN_convS. - rewrite wordToN_zext. - rewrite wordToN_split2. - rewrite wordToN_convS. - rewrite <- Nshiftr_equiv_nat. - repeat rewrite N.shiftr_div_pow2. - apply N.div_le_mono. - - * induction bits; try nomega. - rewrite Nat2N.inj_succ. - rewrite N.pow_succ_r'. - assert (bits <= n)%nat as Hc by omega. - apply IHbits in Hc. - intro Hc'; contradict Hc. - apply (N.mul_cancel_l _ _ 2); - try rewrite Hc'; - try assumption; - nomega. - - * apply N.lt_le_incl. - assumption. - - + rewrite wordToN_nat. - unfold wzero. - rewrite wordToNat_natToWord_idempotent; simpl; - try apply N_ge_0; - try apply Npow2_gt0. - - - nomega. - - Qed. - - Lemma shiftr_bound' : forall {n} (w : word n) b bits, - (&w <= b)%N - -> (&(shiftr w bits) <= N.shiftr_nat b bits)%N. - Proof. - intros. - transitivity (N.shiftr_nat b bits). - - - unfold shiftr, extend, high. - destruct (le_dec bits n); try omega. - - + rewrite wordToN_convS. - rewrite wordToN_zext. - rewrite wordToN_split2. - rewrite wordToN_convS. - rewrite <- Nshiftr_equiv_nat. - repeat rewrite N.shiftr_div_pow2. - apply N.div_le_mono; [|assumption]. - - induction bits; try nomega. - rewrite Nat2N.inj_succ. - rewrite N.pow_succ_r'. - assert (bits <= n)%nat as Hc by omega. - apply IHbits in Hc. - intro Hc'; contradict Hc. - apply (N.mul_cancel_l _ _ 2); - try rewrite Hc'; - try assumption; - nomega. - - + rewrite wordToN_nat. - unfold wzero. - rewrite wordToNat_natToWord_idempotent; simpl; - try apply N_ge_0; - try apply Npow2_gt0. - - - apply N.eq_le_incl; reflexivity. - Qed. - - Lemma mask_bound : forall {n} (w : word n) m, - (&(mask m w) < Npow2 m)%N. - Proof. - intros. - unfold mask in *; destruct (le_dec m n); simpl; - try apply extend_bound. - - pose proof (word_size_bound w) as H. - apply (N.le_lt_trans _ (Npow2 n) _). - - - unfold N.le, N.lt in *; rewrite H; intro H0; inversion H0. - - - clear H. - replace m with ((m - n) + n) by nomega. - replace (Npow2 n) with (1 * (Npow2 n))%N - by (rewrite N.mul_comm; nomega). - rewrite Npow2_split. - apply N.mul_lt_mono_pos_r; try apply Npow2_gt0. - assert (0 < m - n)%nat by omega. - induction (m - n); try inversion H; try abstract ( - simpl; replace 2 with (S 1) by omega; - apply N.lt_1_2); subst. - - assert (0 < n1)%nat as Z by omega; apply IHn1 in Z. - apply (N.le_lt_trans _ (Npow2 n1) _). - - + apply N.lt_le_incl; assumption. - - + rewrite Npow2_succ. - replace' (Npow2 n1) with (1 * Npow2 n1)%N at 1 by (apply N.mul_1_l). - apply N.mul_lt_mono_pos_r; try abstract (vm_compute; reflexivity). - apply (N.lt_le_trans _ 1 _); try abstract (vm_compute; reflexivity). - apply N.lt_le_incl; assumption. - Qed. - - Lemma mask_update_bound : forall {n} (w : word n) b m, - (1 < n)%nat - -> (&w < b)%N - -> (&(mask m w) < (N.min b (Npow2 m)))%N. - Proof. - intros. - assert (& w mod Npow2 m < b)%N. { - destruct (Nge_dec (&w) (Npow2 m)). - - - apply (N.lt_le_trans _ (Npow2 m) _). - - + pose proof (N.mod_bound_pos (&w) (Npow2 m) - (N_ge_0 _) (Npow2_gt0 _)) as H1. - destruct H1. - assumption. - - + transitivity (&w); try abstract (apply ge_to_le; assumption). - apply N.lt_le_incl; assumption. - - - rewrite N.mod_small; assumption. - } - - unfold mask, N.min, extend, low; - destruct (le_dec m n), - (N.compare b (Npow2 m)); simpl; - repeat first [ - rewrite wordToN_convS | - rewrite wordToN_zext | - rewrite wordToN_wones | - rewrite wordToN_split1 | - rewrite N.land_ones | - rewrite <- Npow2_N ]; - try assumption. - - - pose proof (N.mod_bound_pos (&w) (Npow2 m) (N_ge_0 _) (Npow2_gt0 _)) as Z. - destruct Z. - assumption. - - - apply (N.lt_le_trans _ (Npow2 n) _); - try apply word_size_bound. - apply Npow2_ordered. - omega. - Qed. - - Lemma plus_overflow_bound: forall x y a b, - (x < a)%N - -> (y < b - a)%N - -> (x + y < b)%N. - Proof. intros; nomega. Qed. - -End Bounds. - -(** Constant Tactics **) - -Ltac assert_nat_constant t := - timeout 1 (match (eval vm_compute in t) with - | O => idtac - | S ?n => assert_nat_constant n - | _ => fail - end). - -Ltac assert_pos_constant t := - timeout 1 (match (eval vm_compute in t) with - | xH => idtac - | xI ?p => assert_pos_constant p - | xO ?p => assert_pos_constant p - | _ => fail - end). - -Ltac assert_bin_constant t := - timeout 1 (match (eval vm_compute in t) with - | N.pos ?p => assert_pos_constant p - | N0 => idtac - | _ => fail - end). - -Ltac assert_word_constant t := - timeout 1 (match (eval vm_compute in t) with - | WO => idtac - | WS _ ?w => assert_word_constant w - | _ => fail - end). - -(** Bounding Tactics **) - -Ltac multi_apply0 A L := pose proof (L A). - -Ltac multi_apply1 A L := - match goal with - | [ H: (wordToN A < ?b)%N |- _] => pose proof (L A b H) - end. - -Ltac multi_apply2 A B L := - match goal with - | [ H1: (wordToN A < ?b1)%N, H2: (wordToN B < ?b2)%N |- _] => pose proof (L A B b1 b2 H1 H2) - end. - -Ltac multi_recurse n T := - match goal with - | [ H: (wordToN T < _)%N |- _] => idtac - | _ => - is_var T; - let T' := (eval cbv delta [T] in T) in multi_recurse n T'; - match goal with - | [ H : T' < ?x |- _ ] => - pose proof (H : T < x) - end - - | _ => - match T with - | ?W1 ^+ ?W2 => - multi_recurse n W1; multi_recurse n W2; - multi_apply2 W1 W2 (@wplus_bound n) - - | ?W1 ^* ?W2 => - multi_recurse n W1; multi_recurse n W2; - multi_apply2 W1 W2 (@wmult_bound n) - - | mask ?m ?w => - multi_recurse n w; - multi_apply1 w (fun b => @mask_update_bound n w b) - - | mask ?m ?w => - multi_recurse n w; - pose proof (@mask_bound n w m) - - | shiftr ?w ?bits => - multi_recurse n w; - match goal with - | [ H: (w < ?b)%N |- _] => - pose proof (@shiftr_bound n w b bits H) - end - - | NToWord _ ?k => pose proof (@constant_bound_N n k) - | natToWord _ ?k => pose proof (@constant_bound_nat n k) - | _ => pose proof (@word_size_bound n T) - end - end. - -Lemma unwrap_let: forall {n} (y: word n) (f: word n -> word n) (b: N), - (&(let x := y in f x) < b)%N <-> let x := y in (&(f x) < b)%N. -Proof. intuition. Qed. - -Ltac bound_compute := - repeat (try assumption; match goal with - | [|- let A := ?B in _] => - match (type of B) with - | word ?n => multi_recurse n B; intro - end - - | [|- ((let A := _ in _) < _)%N] => - apply unwrap_let - - | [ H: (wordToN ?W < ?b0)%N |- (wordToN ?W < ?b1)%N ] => - try eassumption; eapply (N.lt_le_trans _ b0 _); try eassumption - - | [|- (@wordToN ?n ?W < ?b)%N ] => - multi_recurse n W - - | [|- (?x + ?y < ?b)%N ] => - eapply plus_overflow_bound - - | [|- (?a <= ?b)%N ] => - is_evar b; apply N.eq_le_incl; reflexivity - - | [|- (?a <= ?b)%N ] => - is_evar a; apply N.eq_le_incl; reflexivity - - | [|- (?a <= ?b)%N ] => - assert_bin_constant a; - assert_bin_constant b; - vm_compute; - try reflexivity; - try abstract (let H := fresh in intro H; inversion H) - - | [|- (?x < ?b)%N ] => - assert_bin_constant x; - assert_bin_constant b; - vm_compute; reflexivity - - (* cleanup generated nat goals *) - | [|- (?a <= ?b)%nat ] => omega - | [|- (?a < ?b)%nat ] => omega - end). - -(* for x : word n *) -Ltac find_bound_on x := - match (type of x) with - | word ?n => - match x with - | let A := ?b in ?c => find_bound_on b; set (A := b) - | _ => multi_recurse n x - end - | _ => idtac - end. diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v deleted file mode 100644 index e9300ff0f..000000000 --- a/src/Assembly/Compile.v +++ /dev/null @@ -1,299 +0,0 @@ -Require Import Coq.Logic.Eqdep. -Require Import Coq.Arith.Compare_dec Coq.Bool.Sumbool. -Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. - -Require Import Crypto.Assembly.PhoasCommon. -Require Import Crypto.Assembly.HL. -Require Import Crypto.Assembly.LL. -Require Import Crypto.Assembly.QhasmEvalCommon. -Require Import Crypto.Assembly.QhasmCommon. -Require Import Crypto.Assembly.Qhasm. - -Local Arguments LetIn.Let_In _ _ _ _ / . - -Module CompileHL. - Section Compilation. - Context {T: Type}. - - Fixpoint compile {T t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t := - match e with - | HL.Const _ n => LL.Return (LL.Const n) - - | HL.Var _ arg => LL.Return arg - - | HL.Binop t1 t2 t3 op e1 e2 => - LL.under_lets (compile e1) (fun arg1 => - LL.under_lets (compile e2) (fun arg2 => - LL.LetBinop op arg1 arg2 (fun v => - LL.Return v))) - - | HL.Let _ ex _ eC => - LL.under_lets (compile ex) (fun arg => - compile (eC arg)) - - | HL.Pair t1 e1 t2 e2 => - LL.under_lets (compile e1) (fun arg1 => - LL.under_lets (compile e2) (fun arg2 => - LL.Return (LL.Pair arg1 arg2))) - - | HL.MatchPair _ _ ep _ eC => - LL.under_lets (compile ep) (fun arg => - let (a1, a2) := LL.match_arg_Prod arg in - compile (eC a1 a2)) - end. - - Definition Compile {T t} (e:@HL.Expr T t) : @LL.expr T T t := - compile (e (@LL.arg T T)). - End Compilation. - - Section Correctness. - Context {T: Type}. - - Lemma compile_correct {_: Evaluable T} {t} e1 e2 G (wf:HL.wf G e1 e2) : - List.Forall (fun v => let 'existT _ (x, a) := v in LL.interp_arg a = x) G -> - LL.interp (compile e2) = HL.interp e1 :> interp_type t. - Proof using Type. - induction wf; - repeat match goal with - | [HIn:In ?x ?l, HForall:Forall _ ?l |- _ ] => - (pose proof (proj1 (Forall_forall _ _) HForall _ HIn); clear HIn) - | [ H : LL.match_arg_Prod _ = (_, _) |- _ ] => - apply LL.match_arg_Prod_correct in H - | [ H : LL.Pair _ _ = LL.Pair _ _ |- _ ] => - apply LL.Pair_eq in H - | [ H : (_, _) = (_, _) |- _ ] => inversion H; clear H - | _ => progress intros - | _ => progress simpl in * - | _ => progress subst - | _ => progress specialize_by assumption - | _ => progress break_match - | _ => rewrite !LL.interp_under_lets - | _ => rewrite !LL.interp_arg_uninterp_arg - | _ => progress erewrite_hyp !* - | _ => apply Forall_cons - | _ => solve [intuition (congruence || eauto)] - end. - Qed. - End Correctness. -End CompileHL. - -Module CompileLL. - Import LL Qhasm. - Import QhasmUtil ListNotations. - - Section Compile. - Context {n: nat} {w: Width n}. - - Definition WArg t': Type := @LL.arg (word n) (word n) t'. - Definition WExpr t': Type := @LL.expr (word n) (word n) t'. - - Section Mappings. - Definition indexize (x: nat) : Index n. - intros; destruct (le_dec n 0). - - - exists 0; abstract intuition auto with zarith. - - exists (x mod n)%nat. - abstract (pose proof (Nat.mod_bound_pos x n); - omega). - Defined. - - Definition getMapping (x: WArg TT) := - match x with - | Const v => constM n (@constant n w v) - | Var v => regM n (@reg n w (wordToNat v)) - end. - - Definition getReg (x: Mapping n): option (Reg n) := - match x with | regM r => Some r | _ => None end. - - Definition getConst (x: Mapping n): option (QhasmCommon.Const n) := - match x with | constM c => Some c | _ => None end. - - Definition makeA (output input: Mapping n): list Assignment := - match (output, input) with - | (regM r, constM c) => [AConstInt r c] - | (regM r0, regM r1) => [ARegReg r0 r1] - | _ => [] - end. - - Definition makeOp {t1 t2 t3} (op: binop t1 t2 t3) (tmp out: Reg n) (in1 in2: Mapping n): - option (Reg n * list Assignment * Operation) := - let mov := - if (EvalUtil.mapping_dec (regM _ out) in1) - then [] - else makeA (regM _ out) in1 in - - match op with - | OPadd => - match in2 with - | regM r1 => Some (out, mov, IOpReg IAdd out r1) - | constM c => Some (out, mov, IOpConst IAdd out c) - | _ => None - end - - | OPsub => - match in2 with - | regM r1 => Some (out, mov, IOpReg ISub out r1) - | constM c => Some (out, mov, IOpConst ISub out c) - | _ => None - end - - | OPmul => - match in2 with - | regM r1 => Some (out, mov, DOp Mult out r1 None) - | constM c => Some (out, mov ++ (makeA (regM _ tmp) in2), DOp Mult out tmp None) - | _ => None - end - - | OPand => - match in2 with - | regM r1 => Some (out, mov, IOpReg IAnd out r1) - | constM c => Some (out, mov, IOpConst IAnd out c) - | _ => None - end - - | OPshiftr => - match in2 with - | constM (constant _ _ w) => - Some (out, mov, ROp Shr out (indexize (wordToNat w))) - | _ => None - end - end. - - End Mappings. - - Section TypeDec. - Fixpoint type_eqb (t0 t1: type): bool := - match (t0, t1) with - | (TT, TT) => true - | (Prod t0a t0b, Prod t1a t1b) => andb (type_eqb t0a t1a) (type_eqb t0b t1b) - | _ => false - end. - - Lemma type_eqb_spec: forall t0 t1, type_eqb t0 t1 = true <-> t0 = t1. - Proof using Type. - intros; split. - - - revert t1; induction t0 as [|t0a IHt0a t0b IHt0b]. - - + induction t1; intro H; simpl in H; inversion H; reflexivity. - - + induction t1; intro H; simpl in H; inversion H. - apply andb_true_iff in H; destruct H as [Ha Hb]. - - apply IHt0a in Ha; apply IHt0b in Hb; subst. - reflexivity. - - - intro H; subst. - induction t1; simpl; [reflexivity|]; apply andb_true_iff; intuition. - Qed. - - Definition type_dec (t0 t1: type): {t0 = t1} + {t0 <> t1}. - refine (match (type_eqb t0 t1) as b return _ = b -> _ with - | true => fun e => left _ - | false => fun e => right _ - end eq_refl); - [ abstract (apply type_eqb_spec in e; assumption) - | abstract (intro H; apply type_eqb_spec in H; - rewrite e in H; contradict H; intro C; inversion C) ]. - Defined. - End TypeDec. - - Fixpoint vars {t} (a: WArg t): list nat := - match t as t' return WArg t' -> list nat with - | TT => fun a' => - match a' with - | Var v' => [wordToNat v'] - | _ => @nil nat - end - | Prod t0 t1 => fun a' => - match a' with - | Pair _ _ a0 a1 => (vars a0) ++ (vars a1) - | _ => I (* dummy *) - end - end a. - - Definition getOutputSlot (nextReg: nat) - (op: binop TT TT TT) (x: WArg TT) (y: WArg TT) : option nat := - match (makeOp op (reg w nextReg) (reg w (S nextReg)) (getMapping x) (getMapping y)) with - | Some (reg _ _ r, _ , _) => Some r - | _ => None - end. - - Section ExprF. - Context (Out: Type) - (update: Reg n -> WArg TT -> binop TT TT TT -> WArg TT -> WArg TT -> Out -> option Out) - (get: forall t', WArg t' -> option Out). - - Definition opToTT {t1 t2 t3} (op: binop t1 t2 t3): option (binop TT TT TT) := - match op with - | OPadd => Some OPadd - | OPsub => Some OPsub - | OPmul => Some OPmul - | OPand => Some OPand - | OPshiftr => Some OPshiftr - end. - - Definition argToTT {t} (a: WArg t): option (WArg TT) := - match t as t' return WArg t' -> _ with - | TT => fun a' => Some a' - | _ => fun a' => None - end a. - - Fixpoint zeros (t: type): WArg t := - match t with - | TT => Const (@wzero n) - | Prod t0 t1 => Pair (zeros t0) (zeros t1) - end. - - Fixpoint exprF {t} (nextRegName: nat) (p: WExpr t) {struct p}: option Out := - match p with - | LetBinop t1 t2 t3 op x y t' eC => - omap (opToTT op) (fun op' => - omap (argToTT x) (fun x' => - omap (argToTT y) (fun y' => - omap (getOutputSlot nextRegName op' x' y') (fun r => - let var := - match t3 as t3' return WArg t3' with - | TT => Var (natToWord _ r) - | _ => zeros _ - end in - - omap (exprF (S (S nextRegName)) (eC var)) (fun out => - omap (argToTT var) (fun var' => - update (reg w nextRegName) var' op' x' y' out)))))) - | Return _ a => get _ a - end. - End ExprF. - - Definition getProg := - @exprF Program - (fun rt var op x y out => - omap (getReg (getMapping var)) (fun rv => - match (makeOp op rt rv (getMapping x) (getMapping y)) with - | Some (reg _ _ r, a, op') => - Some ((map QAssign a) ++ ((QOp op') :: out)) - | _ => None - end)) - (fun t' a => Some []). - - Definition getOuts := - @exprF (list nat) - (fun rt var op x y out => Some out) - (fun t' a => Some (vars a)). - - Fixpoint fillInputs t inputs (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t := - match inputs as inputs' return NAry inputs' Z (WExpr t) -> NAry O Z (WExpr t) with - | O => fun p => p - | S inputs'' => fun p => @fillInputs _ _ (p (Z.of_nat inputs)) - end prog. - Global Arguments fillInputs {t inputs} _. - - Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) := - let p' := fillInputs p in - - omap (getOuts _ (S inputs) p') (fun outs => - omap (getProg _ (S inputs) p') (fun prog => - Some (prog, outs))). - End Compile. -End CompileLL. diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v deleted file mode 100644 index f677b6d58..000000000 --- a/src/Assembly/Conversions.v +++ /dev/null @@ -1,458 +0,0 @@ -Require Import Crypto.Assembly.PhoasCommon. - -Require Export Crypto.Assembly.QhasmUtil. -Require Export Crypto.Assembly.QhasmEvalCommon. -Require Export Crypto.Assembly.WordizeUtil. -Require Export Crypto.Assembly.Evaluables. -Require Export Crypto.Assembly.HL. -Require Export Crypto.Assembly.LL. - -Require Export FunctionalExtensionality. - -Require Import Bedrock.Nomega. - -Require Import Coq.ZArith.ZArith_dec. -Require Import Coq.ZArith.Znat. - -Require Import Coq.NArith.Nnat Coq.NArith.Ndigits. - -Require Import Coq.Bool.Sumbool. -Require Import Coq.Program.Basics. - -Local Arguments LetIn.Let_In _ _ _ _ / . - -Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t. -Proof. - induction t; [refine (f x)|]. - destruct x as [x1 x2]. - refine (IHt1 x1, IHt2 x2). -Defined. - -Module HLConversions. - Import HL. - - Fixpoint convertExpr {A B: Type} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t := - match a with - | Const E x => Const (@toT B EB (@fromT A E x)) - | Var t x => @Var B _ t x - | Binop t1 t2 t3 o e1 e2 => - @Binop B _ t1 t2 t3 o (convertExpr e1) (convertExpr e2) - | Let tx e tC f => - Let (convertExpr e) (fun x => convertExpr (f x)) - | Pair t1 e1 t2 e2 => Pair (convertExpr e1) (convertExpr e2) - | MatchPair t1 t2 e tC f => MatchPair (convertExpr e) (fun x y => - convertExpr (f x y)) - end. -End HLConversions. - -Module LLConversions. - Import LL. - - Section VarConv. - Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - - Definition convertVar {t} (a: interp_type (T := A) t): interp_type (T := B) t. - Proof. - induction t as [| t3 IHt1 t4 IHt2]. - - - refine (@toT B EB (@fromT A EA _)); assumption. - - - destruct a as [a1 a2]; constructor; - [exact (IHt1 a1) | exact (IHt2 a2)]. - Defined. - End VarConv. - - Section ArgConv. - Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - - Fixpoint convertArg {V} t {struct t}: @arg A V t -> @arg B V t := - match t as t' return @arg A V t' -> @arg B V t' with - | TT => fun x => - match x with - | Const c => Const (convertVar (t := TT) c) - | Var v => Var v - end - | Prod t0 t1 => fun x => - match (match_arg_Prod x) with - | (a, b) => Pair ((convertArg t0) a) ((convertArg t1) b) - end - end. - End ArgConv. - - Section ExprConv. - Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - - Fixpoint convertExpr {t V} (a: @expr A V t): @expr B V t := - match a with - | LetBinop _ _ out op a b _ eC => - LetBinop (T := B) op (convertArg _ a) (convertArg _ b) (fun x: (arg out) => - convertExpr (eC (convertArg _ x))) - - | Return _ a => Return (convertArg _ a) - end. - End ExprConv. - - Section Defaults. - Context {t: type} {n: nat}. - - Definition Word := word n. - Definition Bounded := option (@BoundedWord n). - Definition RWV := option (RangeWithValue). - - Transparent Word Bounded RWV. - - Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n. - Instance ZEvaluable' : Evaluable Z := ZEvaluable. - - Existing Instance ZEvaluable'. - Existing Instance WordEvaluable. - Existing Instance BoundedEvaluable. - Existing Instance RWVEvaluable'. - - Definition ZToWord a := @convertExpr Z Word _ _ t a. - Definition ZToBounded a := @convertExpr Z Bounded _ _ t a. - Definition ZToRWV a := @convertExpr Z RWV _ _ t a. - - Definition varZToWord a := @convertVar Z Word _ _ t a. - Definition varZToBounded a := @convertVar Z Bounded _ _ t a. - Definition varZToRWV a := @convertVar Z RWV _ _ t a. - - Definition varWordToZ a := @convertVar Word Z _ _ t a. - Definition varBoundedToZ a := @convertVar Bounded Z _ _ t a. - Definition varRWVToZ a := @convertVar RWV Z _ _ t a. - - Definition zinterp E := @interp Z _ t E. - Definition wordInterp E := @interp' Word _ _ t (fun x => NToWord n (Z.to_N x)) E. - Definition boundedInterp E := @interp Bounded _ t E. - Definition rwvInterp E := @interp RWV _ t E. - - Section Operations. - Context {tx ty tz: type}. - - Definition opZ (op: binop tx ty tz) - (x: @interp_type Z tx) (y: @interp_type Z ty): @interp_type Z tz := - @interp_binop Z _ _ _ _ op x y. - - Definition opBounded (op: binop tx ty tz) - (x: @interp_type Bounded tx) (y: @interp_type Bounded ty): @interp_type Bounded tz := - @interp_binop Bounded _ _ _ _ op x y. - - - Definition opWord (op: binop tx ty tz) - (x: @interp_type Word tx) (y: @interp_type Word ty): @interp_type Word tz := - @interp_binop Word _ _ _ _ op x y. - - Definition opRWV (op: binop tx ty tz) - (x: @interp_type RWV tx) (y: @interp_type RWV ty): @interp_type RWV tz := - @interp_binop RWV _ _ _ _ op x y. - End Operations. - - Definition rangeOf := fun x => - Some (rwv 0%N (Z.to_N x) (Z.to_N x)). - - Definition ZtoB := fun x => omap (rangeOf x) (bwFromRWV (n := n)). - End Defaults. - - Section Correctness. - Context {n: nat}. - - Definition W := (word n). - Definition B := (@Bounded n). - Definition R := (option RangeWithValue). - - Instance RE : Evaluable R := @RWVEvaluable n. - Instance ZE : Evaluable Z := ZEvaluable. - Instance WE : Evaluable W := @WordEvaluable n. - Instance BE : Evaluable B := @BoundedEvaluable n. - - Transparent ZE RE WE BE W B R. - - Existing Instance ZE. - Existing Instance RE. - Existing Instance WE. - Existing Instance BE. - - Ltac kill_dec := - repeat match goal with - | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b) - | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b) - end. - - Section BoundsChecking. - Context {T: Type} {E: Evaluable T} {f : T -> B}. - - Definition getBounds {t} (e : @expr T T t): @interp_type B t := - interp' f (@convertExpr T B _ _ t _ e). - - Fixpoint bcheck' {t} (x: @interp_type B t) := - match t as t' return (interp_type t') -> bool with - | TT => fun x' => - match x' with - | Some _ => true - | None => false - end - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => andb (bcheck' x0) (bcheck' x1) - end - end x. - - Definition bcheck {t} (e : expr t): bool := bcheck' (getBounds e). - End BoundsChecking. - - Section UtilityLemmas. - Context {A B} {EA: Evaluable A} {EB: Evaluable B}. - - Lemma convertArg_interp' : forall {t V} f (x: @arg A V t), - (interp_arg' (fun z => toT (fromT (f z))) (@convertArg A B EA EB _ t x)) - = @convertVar A B EA EB t (interp_arg' f x). - Proof using Type. - intros. - induction x as [| |t0 t1 i0 i1]; simpl; [reflexivity|reflexivity|]. - induction EA, EB; simpl; f_equal; assumption. - Qed. - - Lemma convertArg_var: forall {A B EA EB t} V (x: @interp_type A t), - @convertArg A B EA EB V t (uninterp_arg x) = uninterp_arg (var := V) (@convertVar A B EA EB t x). - Proof using Type. - induction t as [|t0 IHt_0 t1 IHt_1]; simpl; intros; [reflexivity|]. - induction x as [a b]; simpl; f_equal; - induction t0 as [|t0a IHt0_0 t0b IHt0_1], - t1 as [|t1a IHt1_0]; simpl in *; - try rewrite IHt_0; - try rewrite IHt_1; - reflexivity. - Qed. - - Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e f, - bcheck (t := tz) (f := f) (LetBinop op x y e) = true - -> opZ op (interp_arg x) (interp_arg y) = - varBoundedToZ (n := n) (opBounded op - (interp_arg' f (convertArg _ x)) - (interp_arg' f (convertArg _ y))). - Proof. - Admitted. - - Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e f, - bcheck (t := tz) (f := f) (LetBinop op x y e) = true - -> opZ op (interp_arg x) (interp_arg y) = - varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))). - Proof. - Admitted. - - Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None. - Proof using Type. - intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV; - simpl; try break_match; simpl; try abstract (intro Z; inversion Z); - pose proof (Npow2_gt0 n); simpl in *; nomega. - Qed. - - Lemma double_conv_var: forall t x, - @convertVar R Z _ _ t (@convertVar B R _ _ t x) = - @convertVar B Z _ _ t x. - Proof. - intros. - Admitted. - - Lemma double_conv_arg: forall V t a, - @convertArg R B _ _ V t (@convertArg Z R _ _ V t a) = - @convertArg Z B _ _ V t a. - Proof. - intros. - Admitted. - End UtilityLemmas. - - - Section Spec. - Ltac kill_just n := - match goal with - | [|- context[just ?x] ] => - let Hvalue := fresh in let Hvalue' := fresh in - let Hlow := fresh in let Hlow' := fresh in - let Hhigh := fresh in let Hhigh' := fresh in - let Hnone := fresh in let Hnone' := fresh in - - let B := fresh in - - pose proof (just_value_spec (n := n) x) as Hvalue; - pose proof (just_low_spec (n := n) x) as Hlow; - pose proof (just_high_spec (n := n) x) as Hhigh; - pose proof (just_None_spec (n := n) x) as Hnone; - - destruct (just x); - - try pose proof (Hlow _ eq_refl) as Hlow'; - try pose proof (Hvalue _ eq_refl) as Hvalue'; - try pose proof (Hhigh _ eq_refl) as Hhigh'; - try pose proof (Hnone eq_refl) as Hnone'; - - clear Hlow Hhigh Hvalue Hnone - end. - - Lemma RangeInterp_bounded_spec: forall {t} (E: @expr Z Z t), - bcheck (f := ZtoB) E = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (ZToWord _ E). - Proof. - intros t E S. - unfold zinterp, ZToWord, wordInterp. - - induction E as [tx ty tz op x y z|]; simpl; try reflexivity. - - - repeat rewrite convertArg_var in *. - repeat rewrite convertArg_interp in *. - - rewrite H; clear H; repeat f_equal. - - + pose proof (ZToWord_binop_correct op x y) as C; - unfold opZ, opWord, varWordToZ, varZToWord in C; - simpl in C. - - assert (N.pred (Npow2 n) >= 0)%N. { - apply N.le_ge. - rewrite <- (N.pred_succ 0). - apply N.le_pred_le_succ. - rewrite N.succ_pred; [| apply N.neq_0_lt_0; apply Npow2_gt0]. - apply N.le_succ_l. - apply Npow2_gt0. - } - - admit. (* - induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C; - unfold bcheck, getBounds, boundedInterp, bwFromRWV in *; simpl in *; - kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *) - - + unfold bcheck, getBounds in *. - replace (interp_binop op (interp_arg x) (interp_arg y)) - with (varBoundedToZ (n := n) (opBounded op - (interp_arg' ZtoB (convertArg _ x)) - (interp_arg' ZtoB (convertArg _ y)))). - - * rewrite <- S; f_equal; clear S. - simpl; repeat f_equal. - unfold varBoundedToZ, opBounded. - repeat rewrite convertArg_var. - Arguments convertArg _ _ _ _ _ _ _ : clear implicits. - admit. - - * pose proof (ZToBounded_binop_correct op x y) as C; - unfold opZ, opWord, varZToBounded, - varBoundedToZ in *; - simpl in C. - - Local Opaque toT fromT. - - induction op; erewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity; - unfold bcheck, getBounds; simpl; - pose proof roundTrip_0 as H; - induction (toT (fromT _)); first [reflexivity|contradict H; reflexivity]. - - Local Transparent toT fromT. - - - simpl in S. - induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity. - admit. - - (* - + f_equal. - unfold bcheck, getBounds, boundedInterp in S; simpl in S. - kill_dec; simpl; [reflexivity|simpl in S; inversion S]. - - + f_equal. - unfold bcheck, getBounds, boundedInterp, boundVarInterp in S; simpl in S; - kill_dec; simpl; try reflexivity; try nomega. - inversion S. - admit. - admit. - - + unfold bcheck in S; simpl in S; - apply andb_true_iff in S; destruct S as [S0 S1]; - rewrite IHa0, IHa1; [reflexivity| |]; - unfold bcheck, getBounds; simpl; assumption. *) - Admitted. - End Spec. - - Section RWVSpec. - Section Defs. - Context {V} {f : V -> R}. - - Definition getRanges {t} (e : @expr R V t): @interp_type (option (Range N)) t := - typeMap (option_map rwvToRange) (interp' f e). - - Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := - match t as t' return (interp_type t') -> bool with - | TT => fun x' => orElse false (option_map (checkRWV (n := n)) x') - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => andb (check' x0) (check' x1) - end - end x. - - Definition check {t} (e : @expr R V t): bool := check' (interp' f e). - End Defs. - - Ltac kill_dec := - repeat match goal with - | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b) - | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b) - end. - - Lemma check_spec' : forall {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) x y, - @convertVar B R _ _ TT ( - omap (interp_arg' ZtoB (convertArg TT x)) (fun X => - omap (interp_arg' ZtoB (convertArg TT y)) (fun Y => - bapp op X Y))) = - omap (interp_arg' rangeOf x) (fun X => - omap (interp_arg' rangeOf y) (fun Y => - rwv_app (n := n) op X Y)). - Proof. - Admitted. - - Lemma check_spec: forall {t} (E: @expr Z Z t), - check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true - -> bcheck (f := ZtoB) E = true. - Proof. - intros t E H. - induction E as [tx ty tz op x y z eC IH| t a]. - - - unfold bcheck, getBounds, check in *. - - simpl; apply IH; clear IH; rewrite <- H; clear H. - simpl; rewrite convertArg_var; repeat f_equal. - - unfold interp_binop, RE, WE, BE, ZE, - BoundedEvaluable, RWVEvaluable, ZEvaluable, - eadd, emul, esub, eshiftr, eand. - - admit. - - (*induction op; rewrite check_spec'; reflexivity. *) - - - unfold bcheck, getBounds, check in *. - - induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1]. - - + admit. - - - + unfold rangeOf in *. - simpl in *; kill_dec; try reflexivity; try inversion H. - admit. - - + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ]; - apply andb_true_iff in H; destruct H as [H1 H2]; - assumption. - Admitted. - - Lemma RangeInterp_spec: forall {t} (E: @expr Z Z t), - check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) - = wordInterp (ZToWord _ E). - Proof using Type. - intros. - apply RangeInterp_bounded_spec. - apply check_spec. - assumption. - Qed. - End RWVSpec. - End Correctness. -End LLConversions. diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v deleted file mode 100644 index 433915da3..000000000 --- a/src/Assembly/Evaluables.v +++ /dev/null @@ -1,782 +0,0 @@ -Require Import Bedrock.Word Bedrock.Nomega. -Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.ZArith.ZArith Coq.ZArith.Znat Coq.ZArith.ZArith_dec Coq.NArith.Ndec. -Require Import Coq.Lists.List Coq.Program.Basics Crypto.Util.Bool Crypto.Tactics.Algebra_syntax.Nsatz Coq.Bool.Sumbool Coq.Init.Datatypes. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. -Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.WordizeUtil Crypto.Assembly.Bounds. -Require Import Coq.Logic.ProofIrrelevance. - -Import ListNotations. - -Section BaseTypes. - Inductive Range T := | range: forall (low high: T), Range T. - - Record RangeWithValue := rwv { - rwv_low: N; - rwv_value: N; - rwv_high: N - }. - - Record BoundedWord {n} := bounded { - bw_low: N; - bw_value: word n; - bw_high: N; - - ge_low: (bw_low <= wordToN bw_value)%N; - le_high: (wordToN bw_value <= bw_high)%N; - high_bound: (bw_high < Npow2 n)%N - }. -End BaseTypes. - -Section Evaluability. - Class Evaluable T := evaluator { - ezero: T; - - (* Conversions *) - toT: option RangeWithValue -> T; - fromT: T -> option RangeWithValue; - - (* Operations *) - eadd: T -> T -> T; - esub: T -> T -> T; - emul: T -> T -> T; - eshiftr: T -> T -> T; - eand: T -> T -> T; - - (* Comparisons *) - eltb: T -> T -> bool; - eeqb: T -> T -> bool - }. -End Evaluability. - -Section Z. - Context {n: nat}. - - Instance ZEvaluable : Evaluable Z := { - ezero := 0%Z; - - (* Conversions *) - toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); - fromT := fun x => Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x)); - - (* Operations *) - eadd := Z.add; - esub := Z.sub; - emul := Z.mul; - eshiftr := Z.shiftr; - eand := Z.land; - - (* Comparisons *) - eltb := Z.ltb; - eeqb := Z.eqb - }. - - Instance ConstEvaluable : Evaluable Z := { - ezero := 0%Z; - - (* Conversions *) - toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); - fromT := fun x => - if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x)) - then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x)) - else None; - - (* Operations *) - eadd := Z.add; - esub := Z.sub; - emul := Z.mul; - eshiftr := Z.shiftr; - eand := Z.land; - - (* Comparisons *) - eltb := Z.ltb; - eeqb := Z.eqb - }. - - Instance InputEvaluable : Evaluable Z := { - ezero := 0%Z; - - (* Conversions *) - toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); - fromT := fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x)); - - (* Operations *) - eadd := Z.add; - esub := Z.sub; - emul := Z.mul; - eshiftr := Z.shiftr; - eand := Z.land; - - (* Comparisons *) - eltb := Z.ltb; - eeqb := Z.eqb - }. -End Z. - -Section Word. - Context {n: nat}. - - Instance WordEvaluable : Evaluable (word n) := { - ezero := wzero n; - - (* Conversions *) - toT := fun x => @NToWord n (orElse 0%N (option_map rwv_value x)); - fromT := fun x => let v := @wordToN n x in (Some (rwv v v v)); - - (* Operations *) - eadd := @wplus n; - esub := @wminus n; - emul := @wmult n; - eshiftr := fun x y => @shiftr n x (wordToNat y); - eand := @wand n; - - (* Comparisons *) - eltb := fun x y => N.ltb (wordToN x) (wordToN y); - eeqb := fun x y => proj1_sig (bool_of_sumbool (@weq n x y)) - }. -End Word. - -Section RangeUpdate. - Context {n: nat}. - - Definition validBinaryWordOp - (rangeF: Range N -> Range N -> option (Range N)) - (wordF: word n -> word n -> word n): Prop := - forall (low0 high0 low1 high1: N) (x y: word n), - (low0 <= wordToN x)%N -> (wordToN x <= high0)%N -> (high0 < Npow2 n)%N - -> (low1 <= wordToN y)%N -> (wordToN y <= high1)%N -> (high1 < Npow2 n)%N - -> match rangeF (range N low0 high0) (range N low1 high1) with - | Some (range low2 high2) => - (low2 <= @wordToN n (wordF x y))%N - /\ (@wordToN n (wordF x y) <= high2)%N - /\ (high2 < Npow2 n)%N - | _ => True - end. - - Section BoundedSub. - Lemma NToWord_Npow2: wzero n = NToWord n (Npow2 n). - Proof using Type. - induction n as [|n0]. - - + repeat rewrite shatter_word_0; reflexivity. - - + unfold wzero in *; simpl in *. - rewrite IHn0; simpl. - induction (Npow2 n0); simpl; reflexivity. - Qed. - - Lemma bWSub_lem: forall (x0 x1: word n) (low0 high1: N), - (low0 <= wordToN x0)%N -> (wordToN x1 <= high1)%N -> - (low0 - high1 <= & (x0 ^- x1))%N. - Proof using Type. - intros. - - destruct (Nge_dec (wordToN x1) 1)%N as [e|e]. - destruct (Nge_dec (wordToN x1) (wordToN x0)). - - - unfold wminus, wneg. - assert (low0 <= high1)%N. { - transitivity (wordToN x0); [assumption|]. - transitivity (wordToN x1); [apply N.ge_le|]; assumption. - } - - replace (low0 - high1)%N with 0%N; [apply N_ge_0|]. - symmetry. - apply N.sub_0_le. - assumption. - - - transitivity (wordToN x0 - wordToN x1)%N. - - + transitivity (wordToN x0 - high1)%N; - [apply N.sub_le_mono_r | apply N.sub_le_mono_l]; - assumption. - - + assert (& x0 - & x1 < Npow2 n)%N. { - transitivity (wordToN x0); - try apply word_size_bound; - apply N.sub_lt. - - + apply N.lt_le_incl; assumption. - - + nomega. - } - - assert (& x0 - & x1 + & x1 < Npow2 n)%N. { - replace (wordToN x0 - wordToN x1 + wordToN x1)%N - with (wordToN x0) by nomega. - apply word_size_bound. - } - - assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. { - apply NToWord_equal. - rewrite <- wordize_plus; rewrite wordToN_NToWord; - try assumption. - nomega. - } - - apply N.eq_le_incl. - rewrite Hv. - unfold wminus. - rewrite <- wplus_assoc. - rewrite wminus_inv. - rewrite (wplus_comm (NToWord n (wordToN x0 - wordToN x1)) (wzero n)). - rewrite wplus_unit. - rewrite <- wordize_plus; [nomega|]. - rewrite wordToN_NToWord; assumption. - - - unfold wminus, wneg. - assert (wordToN x1 = 0)%N as e' by nomega. - rewrite e'. - replace (Npow2 n - 0)%N with (Npow2 n) by nomega. - rewrite <- NToWord_Npow2. - - erewrite <- wordize_plus; - try rewrite wordToN_zero; - replace (wordToN x0 + 0)%N with (wordToN x0)%N by nomega; - try apply word_size_bound. - - transitivity low0; try assumption. - apply N.le_sub_le_add_r. - apply N.le_add_r. - Qed. - End BoundedSub. - - Section LandOnes. - Definition getBits (x: N) := N.succ (N.log2 x). - - Lemma land_intro_ones: forall x, x = N.land x (N.ones (getBits x)). - Proof using Type. - intros. - rewrite N.land_ones_low; [reflexivity|]. - unfold getBits; nomega. - Qed. - - Lemma land_lt_Npow2: forall x k, (N.land x (N.ones k) < 2 ^ k)%N. - Proof using Type. - intros. - rewrite N.land_ones. - apply N.mod_lt. - rewrite <- (N2Nat.id k). - rewrite <- Npow2_N. - apply N.neq_0_lt_0. - apply Npow2_gt0. - Qed. - - Lemma land_prop_bound_l: forall a b, (N.land a b < Npow2 (N.to_nat (getBits a)))%N. - Proof using Type. - intros; rewrite Npow2_N. - rewrite (land_intro_ones a). - rewrite <- N.land_comm. - rewrite N.land_assoc. - rewrite N2Nat.id. - apply (N.lt_le_trans _ (2 ^ (getBits a))%N _); [apply land_lt_Npow2|]. - rewrite <- (N2Nat.id (getBits a)). - rewrite <- (N2Nat.id (getBits (N.land _ _))). - repeat rewrite <- Npow2_N. - rewrite N2Nat.id. - apply Npow2_ordered. - apply to_nat_le. - apply N.eq_le_incl; f_equal. - apply land_intro_ones. - Qed. - - Lemma land_prop_bound_r: forall a b, (N.land a b < Npow2 (N.to_nat (getBits b)))%N. - Proof using Type. - intros; rewrite N.land_comm; apply land_prop_bound_l. - Qed. - End LandOnes. - - Lemma range_add_valid : - validBinaryWordOp - (fun range0 range1 => - match (range0, range1) with - | (range low0 high0, range low1 high1) => - if (overflows n (high0 + high1)) - then None - else Some (range N (low0 + low1) (high0 + high1)) - end)%N - (@wplus n). - Proof using Type. - unfold validBinaryWordOp; intros. - - destruct (overflows n (high0 + high1))%N; repeat split; try assumption. - - - rewrite <- wordize_plus. - - + apply N.add_le_mono; assumption. - - + apply (N.le_lt_trans _ (high0 + high1)%N _); [|assumption]. - apply N.add_le_mono; assumption. - - - transitivity (wordToN x + wordToN y)%N; [apply plus_le|]. - apply N.add_le_mono; assumption. - Qed. - - Lemma range_sub_valid : - validBinaryWordOp - (fun range0 range1 => - match (range0, range1) with - | (range low0 high0, range low1 high1) => - if (Nge_dec low0 high1) - then Some (range N (low0 - high1)%N - (if (Nge_dec high0 (Npow2 n)) then N.pred (Npow2 n) else - if (Nge_dec high1 (Npow2 n)) then N.pred (Npow2 n) else - high0 - low1)%N) - else None - end) - (@wminus n). - Proof using Type. - unfold validBinaryWordOp; intros. - - Ltac kill_preds := - repeat match goal with - | [|- (N.pred _ < _)%N] => - rewrite <- (N.pred_succ (Npow2 n)); - apply -> N.pred_lt_mono; instantiate; - rewrite N.pred_succ; - [ apply N.lt_succ_diag_r - | apply N.neq_0_lt_0; apply Npow2_gt0] - | [|- (wordToN _ <= N.pred _)%N] => apply N.lt_le_pred - end. - - destruct (Nge_dec high0 (Npow2 n)), - (Nge_dec high1 (Npow2 n)), - (Nge_dec low0 high1); - repeat split; kill_preds; - repeat match goal with - | [|- (wordToN _ < Npow2 _)%N] => apply word_size_bound - | [|- (?x - _ < Npow2)%N] => transitivity x; [nomega|] - | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem - | [|- (wordToN _ <= _ - _)%N] => eapply wminus_bound - | [|- (0 <= _)%N] => apply N_ge_0 - end; try eassumption. - - - apply N.le_ge. - transitivity high1; [assumption|]. - transitivity low0; [|assumption]. - apply N.ge_le; assumption. - - - apply (N.le_lt_trans _ high0 _); [|assumption]. - replace high0 with (high0 - 0)%N by nomega. - replace' (high0 - 0)%N with high0 at 1 by nomega. - apply N.sub_le_mono_l. - apply N.ge_le; nomega. - Qed. - - Lemma range_mul_valid : - validBinaryWordOp - (fun range0 range1 => - match (range0, range1) with - | (range low0 high0, range low1 high1) => - if (overflows n (high0 * high1)) then None else - Some (range N (low0 * low1) (high0 * high1))%N - end) - (@wmult n). - Proof using Type. - unfold validBinaryWordOp; intros. - destruct (overflows n (high0 * high1))%N; repeat split. - - - rewrite <- wordize_mult. - - + apply N.mul_le_mono; assumption. - - + apply (N.le_lt_trans _ (high0 * high1)%N _); [|assumption]. - apply N.mul_le_mono; assumption. - - - transitivity (wordToN x * wordToN y)%N; [apply mult_le|]. - apply N.mul_le_mono; assumption. - - - assumption. - Qed. - - Lemma range_shiftr_valid : - validBinaryWordOp - (fun range0 range1 => - match (range0, range1) with - | (range low0 high0, range low1 high1) => - Some (range N (N.shiftr low0 high1) ( - if (Nge_dec high0 (Npow2 n)) - then (N.pred (Npow2 n)) - else (N.shiftr high0 low1)))%N - end) - (fun x k => extend (Nat.eq_le_incl _ _ eq_refl) (shiftr x (wordToNat k))). - Proof using Type. - unfold validBinaryWordOp; intros. - repeat split; unfold extend; try rewrite wordToN_convS, wordToN_zext. - - - rewrite <- wordize_shiftr. - rewrite <- Nshiftr_equiv_nat. - repeat rewrite N.shiftr_div_pow2. - transitivity (wordToN x / 2 ^ high1)%N. - - + apply N.div_le_mono; [|assumption]. - rewrite <- (N2Nat.id high1). - rewrite <- Npow2_N. - apply N.neq_0_lt_0. - apply Npow2_gt0. - - + apply N.div_le_compat_l; split. - - * rewrite <- Npow2_N; apply Npow2_gt0. - - * rewrite <- (N2Nat.id high1). - repeat rewrite <- Npow2_N. - apply Npow2_ordered. - rewrite <- (Nat2N.id (wordToNat y)). - apply to_nat_le. - rewrite <- wordToN_nat. - assumption. - - - destruct (Nge_dec high0 (Npow2 n)); - [apply N.lt_le_pred; apply word_size_bound |]. - - etransitivity; [eapply shiftr_bound'; eassumption|]. - - rewrite <- (Nat2N.id (wordToNat y)). - rewrite <- Nshiftr_equiv_nat. - rewrite N2Nat.id. - rewrite <- wordToN_nat. - repeat rewrite N.shiftr_div_pow2. - - apply N.div_le_compat_l; split; - rewrite <- (N2Nat.id low1); - [| rewrite <- (N2Nat.id (wordToN y))]; - repeat rewrite <- Npow2_N; - [apply Npow2_gt0 |]. - apply Npow2_ordered. - apply to_nat_le. - assumption. - - - destruct (Nge_dec high0 (Npow2 n)). - - + rewrite <- (N.pred_succ (Npow2 n)). - apply -> N.pred_lt_mono; instantiate; - rewrite (N.pred_succ (Npow2 n)); - [nomega|]. - apply N.neq_0_lt_0. - apply Npow2_gt0. - - + eapply N.le_lt_trans; [|eassumption]. - rewrite N.shiftr_div_pow2. - apply N.div_le_upper_bound. - - * induction low1; simpl; intro Z; inversion Z. - - * replace' high0 with (1 * high0)%N at 1 - by (rewrite N.mul_comm; nomega). - apply N.mul_le_mono; [|reflexivity]. - rewrite <- (N2Nat.id low1). - rewrite <- Npow2_N. - apply Npow2_ge1. - Qed. - - Lemma range_and_valid : - validBinaryWordOp - (fun range0 range1 => - match (range0, range1) with - | (range low0 high0, range low1 high1) => - let upper := (N.pred (Npow2 (min (N.to_nat (getBits high0)) (N.to_nat (getBits high1)))))%N in - Some (range N 0%N (if (Nge_dec upper (Npow2 n)) then (N.pred (Npow2 n)) else upper)) - end) - (@wand n). - Proof using Type. - unfold validBinaryWordOp; intros. - repeat split; [apply N_ge_0 | |]. - destruct (lt_dec (N.to_nat (getBits high0)) (N.to_nat (getBits high1))), - (Nge_dec _ (Npow2 n)); - try apply N.lt_le_pred; - try apply word_size_bound. - - - rewrite min_l; [|omega]. - rewrite wordize_and. - apply (N.lt_le_trans _ (Npow2 (N.to_nat (getBits (wordToN x)))) _); - [apply land_prop_bound_l|]. - apply Npow2_ordered. - apply to_nat_le. - unfold getBits. - apply N.le_pred_le_succ. - rewrite N.pred_succ. - apply N.log2_le_mono. - assumption. - - - rewrite min_r; [|omega]. - rewrite wordize_and. - apply (N.lt_le_trans _ (Npow2 (N.to_nat (getBits (wordToN y)))) _); - [apply land_prop_bound_r|]. - apply Npow2_ordered. - apply to_nat_le. - unfold getBits. - apply N.le_pred_le_succ. - rewrite N.pred_succ. - apply N.log2_le_mono. - assumption. - - - destruct (Nge_dec _ (Npow2 n)); [|assumption]. - - rewrite <- (N.pred_succ (Npow2 n)). - apply -> N.pred_lt_mono; instantiate; - rewrite (N.pred_succ (Npow2 n)); - [nomega|]. - apply N.neq_0_lt_0. - apply Npow2_gt0. - Qed. -End RangeUpdate. - -Section BoundedWord. - Context {n: nat}. - - Definition BW := @BoundedWord n. - Transparent BW. - - Definition bapp {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: BW): option BW. - - refine ( - let op' := op _ _ _ _ _ _ - (ge_low X) (le_high X) (high_bound X) - (ge_low Y) (le_high Y) (high_bound Y) in - - let result := rangeF - (range N (bw_low X) (bw_high X)) - (range N (bw_low Y) (bw_high Y)) in - - match result as r' return result = r' -> _ with - | Some (range low high) => fun e => - Some (@bounded n low (wordF (bw_value X) (bw_value Y)) high _ _ _) - | None => fun _ => None - end eq_refl); abstract ( - - pose proof op' as p; clear op'; - unfold result in *; - rewrite e in p; - destruct p as [p0 p1]; destruct p1 as [p1 p2]; - assumption). - Defined. - - Definition rapp {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: Range N): option (Range N) := - rangeF X Y. - - Definition vapp {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: word n): option (word n) := - Some (wordF X Y). - - Definition bwToRWV (w: BW): RangeWithValue := - rwv (bw_low w) (wordToN (bw_value w)) (bw_high w). - - Definition bwFromRWV (r: RangeWithValue): option BW. - refine - match r with - | rwv l v h => - match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with - | (left p0, left p1, left p2) => Some (@bounded n l (NToWord n l) h _ _ _) - | _ => None - end - end; try rewrite wordToN_NToWord; - - assert (N.succ h <= Npow2 n)%N by abstract ( - apply N.ge_le in p2; - rewrite <- (N.pred_succ h) in p2; - apply -> N.le_pred_le_succ in p2; - rewrite N.succ_pred in p2; [assumption |]; - apply N.neq_0_lt_0; - apply Npow2_gt0); - - try abstract (apply (N.lt_le_trans _ (N.succ h) _); - [nomega|assumption]); - - [reflexivity| etransitivity; apply N.ge_le; eassumption]. - Defined. - - Definition bwToRange (w: BW): Range N := - range N (bw_low w) (bw_high w). - - Definition bwFromRange (r: Range N): option BW. - refine - match r with - | range l h => - match (Nge_dec h l, Nge_dec (N.pred (Npow2 n)) h) with - | (left p0, left p1) => Some (@bounded n l (NToWord n l) h _ _ _) - | _ => None - end - end; try rewrite wordToN_NToWord; - - assert (N.succ h <= Npow2 n)%N by abstract ( - apply N.ge_le in p1; - rewrite <- (N.pred_succ h) in p1; - apply -> N.le_pred_le_succ in p1; - rewrite N.succ_pred in p1; [assumption |]; - apply N.neq_0_lt_0; - apply Npow2_gt0); - - try abstract (apply (N.lt_le_trans _ (N.succ h) _); - [nomega|assumption]); - - [reflexivity|apply N.ge_le; assumption]. - Defined. - - Definition just (x: N): option BW. - refine - match Nge_dec (N.pred (Npow2 n)) x with - | left p => Some (@bounded n x (NToWord n x) x _ _ _) - | right _ => None - end; try rewrite wordToN_NToWord; try reflexivity; - - assert (N.succ x <= Npow2 n)%N by abstract ( - apply N.ge_le in p; - rewrite <- (N.pred_succ x) in p; - apply -> N.le_pred_le_succ in p; - rewrite N.succ_pred in p; [assumption |]; - apply N.neq_0_lt_0; - apply Npow2_gt0); - - try abstract ( - apply (N.lt_le_trans _ (N.succ x) _); - [nomega|assumption]). - Defined. - - Lemma just_None_spec: forall x, just x = None -> (x >= Npow2 n)%N. - Proof using Type. - intros x H; unfold just in *. - destruct (Nge_dec (N.pred (Npow2 n)) x) as [p|p]; [inversion H |]. - rewrite <- (N.pred_succ x) in p. - apply N.lt_pred_lt_succ in p. - rewrite N.succ_pred in p; [|apply N.neq_0_lt_0; nomega]. - apply N.le_succ_l in p. - apply N.le_ge; apply N.succ_le_mono; assumption. - Qed. - - Lemma just_value_spec: forall x b, just x = Some b -> bw_value b = NToWord n x. - Proof using Type. - intros x b H; destruct b; unfold just in *; - destruct (Nge_dec (N.pred (Npow2 n)) x); - simpl in *; inversion H; subst; reflexivity. - Qed. - - Lemma just_low_spec: forall x b, just x = Some b -> bw_low b = x. - Proof using Type. - intros x b H; destruct b; unfold just in *; - destruct (Nge_dec (N.pred (Npow2 n)) x); - simpl in *; inversion H; subst; reflexivity. - Qed. - - Lemma just_high_spec: forall x b, just x = Some b -> bw_high b = x. - Proof using Type. - intros x b H; destruct b; unfold just in *; - destruct (Nge_dec (N.pred (Npow2 n)) x); - simpl in *; inversion H; subst; reflexivity. - Qed. - - Definition any: BW. - refine (@bounded n 0%N (wzero n) (N.pred (Npow2 n)) _ _ _); - try rewrite wordToN_zero; - try reflexivity; - try abstract (apply N.lt_le_pred; apply Npow2_gt0). - - apply N.lt_pred_l; apply N.neq_0_lt_0; apply Npow2_gt0. - Defined. - - Instance BoundedEvaluable : Evaluable (option BW) := { - ezero := Some any; - - toT := fun x => omap x bwFromRWV; - fromT := option_map bwToRWV; - - eadd := fun x y => omap x (fun X => omap y (fun Y => bapp range_add_valid X Y)); - esub := fun x y => omap x (fun X => omap y (fun Y => bapp range_sub_valid X Y)); - emul := fun x y => omap x (fun X => omap y (fun Y => bapp range_mul_valid X Y)); - eshiftr := fun x y => omap x (fun X => omap y (fun Y => bapp range_shiftr_valid X Y)); - eand := fun x y => omap x (fun X => omap y (fun Y => bapp range_and_valid X Y)); - - eltb := fun x y => - orElse false (omap x (fun X => omap y (fun Y => - Some (N.ltb (wordToN (bw_value X)) (wordToN (bw_value Y)))))); - - eeqb := fun x y => - orElse false (omap x (fun X => omap y (fun Y => - Some (N.eqb (wordToN (bw_value X)) (wordToN (bw_value Y)))))) - }. -End BoundedWord. - -Section RangeWithValue. - Context {n: nat}. - - Definition rwv_app {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: RangeWithValue): option (RangeWithValue) := - omap (rangeF (range N (rwv_low X) (rwv_high X)) - (range N (rwv_low Y) (rwv_high Y))) (fun r' => - match r' with - | range l h => Some ( - rwv l (wordToN (wordF (NToWord n (rwv_value X)) - (NToWord n (rwv_value Y)))) h) - end). - - Definition checkRWV (x: RangeWithValue): bool := - match x with - | rwv l v h => - match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with - | (left _, left _, left _) => true - | _ => false - end - end. - - Lemma rwv_None_spec : forall {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: RangeWithValue), - omap (rwv_app op X Y) (bwFromRWV (n := n)) <> None. - Proof. - Admitted. - - Definition rwvToRange (x: RangeWithValue): Range N := - range N (rwv_low x) (rwv_high x). - - Definition rwvFromRange (x: Range N): RangeWithValue := - match x with - | range l h => rwv l h h - end. - - Lemma bwToFromRWV: forall x, option_map (@bwToRWV n) (omap x bwFromRWV) = x. - Proof. - Admitted. - - Instance RWVEvaluable : Evaluable (option RangeWithValue) := { - ezero := None; - - toT := fun x => x; - fromT := fun x => omap x (fun x' => if (checkRWV x') then x else None); - - eadd := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_add_valid X Y)); - - esub := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_sub_valid X Y)); - - emul := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_mul_valid X Y)); - - eshiftr := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_shiftr_valid X Y)); - - eand := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_and_valid X Y)); - - eltb := fun x y => - match (x, y) with - | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => - N.ltb xv yv - - | _ => false - end; - - eeqb := fun x y => - match (x, y) with - | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => - andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv) - - | _ => false - end - }. -End RangeWithValue. diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v deleted file mode 100644 index a904f14b1..000000000 --- a/src/Assembly/GF25519.v +++ /dev/null @@ -1,313 +0,0 @@ -Require Import Coq.ZArith.Znat. -Require Import Coq.ZArith.ZArith. - -Require Import Crypto.Assembly.Pipeline. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.Specific.GF25519. -Require Import Crypto.Util.Tuple. - -Require InitialRing. - -Module GF25519. - Definition bits: nat := 64. - Definition width: Width bits := W64. - - Existing Instance ZEvaluable. - - Fixpoint makeBoundList {n} k (b: @BoundedWord n) := - match k with - | O => nil - | S k' => cons b (makeBoundList k' b) - end. - - Section DefaultBounds. - Import ListNotations. - - Local Notation rr exp := (2^exp + 2^(exp-3))%Z. - - Definition feBound: list Z := - [rr 26; rr 27; rr 26; rr 27; rr 26; - rr 27; rr 26; rr 27; rr 26; rr 27]. - End DefaultBounds. - - Definition FE: type. - Proof. - let T := eval vm_compute in fe25519 in - let t := HL.reify_type T in - exact t. - Defined. - - Section Expressions. - Definition flatten {T}: (@interp_type Z FE -> T) -> NAry 10 Z T. - intro F; refine (fun (a b c d e f g h i j: Z) => - F (a, b, c, d, e, f, g, h, i, j)). - Defined. - - Definition unflatten {T}: - (forall a b c d e f g h i j : Z, T (a, b, c, d, e, f, g, h, i, j)) - -> (forall x: @interp_type Z FE, T x). - Proof. - intro F; refine (fun (x: @interp_type Z FE) => - let '(a, b, c, d, e, f, g, h, i, j) := x in - F a b c d e f g h i j). - Defined. - - Ltac intro_vars_for R := revert R; - match goal with - | [ |- forall x, @?T x ] => apply (@unflatten T); intros - end. - - Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_add. - - Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_sub. - - Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in mul. - - Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in opp. - - Definition ge25519_add' (P Q: @interp_type Z FE): - { r: @HL.Expr Z FE | HL.Interp r = ge25519_add_expr P Q }. - Proof. - intro_vars_for P. - intro_vars_for Q. - - eexists. - - cbv beta delta [ge25519_add_expr]. - - etransitivity; [reflexivity|]. - - let R := HL.rhs_of_goal in - let X := HL.Reify R in - transitivity (HL.Interp (X bits)); [reflexivity|]. - - cbv iota beta delta [ HL.Interp - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - - reflexivity. - Defined. - - Definition ge25519_sub' (P Q: @interp_type Z FE): - { r: @HL.Expr Z FE | HL.Interp r = ge25519_sub_expr P Q }. - Proof. - intro_vars_for P. - intro_vars_for Q. - - eexists. - - cbv beta delta [ge25519_sub_expr]. - - etransitivity; [reflexivity|]. - - let R := HL.rhs_of_goal in - let X := HL.Reify R in - transitivity (HL.Interp (X bits)); [reflexivity|]. - - cbv iota beta delta [ HL.Interp - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - - reflexivity. - Defined. - - Definition ge25519_mul' (P Q: @interp_type Z FE): - { r: @HL.Expr Z FE | HL.Interp r = ge25519_mul_expr P Q }. - Proof. - intro_vars_for P. - intro_vars_for Q. - - eexists. - - cbv beta delta [ge25519_mul_expr]. - - etransitivity; [reflexivity|]. - - let R := HL.rhs_of_goal in - let X := HL.Reify R in - transitivity (HL.Interp (X bits)); [reflexivity|]. - - cbv iota beta delta [ HL.Interp - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - - reflexivity. - Defined. - - Definition ge25519_opp' (P: @interp_type Z FE): - { r: @HL.Expr Z FE | HL.Interp r = ge25519_opp_expr P }. - Proof. - intro_vars_for P. - - eexists. - - cbv beta delta [ge25519_opp_expr zero_]. - - etransitivity; [reflexivity|]. - - let R := HL.rhs_of_goal in - let X := HL.Reify R in - transitivity (HL.Interp (X bits)); [reflexivity|]. - - cbv iota beta delta [ HL.Interp - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - - reflexivity. - Defined. - - Definition ge25519_add (P Q: @interp_type Z FE) := - proj1_sig (ge25519_add' P Q). - - Definition ge25519_sub (P Q: @interp_type Z FE) := - proj1_sig (ge25519_sub' P Q). - - Definition ge25519_mul (P Q: @interp_type Z FE) := - proj1_sig (ge25519_mul' P Q). - - Definition ge25519_opp (P: @interp_type Z FE) := - proj1_sig (ge25519_opp' P). - End Expressions. - - Module AddExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition prog: NAry 20 Z (@HL.Expr Z ResultType) := - Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))). - End AddExpr. - - Module SubExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in - carry_sub. - - Definition prog: NAry 20 Z (@HL.Expr Z ResultType) := - Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))). - End SubExpr. - - Module MulExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition prog: NAry 20 Z (@HL.Expr Z ResultType) := - Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_mul p q)))). - End MulExpr. - - Module OppExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 10. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound. - - Definition prog: NAry 10 Z (@HL.Expr Z ResultType) := - Eval cbv in (flatten ge25519_opp). - End OppExpr. - - Module Add := Pipeline AddExpr. - Module Sub := Pipeline SubExpr. - Module Mul := Pipeline MulExpr. - Module Opp := Pipeline OppExpr. - - Section Instantiation. - Import InitialRing. - - Definition Binary : Type := NAry 20 (word bits) (@interp_type (word bits) FE). - Definition Unary : Type := NAry 10 (word bits) (@interp_type (word bits) FE). - - Ltac ast_simpl := cbv [ - Add.bits Add.inputs AddExpr.inputs Add.ResultType AddExpr.ResultType - Add.W Add.R Add.ZEvaluable Add.WEvaluable Add.REvaluable - Add.AST.progW Add.LL.progW Add.HL.progW AddExpr.prog - - Sub.bits Sub.inputs SubExpr.inputs Sub.ResultType SubExpr.ResultType - Sub.W Sub.R Sub.ZEvaluable Sub.WEvaluable Sub.REvaluable - Sub.AST.progW Sub.LL.progW Sub.HL.progW SubExpr.prog - - Mul.bits Mul.inputs MulExpr.inputs Mul.ResultType MulExpr.ResultType - Mul.W Mul.R Mul.ZEvaluable Mul.WEvaluable Mul.REvaluable - Mul.AST.progW Mul.LL.progW Mul.HL.progW MulExpr.prog - - Opp.bits Opp.inputs OppExpr.inputs Opp.ResultType OppExpr.ResultType - Opp.W Opp.R Opp.ZEvaluable Opp.WEvaluable Opp.REvaluable - Opp.AST.progW Opp.LL.progW Opp.HL.progW OppExpr.prog - - HLConversions.convertExpr CompileHL.Compile CompileHL.compile - - LL.interp LL.uninterp_arg LL.under_lets LL.interp_arg - - ZEvaluable WordEvaluable RWVEvaluable rwv_value - eadd esub emul eand eshiftr toT fromT - - interp_binop interp_type FE liftN NArgMap id - omap option_map orElse]. - - (* Tack this on to make a simpler AST, but it really slows us down *) - Ltac word_simpl := cbv [ - AddExpr.bits SubExpr.bits MulExpr.bits OppExpr.bits bits - NToWord posToWord natToWord wordToNat wordToN wzero' - Nat.mul Nat.add]. - - Ltac kill_conv := let p := fresh in - pose proof N2Z.id as p; unfold Z.to_N in p; - repeat rewrite p; clear p; - repeat rewrite NToWord_wordToN. - - Local Notation unary_eq f g - := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - f x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - = g x0 x1 x2 x3 x4 x5 x6 x7 x8 x9). - Local Notation binary_eq f g - := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9, - f x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9 - = g x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9). - - Definition add' - : {f: Binary | - binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Add.AST.progW) }. - Proof. eexists; intros; ast_simpl; kill_conv; reflexivity. Defined. - - Definition sub' - : {f: Binary | - binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Sub.AST.progW) }. - Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined. - - Definition mul' - : {f: Binary | - binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Mul.AST.progW) }. - Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined. - - Definition opp' : {f: Unary | - unary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Opp.AST.progW) }. - Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined. - - Definition add := Eval simpl in proj1_sig add'. - Definition sub := Eval simpl in proj1_sig sub'. - Definition mul := Eval simpl in proj1_sig mul'. - Definition opp := Eval simpl in proj1_sig opp'. - End Instantiation. -End GF25519. -(* -Extraction "GF25519Add" GF25519.Add. -Extraction "GF25519Sub" GF25519.Sub. -Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp. -*) diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v deleted file mode 100644 index e9eecd4c8..000000000 --- a/src/Assembly/HL.v +++ /dev/null @@ -1,212 +0,0 @@ -Require Import Crypto.Assembly.PhoasCommon. -Require Import Coq.setoid_ring.InitialRing. -Require Import Crypto.Util.LetIn. - -Module HL. - Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t. - Proof. - induction t; [refine (f x)|]. - destruct x as [x1 x2]. - refine (IHt1 x1, IHt2 x2). - Defined. - - Section Language. - Context {T: Type}. - Context {E: Evaluable T}. - - Section expr. - Context {var : type -> Type}. - - Inductive expr : type -> Type := - | Const : forall {_ : Evaluable T}, @interp_type T TT -> expr TT - | Var : forall {t}, var t -> expr t - | Binop : forall {t1 t2 t3}, binop t1 t2 t3 -> expr t1 -> expr t2 -> expr t3 - | Let : forall {tx}, expr tx -> forall {tC}, (var tx -> expr tC) -> expr tC - | Pair : forall {t1}, expr t1 -> forall {t2}, expr t2 -> expr (Prod t1 t2) - | MatchPair : forall {t1 t2}, expr (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> expr tC) -> expr tC. - End expr. - - Local Notation ZConst z := (@Const Z ConstEvaluable _ z%Z). - - Fixpoint interp {t} (e: @expr interp_type t) : @interp_type T t := - match e in @expr _ t return interp_type t with - | Const _ x => x - | Var _ n => n - | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2) - | Let _ ex _ eC => dlet x := interp ex in interp (eC x) - | Pair _ e1 _ e2 => (interp e1, interp e2) - | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2) - end. - - Definition Expr t : Type := forall var, @expr var t. - - Definition Interp {t} (e: Expr t) : interp_type t := interp (e interp_type). - End Language. - - Definition zinterp {t} E := @interp Z ZEvaluable t E. - - Definition ZInterp {t} E := @Interp Z ZEvaluable t E. - - Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E. - - Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E. - - Existing Instance ZEvaluable. - - Example example_Expr : Expr TT := fun var => ( - Let (Const 7) (fun a => - Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p => - MatchPair (Var p) (fun x y => - Binop OPadd (Var x) (Var y)))))%Z. - - Example interp_example_Expr : ZInterp example_Expr = 28%Z. - Proof. reflexivity. Qed. - - (* Reification assumes the argument type is Z *) - - Ltac reify_type t := - lazymatch t with - | BinInt.Z => constr:(TT) - | prod ?l ?r => - let l := reify_type l in - let r := reify_type r in - constr:(Prod l r) - end. - - Ltac reify_binop op := - lazymatch op with - | Z.add => constr:(OPadd) - | Z.sub => constr:(OPsub) - | Z.mul => constr:(OPmul) - | Z.land => constr:(OPand) - | Z.shiftr => constr:(OPshiftr) - end. - - Class reify (n: nat) {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T. - Definition reify_var_for_in_is {T} (x:T) (t:type) {eT} (e:eT) := False. - - Ltac reify n var e := - lazymatch e with - | let x := ?ex in @?eC x => - let ex := reify n var ex in - let eC := reify n var eC in - constr:(Let (T:=Z) (var:=var) ex eC) - | match ?ep with (v1, v2) => @?eC v1 v2 end => - let ep := reify n var ep in - let eC := reify n var eC in - constr:(MatchPair (T:=Z) (var:=var) ep eC) - | pair ?a ?b => - let a := reify n var a in - let b := reify n var b in - constr:(Pair (T:=Z) (var:=var) a b) - | ?op ?a ?b => - let op := reify_binop op in - let b := reify n var b in - let a := reify n var a in - constr:(Binop (T:=Z) (var:=var) op a b) - | (fun x : ?T => ?C) => - let t := reify_type T in - (* Work around Coq 8.5 and 8.6 bug *) - (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *) - (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) - (* even if its Gallina name matches a Ltac in this tactic. *) - (* [C] here is an open term that references "x" by name *) - let maybe_x := fresh x in - let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : var t) (_:reify_var_for_in_is x t not_x) => - (_ : reify n var C)) - with fun _ v _ => @?C v => C end - | ?x => - lazymatch goal with - | _:reify_var_for_in_is x ?t ?v |- _ => constr:(@Var Z var t v) - | _ => let x' := eval cbv in x in - match isZcst x with - | true => constr:(@Const Z var (@ConstEvaluable n) x) - | false => constr:(@Const Z var InputEvaluable x) - end - end - end. - - Hint Extern 0 (reify ?n ?var ?e) => (let e := reify n var e in eexact e) : typeclass_instances. - - Ltac Reify e := - lazymatch constr:(fun (n: nat) (var:type->Type) => (_:reify n var e)) with - (fun n var => ?C) => constr:(fun (n: nat) (var:type->Type) => C) (* copy the term but not the type cast *) - end. - - Definition zinterp_type := @interp_type Z. - Transparent zinterp_type. - - Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify (T:=Z) 16 zinterp_type ((fun x => x+x) x)%Z. - intros. - let A := (reify 16 zinterp_type (x + x + 1)%Z) in idtac A. - Abort. - - Goal False. - let z := (reify 16 zinterp_type (let x := 0 in x)%Z) in pose z. - Abort. - - Ltac lhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(LHS) end. - Ltac rhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(RHS) end. - - Ltac Reify_rhs n := - let rhs := rhs_of_goal in - let RHS := Reify rhs in - transitivity (ZInterp (RHS n)); - [|cbv iota beta delta [ZInterp Interp interp_type interp_binop interp]; reflexivity]. - - Goal (0 = let x := 1+2 in x*3)%Z. - Reify_rhs 32. - Abort. - - Goal (0 = let x := 1 in let y := 2 in x * y)%Z. - Reify_rhs 32. - Abort. - - Section wf. - Context {T : Type} {var1 var2 : type -> Type}. - - Local Notation "x ≡ y" := (existT _ _ (x, y)). - - Definition Texpr var t := @expr Z var t. - - Inductive wf : list (sigT (fun t => var1 t * var2 t))%type -> forall {t}, Texpr var1 t -> Texpr var2 t -> Prop := - | WfConst : forall G n, wf G (Const n) (Const n) - | WfVar : forall G t x x', In (x ≡ x') G -> @wf G t (Var x) (Var x') - | WfBinop : forall G {t1} {t2} {t3} (e1:Texpr var1 t1) (e2:Texpr var1 t2) - (e1':Texpr var2 t1) (e2':Texpr var2 t2) - (op: binop t1 t2 t3), - wf G e1 e1' - -> wf G e2 e2' - -> wf G (Binop op e1 e2) (Binop op e1' e2') - | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> Texpr _ t2) e2', - wf G e1 e1' - -> (forall x1 x2, wf ((x1 ≡ x2) :: G) (e2 x1) (e2' x2)) - -> wf G (Let e1 e2) (Let e1' e2') - | WfPair : forall G {t1} {t2} (e1: Texpr var1 t1) (e2: Texpr var1 t2) - (e1': Texpr var2 t1) (e2': Texpr var2 t2), - wf G e1 e1' - -> wf G e2 e2' - -> wf G (Pair e1 e2) (Pair e1' e2') - | WfMatchPair : forall G t1 t2 tC ep ep' (eC : _ t1 -> _ t2 -> Texpr _ tC) eC', - wf G ep ep' - -> (forall x1 x2 y1 y2, wf ((x1 ≡ x2) :: (y1 ≡ y2) :: G) (eC x1 y1) (eC' x2 y2)) - -> wf G (MatchPair ep eC) (MatchPair ep' eC'). - End wf. - - Definition Wf {T: Type} {t} (E : Expr t) := forall var1 var2, wf nil (E var1) (E var2). - - Example example_Expr_Wf : Wf (T := Z) example_Expr. - Proof. - unfold Wf; repeat match goal with - | [ |- wf _ _ _ ] => constructor - | [ |- In ?x (cons ?x _) ] => constructor 1; reflexivity - | [ |- In _ _ ] => constructor 2 - | _ => intros - end. - Qed. - - Axiom Wf_admitted : forall {t} (E:Expr t), @Wf Z t E. - Ltac admit_Wf := apply Wf_admitted. - -End HL. diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v deleted file mode 100644 index c2faf955d..000000000 --- a/src/Assembly/LL.v +++ /dev/null @@ -1,180 +0,0 @@ -Require Import Crypto.Assembly.PhoasCommon. -Require Import Crypto.Util.LetIn. - -Local Arguments Let_In / _ _ _ _. - -Module LL. - Section Language. - Context {T: Type}. - Context {E: Evaluable T}. - - (* A very restricted language where binary operations are restricted - to returning [T] and must appear in [let] binders, and all pairs - must be constructed in the return clause. No matching on pairs is - allowed *) - - Section expr. - Context {var: Type}. - - Inductive arg : type -> Type := - | Const : @interp_type T TT -> arg TT - | Var : var -> arg TT - | Pair : forall {t1 t2}, arg t1 -> arg t2 -> arg (Prod t1 t2). - - Inductive expr : type -> Type := - | LetBinop : forall {t1 t2 t3}, binop t1 t2 t3 -> arg t1 -> arg t2 -> - forall {tC}, (arg t3 -> expr tC) -> expr tC - | Return : forall {t}, arg t -> expr t. - End expr. - - Definition Expr t := forall var, @expr var t. - - Fixpoint interp_arg' {V t} (f: V -> T) (e: arg t) : interp_type t := - match e with - | Pair _ _ x y => (interp_arg' f x, interp_arg' f y) - | Const x => x - | Var x => f x - end. - - Fixpoint interp_arg {t} (e: arg t) : interp_type t := - match e with - | Pair _ _ x y => (interp_arg x, interp_arg y) - | Const x => x - | Var x => x - end. - - Lemma interp_arg_spec: forall {t} (x: arg t), interp_arg x = interp_arg' id x. - Proof using Type. - intros; induction x; unfold id in *; simpl; repeat f_equal; - first [reflexivity| assumption]. - Qed. - - Fixpoint uninterp_arg {var t} (x: interp_type t) : @arg var t := - match t as t' return interp_type t' -> arg t' with - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => Pair (uninterp_arg x0) (uninterp_arg x1) - end - | TT => Const - end x. - - Fixpoint uninterp_arg_as_var {var t} (x: @interp_type var t) : @arg var t := - match t as t' return @interp_type var t' -> @arg var t' with - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => Pair (uninterp_arg_as_var x0) (uninterp_arg_as_var x1) - end - | TT => Var - end x. - - Fixpoint interp' {V t} (f: V -> T) (e:expr t) : interp_type t := - match e with - | LetBinop _ _ _ op a b _ eC => - let x := interp_binop op (interp_arg' f a) (interp_arg' f b) in interp' f (eC (uninterp_arg x)) - | Return _ a => interp_arg' f a - end. - - Fixpoint interp {t} (e:expr t) : interp_type t := - match e with - | LetBinop _ _ _ op a b _ eC => - dlet x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x)) - | Return _ a => interp_arg a - end. - - Lemma interp_spec: forall {t} (e: expr t), interp e = interp' id e. - Proof using Type. - intros; induction e; unfold id in *; simpl; repeat f_equal; - try rewrite H; simpl; repeat f_equal; - rewrite interp_arg_spec; repeat f_equal. - Qed. - End Language. - - Transparent interp interp_arg. - - Example example_expr : - (@interp Z (ZEvaluable) _ - (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z. - Proof. reflexivity. Qed. - - Section under_lets. - Context {T: Type}. - - Fixpoint under_lets {t var} (e: @expr T var t) {struct e} : - forall {tC} (C: @arg T var t -> @expr T var tC), @expr T var tC := - match e with - | LetBinop _ _ _ op a b tC eC => fun tC C => LetBinop op a b (fun v => @under_lets _ _ (eC v) _ C) - | Return t a => fun _ C => C a - end. - End under_lets. - - Lemma under_lets_correct {T} {E: Evaluable T} {t} (e: expr t) {tC} - (C: arg t -> expr tC) - (C_Proper : forall a1 a2, interp_arg a1 = interp_arg a2 -> interp (C a1) = interp (C a2)) : - forall a, interp_arg a = interp e -> interp (under_lets e C) = interp (C a). - Proof. induction e; repeat (intuition (congruence || eauto); simpl). Qed. - - Section match_arg. - Context {T : Type}. - - Arguments arg _ _ _ : clear implicits. - Arguments expr _ _ _ : clear implicits. - - Definition match_arg_Prod {var t1 t2} (a:arg T var (Prod t1 t2)) : (arg T var t1 * arg T var t2) := - match a with - | Pair _ _ a1 a2 => (a1, a2) - | _ => I (* dummy *) - end. - - Global Arguments match_arg_Prod / : simpl nomatch. - - Lemma match_arg_Prod_correct_helper {var t} (a: arg T var t) : - match t return arg T var t -> Prop with - | Prod _ _ => fun a => forall a1 a2, - match_arg_Prod a = (a1, a2) <-> a = Pair a1 a2 - | _ => fun _ => True - end a. - Proof using Type. - unfold match_arg_Prod; destruct a; - repeat match goal with - | _ => split - | _ => intro - | _ => progress simpl in * - | _ => break_match - | _ => intuition congruence - | H: _ |- _ => eapply (f_equal match_arg_Prod) in H - end. - Qed. - - Lemma match_arg_Prod_correct {var t1 t2} (a:arg T var (Prod t1 t2)) (a1:arg T var t1) (a2:arg T var t2) : - match_arg_Prod a = (a1, a2) <-> a = Pair a1 a2. - Proof using Type. - pose proof (match_arg_Prod_correct_helper a) as H; simpl in H; rewrite H; reflexivity. - Qed. - End match_arg. - - Lemma interp_arg_uninterp_arg : forall T t (a:interp_type t), @interp_arg T t (uninterp_arg a) = a. - Proof. - induction t as [|i0 v0 i1 v1]; simpl; intros; try reflexivity. - break_match; subst; simpl. - unfold interp_arg in *. - simpl; rewrite v0, v1; reflexivity. - Qed. - - Lemma interp_under_lets {T} {_: Evaluable T} {t: type} {tC: type} - (e: @expr T T t) - (C: @arg T T t -> @expr T T tC) - (C_Proper : forall a1 a2, interp_arg a1 = interp_arg a2 -> - interp (C a1) = interp (C a2)) : - interp (under_lets e C) = interp (C (uninterp_arg (interp e))). - Proof. - intros; apply under_lets_correct; - [ assumption - | rewrite interp_arg_uninterp_arg; reflexivity ]. - Qed. - - Lemma Pair_eq T var t0 t1 x0 x1 x0' x1' : @Pair T var t0 t1 x0 x1 = @Pair T var t0 t1 x0' x1' <-> (x0, x1) = (x0', x1'). - Proof. - split; intro H; try congruence. - apply (f_equal match_arg_Prod) in H; assumption. - Qed. -End LL. diff --git a/src/Assembly/Output.ml b/src/Assembly/Output.ml deleted file mode 100644 index d84aee0a2..000000000 --- a/src/Assembly/Output.ml +++ /dev/null @@ -1,14 +0,0 @@ - -open Result - -let list_to_string s = - let rec loop s n = - match s with - [] -> String.make n '?' - | car :: cdr -> - let result = loop cdr (n + 1) in - Bytes.set result n car; - result - in loop s 0 ;; - -print_string (list_to_string result) ;; diff --git a/src/Assembly/PhoasCommon.v b/src/Assembly/PhoasCommon.v deleted file mode 100644 index fbdc4c349..000000000 --- a/src/Assembly/PhoasCommon.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Export Coq.ZArith.BinInt. -Require Export Coq.NArith.BinNat. -Require Export Coq.Bool.Bool. -Require Export Coq.Lists.List. - -Require Export Bedrock.Word Bedrock.Nomega. - -Require Export Crypto.Util.GlobalSettings. -Require Export Crypto.Util.Tactics. -Require Export Crypto.Util.Notations. -Require Export Crypto.Tactics.VerdiTactics. - -Require Export Crypto.Assembly.Evaluables. - -Section Definitions. - Context {T: Type} {E: Evaluable T}. - - Inductive type := TT | Prod : type -> type -> type. - - Fixpoint interp_type (t:type): Type := - match t with - | TT => T - | Prod a b => prod (interp_type a) (interp_type b) - end. - - Inductive binop : type -> type -> type -> Type := - | OPadd : binop TT TT TT - | OPsub : binop TT TT TT - | OPmul : binop TT TT TT - | OPand : binop TT TT TT - | OPshiftr : binop TT TT TT. - (* TODO: should [Pair] be a [binop]? *) - - Definition interp_binop {t1 t2 t} (op:binop t1 t2 t) : interp_type t1 -> interp_type t2 -> interp_type t := - match op with - | OPadd => @eadd T E - | OPsub => @esub T E - | OPmul => @emul T E - | OPand => @eand T E - | OPshiftr => @eshiftr T E - end. -End Definitions. diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v deleted file mode 100644 index 40d5abca9..000000000 --- a/src/Assembly/Pipeline.v +++ /dev/null @@ -1,140 +0,0 @@ -Require Export Crypto.Assembly.QhasmCommon. - -Require Export Crypto.Assembly.PhoasCommon. -Require Export Crypto.Assembly.HL. -Require Export Crypto.Assembly.LL. -Require Export Crypto.Assembly.Compile. -Require Export Crypto.Assembly.Conversions. -Require Export Crypto.Assembly.StringConversion. -Require Export Crypto.Assembly.State. - -Require Export Crypto.Util.Notations. -Require Export Crypto.Util.LetIn. - -Require Export Coq.ZArith.BinInt. - -Require Export ExtrOcamlBasic. -Require Export ExtrOcamlString. - -Module Type Expression. - Parameter bits: nat. - Parameter width: Width bits. - Parameter inputs: nat. - Parameter inputBounds: list Z. - Parameter ResultType: type. - - Parameter prog: NAry inputs Z (@HL.Expr Z ResultType). -End Expression. - -Module Pipeline (Input: Expression). - Definition bits := Input.bits. - Definition inputs := Input.inputs. - Definition ResultType := Input.ResultType. - - Hint Unfold bits inputs ResultType. - Definition width: Width bits := Input.width. - - Definition W: Type := word bits. - Definition R: Type := option RangeWithValue. - Definition B: Type := option (@BoundedWord bits). - - Instance ZEvaluable : Evaluable Z := ZEvaluable. - Instance WEvaluable : Evaluable W := @WordEvaluable bits. - Instance REvaluable : Evaluable R := @RWVEvaluable bits. - Instance BEvaluable : Evaluable B := @BoundedEvaluable bits. - - Existing Instances ZEvaluable WEvaluable REvaluable BEvaluable. - - Module Util. - Fixpoint applyProgOn {A B k} (d: A) ins (f: NAry k A B): B := - match k as k' return NAry k' A B -> B with - | O => id - | S m => fun f' => - match ins with - | cons x xs => @applyProgOn A B m d xs (f' x) - | nil => @applyProgOn A B m d nil (f' d) - end - end f. - End Util. - - Module HL. - Definition progZ: NAry inputs Z (@HL.Expr Z ResultType) := - Input.prog. - - Definition progR: NAry inputs Z (@HL.Expr R ResultType) := - liftN (fun x v => @HLConversions.convertExpr Z R _ _ _ (x v)) Input.prog. - - Definition progW: NAry inputs Z (@HL.Expr W ResultType) := - liftN (fun x v => @HLConversions.convertExpr Z W _ _ _ (x v)) Input.prog. - End HL. - - Module LL. - Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) := - liftN CompileHL.Compile HL.progZ. - - Definition progR: NAry inputs Z (@LL.expr R R ResultType) := - liftN CompileHL.Compile HL.progR. - - Definition progW: NAry inputs Z (@LL.expr W W ResultType) := - liftN CompileHL.Compile HL.progW. - End LL. - - Module AST. - Definition progZ: NAry inputs Z (@interp_type Z ResultType) := - liftN LL.interp LL.progZ. - - Definition progR: NAry inputs Z (@interp_type R ResultType) := - liftN LL.interp LL.progR. - - Definition progW: NAry inputs Z (@interp_type W ResultType) := - liftN LL.interp LL.progW. - End AST. - - Module Qhasm. - Definition pair := - @CompileLL.compile bits width ResultType _ LL.progW. - - Definition prog := option_map (@fst _ _) pair. - - Definition outputRegisters := option_map (@snd _ _) pair. - - Definition code := option_map StringConversion.convertProgram prog. - End Qhasm. - - Module Bounds. - Definition input := map (fun x => range N 0%N (Z.to_N x)) Input.inputBounds. - - Definition upper := Z.of_N (wordToN (wones bits)). - - Definition prog := - Util.applyProgOn upper Input.inputBounds LL.progR. - - Definition valid := LLConversions.check (n := bits) (f := id) prog. - - Definition output := - typeMap (option_map (fun x => range N (rwv_low x) (rwv_high x))) - (LL.interp prog). - End Bounds. -End Pipeline. - -Module SimpleExample. - Module SimpleExpression <: Expression. - Import ListNotations. - - Definition bits: nat := 32. - Definition width: Width bits := W32. - Definition inputs: nat := 1. - Definition ResultType := TT. - - Definition inputBounds: list Z := [ (2^30)%Z ]. - - Existing Instance ZEvaluable. - - Definition prog: NAry 1 Z (@HL.Expr Z TT). - intros x var. - refine (HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)). - Defined. - End SimpleExpression. - - Module SimplePipeline := Pipeline SimpleExpression. -End SimpleExample. diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v deleted file mode 100644 index 9e376f71b..000000000 --- a/src/Assembly/Qhasm.v +++ /dev/null @@ -1,81 +0,0 @@ -Require Import QhasmCommon QhasmEvalCommon. -Require Import List NPeano. - -Module Qhasm. - Import ListNotations. - Import QhasmEval. - - Definition State := State. - - (* Program Types *) - Inductive QhasmStatement := - | QAssign: Assignment -> QhasmStatement - | QOp: Operation -> QhasmStatement - | QCond: Conditional -> Label -> QhasmStatement - | QLabel: Label -> QhasmStatement - | QCall: Label -> QhasmStatement - | QRet: QhasmStatement. - - Hint Constructors QhasmStatement. - - Definition Program := list QhasmStatement. - - (* Only execute while loops a fixed number of times. - TODO (rsloan): can we do any better? *) - - Fixpoint getLabelMap' (prog: Program) (cur: LabelMap) (index: nat): LabelMap := - match prog with - | p :: ps => - match p with - | QLabel label => @getLabelMap' ps (NatM.add label index cur) (S index) - | _ => @getLabelMap' ps cur (S index) - end - | [] => cur - end. - - Definition getLabelMap (prog: Program): LabelMap := - getLabelMap' prog (NatM.empty nat) O. - - Inductive QhasmEval: nat -> Program -> LabelMap -> State -> State -> Prop := - | QEOver: forall p n m s, (n > (length p))%nat -> QhasmEval n p m s s - | QEZero: forall p s m, QhasmEval O p m s s - | QEAssign: forall n p m a s s' s'', - (nth_error p n) = Some (QAssign a) - -> evalAssignment a s = Some s' - -> QhasmEval (S n) p m s' s'' - -> QhasmEval n p m s s'' - | QEOp: forall n p m a s s' s'', - (nth_error p n) = Some (QOp a) - -> evalOperation a s = Some s' - -> QhasmEval (S n) p m s' s'' - -> QhasmEval n p m s s'' - | QECondTrue: forall (n loc next: nat) p m c l s s', - (nth_error p n) = Some (QCond c l) - -> evalCond c s = Some true - -> NatM.find l m = Some loc - -> QhasmEval loc p m s s' - -> QhasmEval n p m s s' - | QECondFalse: forall (n loc next: nat) p m c l s s', - (nth_error p n) = Some (QCond c l) - -> evalCond c s = Some false - -> QhasmEval (S n) p m s s' - -> QhasmEval n p m s s' - | QERet: forall (n n': nat) s s' s'' p m, - (nth_error p n) = Some QRet - -> popRet s = Some (s', n') - -> QhasmEval n' p m s' s'' - -> QhasmEval n p m s s'' - | QECall: forall (w n n' lbl: nat) s s' s'' p m, - (nth_error p n) = Some (QCall lbl) - -> NatM.find lbl m = Some n' - -> QhasmEval n' p m (pushRet (S n) s') s'' - -> QhasmEval n p m s s'' - | QELabel: forall n p m l s s', - (nth_error p n) = Some (QLabel l) - -> QhasmEval (S n) p m s s' - -> QhasmEval n p m s s'. - - Definition evaluatesTo := fun p => @QhasmEval O p (getLabelMap p). - - (* world peace *) -End Qhasm. diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v deleted file mode 100644 index dfb080e8c..000000000 --- a/src/Assembly/QhasmCommon.v +++ /dev/null @@ -1,149 +0,0 @@ -Require Export Coq.Strings.String Coq.Lists.List Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. -Require Export Bedrock.Word. - -(* Utilities *) -Definition Label := nat. - -Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}. -Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. - -Fixpoint NAry (n: nat) (A: Type) (B: Type): Type := - match n with - | (S m) => A -> NAry m A B - | O => B - end. - -Fixpoint liftN {n A B C} (f: B -> C) (x: NAry n A B) {struct n}: NAry n A C := - match n as n' return NAry n' A B -> NAry n' A C with - | S m => fun x' => (fun arg => liftN f (x' arg)) - | O => f - end x. - -Fixpoint NArgMap {n A B C} (f: A -> B) (x: NAry n B C) {struct n}: NAry n A C := - match n as n' return NAry n' B C -> NAry n' A C with - | S m => fun x' => (fun arg => NArgMap f (x' (f arg))) - | O => id - end x. - -Inductive Either A B := - | xleft: A -> Either A B - | xright: B -> Either A B. - -Definition convert {A B: Type} (x: A) (H: A = B): B := - eq_rect A (fun B0 : Type => B0) x B H. - -(* Asm Types *) -Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64. - -(* A constant value *) -Inductive Const: nat -> Type := - | constant: forall {n}, Width n -> word n -> Const n. - -(* A variable in any register *) -Inductive Reg: nat -> Type := - | reg: forall {n}, Width n -> nat -> Reg n. - -(* A variable on the stack. We should use this sparingly. *) -Inductive Stack: nat -> Type := - | stack: forall {n}, Width n -> nat -> Stack n. - -(* A pointer to a memory block. Called as: - mem width index length - where length is in words of size width. - - All Mem pointers will be declared as Stack arguments in the - resulting qhasm output *) -Inductive Mem: nat -> nat -> Type := - | mem: forall {n m}, Width n -> nat -> Mem n m. - -(* The state of the carry flag: - 1 = Some true - 0 = Some false - unknown = None *) -Definition Carry := option bool. - -(* Assignments *) - -Inductive Assignment : Type := - | ARegMem: forall {n m}, Reg n -> Mem n m -> Index m -> Assignment - | AMemReg: forall {n m}, Mem n m -> Index m -> Reg n -> Assignment - | AStackReg: forall {n}, Stack n -> Reg n -> Assignment - | ARegStack: forall {n}, Reg n -> Stack n -> Assignment - | ARegReg: forall {n}, Reg n -> Reg n -> Assignment - | AConstInt: forall {n}, Reg n -> Const n -> Assignment. - -(* Operations *) - -Inductive IntOp := - | IAdd: IntOp - | ISub: IntOp - | IXor: IntOp - | IAnd: IntOp - | IOr: IntOp. - -Inductive CarryOp := | AddWithCarry: CarryOp. - -Inductive DualOp := | Mult: DualOp. - -Inductive RotOp := | Shl: RotOp | Shr: RotOp. - -Inductive Operation := - | IOpConst: forall {n}, IntOp -> Reg n -> Const n -> Operation - | IOpReg: forall {n}, IntOp -> Reg n -> Reg n -> Operation - | IOpMem: forall {n m}, IntOp -> Reg n -> Mem n m -> Index m -> Operation - | IOpStack: forall {n}, IntOp -> Reg n -> Stack n -> Operation - | DOp: forall {n}, DualOp -> Reg n -> Reg n -> option (Reg n) -> Operation - | ROp: forall {n}, RotOp -> Reg n -> Index n -> Operation - | COp: forall {n}, CarryOp -> Reg n -> Reg n -> Operation. - -(* Control Flow *) - -Inductive TestOp := - | TEq: TestOp | TLt: TestOp | TLe: TestOp - | TGt: TestOp | TGe: TestOp. - -Inductive Conditional := - | CTrue: Conditional - | CZero: forall n, Reg n -> Conditional - | CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional - | CConst: forall n, TestOp -> Reg n -> Const n -> Conditional. - -(* Generalized Variable Entry *) - -Inductive Mapping (n: nat) := - | regM: forall (r: Reg n), Mapping n - | stackM: forall (s: Stack n), Mapping n - | memM: forall {m} (x: Mem n m) (i: Index m), Mapping n - | constM: forall (x: Const n), Mapping n. - -(* Parameter Accessors *) - -Definition constWidth {n} (x: Const n): nat := n. - -Definition regWidth {n} (x: Reg n): nat := n. - -Definition stackWidth {n} (x: Stack n): nat := n. - -Definition memWidth {n m} (x: Mem n m): nat := n. - -Definition memLength {n m} (x: Mem n m): nat := m. - -Definition constValueW {n} (x: Const n): word n := - match x with | @constant n _ v => v end. - -Definition constValueN {n} (x: Const n): nat := - match x with | @constant n _ v => wordToNat v end. - -Definition regName {n} (x: Reg n): nat := - match x with | @reg n _ v => v end. - -Definition stackName {n} (x: Stack n): nat := - match x with | @stack n _ v => v end. - -Definition memName {n m} (x: Mem n m): nat := - match x with | @mem n m _ v => v end. - -(* Hints *) -Hint Constructors - Reg Stack Const Mem Mapping - Assignment Operation Conditional. diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v deleted file mode 100644 index 9760dc869..000000000 --- a/src/Assembly/QhasmEvalCommon.v +++ /dev/null @@ -1,299 +0,0 @@ -Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. -Require Import Coq.ZArith.ZArith Coq.Bool.Sumbool. -Require Import Bedrock.Word. -Require Import Coq.Logic.Eqdep_dec Coq.Logic.ProofIrrelevance. -Require Export Crypto.Util.FixCoqMistakes. - -Module EvalUtil. - Definition evalTest {n} (o: TestOp) (a b: word n): bool := - let c := (N.compare (wordToN a) (wordToN b)) in - - let eqBit := match c with | Eq => true | _ => false end in - let ltBit := match c with | Lt => true | _ => false end in - let gtBit := match c with | Gt => true | _ => false end in - - match o with - | TEq => eqBit - | TLt => ltBit - | TLe => orb (eqBit) (ltBit) - | TGt => gtBit - | TGe => orb (eqBit) (gtBit) - end. - - Definition evalIntOp {b} (io: IntOp) (x y: word b) := - match io return (word b) * option bool with - | ISub => (wminus x y, None) - | IXor => (wxor x y, None) - | IAnd => (wand x y, None) - | IOr => (wor x y, None) - | IAdd => - let v := (wordToN x + wordToN y)%N in - let c := (overflows b (&x + &y)%N)%w in - - match c as c' return c' = c -> _ with - | right _ => fun _ => (NToWord b v, Some false) - | left _ => fun _ => (NToWord b v, Some true) - end eq_refl - end. - - Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool := - match io with - | AddWidthCarry => - let c' := (overflows b (&x + &y + (if c then 1 else 0))%N)%w in - let v := addWithCarry x y c in - - match c' as c'' return c' = c'' -> _ with - | right _ => fun _ => (v, false) - | left _ => fun _ => (v, true) - end eq_refl - end. - - Definition highBits {n} (m: nat) (x: word n) := snd (break m x). - - Definition multHigh {n} (x y: word n): word n. - refine (@extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y))); - abstract omega. - Defined. - - Definition evalDualOp {n} (duo: DualOp) (x y: word n) := - match duo with - | Mult => (x ^* y, multHigh x y) - end. - - Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) := - match ro with - | Shl => NToWord b (N.shiftl_nat (wordToN x) n) - | Shr => NToWord b (N.shiftr_nat (wordToN x) n) - end. - - (* Width decideability *) - - Definition getWidth (n: nat): option (Width n) := - match n with - | 32 => Some W32 - | 64 => Some W64 - | _ => None - end. - - Lemma getWidth_eq {n} (a: Width n): Some a = getWidth n. - Proof. induction a; unfold getWidth; simpl; intuition. Qed. - - Lemma width_eq {n} (a b: Width n): a = b. - Proof. - assert (Some a = Some b) as H by ( - replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition); - replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition); - intuition). - inversion H; intuition. - Qed. - - (* Mapping Conversions *) - - Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n := - constM _ (constant spec w). - - Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n := - regM _ r. - - Definition stackToM {n: nat} {spec: Width n} (s: Stack n): Mapping n := - stackM _ s. - - Definition constToM {n: nat} {spec: Width n} (c: Const n): Mapping n := - constM _ c. - - Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}. - refine (match (a, b) as p' return (a, b) = p' -> _ with - | (regM v, regM v') => fun _ => - if (Nat.eq_dec (regName v) (regName v')) - then left _ - else right _ - - | (stackM v, stackM v') => fun _ => - if (Nat.eq_dec (stackName v) (stackName v')) - then left _ - else right _ - - | (constM v, constM v') => fun _ => - if (Nat.eq_dec (constValueN v) (constValueN v')) - then left _ - else right _ - - | (memM _ v i, memM _ v' i') => fun _ => - if (Nat.eq_dec (memName v) (memName v')) - then if (Nat.eq_dec (memLength v) (memLength v')) - then if (Nat.eq_dec (proj1_sig i) (proj1_sig i')) - then left _ else right _ else right _ else right _ - - | _ => fun _ => right _ - end (eq_refl (a, b))); - try destruct v, v'; subst; - unfold regName, stackName, constValueN, memName, memLength in *; - repeat progress (try apply f_equal; subst; match goal with - (* Makeshift intuition *) - | [ |- ?x = ?x ] => reflexivity - | [ H: ?x <> ?x |- _ ] => destruct H - | [ |- ?x = ?y ] => apply proof_irrelevance - - (* Destruct the widths *) - | [ w0: Width ?x, w1: Width ?x |- _ ] => - let H := fresh in - assert (w0 = w1) as H by (apply width_eq); - rewrite H in *; - clear w0 H - - (* Invert <> *) - | [ |- regM _ _ <> _ ] => let H := fresh in (intro H; inversion H) - | [ |- memM _ _ _ <> _ ] => let H := fresh in (intro H; inversion H) - | [ |- stackM _ _ <> _ ] => let H := fresh in (intro H; inversion H) - | [ |- constM _ _ <> _ ] => let H := fresh in (intro H; inversion H) - - (* Invert common structures *) - | [ H: regName _ = regName _ |- _ ] => inversion_clear H - | [ H: (_, _) = _ |- _ ] => inversion_clear H - | [ H: ?x = _ |- _ ] => is_var x; rewrite H in *; clear H - - (* Destruct sigmas, exist, existT *) - | [ H: proj1_sig ?a = proj1_sig ?b |- _ ] => - let l0 := fresh in let l1 := fresh in - destruct a, b; simpl in H; subst - | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] => - let l0 := fresh in let l1 := fresh in - destruct a, b; simpl in H; subst - | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => - apply (inj_pair2_eq_dec _ Nat.eq_dec) in H; - subst; intuition - | [ H: exist _ _ _ = exist _ _ _ |- _ ] => - inversion H; subst; intuition - - (* Single specialized wordToNat proof *) - | [ H: wordToNat ?a = wordToNat ?b |- ?a = ?b] => - rewrite <- (natToWord_wordToNat a); - rewrite <- (natToWord_wordToNat b); - rewrite H; reflexivity - - | _ => idtac - end). - Defined. - - Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}. - assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true}) - by abstract (destruct (a <? b)%nat; intuition auto with bool); - destruct H. - - - left; abstract (apply Nat.ltb_lt; intuition). - - - right; abstract (rewrite Nat.ltb_lt in *; intuition auto with zarith). - Defined. - - Fixpoint stackNames {n} (lst: list (Mapping n)): list nat := - match lst with - | nil => nil - | cons c cs => - match c with - | stackM v => cons (stackName v) (stackNames cs) - | _ => stackNames cs - end - end. - - Fixpoint regNames {n} (lst: list (Mapping n)): list nat := - match lst with - | nil => nil - | cons c cs => - match c with - | regM v => cons (regName v) (regNames cs) - | _ => regNames cs - end - end. - -End EvalUtil. - -Module QhasmEval. - Export EvalUtil FullState. - - Definition evalCond (c: Conditional) (state: State): option bool := - match c with - | CTrue => Some true - | CZero n r => - omap (getReg r state) (fun v => - if (Nat.eq_dec O (wordToNat v)) - then Some true - else Some false) - | CReg n o a b => - omap (getReg a state) (fun va => - omap (getReg b state) (fun vb => - Some (evalTest o va vb))) - | CConst n o a c => - omap (getReg a state) (fun va => - Some (evalTest o va (constValueW c))) - end. - - Definition evalOperation (o: Operation) (state: State): option State := - match o with - | IOpConst _ o r c => - omap (getReg r state) (fun v => - let (v', co) := (evalIntOp o v (constValueW c)) in - Some (setCarryOpt co (setReg r v' state))) - - | IOpReg _ o a b => - omap (getReg a state) (fun va => - omap (getReg b state) (fun vb => - let (v', co) := (evalIntOp o va vb) in - Some (setCarryOpt co (setReg a v' state)))) - - | IOpStack _ o a b => - omap (getReg a state) (fun va => - omap (getStack b state) (fun vb => - let (v', co) := (evalIntOp o va vb) in - Some (setCarryOpt co (setReg a v' state)))) - - | IOpMem _ _ o r m i => - omap (getReg r state) (fun va => - omap (getMem m i state) (fun vb => - let (v', co) := (evalIntOp o va vb) in - Some (setCarryOpt co (setReg r v' state)))) - - | DOp _ o a b (Some x) => - omap (getReg a state) (fun va => - omap (getReg b state) (fun vb => - let (low, high) := (evalDualOp o va vb) in - Some (setReg x high (setReg a low state)))) - - | DOp _ o a b None => - omap (getReg a state) (fun va => - omap (getReg b state) (fun vb => - let (low, high) := (evalDualOp o va vb) in - Some (setReg a low state))) - - | ROp _ o r i => - omap (getReg r state) (fun v => - let v' := (evalRotOp o v i) in - Some (setReg r v' state)) - - | COp _ o a b => - omap (getReg a state) (fun va => - omap (getReg b state) (fun vb => - match (getCarry state) with - | None => None - | Some c0 => - let (v', c') := (evalCarryOp o va vb c0) in - Some (setCarry c' (setReg a v' state)) - end)) - end. - - Definition evalAssignment (a: Assignment) (state: State): option State := - match a with - | ARegMem _ _ r m i => - omap (getMem m i state) (fun v => Some (setReg r v state)) - | AMemReg _ _ m i r => - omap (getReg r state) (fun v => Some (setMem m i v state)) - | AStackReg _ a b => - omap (getReg b state) (fun v => Some (setStack a v state)) - | ARegStack _ a b => - omap (getStack b state) (fun v => Some (setReg a v state)) - | ARegReg _ a b => - omap (getReg b state) (fun v => Some (setReg a v state)) - | AConstInt _ r c => - Some (setReg r (constValueW c) state) - end. - -End QhasmEval. diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v deleted file mode 100644 index b7dd90da6..000000000 --- a/src/Assembly/QhasmUtil.v +++ /dev/null @@ -1,91 +0,0 @@ -Require Import ZArith NArith NPeano. -Require Import QhasmCommon. -Require Export Bedrock.Word Bedrock.Nomega. - -Delimit Scope nword_scope with w. -Local Open Scope nword_scope. - -Notation "& x" := (wordToN x) (at level 30) : nword_scope. -Notation "** x" := (NToWord _ x) (at level 30) : nword_scope. - -Section Util. - Definition convS {n m} (x: word n) (H: n = m): word m. - refine (eq_rect _ (fun B0 : Set => B0) x _ _). - abstract (subst; intuition). - Defined. - - Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k. - refine (split1 k (n - k) (convS w _)); abstract omega. - Defined. - - Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word (n - k). - refine (split2 k (n - k) (convS w _)); abstract omega. - Defined. - - Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n. - refine (convS (zext w (n - k)) _); abstract omega. - Defined. - - Definition shiftr {n} (w: word n) (k: nat): word n. - refine match (le_dec k n) with - | left p => extend _ (@high k _ _ w) - | right _ => wzero n - end; abstract nomega. - Defined. - - Definition mask {n} (k: nat) (w: word n): word n := - match (le_dec k n) with - | left p => extend p (low p w) - | right _ => w - end. - - Definition Nge_dec (x y: N) : - {(x >= y)%N} + {(x < y)%N}. - refine ( - let c := (x ?= y)%N in - match c as c' return c = c' -> _ with - | Lt => fun _ => right _ - | _ => fun _ => left _ - end eq_refl); abstract ( - unfold c in *; unfold N.lt, N.ge; - repeat match goal with - | [ H: (_ ?= _)%N = _ |- _] => - rewrite H; intuition; try inversion H - | [ H: Eq = _ |- _] => inversion H - | [ H: Gt = _ |- _] => inversion H - | [ H: Lt = _ |- _] => inversion H - end). - Defined. - - Definition overflows (n: nat) (x: N) := Nge_dec x (Npow2 n). - - Definition ind (b: bool): N := if b then 1%N else 0%N. - - Definition ind' {A B} (b: {A} + {B}): N := if b then 1%N else 0%N. - - Definition break {n} (m: nat) (x: word n): word m * word (n - m). - refine match (le_dec m n) with - | left p => (extend _ (low p x), extend _ (@high m n _ x)) - | right p => (extend _ x, extend _ WO) - end; try abstract intuition. - Defined. - - Definition addWithCarry {n} (x y: word n) (c: bool): word n := - x ^+ y ^+ (natToWord _ (if c then 1 else 0)). - - Definition omap {A B} (x: option A) (f: A -> option B) := - match x with - | Some y => f y - | _ => None - end. - - Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity). - - Definition orElse {T} (d: T) (o: option T): T := - match o with - | Some v => v - | None => d - end. -End Util. - -Close Scope nword_scope.
\ No newline at end of file diff --git a/src/Assembly/State.v b/src/Assembly/State.v deleted file mode 100644 index 3467a5cad..000000000 --- a/src/Assembly/State.v +++ /dev/null @@ -1,331 +0,0 @@ -Require Export Coq.Strings.String Coq.Lists.List Coq.Init.Logic. -Require Export Bedrock.Word. - -Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec. -Require Import Coq.Arith.Compare_dec Coq.omega.Omega. -Require Import Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx. -Require Import Coq.FSets.FMapPositive Coq.FSets.FMapFullAVL Coq.Logic.JMeq. - -Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmCommon. - -Require Export Crypto.Util.FixCoqMistakes. - -(* We want to use pairs and triples as map keys: *) - -Module Pair_as_OT <: UsualOrderedType. - Definition t := (nat * nat)%type. - - Definition eq := @eq t. - Definition eq_refl := @eq_refl t. - Definition eq_sym := @eq_sym t. - Definition eq_trans := @eq_trans t. - - Definition lt (a b: t) := - if (Nat.eq_dec (fst a) (fst b)) - then lt (snd a) (snd b) - else lt (fst a) (fst b). - - Lemma conv: forall {x0 x1 y0 y1: nat}, - (x0 = y0 /\ x1 = y1) <-> (x0, x1) = (y0, y1). - Proof. - intros; split; intros. - - destruct H; destruct H0; subst; intuition. - - inversion_clear H; intuition. - Qed. - - Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. - intros; destruct x as [x0 x1], y as [y0 y1], z as [z0 z1]; - unfold lt in *; simpl in *; - destruct (Nat.eq_dec x0 y0), (Nat.eq_dec y0 z0), (Nat.eq_dec x0 z0); - omega. - Qed. - - Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - intros; destruct x as [x0 x1], y as [y0 y1]; - unfold lt, eq in *; simpl in *; - destruct (Nat.eq_dec x0 y0); subst; intuition; - inversion H0; subst; omega. - Qed. - - Definition compare x y : Compare lt eq x y. - destruct x as [x0 x1], y as [y0 y1]; - destruct (Nat_as_OT.compare x0 y0); - unfold Nat_as_OT.lt, Nat_as_OT.eq in *. - - - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition auto with zarith). - - - destruct (Nat_as_OT.compare x1 y1); - unfold Nat_as_OT.lt, Nat_as_OT.eq in *. - - + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition). - + apply EQ; abstract (unfold lt; simpl; subst; intuition auto with relations). - + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). - - - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). - Defined. - - Definition eq_dec (a b: t): {a = b} + {a <> b}. - destruct (compare a b); - destruct a as [a0 a1], b as [b0 b1]. - - - right; abstract ( - unfold lt in *; simpl in *; - destruct (Nat.eq_dec a0 b0); intuition; - inversion H; intuition auto with zarith). - - - left; abstract (inversion e; intuition). - - - right; abstract ( - unfold lt in *; simpl in *; - destruct (Nat.eq_dec b0 a0); intuition; - inversion H; intuition auto with zarith). - Defined. -End Pair_as_OT. - -Module Triple_as_OT <: UsualOrderedType. - Definition t := (nat * nat * nat)%type. - - Definition get0 (x: t) := fst (fst x). - Definition get1 (x: t) := snd (fst x). - Definition get2 (x: t) := snd x. - - Definition eq := @eq t. - Definition eq_refl := @eq_refl t. - Definition eq_sym := @eq_sym t. - Definition eq_trans := @eq_trans t. - - Definition lt (a b: t) := - if (Nat.eq_dec (get0 a) (get0 b)) - then - if (Nat.eq_dec (get1 a) (get1 b)) - then lt (get2 a) (get2 b) - else lt (get1 a) (get1 b) - else lt (get0 a) (get0 b). - - Lemma conv: forall {x0 x1 x2 y0 y1 y2: nat}, - (x0 = y0 /\ x1 = y1 /\ x2 = y2) <-> (x0, x1, x2) = (y0, y1, y2). - Proof. - intros; split; intros. - - destruct H; destruct H0; subst; intuition. - - inversion_clear H; intuition. - Qed. - - Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. - intros; unfold lt in *; - destruct (Nat.eq_dec (get0 x) (get0 y)), - (Nat.eq_dec (get1 x) (get1 y)), - (Nat.eq_dec (get0 y) (get0 z)), - (Nat.eq_dec (get1 y) (get1 z)), - (Nat.eq_dec (get0 x) (get0 z)), - (Nat.eq_dec (get1 x) (get1 z)); - omega. - Qed. - - Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - intros; unfold lt, eq in *; - destruct (Nat.eq_dec (get0 x) (get0 y)), - (Nat.eq_dec (get1 x) (get1 y)); - subst; intuition; - inversion H0; subst; omega. - Qed. - - Ltac compare_tmp x y := - abstract ( - unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *; - destruct (Nat.eq_dec (get0 x) (get0 y)); - destruct (Nat.eq_dec (get1 x) (get1 y)); - simpl; intuition auto with zarith). - - Ltac compare_eq x y := - abstract ( - unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq, get0, get1 in *; - destruct x as [x x2], y as [y y2]; - destruct x as [x0 x1], y as [y0 y1]; - simpl in *; subst; intuition). - - Definition compare x y : Compare lt eq x y. - destruct (Nat_as_OT.compare (get0 x) (get0 y)). - - - apply LT; compare_tmp x y. - - destruct (Nat_as_OT.compare (get1 x) (get1 y)). - + apply LT; compare_tmp x y. - + destruct (Nat_as_OT.compare (get2 x) (get2 y)). - * apply LT; compare_tmp x y. - * apply EQ; compare_eq x y. - * apply GT; compare_tmp y x. - + apply GT; compare_tmp y x. - - apply GT; compare_tmp y x. - Defined. - - Definition eq_dec (a b: t): {a = b} + {a <> b}. - destruct (compare a b); - destruct a as [a a2], b as [b b2]; - destruct a as [a0 a1], b as [b0 b1]. - - - right; abstract ( - unfold lt, get0, get1, get2 in *; simpl in *; - destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1); - intuition; inversion H; intuition auto with zarith). - - - left; abstract (inversion e; intuition). - - - right; abstract ( - unfold lt, get0, get1, get2 in *; simpl in *; - destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1); - intuition; inversion H; intuition auto with zarith). - Defined. -End Triple_as_OT. - -Module StateCommon. - Export ListNotations. - - Module NatM := FMapFullAVL.Make(Nat_as_OT). - Module PairM := FMapFullAVL.Make(Pair_as_OT). - Module TripleM := FMapFullAVL.Make(Triple_as_OT). - - Definition NatNMap: Type := NatM.t N. - Definition PairNMap: Type := PairM.t N. - Definition TripleNMap: Type := TripleM.t N. - Definition LabelMap: Type := NatM.t nat. -End StateCommon. - -Module ListState. - Export StateCommon. - - Definition ListState (n: nat) := ((list (word n)) * TripleNMap * (option bool))%type. - - Definition emptyState {n}: ListState n := ([], TripleM.empty N, None). - - Definition getVar {n: nat} (name: nat) (st: ListState n): option (word n) := - nth_error (fst (fst st)) name. - - Definition getList {n: nat} (st: ListState n): list (word n) := - fst (fst st). - - Definition setList {n: nat} (lst: list (word n)) (st: ListState n): ListState n := - (lst, snd (fst st), snd st). - - Definition getMem {n: nat} (name index: nat) (st: ListState n): option (word n) := - omap (TripleM.find (n, name, index) (snd (fst st))) (fun v => Some (NToWord n v)). - - Definition setMem {n: nat} (name index: nat) (v: word n) (st: ListState n): ListState n := - (fst (fst st), TripleM.add (n, name, index) (wordToN v) (snd (fst st)), snd st). - - Definition getCarry {n: nat} (st: ListState n): option bool := (snd st). - - Definition setCarry {n: nat} (v: bool) (st: ListState n): ListState n := - (fst st, Some v). - - Definition setCarryOpt {n: nat} (v: option bool) (st: ListState n): ListState n := - match v with - | Some v' => (fst st, v) - | None => st - end. - -End ListState. - -Module FullState. - Export StateCommon. - - (* The Big Definition *) - - Inductive State := - | fullState (regState: PairNMap) - (stackState: PairNMap) - (memState: TripleNMap) - (retState: list nat) - (carry: Carry): State. - - Definition emptyState: State := - fullState (PairM.empty N) (PairM.empty N) (TripleM.empty N) [] None. - - (* Register *) - - Definition getReg {n} (r: Reg n) (state: State): option (word n) := - match state with - | fullState regS _ _ _ _ => - match (PairM.find (n, regName r) regS) with - | Some v => Some (NToWord n v) - | None => None - end - end. - - Definition setReg {n} (r: Reg n) (value: word n) (state: State): State := - match state with - | fullState regS stackS memS retS carry => - fullState (PairM.add (n, regName r) (wordToN value) regS) - stackS memS retS carry - end. - - (* Stack *) - - Definition getStack {n} (s: Stack n) (state: State): option (word n) := - match state with - | fullState _ stackS _ _ _ => - match (PairM.find (n, stackName s) stackS) with - | Some v => Some (NToWord n v) - | None => None - end - end. - - Definition setStack {n} (s: Stack n) (value: word n) (state: State): State := - match state with - | fullState regS stackS memS retS carry => - fullState regS - (PairM.add (n, stackName s) (wordToN value) stackS) - memS retS carry - end. - - (* Memory *) - - Definition getMem {n m} (x: Mem n m) (i: Index m) (state: State): option (word n) := - match state with - | fullState _ _ memS _ _ => - match (TripleM.find (n, memName x, proj1_sig i) memS) with - | Some v => Some (NToWord n v) - | None => None - end - end. - - Definition setMem {n m} (x: Mem n m) (i: Index m) (value: word n) (state: State): State := - match state with - | fullState regS stackS memS retS carry => - fullState regS stackS - (TripleM.add (n, memName x, proj1_sig i) (wordToN value) memS) - retS carry - end. - - (* Return Pointers *) - - Definition pushRet (x: nat) (state: State): State := - match state with - | fullState regS stackS memS retS carry => - fullState regS stackS memS (cons x retS) carry - end. - - Definition popRet (state: State): option (State * nat) := - match state with - | fullState regS stackS memS [] carry => None - | fullState regS stackS memS (r :: rs) carry => - Some (fullState regS stackS memS rs carry, r) - end. - - (* Carry State Manipulations *) - - Definition getCarry (state: State): Carry := - match state with - | fullState _ _ _ _ b => b - end. - - Definition setCarry (value: bool) (state: State): State := - match state with - | fullState regS stackS memS retS carry => - fullState regS stackS memS retS (Some value) - end. - - Definition setCarryOpt (value: option bool) (state: State): State := - match value with - | Some c' => setCarry c' state - | _ => state - end. -End FullState. diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v deleted file mode 100644 index f1ec58dca..000000000 --- a/src/Assembly/StringConversion.v +++ /dev/null @@ -1,367 +0,0 @@ -Require Export Coq.Strings.String Coq.Strings.Ascii Coq.Program.Basics Coq.Bool.Sumbool. -Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Qhasm. -Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano. -Require Export Bedrock.Word. - -Module StringConversion. - Import Qhasm ListNotations. - - Section Hex. - Local Open Scope string_scope. - - Definition natToDigit (n : nat) : string := - match n with - | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" - | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7" - | 8 => "8" | 9 => "9" | 10 => "A" | 11 => "B" - | 12 => "C" | 13 => "D" | 14 => "E" | _ => "F" - end. - - Fixpoint nToHex' (n: N) (digitsLeft: nat): string := - match digitsLeft with - | O => "" - | S nextLeft => - match n with - | N0 => "0" - | _ => (nToHex' (N.shiftr_nat n 4) nextLeft) ++ - (natToDigit (N.to_nat (N.land n 15%N))) - end - end. - - Definition nToHex (n: N): string := - let size := (N.size n) in - let div4 := fun x => (N.shiftr x 2%N) in - let size' := (size + 4 - (N.land size 3))%N in - nToHex' n (N.to_nat (div4 size')). - - End Hex. - - Section Elements. - Local Open Scope string_scope. - - Definition nameSuffix (n: nat): string := - (nToHex (N.of_nat n)). - - Coercion wordToString {n} (w: word n): string := - "0x" ++ (nToHex (wordToN w)). - - Coercion constToString {n} (c: Const n): string := - match c with | constant _ _ w => wordToString w end. - - Coercion regToString {n} (r: Reg n): string := - match r with - | reg _ W32 n => "w" ++ (nameSuffix n) - | reg _ W64 n => "d" ++ (nameSuffix n) - end. - - Coercion natToString (n: nat): string := - "0x" ++ (nToHex (N.of_nat n)). - - Coercion stackToString {n} (s: Stack n): string := - match s with - | stack _ W32 n => "ws" ++ (nameSuffix n) - | stack _ W64 n => "ds" ++ (nameSuffix n) - end. - - Coercion memToString {n m} (s: Mem n m): string := - match s with - | mem _ _ W32 v => "wm" ++ (nameSuffix v) - | mem _ _ W64 v => "dm" ++ (nameSuffix v) - end. - - Coercion stringToSome (x: string): option string := Some x. - - Definition stackLocation {n} (s: Stack n): word 32 := - combine (natToWord 8 n) (natToWord 24 n). - - Definition assignmentToString (a: Assignment): option string := - let f := fun x => if (Nat.eq_dec x 32) then "32" else "64" in - match a with - | ARegStack n r s => r ++ " = *(int" ++ f n ++ " *)" ++ s - | AStackReg n s r => "*(int" ++ f n ++ " *) " ++ s ++ " = " ++ r - | ARegMem n m r v i => r ++ " = " ++ "*(int" ++ f n ++ " *) (" ++ v ++ " + " ++ i ++ ")" - | AMemReg n m v i r => "*(int" ++ f n ++ " *) (" ++ v ++ " + " ++ i ++ ") = " ++ r - | ARegReg n a b => a ++ " = " ++ b - | AConstInt n r c => r ++ " = " ++ c - end. - - Coercion intOpToString (b: IntOp): string := - match b with - | IAdd => "+" - | ISub => "-" - | IXor => "^" - | IAnd => "&" - | IOr => "|" - end. - - Coercion dualOpToString (b: DualOp): string := - match b with - | Mult => "*" - end. - - Coercion carryOpToString (b: CarryOp): string := - match b with - | AddWithCarry => "+" - end. - - Coercion rotOpToString (r: RotOp): string := - match r with - | Shl => "<<" - | Shr => ">>" - end. - - Definition operationToString (op: Operation): option string := - let f := fun x => ( - if (Nat.eq_dec x 32) - then "32" - else if (Nat.eq_dec x 64) - then "64" - else "128") in - - match op with - | IOpConst n o r c => - r ++ " " ++ o ++ "= " ++ c - | IOpReg n o a b => - a ++ " " ++ o ++ "= " ++ b - | IOpMem n _ o a b i => - a ++ " " ++ o ++ "= *(int" ++ (f n) ++ "* " ++ b ++ " + " ++ i ++ ")" - | IOpStack n o a b => - a ++ " " ++ o ++ "= " ++ b - | DOp n o a b x => - match x with - | Some r => - "(int" ++ (f (2 * n)) ++ ") " ++ r ++ " " ++ a ++ " " ++ o ++ "= " ++ b - | None => a ++ " " ++ o ++ "= " ++ b - end - | COp n o a b => - a ++ " " ++ o ++ "= " ++ b - | ROp n o r i => - r ++ " " ++ o ++ "= " ++ i - end. - - Definition testOpToString (t: TestOp): bool * string := - match t with - | TEq => (true, "=") - | TLt => (true, "<") - | TGt => (true, ">") - | TLe => (false, ">") - | TGe => (false, "<") - end. - - Definition conditionalToString (c: Conditional): string * string := - match c with - | CTrue => ("=? 0", "=") - | CZero n r => ("=? " ++ r, "=") - | CReg n t a b => - match (testOpToString t) with - | (true, s) => - (s ++ "? " ++ a ++ " - " ++ b, s) - | (false, s) => - (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s) - end - - | CConst n t a b => - match (testOpToString t) with - | (true, s) => - (s ++ "? " ++ a ++ " - " ++ b, s) - | (false, s) => - (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s) - end - end. - - End Elements. - - Section Parsing. - Definition convM {n m} (x: list (Mapping n)): list (Mapping m). - destruct (Nat.eq_dec n m); subst. exact x. exact []. - Defined. - - Arguments regM [n] r. - Arguments stackM [n] s. - Arguments memM [n m] x i. - Arguments constM [n] x. - - Fixpoint entries (width: nat) (prog: list QhasmStatement): list (Mapping width) := - match prog with - | cons s next => - match s with - | QAssign a => - match a with - | ARegStack n r s => convM [regM r; stackM s] - | AStackReg n s r => convM [regM r; stackM s] - | ARegMem n m a b i => convM [regM a; memM b i] - | AMemReg n m a i b => convM [memM a i; regM b] - | ARegReg n a b => convM [regM a; regM b] - | AConstInt n r c => convM [regM r; constM c] - end - | QOp o => - match o with - | IOpConst _ o a c => convM [regM a; constM c] - | IOpReg _ o a b => convM [regM a; regM b] - | IOpStack _ o a b => convM [regM a; stackM b] - | IOpMem _ _ o a b i => convM [regM a; memM b i] - | DOp _ o a b (Some x) => convM [regM a; regM b; regM x] - | DOp _ o a b None => convM [regM a; regM b] - | ROp _ o a i => convM [regM a] - | COp _ o a b => convM [regM a; regM b] - end - | QCond c _ => - match c with - | CTrue => [] - | CZero n r => convM [regM r] - | CReg n o a b => convM [regM a; regM b] - | CConst n o a c => convM [regM a; constM c] - end - | _ => [] - end ++ (entries width next) - | nil => nil - end. - - Definition flatMapOpt {A B} (lst: list A) (f: A -> option B): list B := - fold_left - (fun lst a => match (f a) with | Some x => cons x lst | _ => lst end) - lst []. - - Definition flatMapList {A B} (lst: list A) (f: A -> list B): list B := - fold_left (fun lst a => lst ++ (f a)) lst []. - - Fixpoint dedup {n} (l : list (Mapping n)) : list (Mapping n) := - match l with - | [] => [] - | x::xs => - if in_dec EvalUtil.mapping_dec x xs - then dedup xs - else x::(dedup xs) - end. - - Definition getRegNames (n: nat) (lst: list (Mapping n)): list nat := - flatMapOpt (dedup lst) (fun e => - match e with | regM (reg _ _ x) => Some x | _ => None end). - - Definition getStackNames (n: nat) (lst: list (Mapping n)): list nat := - flatMapOpt (dedup lst) (fun e => - match e with | stackM (stack _ _ x) => Some x | _ => None end). - - Definition getMemNames (n: nat) (lst: list (Mapping n)): list nat := - flatMapOpt (dedup lst) (fun e => - match e with | memM _ (mem _ _ _ x) _ => Some x | _ => None end). - - Fixpoint getInputs' (n: nat) (prog: list QhasmStatement) (init: list (Mapping n)): list (Mapping n) := - let f := fun rs => filter (fun x => - negb (proj1_sig (bool_of_sumbool (in_dec EvalUtil.mapping_dec x init)))) rs in - let g := fun {w} p => (@convM w n (fst p), @convM w n (snd p)) in - match prog with - | [] => [] - | cons p ps => - let requiredCommaUsed := match p with - | QAssign a => - match a with - | ARegStack n r s => g ([stackM s], [regM r; stackM s]) - | AStackReg n s r => g ([regM r], [regM r; stackM s]) - | ARegMem n m r x i => g ([memM x i], [regM r; memM x i]) - | AMemReg n m x i r => g ([regM r], [regM r; memM x i]) - | ARegReg n a b => g ([regM b], [regM a; regM b]) - | AConstInt n r c => g ([], [regM r]) - end - | QOp o => - match o with - | IOpConst _ o a c => g ([regM a], [regM a]) - | IOpReg _ o a b => g ([regM a], [regM a; regM b]) - | IOpStack _ o a b => g ([regM a], [regM a; stackM b]) - | IOpMem _ _ o a b i => g ([regM a], [regM a; memM b i]) - | DOp _ o a b (Some x) => g ([regM a; regM b], [regM a; regM b; regM x]) - | DOp _ o a b None => g ([regM a; regM b], [regM a; regM b]) - | ROp _ o a i => g ([regM a], [regM a]) - | COp _ o a b => g ([regM a], [regM a; regM b]) - end - | QCond c _ => - match c with - | CTrue => ([], []) - | CZero n r => g ([], [regM r]) - | CReg n o a b => g ([], [regM a; regM b]) - | CConst n o a c => g ([], [regM a]) - end - | _ => ([], []) - end in match requiredCommaUsed with - | (r, u) => ((f r) ++ (getInputs' n ps ((f u) ++ init))) - end - end. - - Definition getInputs (n: nat) (prog: list QhasmStatement) := getInputs' n prog []. - - Definition mappingDeclaration {n} (x: Mapping n): option string := - match x with - | regM (reg _ w x) => - match w with - | W32 => Some ("int32 " ++ (reg w x))%string - | W64 => Some ("int64 " ++ (reg w x))%string - end - - | stackM (stack _ w x) => - match w with - | W32 => Some ("stack32 " ++ (stack w x))%string - | W64 => Some ("stack64 " ++ (stack w x))%string - end - - | memM _ (mem _ m w x) _ => - match w with - | W32 => Some ("stack32 " ++ (@mem _ m w x))%string - | W64 => Some ("stack64 " ++ (@mem _ m w x))%string - end - - | _ => None - end. - - Definition inputDeclaration {n} (x: Mapping n): option string := - match x with - | regM r => Some ("input " ++ r)%string - | stackM s => Some ("input " ++ s)%string - | memM _ m i => Some ("input " ++ m)%string - | _ => None - end. - - End Parsing. - - (* Macroscopic Conversion Methods *) - Definition optionToList {A} (o: option A): list A := - match o with - | Some a => [a] - | None => [] - end. - - Definition convertStatement (statement: QhasmStatement): list string := - match statement with - | QAssign a => optionToList (assignmentToString a) - | QOp o => optionToList (operationToString o) - | QCond c l => - match (conditionalToString c) with - | (s1, s2) => - let s' := ("goto lbl" ++ l ++ " if " ++ s2)%string in - [s1; s'] - end - | QLabel l => [("lbl" ++ l ++ ": ")%string] - | QCall l => [("push %eip+2")%string; ("goto" ++ l)%string] - | QRet => [("pop %eip")%string] - end. - - Definition convertProgram (prog: Qhasm.Program): option string := - let decls := fun x => flatMapList (dedup (entries x prog)) - (compose optionToList mappingDeclaration) in - - let inputs := fun x => flatMapList (getInputs x prog) - (compose optionToList inputDeclaration) in - - let stmts := (flatMapList prog convertStatement) in - let enter := [("enter prog")%string] in - let leave := [("leave")%string] in - let blank := [EmptyString] in - let newline := String (ascii_of_nat 10) EmptyString in - - Some (fold_left (fun x y => (x ++ newline ++ y)%string) - (decls 32 ++ inputs 32 ++ - decls 64 ++ inputs 64 ++ blank ++ - enter ++ blank ++ - stmts ++ blank ++ - leave ++ blank) EmptyString). - -End StringConversion. diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v deleted file mode 100644 index b5f246fb1..000000000 --- a/src/Assembly/WordizeUtil.v +++ /dev/null @@ -1,996 +0,0 @@ -Require Import Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec. -Require Import List Omega NArith Nnat BoolEq Compare_dec. -Require Import SetoidTactics. -Require Import ProofIrrelevance FunctionalExtensionality. -Require Import QhasmUtil QhasmEvalCommon. - -(* Custom replace-at wrapper for 8.4pl3 compatibility *) -Definition ltac_nat_from_int (x:BinInt.Z) : nat := - match x with - | BinInt.Z0 => 0%nat - | BinInt.Zpos p => BinPos.nat_of_P p - | BinInt.Zneg p => 0%nat - end. - -Ltac nat_from_number N := - match type of N with - | nat => constr:(N) - | BinInt.Z => let N' := constr:(ltac_nat_from_int N) in eval compute in N' - end. - -Tactic Notation "replace'" constr(x) "with" constr(y) "at" constr(n) "by" tactic(tac) := - let tmp := fresh in ( - match nat_from_number n with - | 1 => set (tmp := x) at 1 - | 2 => set (tmp := x) at 2 - | 3 => set (tmp := x) at 3 - | 4 => set (tmp := x) at 4 - | 5 => set (tmp := x) at 5 - end; - replace tmp with y by (unfold tmp; tac); - clear tmp). - -(* Word-shattering tactic *) -Ltac shatter a := - let H := fresh in - pose proof (shatter_word a) as H; simpl in H; - try rewrite H in *; clear H. - -Section Misc. - Local Open Scope nword_scope. - - Lemma word_replace: forall n m, n = m -> word n = word m. - Proof. intros; subst; intuition. Qed. - - Lemma of_nat_lt: forall x b, (x < b)%nat <-> (N.of_nat x < N.of_nat b)%N. - Proof. - intros x b; split; intro H. - - - unfold N.lt; rewrite N2Nat.inj_compare. - repeat rewrite Nat2N.id. - apply nat_compare_lt in H. - intuition. - - - unfold N.lt in H; rewrite N2Nat.inj_compare in H. - repeat rewrite Nat2N.id in H. - apply nat_compare_lt in H. - intuition. - Qed. - - Lemma to_nat_lt: forall x b, (x < b)%N <-> (N.to_nat x < N.to_nat b)%nat. - Proof. - intros x b; split; intro H. - - - unfold N.lt in H; rewrite N2Nat.inj_compare in H. - apply nat_compare_lt in H. - intuition. - - - unfold N.lt; rewrite N2Nat.inj_compare. - apply nat_compare_lt. - intuition. - Qed. - - Lemma to_nat_le: forall x b, (x <= b)%N <-> (N.to_nat x <= N.to_nat b)%nat. - Proof. - intros x b; split; intro H. - - - unfold N.le in H; rewrite N2Nat.inj_compare in H. - apply nat_compare_le in H. - intuition. - - - unfold N.le; rewrite N2Nat.inj_compare. - apply nat_compare_le. - intuition. - Qed. - - Lemma word_size_bound : forall {n} (w: word n), (&w < Npow2 n)%N. - Proof. - intros; pose proof (wordToNat_bound w) as B; - rewrite of_nat_lt in B; - rewrite <- Npow2_nat in B; - rewrite N2Nat.id in B; - rewrite <- wordToN_nat in B; - assumption. - Qed. - - Lemma ge_to_le: forall (x y: N), (x >= y)%N <-> (y <= x)%N. - Proof. - intros x y; split; intro H; - unfold N.ge, N.le in *; - intro H0; contradict H; - rewrite N.compare_antisym; - rewrite H0; simpl; intuition. - Qed. - - Lemma N_ge_0: forall x: N, (0 <= x)%N. - Proof. - intro x0; unfold N.le. - pose proof (N.compare_0_r x0) as H. - rewrite N.compare_antisym in H. - induction x0; simpl in *; - intro V; inversion V. - Qed. - - Lemma Pos_ge_1: forall p, (1 <= N.pos p)%N. - Proof. - intro. - replace (N.pos p) with (N.succ (N.pos p - 1)%N) by ( - induction p; simpl; - try rewrite Pos.succ_pred_double; - try reflexivity). - unfold N.succ. - apply N.le_pred_le_succ. - replace (N.pred 1%N) with 0%N by (simpl; intuition). - apply N_ge_0. - Qed. - - Lemma testbit_wones_false: forall n k, - (k >= N.of_nat n)%N - -> false = N.testbit (& wones n) k. - Proof. - induction n; try abstract (simpl; intuition). - induction k; try abstract ( - intro H; destruct H; simpl; intuition). - - intro H. - assert (N.pos p - 1 >= N.of_nat n)%N as Z. - apply ge_to_le; - apply ge_to_le in H; - apply (N.add_le_mono_r _ _ 1%N); - replace (N.of_nat n + 1)%N with (N.of_nat (S n)); - replace (N.pos p - 1 + 1)%N with (N.pos p); - try rewrite N.sub_add; - try assumption; - try nomega; - apply Pos_ge_1. - - rewrite (IHn (N.pos p - 1)%N Z) at 1. - - assert (N.pos p = N.succ (N.pos p - 1)) as Hp by ( - rewrite <- N.pred_sub; - rewrite N.succ_pred; - try abstract intuition; - intro H0; inversion H0). - - symmetry. - rewrite Hp at 1. - rewrite Hp in H. - - revert H; clear IHn Hp Z; - generalize (N.pos p - 1)%N as x; - intros x H. - - replace (& wones (S n)) with (2 * & (wones n) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - - rewrite N.testbit_succ_r; reflexivity. - Qed. - - Lemma testbit_wones_true: forall n k, - (k < N.of_nat n)%N - -> true = N.testbit (& wones n) k. - Proof. - induction n; intros k H; try nomega. - destruct (N.eq_dec k (N.of_nat n)). - - - clear IHn H; subst. - induction n. - - + simpl; intuition. - - + replace (& (wones (S (S n)))) - with (2 * (& (wones (S n))) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite Nat2N.inj_succ. - rewrite N.testbit_succ_r. - assumption. - - - induction k. - - + replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite N.testbit_0_r. - reflexivity. - - + assert (N.pos p < N.of_nat n)%N as IH by ( - rewrite Nat2N.inj_succ in H; - nomega). - apply N.lt_lt_pred in IH. - apply IHn in IH. - replace (N.pos p) with (N.succ (N.pred (N.pos p))) by ( - induction p; simpl; - try rewrite Pos.succ_pred_double; - intuition). - replace (& (wones (S n))) with (2 * (& (wones n)) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - rewrite N.testbit_succ_r. - assumption. - Qed. - - - Lemma plus_le: forall {n} (x y: word n), - (& (x ^+ y) <= &x + &y)%N. - Proof. - intros. - unfold wplus, wordBin. - rewrite wordToN_nat. - rewrite NToWord_nat. - pose proof (wordToNat_natToWord n (N.to_nat (& x + & y))) as H. - destruct H as [k H]. - destruct H as [Heq Hk]. - rewrite Heq. - rewrite Nat2N.inj_sub. - rewrite N2Nat.id. - generalize (&x + &y)%N; intro a. - generalize (N.of_nat (k * pow2 n))%N; intro b. - clear Heq Hk; clear x y k; clear n. - replace a with (a - 0)%N by nomega. - replace' (a - 0)%N with a at 1 by nomega. - apply N.sub_le_mono_l. - apply N_ge_0. - Qed. - - Lemma mult_le: forall {n} (x y: word n), - (& (x ^* y) <= &x * &y)%N. - Proof. - intros. - unfold wmult, wordBin. - rewrite wordToN_nat. - rewrite NToWord_nat. - pose proof (wordToNat_natToWord n (N.to_nat (& x * & y))) as H. - destruct H as [k H]. - destruct H as [Heq Hk]. - rewrite Heq. - rewrite Nat2N.inj_sub. - rewrite N2Nat.id. - generalize (&x * &y)%N; intro a. - generalize (N.of_nat (k * pow2 n))%N; intro b. - clear Heq Hk; clear x y k; clear n. - replace a with (a - 0)%N by nomega. - replace' (a - 0)%N with a at 1 by nomega. - apply N.sub_le_mono_l. - apply N_ge_0. - Qed. - - Lemma log2_conv: forall z, Z.log2 z = Z.of_N (N.log2 (Z.to_N z)). - Proof. - intro z; induction z as [| |p]; auto. - induction p; auto. - Qed. -End Misc. - -Section Exp. - Local Open Scope nword_scope. - - Lemma pow2_inv : forall n m, pow2 n = pow2 m -> n = m. - Proof. - induction n; intros; simpl in *; - induction m; simpl in *; try omega. - f_equal; apply IHn. - omega. - Qed. - - Lemma pow2_gt0 : forall n, (pow2 n > O)%nat. - Proof. induction n; simpl; omega. Qed. - - Lemma pow2_N_bound: forall n j, - (j < pow2 n)%nat -> (N.of_nat j < Npow2 n)%N. - Proof. - intros. - rewrite <- Npow2_nat in H. - unfold N.lt. - rewrite N2Nat.inj_compare. - rewrite Nat2N.id. - apply nat_compare_lt in H. - assumption. - Qed. - - Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N. - Proof. - intros; induction x. - - - simpl; apply N.lt_1_r; intuition. - - - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition. - apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0. - - + intuition; inversion H. - - + apply N.neq_0_lt_0 in IHx; intuition. - Qed. - - Lemma Npow2_ge1 : forall x, (1 <= Npow2 x)%N. - Proof. - intro x. - pose proof (Npow2_gt0 x) as Z. - apply N.lt_pred_le; simpl. - assumption. - Qed. - - Lemma Npow2_split: forall a b, - (Npow2 (a + b) = (Npow2 a) * (Npow2 b))%N. - Proof. - intros; revert a. - induction b. - - - intros; simpl; replace (a + 0) with a; try nomega. - rewrite N.mul_1_r; intuition. - - - intros. - replace (a + S b) with (S a + b) by omega. - rewrite (IHb (S a)); simpl; clear IHb. - induction (Npow2 a), (Npow2 b); simpl; intuition. - rewrite Pos.mul_xO_r; intuition. - Qed. - - Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N. - Proof. - induction n. - - - simpl; intuition. - - - rewrite Nat2N.inj_succ. - rewrite N.pow_succ_r; try apply N_ge_0. - rewrite <- IHn. - simpl; intuition. - Qed. - - Lemma Npow2_succ: forall n, (Npow2 (S n) = 2 * (Npow2 n))%N. - Proof. intros; simpl; induction (Npow2 n); intuition. Qed. - - Lemma Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N. - Proof. - induction n; intros m H; try rewrite Npow2_succ. - - - simpl; apply Npow2_ge1. - - - induction m; try rewrite Npow2_succ. - - + inversion H. - - + assert (n <= m)%nat as H0 by omega. - apply IHn in H0. - apply N.mul_le_mono_l. - assumption. - Qed. -End Exp. - -Section Conversions. - Local Open Scope nword_scope. - - Lemma NToWord_wordToN: forall sz x, NToWord sz (wordToN x) = x. - Proof. - intros. - rewrite NToWord_nat. - rewrite wordToN_nat. - rewrite Nat2N.id. - rewrite natToWord_wordToNat. - intuition. - Qed. - - Lemma NToWord_equal: forall n (x y: word n), - wordToN x = wordToN y -> x = y. - Proof. - intros. - rewrite <- (NToWord_wordToN _ x). - rewrite <- (NToWord_wordToN _ y). - rewrite H; reflexivity. - Qed. - - Lemma wordToN_NToWord: forall sz x, (x < Npow2 sz)%N -> wordToN (NToWord sz x) = x. - Proof. - intros. - rewrite NToWord_nat. - rewrite wordToN_nat. - rewrite <- (N2Nat.id x). - apply Nat2N.inj_iff. - rewrite Nat2N.id. - apply natToWord_inj with (sz:=sz); - try rewrite natToWord_wordToNat; - intuition. - - - apply wordToNat_bound. - - rewrite <- Npow2_nat; apply to_nat_lt; assumption. - Qed. - - Lemma Npow2_ignore: forall {n} (x: word n), - x = NToWord _ (& x + Npow2 n). - Proof. - intros. - rewrite <- (NToWord_wordToN n x) at 1. - repeat rewrite NToWord_nat. - rewrite N2Nat.inj_add. - rewrite Npow2_nat. - replace' (N.to_nat (&x)) - with ((N.to_nat (&x) + pow2 n) - 1 * pow2 n) - at 1 by omega. - rewrite drop_sub; [intuition|omega]. - Qed. -End Conversions. - -Section SpecialFunctions. - Local Open Scope nword_scope. - - Lemma convS_id: forall n x p, (@convS n n x p) = x. - Proof. - intros; unfold convS; vm_compute. - replace (convS_subproof n n x p) - with (eq_refl (word n)) by (apply proof_irrelevance). - reflexivity. - Qed. - - Lemma wordToN_convS: forall {n m} x p, - wordToN (@convS n m x p) = wordToN x. - Proof. - intros. - revert x. - rewrite p. - intro x. - rewrite convS_id. - reflexivity. - Qed. - - Lemma wordToN_zext: forall {n m} (x: word n), - wordToN (@zext n x m) = wordToN x. - Proof. - intros; induction x; simpl; intuition. - - - unfold zext, Word.combine. - rewrite wordToN_nat. - unfold wzero. - rewrite (@wordToNat_natToWord_idempotent m 0); simpl; intuition. - apply Npow2_gt0. - - - unfold zext in IHx; rewrite IHx; clear IHx; - destruct b; intuition. - Qed. - - Lemma wordToN_div2: forall {n} (x: word (S n)), - N.div2 (&x) = & (wtl x). - Proof. - intros. - pose proof (shatter_word x) as Hx; simpl in Hx; rewrite Hx; simpl. - destruct (whd x). - replace (match & wtl x with - | 0%N => 0%N - | N.pos q => N.pos (xO q) - end) - with (N.double (& (wtl x))) - by (induction (& (wtl x)); simpl; intuition). - - - rewrite N.div2_succ_double. - reflexivity. - - - induction (& (wtl x)); simpl; intuition. - Qed. - - Fixpoint wbit {n} (x: word n) (k: nat): bool := - match n as n' return word n' -> bool with - | O => fun _ => false - | S m => fun x' => - match k with - | O => (whd x') - | S k' => wbit (wtl x') k' - end - end x. - - Lemma wbit_wtl: forall {n} (x: word (S n)) k, - wbit x (S k) = wbit (wtl x) k. - Proof. - intros. - pose proof (shatter_word x) as Hx; - simpl in Hx; rewrite Hx; simpl. - reflexivity. - Qed. - - Lemma wordToN_testbit: forall {n} (x: word n) k, - N.testbit (& x) k = wbit x (N.to_nat k). - Proof. - assert (forall x: N, match x with - | 0%N => 0%N - | N.pos q => N.pos (q~0)%positive - end = N.double x) as kill_match by ( - induction x; simpl; intuition). - - induction n; intros. - - - shatter x; simpl; intuition. - - - revert IHn; rewrite <- (N2Nat.id k). - generalize (N.to_nat k) as k'; intros; clear k. - rewrite Nat2N.id in *. - - induction k'. - - + clear IHn; induction x; simpl; intuition. - destruct (& x), b; simpl; intuition. - - + clear IHk'. - shatter x; simpl. - - rewrite N.succ_double_spec; simpl. - - rewrite kill_match. - replace (N.pos (Pos.of_succ_nat k')) - with (N.succ (N.of_nat k')) - by (rewrite <- Nat2N.inj_succ; - simpl; intuition). - - rewrite N.double_spec. - replace (N.succ (2 * & wtl x)) - with (2 * & wtl x + 1)%N - by nomega. - - destruct (whd x); - try rewrite N.testbit_odd_succ; - try rewrite N.testbit_even_succ; - try abstract ( - unfold N.le; simpl; - induction (N.of_nat k'); intuition; - try inversion H); - rewrite IHn; - rewrite Nat2N.id; - reflexivity. - Qed. - - Lemma wordToN_split1: forall {n m} x, - & (@split1 n m x) = N.land (& x) (& (wones n)). - Proof. - intros. - - pose proof (Word.combine_split _ _ x) as C; revert C. - generalize (split1 n m x) as a, (split2 n m x) as b. - intros a b C; rewrite <- C; clear C x. - - apply N.bits_inj_iff; unfold N.eqf; intro x. - rewrite N.land_spec. - repeat rewrite wordToN_testbit. - revert x a b. - - induction n, m; intros; - shatter a; shatter b; - induction (N.to_nat x) as [|n0]; - try rewrite <- (Nat2N.id n0); - try rewrite andb_false_r; - try rewrite andb_true_r; - simpl; intuition. - Qed. - - Lemma wordToN_split2: forall {n m} x, - & (@split2 n m x) = N.shiftr (& x) (N.of_nat n). - Proof. - intros. - - pose proof (Word.combine_split _ _ x) as C; revert C. - generalize (split1 n m x) as a, (split2 n m x) as b. - intros a b C. - rewrite <- C; clear C x. - - apply N.bits_inj_iff; unfold N.eqf; intro x; - rewrite N.shiftr_spec; - repeat rewrite wordToN_testbit; - try apply N_ge_0. - - revert x a b. - induction n, m; intros; - shatter a; - try apply N_ge_0. - - - simpl; intuition. - - - replace (x + N.of_nat 0)%N with x by nomega. - simpl; intuition. - - - rewrite (IHn x (wtl a) b). - rewrite <- (N2Nat.id x). - repeat rewrite <- Nat2N.inj_add. - repeat rewrite Nat2N.id; simpl. - replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega. - reflexivity. - - - rewrite (IHn x (wtl a) b). - rewrite <- (N2Nat.id x). - repeat rewrite <- Nat2N.inj_add. - repeat rewrite Nat2N.id; simpl. - replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega. - reflexivity. - Qed. - - Lemma wordToN_combine: forall {n m} a b, - & (@Word.combine n a m b) = N.lxor (N.shiftl (& b) (N.of_nat n)) (& a). - Proof. - intros; symmetry. - - replace' a with (Word.split1 _ _ (Word.combine a b)) at 1 - by (apply Word.split1_combine). - - replace' b with (Word.split2 _ _ (Word.combine a b)) at 1 - by (apply Word.split2_combine). - - generalize (Word.combine a b); intro x; clear a b. - - rewrite wordToN_split1, wordToN_split2. - generalize (&x); clear x; intro x. - apply N.bits_inj_iff; unfold N.eqf; intro k. - - rewrite N.lxor_spec. - destruct (Nge_dec k (N.of_nat n)). - - - rewrite N.shiftl_spec_high; try apply N_ge_0; - try (apply ge_to_le; assumption). - rewrite N.shiftr_spec; try apply N_ge_0. - replace (k - N.of_nat n + N.of_nat n)%N with k by nomega. - rewrite N.land_spec. - induction (N.testbit x k); - replace (N.testbit (& wones n) k) with false; - simpl; intuition; - try apply testbit_wones_false; - try assumption. - - - rewrite N.shiftl_spec_low; try assumption; try apply N_ge_0. - rewrite N.land_spec. - induction (N.testbit x k); - replace (N.testbit (& wones n) k) with true; - simpl; intuition; - try apply testbit_wones_true; - try assumption. - Qed. - - Lemma wordToN_wones: forall x, & (wones x) = N.ones (N.of_nat x). - Proof. - induction x. - - - simpl; intuition. - - - rewrite Nat2N.inj_succ. - replace (& wones (S x)) with (2 * & (wones x) + N.b2n true)%N - by (simpl; rewrite ?N.succ_double_spec; simpl; nomega). - replace (N.ones (N.succ _)) - with (2 * N.ones (N.of_nat x) + N.b2n true)%N. - - + rewrite IHx; nomega. - - + replace (N.succ (N.of_nat x)) with (1 + (N.of_nat x))%N by ( - rewrite N.add_comm; nomega). - rewrite N.ones_add. - replace (N.ones 1) with 1%N by ( - unfold N.ones; simpl; intuition). - simpl. - reflexivity. - Qed. - - Lemma wordToN_zero: forall w, wordToN (wzero w) = 0%N. - Proof. - intros. - unfold wzero; rewrite wordToN_nat. - rewrite wordToNat_natToWord_idempotent; simpl; intuition. - apply Npow2_gt0. - Qed. - - Lemma NToWord_zero: forall w, NToWord w 0%N = wzero w. - Proof. - intros. - unfold wzero; rewrite NToWord_nat. - f_equal. - Qed. - - Ltac propagate_wordToN := - unfold extend, low, high, break; - repeat match goal with - | [|- context[@wordToN _ (@convS _ _ _ _)] ] => - rewrite wordToN_convS - | [|- context[@wordToN _ (@split1 _ _ _)] ] => - rewrite wordToN_split1 - | [|- context[@wordToN _ (@split2 _ _ _)] ] => - rewrite wordToN_split2 - | [|- context[@wordToN _ (@combine _ _ _ _)] ] => - rewrite wordToN_combine - | [|- context[@wordToN _ (@zext _ _ _)] ] => - rewrite wordToN_zext - | [|- context[@wordToN _ (@wones _)] ] => - rewrite wordToN_wones - end. - - Lemma break_spec: forall (m n: nat) (x: word n) low high, - (low, high) = break m x - -> &x = (&high * Npow2 m + &low)%N. - Proof. - intros m n x low high H. - unfold break in H. - destruct (le_dec m n). - - - inversion H; subst; clear H. - propagate_wordToN. - rewrite N.land_ones. - rewrite N.shiftr_div_pow2. - replace (n - (n - m)) with m by omega. - rewrite N.mul_comm. - rewrite Npow2_N. - rewrite <- (N.div_mod' (& x) (2 ^ (N.of_nat m))%N). - reflexivity. - - - inversion H; subst; clear H. - propagate_wordToN; simpl; nomega. - Qed. - - Lemma extend_bound: forall k n (p: (k <= n)%nat) (w: word k), - (& (extend p w) < Npow2 k)%N. - Proof. - intros. - propagate_wordToN. - apply word_size_bound. - Qed. - - Lemma mask_spec : forall (n: nat) (x: word n) m, - & (mask (N.to_nat m) x) = (N.land (& x) (N.ones m)). - Proof. - intros; unfold mask. - destruct (le_dec (N.to_nat m) n). - - - propagate_wordToN. - rewrite N2Nat.id. - reflexivity. - - - rewrite N.land_ones. - rewrite N.mod_small; try reflexivity. - rewrite <- (N2Nat.id m). - rewrite <- Npow2_N. - apply (N.lt_le_trans _ (Npow2 n) _); try apply word_size_bound. - apply Npow2_ordered. - omega. - Qed. - - Lemma mask_bound : forall (n: nat) (x: word n) m, - (& (mask m x) < Npow2 m)%N. - Proof. - intros; unfold mask. - destruct (le_dec m n). - - - apply extend_bound. - - - apply (N.lt_le_trans _ (Npow2 n) _); try apply word_size_bound. - apply Npow2_ordered. - omega. - Qed. - -End SpecialFunctions. - -Section TopLevel. - Local Open Scope nword_scope. - - Coercion ind : bool >-> N. - - Lemma wordize_plus: forall {n} (x y: word n), - (&x + &y < Npow2 n)%N - -> (&x + &y)%N = & (x ^+ y). - Proof. - intros n x y H. - pose proof (word_size_bound x) as Hbx. - pose proof (word_size_bound y) as Hby. - - unfold wplus, wordBin. - rewrite wordToN_NToWord; intuition. - Qed. - - Lemma wordize_awc: forall {n} (x y: word n) (c: bool), - (&x + &y + c < Npow2 n)%N - -> (&x + &y + c)%N = &(addWithCarry x y c). - Proof. - intros n x y c H. - unfold wplus, wordBin, addWithCarry. - destruct c; simpl in *. - - - replace 1%N with (wordToN (natToWord n 1)) in * by ( - rewrite wordToN_nat; - rewrite wordToNat_natToWord_idempotent; - nomega). - - rewrite <- N.add_assoc. - rewrite wordize_plus; try nomega. - rewrite wordize_plus; try nomega. - - + rewrite wplus_assoc. - reflexivity. - - + apply (N.le_lt_trans _ (& x + & y + & natToWord n 1)%N _); - try assumption. - rewrite <- N.add_assoc. - apply N.add_le_mono. - - * apply N.eq_le_incl; reflexivity. - - * apply plus_le. - - - rewrite wplus_comm. - rewrite wplus_unit. - rewrite N.add_0_r in *. - apply wordize_plus; assumption. - Qed. - - Lemma wordize_minus: forall {n} (x y: word n), - (&x >= &y)%N -> (&x - &y)%N = &(x ^- y). - Proof. - intros n x y H. - - destruct (Nge_dec 0%N (&y)). { - unfold wminus, wneg. - replace (& y) with 0%N in * by nomega. - replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N - by (rewrite wordToN_zero; nomega). - rewrite <- Npow2_ignore. - rewrite wplus_comm. - rewrite wplus_unit. - nomega. - } - - assert (& x - & y < Npow2 n)%N. { - transitivity (wordToN x); - try apply word_size_bound; - apply N.sub_lt; - [apply N.ge_le|]; assumption. - } - - assert (& x - & y + & y < Npow2 n)%N. { - replace (& x - & y + & y)%N - with (wordToN x) by nomega; - apply word_size_bound. - } - - assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. { - apply NToWord_equal. - rewrite <- wordize_plus; rewrite wordToN_NToWord; try assumption. - nomega. - } - - symmetry. - rewrite Hv at 1. - unfold wminus. - repeat rewrite <- wplus_assoc. - rewrite wminus_inv. - rewrite wplus_comm. - rewrite wplus_unit. - rewrite wordToN_NToWord; try assumption. - reflexivity. - Qed. - - Lemma wordize_mult: forall {n} (x y: word n), - (&x * &y < Npow2 n)%N - -> (&x * &y)%N = &(x ^* y). - Proof. - intros n x y H. - pose proof (word_size_bound x) as Hbx. - pose proof (word_size_bound y) as Hby. - - unfold wmult, wordBin. - rewrite wordToN_NToWord; intuition. - Qed. - - Lemma wordize_shiftr: forall {n} (x: word n) (k: nat), - (N.shiftr_nat (&x) k) = & (shiftr x k). - Proof. - intros n x k. - unfold shiftr, extend, high. - destruct (le_dec k n). - - - repeat first [ - rewrite wordToN_convS - | rewrite wordToN_zext - | rewrite wordToN_split2 ]. - rewrite <- Nshiftr_equiv_nat. - reflexivity. - - - rewrite (wordToN_nat (wzero n)); unfold wzero. - destruct (Nat.eq_dec n O); subst. - - + rewrite (shatter_word_0 x); simpl; intuition. - rewrite <- Nshiftr_equiv_nat. - rewrite N.shiftr_0_l. - reflexivity. - - + rewrite wordToNat_natToWord_idempotent; - try nomega. - - * pose proof (word_size_bound x). - rewrite <- Nshiftr_equiv_nat. - rewrite N.shiftr_eq_0_iff. - destruct (N.eq_dec (&x) 0%N) as [E|E]; - try rewrite E in *; - try abstract (left; reflexivity). - - right; split; try nomega. - apply (N.le_lt_trans _ (N.log2 (Npow2 n)) _). { - apply N.log2_le_mono. - apply N.lt_le_incl. - assumption. - } - - rewrite Npow2_N. - rewrite N.log2_pow2; try nomega. - apply N_ge_0. - - * simpl; apply Npow2_gt0. - Qed. - - Lemma wordize_and: forall {n} (x y: word n), - & (wand x y) = N.land (&x) (&y). - Proof. - intros. - apply N.bits_inj_iff; unfold N.eqf; intro k. - rewrite N.land_spec. - repeat rewrite wordToN_testbit. - revert x y. - generalize (N.to_nat k) as k'; clear k. - induction n; intros; shatter x; shatter y; simpl; [reflexivity|]. - induction k'; [reflexivity|]. - fold wand. - rewrite IHn. - reflexivity. - Qed. - - Lemma wordize_or: forall {n} (x y: word n), - & (wor x y) = N.lor (&x) (&y). - Proof. - intros. - apply N.bits_inj_iff; unfold N.eqf; intro k. - rewrite N.lor_spec. - repeat rewrite wordToN_testbit. - revert x y. - generalize (N.to_nat k) as k'; clear k. - induction n; intros; shatter x; shatter y; simpl; [reflexivity|]. - induction k'; [reflexivity|]. - rewrite IHn. - reflexivity. - Qed. - - Lemma conv_mask: forall {n} (x: word n) (k: nat), - (k <= n)%nat -> - mask k x = x ^& (NToWord _ (N.ones (N.of_nat k))). - Proof. - intros n x k H. - apply NToWord_equal. - - rewrite <- (Nat2N.id k). - rewrite mask_spec. - apply N.bits_inj_iff; unfold N.eqf; intro m. - rewrite N.land_spec. - repeat rewrite wordToN_testbit. - rewrite <- (N2Nat.id m). - rewrite <- wordToN_wones. - repeat rewrite wordToN_testbit. - repeat rewrite N2Nat.id. - rewrite <- wordToN_wones. - - assert (forall n (a b: word n) k, - wbit (a ^& b) k = andb (wbit a k) (wbit b k)) as Hwand. { - intros n0 a b. - induction n0 as [|n1]; - shatter a; shatter b; - simpl; try reflexivity. - - intro k0; induction k0 as [|k0]; - simpl; try reflexivity. - - fold wand. - rewrite IHn1. - reflexivity. - } - - rewrite Hwand; clear Hwand. - induction (wbit x (N.to_nat m)); - repeat rewrite andb_false_l; - repeat rewrite andb_true_l; - try reflexivity. - - repeat rewrite <- wordToN_testbit. - rewrite wordToN_NToWord; try reflexivity. - apply (N.lt_le_trans _ (Npow2 k) _). - - + apply word_size_bound. - - + apply Npow2_ordered. - omega. - Qed. - - Close Scope nword_scope. -End TopLevel. |