diff options
| -rw-r--r-- | Makefile | 21 | ||||
| -rw-r--r-- | src/Assembly/BoundedWord.v | 416 |
2 files changed, 398 insertions, 39 deletions
@@ -1,11 +1,11 @@ +COQ_ARGS := -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime MOD_NAME := Crypto SRC_DIR := src +MODULES := Curves Galois Rep Specific Tactics Util +VS := $(MODULES:%=src/%/*.v) -.PHONY: coq clean install coqprime update-_CoqProject -.DEFAULT_GOAL := coq - -update-_CoqProject:: - (echo '-R $(SRC_DIR) $(MOD_NAME)'; git ls-files src/*.v) > _CoqProject +.PHONY: coq clean install coqprime +.DEFAULT_GOAL: coq coq: coqprime Makefile.coq $(MAKE) -f Makefile.coq @@ -13,13 +13,14 @@ coq: coqprime Makefile.coq coqprime: $(MAKE) -C coqprime -Makefile.coq: Makefile _CoqProject - coq_makefile -f _CoqProject -o Makefile.coq +Makefile.coq: Makefile $(VS) + coq_makefile -R $(SRC_DIR) $(MOD_NAME) $(COQ_ARGS) $(VS) -o Makefile.coq clean: Makefile.coq $(MAKE) -f Makefile.coq clean rm -f Makefile.coq -install: coq Makefile.coq - $(MAKE) -f Makefile.coq install - $(MAKE) -C coqprime install +install: coq + ln -sfL $(shell pwd)/src $(shell coqtop -where)/user-contrib/Crypto + ln -sfL $(shell pwd)/bedrock/Bedrock $(shell coqtop -where)/user-contrib/Bedrock + diff --git a/src/Assembly/BoundedWord.v b/src/Assembly/BoundedWord.v index 57be975ba..e4e3e9d07 100644 --- a/src/Assembly/BoundedWord.v +++ b/src/Assembly/BoundedWord.v @@ -1,6 +1,6 @@ -Require Import Bedrock.Word. -Require Import NArith PArith Ndigits Compare_dec. +Require Import Bedrock.Word Bedrock.Nomega. +Require Import NArith PArith Ndigits Compare_dec Arith. Require Import ProofIrrelevance. Require Import Ring. @@ -10,18 +10,394 @@ Section BoundedWord. Open Scope Bounded_scope. - (* First, we make our BoundedWord sigma type *) - Definition wordGeN {n: nat} (a: word n) (b: N): Prop := - (wordToN a >= b)%N. + Variable n: nat. + (* Word Operations *) + + Definition shiftr (w: word n) (bits: nat): word n. + destruct (le_dec bits n). + + - replace n with (bits + (n - bits)) in * by (abstract intuition). + refine (zext (split1 bits (n - bits) w) (n - bits)). + + - exact (wzero n). + Defined. + + Lemma shiftr_spec: forall (w : word n) (bits: nat), + wordToN (shiftr w bits) = N.shiftr (wordToN w) (N.of_nat bits). + intros; unfold shiftr; destruct (le_dec bits n). + + - admit. + + - replace (wordToN (wzero n)) with 0%N by admit. + unfold N.shiftr. + induction bits. + + + replace (N.of_nat 0) with 0%N by intuition. + assert (n = 0) by intuition; clear n0; subst. + replace w with WO; intuition. + + + induction bits; admit. + Qed. + + Definition mask (m: nat) (w: word n): word n. + destruct (le_dec m n). + + - replace n with (m + (n - m)) in * by (abstract intuition). + refine (w ^& (zext (wones m) (n - m))). + + - exact w. + Defined. + + (* Definitions of Inequality and simple bounds. *) Definition wordLeN {n: nat} (a: word n) (b: N): Prop := (wordToN a <= b)%N. - Notation "A >= B" := (wordGeN A B) (at level 70) : Bounded_scope. Notation "A <= B" := (wordLeN A B) (at level 70) : Bounded_scope. - Inductive BoundOn {n: nat} (x: word n) : Prop := - | boundBy: forall low high: N, x >= low -> x <= high -> BoundOn x. + Lemma le_ge : forall n m, (n <= m -> m >= n)%nat. + Proof. + intros; omega. + Qed. + + Lemma ge_le : forall n m, (n >= m -> m <= n)%nat. + Proof. + intros; omega. + Qed. + + Ltac ge_to_le := + try apply N.ge_le; + repeat match goal with + | [ H : _ |- _ ] => apply N.le_ge in H + end. + + Ltac ge_to_le_nat := + try apply le_ge; + repeat match goal with + | [ H : _ |- _ ] => apply ge_le in H + end. + + Ltac preomega := unfold wordLeN; intros; ge_to_le; pre_nomega. + + Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N. + + Theorem word_size_bound : forall (w: word n), + w <= Npow2 n - 1. + Proof. + intros; unfold wordLeN; rewrite wordToN_nat. + + assert (B := wordToNat_bound w); + rewrite <- Npow2_nat in B; + apply nat_compare_lt in B. + + unfold N.le; intuition; + rewrite N2Nat.inj_compare in H; + rewrite Nat2N.id in H. + + apply nat_compare_lt in B. + apply nat_compare_gt in H. + + replace (N.to_nat (Npow2 n)) with (S (N.to_nat (Npow2 n - 1))) in * by admit. + intuition. + Qed. + + Theorem constant_bound_N : forall k, + NToWord n k <= k. + Proof. + preomega. + rewrite NToWord_nat. + destruct (le_lt_dec (pow2 n) (N.to_nat k)). + + specialize (wordToNat_bound (natToWord n (N.to_nat k))); nomega. + + rewrite wordToNat_natToWord_idempotent; nomega. + Qed. + + Theorem constant_bound_nat : forall k, + natToWord n k <= N.of_nat k. + Proof. + preomega. + destruct (le_lt_dec (pow2 n) k). + + specialize (wordToNat_bound (natToWord n k)); nomega. + + rewrite wordToNat_natToWord_idempotent; nomega. + Qed. + + Theorem wplus_bound : forall (w1 w2 : word n) b1 b2, + w1 <= b1 + -> w2 <= b2 + -> w1 ^+ w2 <= b1 + b2. + Proof. + preomega. + destruct (le_lt_dec (pow2 n) (N.to_nat b1 + N.to_nat b2)). + + specialize (wordToNat_bound (w1 ^+ w2)); nomega. + + rewrite wplus_alt. + unfold wplusN, wordBinN. + rewrite wordToNat_natToWord_idempotent; nomega. + Qed. + + Theorem wmult_bound : forall (w1 w2 : word n) b1 b2, + w1 <= b1 + -> w2 <= b2 + -> w1 ^* w2 <= b1 * b2. + Proof. + preomega. + destruct (le_lt_dec (pow2 n) (N.to_nat b1 * N.to_nat b2)). + + specialize (wordToNat_bound (w1 ^* w2)); nomega. + + rewrite wmult_alt. + unfold wmultN, wordBinN. + rewrite wordToNat_natToWord_idempotent. + ge_to_le_nat. + + apply Mult.mult_le_compat; nomega. + pre_nomega. + apply Lt.le_lt_trans with (N.to_nat b1 * N.to_nat b2); auto. + apply Mult.mult_le_compat; nomega. + Qed. + + Theorem shiftr_bound : forall (w : word n) b bits, + w <= b + -> shiftr w bits <= N.shiftr b (N.of_nat bits). + Proof. + admit. + Qed. + + Theorem mask_bound : forall (w : word n) m, + mask m w <= Npow2 m - 1. + Proof. + admit. + Qed. + + Theorem mask_update_bound : forall (w : word n) b m, + w <= b + -> mask m w <= (N.min b (Npow2 m - 1)). + Proof. + admit. + Qed. + + + Ltac word_bound := + repeat ( + eassumption + || apply wplus_bound + || apply wmult_bound + || apply mask_update_bound + || apply mask_bound + || apply shiftr_bound + || apply constant_bound_N + || apply constant_bound_nat + || apply word_size_bound + ). + + Notation "$" := (natToWord _). + + Lemma example1 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4, + w1 <= b1 + -> w2 <= b2 + -> w3 <= b3 + -> w4 <= b4 + -> { b | w1 ^+ (w2 ^* w3) ^* w4 <= b }. + Proof. + eexists. + word_bound. + Defined. + + (* Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N) + (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) => + projT1 (example1 H1 H2 H3 H4). *) + + Lemma example2 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4, + w1 <= b1 + -> w2 <= b2 + -> w3 <= b3 + -> w4 <= b4 + -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }. + Proof. + eexists. + word_bound. + Defined. + + (*Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N) + (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) => + projT1 (example2 H1 H2 H3 H4). *) + + Lemma example3 : forall (w1 w2 w3 w4 : word n), + w1 <= Npow2 3 + -> w2 <= Npow2 4 + -> w3 <= Npow2 8 + -> w4 <= Npow2 16 + -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }. + Proof. + eexists. + word_bound. + Defined. + + (* Eval simpl in fun (w1 w2 w3 w4 : word n) + (H1 : w1 <= _) (H2 : w2 <= _) (H3 : w3 <= _) (H4 : w4 <= _) => + projT1 (example3 H1 H2 H3 H4). *) + +End BoundedWord. + +Section MulmodExamples. + + Notation "A <= B" := (wordLeN A B) (at level 70). + Notation "$" := (natToWord _). + + Ltac word_bound := + repeat ( + eassumption + || apply (wplus_bound 32) + || apply (wmult_bound 32) + || apply (mask_update_bound 32) + || apply (mask_bound 32) + || apply (shiftr_bound 32) + || apply (constant_bound_N 32) + || apply (constant_bound_nat 32) + || apply (word_size_bound 32) + ). + + Lemma example_and : forall x : word 32, wand x (NToWord 32 (N.ones 10)) <= 1023. + intros. + replace (wand x (NToWord 32 (N.ones 10))) with (mask 32 10 x) by admit. + word_bound. + Qed. + + Lemma example_shiftr : forall x : word 32, shiftr 32 x 30 <= 3. + intros. + replace 3%N with (N.shiftr (Npow2 32 - 1) (N.of_nat 30)) by (simpl; intuition). + + (* word_bound works but it's slow *) + apply (shiftr_bound 32). + apply (word_size_bound 32). + Qed. + + Lemma example_shiftr2 : forall x : word 32, x <= 1023 -> shiftr 32 x 5 <= 31. + intros. + replace 31%N with (N.shiftr 1023%N 5%N) by (simpl; intuition). + + (* word_bound works but it's slow *) + apply (shiftr_bound 32). + eassumption. + Qed. + + Variable f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : word 32. + Variable g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : word 32. + Hypothesis Hf0 : f0 <= 2^26. + Hypothesis Hf1 : f1 <= 2^25. + Hypothesis Hf2 : f2 <= 2^26. + Hypothesis Hf3 : f3 <= 2^25. + Hypothesis Hf4 : f4 <= 2^26. + Hypothesis Hf5 : f5 <= 2^25. + Hypothesis Hf6 : f6 <= 2^26. + Hypothesis Hf7 : f7 <= 2^25. + Hypothesis Hf8 : f8 <= 2^26. + Hypothesis Hf9 : f9 <= 2^25. + Hypothesis Hg0 : g0 <= 2^26. + Hypothesis Hg1 : g1 <= 2^25. + Hypothesis Hg2 : g2 <= 2^26. + Hypothesis Hg3 : g3 <= 2^25. + Hypothesis Hg4 : g4 <= 2^26. + Hypothesis Hg5 : g5 <= 2^25. + Hypothesis Hg6 : g6 <= 2^26. + Hypothesis Hg7 : g7 <= 2^25. + Hypothesis Hg8 : g8 <= 2^26. + Hypothesis Hg9 : g9 <= 2^25. + + Lemma example_mulmod_s_ppt : { b | f0 ^* g0 <= b}. + eexists. + word_bound. + Defined. + + Lemma example_mulmod_s_pp : { b | f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2) <= b}. + eexists. + word_bound. + Defined. + + Lemma example_mulmod_s_pp_shiftr : + { b | shiftr (f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) 26 <= b}. + eexists. + word_bound. + Qed. + + Lemma example_mulmod_u_fg1 : { b | + (let y : word 32 := (* the type declarations on the let-s make type inference not take forever *) + (f0 ^* g0 ^+ + $19 ^* + (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ + f1 ^* g9 ^* $2)) in + let y0 : word 32 := + (shiftr y 26 ^+ + (f1 ^* g0 ^+ f0 ^* g1 ^+ + $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) in + let y1 : word 32 := + (shiftr y0 25 ^+ + (f2 ^* g0 ^+ f1 ^* g1 ^* $2 ^+ f0 ^* g2 ^+ + $19 ^* (f9 ^* g3 ^* $2 ^+ f8 ^* g4 ^+ f7 ^* g5 ^* $2 ^+ f6 ^* g6 ^+ f5 ^* g7 ^* $2 ^+ f4 ^* g8 ^+ f3 ^* g9 ^* $2))) in + let y2 : word 32 := + (shiftr y1 26 ^+ + (f3 ^* g0 ^+ f2 ^* g1 ^+ f1 ^* g2 ^+ f0 ^* g3 ^+ + $19 ^* (f9 ^* g4 ^+ f8 ^* g5 ^+ f7 ^* g6 ^+ f6 ^* g7 ^+ f5 ^* g8 ^+ f4 ^* g9))) in + let y3 : word 32 := + (shiftr y2 25 ^+ + (f4 ^* g0 ^+ f3 ^* g1 ^* $2 ^+ f2 ^* g2 ^+ f1 ^* g3 ^* $2 ^+ f0 ^* g4 ^+ + $19 ^* (f9 ^* g5 ^* $2 ^+ f8 ^* g6 ^+ f7 ^* g7 ^* $2 ^+ f6 ^* g8 ^+ f5 ^* g9 ^* $2))) in + let y4 : word 32 := + (shiftr y3 26 ^+ + (f5 ^* g0 ^+ f4 ^* g1 ^+ f3 ^* g2 ^+ f2 ^* g3 ^+ f1 ^* g4 ^+ f0 ^* g5 ^+ + $19 ^* (f9 ^* g6 ^+ f8 ^* g7 ^+ f7 ^* g8 ^+ f6 ^* g9))) in + let y5 : word 32 := + (shiftr y4 25 ^+ + (f6 ^* g0 ^+ f5 ^* g1 ^* $2 ^+ f4 ^* g2 ^+ f3 ^* g3 ^* $2 ^+ f2 ^* g4 ^+ f1 ^* g5 ^* $2 ^+ f0 ^* g6 ^+ + $19 ^* (f9 ^* g7 ^* $2 ^+ f8 ^* g8 ^+ f7 ^* g9 ^* $2))) in + let y6 : word 32 := + (shiftr y5 26 ^+ + (f7 ^* g0 ^+ f6 ^* g1 ^+ f5 ^* g2 ^+ f4 ^* g3 ^+ f3 ^* g4 ^+ f2 ^* g5 ^+ f1 ^* g6 ^+ f0 ^* g7 ^+ + $19 ^* (f9 ^* g8 ^+ f8 ^* g9))) in + let y7 : word 32 := + (shiftr y6 25 ^+ + (f8 ^* g0 ^+ f7 ^* g1 ^* $2 ^+ f6 ^* g2 ^+ f5 ^* g3 ^* $2 ^+ f4 ^* g4 ^+ f3 ^* g5 ^* $2 ^+ f2 ^* g6 ^+ f1 ^* g7 ^* $2 ^+ + f0 ^* g8 ^+ $19 ^* f9 ^* g9 ^* $2)) in + let y8 : word 32 := + (shiftr y7 26 ^+ + (f9 ^* g0 ^+ f8 ^* g1 ^+ f7 ^* g2 ^+ f6 ^* g3 ^+ f5 ^* g4 ^+ f4 ^* g5 ^+ f3 ^* g6 ^+ f2 ^* g7 ^+ f1 ^* g8 ^+ + f0 ^* g9)) in + let y9 : word 32 := + ($19 ^* shiftr y8 25 ^+ + wand + (f0 ^* g0 ^+ + $19 ^* + (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ + f2 ^* g8 ^+ f1 ^* g9 ^* $2)) (@NToWord 32 (N.ones 26%N))) in + let fg1 : word 32 := (shiftr y9 26 ^+ + wand + (shiftr y 26 ^+ + (f1 ^* g0 ^+ f0 ^* g1 ^+ + $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) + (@NToWord 32 (N.ones 26%N))) in + fg1) <= b }. + Abort. + + Require Import ZArith. + Variable shiftra : forall {l}, word l -> nat -> word l. (* "arithmetic" aka "signed" bitshift *) + Hypothesis shiftra_spec : forall {l} (w : word l) (n:nat), wordToZ (shiftra w n) = Z.shiftr (wordToZ w) (Z.of_nat n). + + Lemma example_shiftra : forall x : word 4, shiftra x 2 <= 15. + Abort. + + Lemma example_shiftra : forall x : word 4, x <= 7 -> shiftra x 2 <= 1. + Abort. + + Lemma example_mulmod_s_pp_shiftra : + { b | shiftra (f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+ f1 ^* g9 ^* $2)) 26 <= b}. + Abort. +End MulmodExamples. + +(* Old lemmas that might end up being useful Lemma low_word_bound: forall n (x : word n), x >= 0. intros; unfold wordGeN; @@ -96,7 +472,6 @@ Section BoundedWord. intros; apply proof_irrelevance. Qed. - (* Get inequalities from definitions *) Lemma wand_upper_l: forall (n: nat) (x a b: word n), x = wand a b -> x <= (2 * wordToN a)%N. admit. Qed. @@ -152,7 +527,6 @@ Section BoundedWord. inversion H. Qed. - (* Essential operations on bounded words *) Definition bplus {n: nat} {x y: word n} (A: BoundOn x) (B: BoundOn y): BoundOn (wplus x y). destruct A as [low0 high0 lb0 hb0], B as [low1 high1 lb1 hb1]. @@ -165,22 +539,13 @@ Section BoundedWord. - apply (boundBy (x ^+ y) low0 high0); admit. - apply (boundBy (x ^+ y) (low0 + low1)%N (high0 + high1)%N); admit. - (* rewrite wplus_alt; - unfold wplusN, wordGeN, wordBinN in *; simpl; - rewrite wordToN_nat, wordToNat_natToWord_idempotent; - rewrite Nat2N.inj_add; repeat rewrite <- wordToN_nat.*) Defined. Definition bmult {n: nat} {x y: word n} (A: BoundOn x) (B: BoundOn y): BoundOn (wmult x y). destruct A as [low0 high0 lb0 hb0], B as [low1 high1 lb1 hb1]. apply (boundBy (x ^* y) (low0 * low1)%N (high0 * high1)%N); admit. - (* rewrite wmult_alt; - unfold wmultN, wordLeN, wordBinN in *; simpl; - rewrite wordToN_nat, wordToNat_natToWord_idempotent; - rewrite Nat2N.inj_mul; repeat rewrite <- wordToN_nat. *) Defined. - (* Operation replacements *) Lemma bound_plus: forall (n: nat) (a b: word n), bound (wplus a b) = bplus (bound a) (bound b). intros; apply proof_irrelevance. Qed. @@ -189,7 +554,6 @@ Section BoundedWord. intros; apply proof_irrelevance. Qed. - (* Tactics to repeatedly apply the simplification strategy *) Ltac convert_to_bounded := apply bound_eq; repeat first [rewrite bound_plus | rewrite bound_mult]. @@ -209,14 +573,13 @@ Section BoundedWord. | [|- context[sumbool_ind _ _ _ (zero_dec ?x)]] => destruct (zero_dec x) end; subst). - (* Miscellaneous simplifications we'll need *) Ltac word_simpl := repeat ( match goal with | [|- context [unbound _]] => unfold unbound - (*| [ H: (Npow2 ?x = 0)%N |- _] => + | [ H: (Npow2 ?x = 0)%N |- _] => let Z := fresh in - apply (Npow2_nonzero x) in H; intuition *) + apply (Npow2_nonzero x) in H; intuition | [ H: (?x <= 0) |- _] => unfold wordLeN in H; apply replace_zero in H; @@ -230,7 +593,6 @@ Section BoundedWord. bound, bplus, bmult, wand_bound_l, wand_bound_r. - (* The full tactic *) Ltac bound_simpl:= convert_to_bounded; propagate_bounds; @@ -238,8 +600,6 @@ Section BoundedWord. repeat match_match; word_simpl. - (* Example Lemma *) - Lemma example_bound_simpl: forall (n: nat) (a b: word n), a = wand (wzero n) b -> b = a ^+ b. Proof. @@ -248,6 +608,4 @@ Section BoundedWord. propagate_bounds. unfold_ops; simpl. match_match; word_simpl. - Qed. - -End BoundedWord.
\ No newline at end of file + Qed. *) |