From 1aa532bf509f72e2e083743e35a97d271da9009f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 24 Oct 2015 14:00:31 -0400 Subject: primitive positional numeral system definition on top of Z --- src/Galois/BaseSystem.v | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 src/Galois/BaseSystem.v diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v new file mode 100644 index 000000000..fc57bf2a7 --- /dev/null +++ b/src/Galois/BaseSystem.v @@ -0,0 +1,48 @@ +Require Import List. +Require Import ZArith.ZArith. + +Local Open Scope Z. +Local Open Scope list_scope. + +Module Type BaseCoefs. + (* lists coefficients of digits and the digits themselves always have the + * LEAST significant position first. *) + Definition coefs : Type := list Z. + + Parameter bs : coefs. + Axiom bs_good : + forall i j, + let b := nth_default 0 bs in + exists r, + b i * b j = r * b (i+j)%nat. +End BaseCoefs. + +Module BaseSystem (Import B:BaseCoefs). + Definition digits : Type := list Z. + + Definition accumulate p acc := fst p * snd p + acc. + Definition decode u := fold_right accumulate 0 (combine u bs). + + Fixpoint add (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => (u+v)::(add us' vs') + | _, nil => us + | _, _ => vs + end. + Local Infix ".+" := add (at level 50). + + Lemma add_rep : forall us vs, decode (add us vs) = decode us + decode vs. + Proof. + unfold decode, accumulate. + induction bs; destruct us; destruct vs; auto; simpl; try rewrite IHc; ring. + Qed. + + (* mul' is a valid multiplication algorithm if b_i = b_1^i *) + Fixpoint mul' (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul' us' vs + | _, _ => nil + end. + + (* UPNEXT: multiplication for arbitrary good bs *) +End BaseSystem. -- cgit v1.2.3 From e3c245f7af1df45b2666b5570c1c4b87c298477c Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 10:17:50 -0400 Subject: positional number system equivalence transcribed from pencil-and-paper proofs by --- _CoqProject | 1 + src/Galois/BaseSystem.v | 204 +++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 193 insertions(+), 12 deletions(-) diff --git a/_CoqProject b/_CoqProject index 9c07ea0dd..d749c5418 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,5 +7,6 @@ src/Galois/GaloisTheory.v src/Galois/AbstractGaloisField.v src/Galois/ComputationalGaloisField.v src/Galois/ZGaloisField.v +src/Galois/BaseSystem.v src/Curves/PointFormats.v src/Curves/Curve25519.v diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index fc57bf2a7..ac42b7c79 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,19 +1,18 @@ Require Import List. -Require Import ZArith.ZArith. +Require Import ZArith.ZArith ZArith.Zdiv. Local Open Scope Z. -Local Open Scope list_scope. Module Type BaseCoefs. (* lists coefficients of digits and the digits themselves always have the * LEAST significant position first. *) Definition coefs : Type := list Z. - Parameter bs : coefs. + Parameter base : coefs. Axiom bs_good : forall i j, - let b := nth_default 0 bs in - exists r, + let b := nth_default 0 base in + let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. End BaseCoefs. @@ -21,7 +20,8 @@ Module BaseSystem (Import B:BaseCoefs). Definition digits : Type := list Z. Definition accumulate p acc := fst p * snd p + acc. - Definition decode u := fold_right accumulate 0 (combine u bs). + Definition decode bs u := fold_right accumulate 0 (combine u bs). + Hint Unfold decode accumulate. Fixpoint add (us vs:digits) : digits := match us,vs with @@ -31,18 +31,198 @@ Module BaseSystem (Import B:BaseCoefs). end. Local Infix ".+" := add (at level 50). - Lemma add_rep : forall us vs, decode (add us vs) = decode us + decode vs. + Lemma add_rep : forall bs us vs, decode bs (add us vs) = decode bs us + decode bs vs. Proof. unfold decode, accumulate. - induction bs; destruct us; destruct vs; auto; simpl; try rewrite IHc; ring. + induction bs; destruct us; destruct vs; auto; simpl; try rewrite IHbs; ring. Qed. - (* mul' is a valid multiplication algorithm if b_i = b_1^i *) - Fixpoint mul' (us vs:digits) : digits := + Lemma decode_nil : forall bs, decode bs nil = 0. + auto. + Qed. + + (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *) + Fixpoint mul_geomseq (us vs:digits) : digits := match us,vs with - | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul' us' vs + | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs | _, _ => nil end. - (* UPNEXT: multiplication for arbitrary good bs *) + Definition mul_each u := map (Z.mul u). + Lemma mul_each_rep : forall bs u vs, decode bs (mul_each u vs) = u * decode bs vs. + Proof. + unfold decode, accumulate. + induction bs; destruct vs; auto; simpl; try rewrite IHbs; ring. + Qed. + + Definition crosscoef i j : Z := + let b := nth_default 0 base in + (b(i) * b(j)) / b(i+j)%nat. + + Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end. + Lemma zeros_rep : forall bs n, decode bs (zeros n) = 0. + unfold decode, accumulate. + induction bs; destruct n; auto; simpl; try rewrite IHbs; ring. + Qed. + Lemma length_zeros : forall n, length (zeros n) = n. + induction n; simpl; auto. + Qed. + + Lemma app_zeros_zeros : forall n m, (zeros n ++ zeros m) = zeros (n + m). + Admitted. + + Lemma zeros_app0 : forall m, (zeros m ++ 0 :: nil) = zeros (S m). + Admitted. + + Lemma rev_zeros : forall n, rev (zeros n) = zeros n. + Admitted. + + Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. + Admitted. + + (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) + Fixpoint mul_bi' (i:nat) (vsr:digits) := + match vsr with + | v::vsr' => v * crosscoef i (length vsr') :: mul_bi' i vsr' + | nil => nil + end. + Definition mul_bi (i:nat) (vs:digits) : digits := + zeros i ++ rev (mul_bi' i (rev vs)). + + (* + Definition mul_bi (i:nat) (vs:digits) : digits := + let mkEntry := (fun (p:(nat*Z)) => let (j, v) := p in v * crosscoef i j) in + zeros i ++ map mkEntry (@enumerate Z vs). + *) + + Lemma decode_single : forall n bs x, + decode bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. + Proof. + induction n; intros; simpl. + destruct bs; auto; unfold decode, accumulate, nth_default; simpl; ring. + destruct bs; simpl; auto. + unfold decode, accumulate, nth_default in *; simpl in *; auto. + Qed. + + Lemma peel_decode : forall xs ys x y, decode (x::xs) (y::ys) = x*y + decode xs ys. + intros. + unfold decode, accumulate, nth_default in *; simpl in *; ring_simplify; auto. + Qed. + + Lemma decode_highzeros : forall xs bs n, decode bs (xs ++ zeros n) = decode bs xs. + induction xs; intros; simpl; try rewrite zeros_rep; auto. + destruct bs; simpl; auto. + repeat (rewrite peel_decode). + rewrite IHxs; auto. + Qed. + + Lemma mul_bi_single : forall m n x, + decode base (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. + Proof. + unfold mul_bi. + destruct m; simpl; ssimpl_list; simpl; intros. + rewrite decode_single. + unfold crosscoef; simpl. + rewrite plus_0_r. + ring_simplify. + replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. + SearchAbout Z.div. + rewrite Z_div_mult; try ring. + + assert (nth_default 0 base n > 0) by admit; auto. + + intros; simpl; ssimpl_list; simpl. + replace (mul_bi' n (rev (zeros m) ++ 0 :: nil)) with (zeros (S m)) by admit. + intros; simpl; ssimpl_list; simpl. + rewrite length_zeros. + rewrite app_cons_app_app. + rewrite rev_zeros. + intros; simpl; ssimpl_list; simpl. + rewrite zeros_app0. + rewrite app_assoc. + rewrite app_zeros_zeros. + rewrite decode_single. + unfold crosscoef; simpl; ring_simplify. + rewrite NPeano.Nat.add_1_r. + rewrite bs_good. + rewrite Z_div_mult. + rewrite <- Z.mul_assoc. + rewrite <- Z.mul_comm. + rewrite <- Z.mul_assoc. + rewrite <- Z.mul_assoc. + destruct (Z.eq_dec x 0); subst; try ring. + rewrite Z.mul_cancel_l by auto. + rewrite <- bs_good. + ring. + + assert (nth_default 0 base (n + S m) > 0) by admit; auto. + Qed. + + Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil). + induction vs; auto. + intros; simpl; rewrite IHvs; f_equal; ring. + Qed. + + Lemma set_higher : forall bs vs x, + decode bs (vs++x::nil) = decode bs vs + nth_default 0 bs (length vs) * x. + Proof. + intros. + rewrite set_higher'. + rewrite add_rep. + f_equal. + apply decode_single. + Qed. + + Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n. + induction n; auto. + simpl; f_equal; auto. + Qed. + + Lemma mul_bi_add : forall n us vs, + mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. + Proof. + Admitted. + + Lemma mul_bi_rep : forall i vs, decode base (mul_bi i vs) = decode base vs * nth_default 0 base i. + induction vs using rev_ind; intros; simpl. { + unfold mul_bi. + ssimpl_list; rewrite zeros_rep; simpl. + unfold decode; simpl. + ring. + } { + rewrite set_higher. + ring_simplify. + rewrite <- IHvs; clear IHvs. + rewrite <- mul_bi_single. + rewrite <- add_rep. + rewrite <- mul_bi_add. + rewrite set_higher'. + auto. + } + Qed. + + (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) + Fixpoint mul' (usr vs:digits) : digits := + match usr with + | u::usr' => + mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs + | _ => nil + end. + Definition mul us := mul' (rev us). + Local Infix "#*" := mul (at level 40). + + Lemma mul'_rep : forall us vs, decode base (mul' (rev us) vs) = decode base us * decode base vs. + induction us using rev_ind; intros; simpl; try apply decode_nil. + ssimpl_list. + rewrite add_rep. + rewrite IHus; clear IHus. + rewrite set_higher. + rewrite mul_each_rep. + rewrite mul_bi_rep. + ring. + Qed. + + Lemma mul_rep : forall us vs, decode base (us #* vs) = decode base us * decode base vs. + apply mul'_rep. + Qed. End BaseSystem. -- cgit v1.2.3 From cdddf649a0dadd0604235338c2dd7371c04d4653 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 11:40:24 -0400 Subject: bounds checks --- src/Galois/BaseSystem.v | 121 ++++++++++++++++++++++++++++++------------------ 1 file changed, 77 insertions(+), 44 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index ac42b7c79..ecd21b56e 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -9,7 +9,8 @@ Module Type BaseCoefs. Definition coefs : Type := list Z. Parameter base : coefs. - Axiom bs_good : + Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too *) + Axiom base_good : forall i j, let b := nth_default 0 base in let r := (b i * b j) / b (i+j)%nat in @@ -117,45 +118,53 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Lemma mul_bi_single : forall m n x, + (n + m < length base)%nat -> decode base (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. Proof. unfold mul_bi. - destruct m; simpl; ssimpl_list; simpl; intros. - rewrite decode_single. - unfold crosscoef; simpl. - rewrite plus_0_r. - ring_simplify. - replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. - SearchAbout Z.div. - rewrite Z_div_mult; try ring. - - assert (nth_default 0 base n > 0) by admit; auto. - - intros; simpl; ssimpl_list; simpl. - replace (mul_bi' n (rev (zeros m) ++ 0 :: nil)) with (zeros (S m)) by admit. - intros; simpl; ssimpl_list; simpl. - rewrite length_zeros. - rewrite app_cons_app_app. - rewrite rev_zeros. - intros; simpl; ssimpl_list; simpl. - rewrite zeros_app0. - rewrite app_assoc. - rewrite app_zeros_zeros. - rewrite decode_single. - unfold crosscoef; simpl; ring_simplify. - rewrite NPeano.Nat.add_1_r. - rewrite bs_good. - rewrite Z_div_mult. - rewrite <- Z.mul_assoc. - rewrite <- Z.mul_comm. - rewrite <- Z.mul_assoc. - rewrite <- Z.mul_assoc. - destruct (Z.eq_dec x 0); subst; try ring. - rewrite Z.mul_cancel_l by auto. - rewrite <- bs_good. - ring. + destruct m; simpl; ssimpl_list; simpl; intros. { + rewrite decode_single. + unfold crosscoef; simpl. + rewrite plus_0_r. + ring_simplify. + replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. + SearchAbout Z.div. + rewrite Z_div_mult; try ring. + + apply base_positive. + rewrite nth_default_eq. + apply nth_In. + rewrite plus_0_r in *. + auto. + } { + simpl; ssimpl_list; simpl. + replace (mul_bi' n (rev (zeros m) ++ 0 :: nil)) with (zeros (S m)) by admit. + intros; simpl; ssimpl_list; simpl. + rewrite length_zeros. + rewrite app_cons_app_app. + rewrite rev_zeros. + intros; simpl; ssimpl_list; simpl. + rewrite zeros_app0. + rewrite app_assoc. + rewrite app_zeros_zeros. + rewrite decode_single. + unfold crosscoef; simpl; ring_simplify. + rewrite NPeano.Nat.add_1_r. + rewrite base_good. + rewrite Z_div_mult. + rewrite <- Z.mul_assoc. + rewrite <- Z.mul_comm. + rewrite <- Z.mul_assoc. + rewrite <- Z.mul_assoc. + destruct (Z.eq_dec x 0); subst; try ring. + rewrite Z.mul_cancel_l by auto. + rewrite <- base_good. + ring. - assert (nth_default 0 base (n + S m) > 0) by admit; auto. + apply base_positive. + rewrite nth_default_eq. + apply nth_In; auto. + } Qed. Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil). @@ -183,17 +192,27 @@ Module BaseSystem (Import B:BaseCoefs). Proof. Admitted. - Lemma mul_bi_rep : forall i vs, decode base (mul_bi i vs) = decode base vs * nth_default 0 base i. + Lemma mul_bi_rep : forall i vs, + (i + length vs < length base)%nat -> + decode base (mul_bi i vs) = decode base vs * nth_default 0 base i. + Proof. induction vs using rev_ind; intros; simpl. { unfold mul_bi. ssimpl_list; rewrite zeros_rep; simpl. unfold decode; simpl. ring. } { + assert (i + length vs < length base)%nat as inbounds. { + rewrite app_length in *; simpl in *. + rewrite NPeano.Nat.add_1_r, <- plus_n_Sm in *. + etransitivity; eauto. + } + rewrite set_higher. ring_simplify. - rewrite <- IHvs; clear IHvs. - rewrite <- mul_bi_single. + rewrite <- IHvs by auto; clear IHvs. + simpl in *. + rewrite <- mul_bi_single by auto. rewrite <- add_rep. rewrite <- mul_bi_add. rewrite set_higher'. @@ -211,18 +230,32 @@ Module BaseSystem (Import B:BaseCoefs). Definition mul us := mul' (rev us). Local Infix "#*" := mul (at level 40). - Lemma mul'_rep : forall us vs, decode base (mul' (rev us) vs) = decode base us * decode base vs. + Lemma mul'_rep : forall us vs, + (length us + length vs <= length base)%nat -> + decode base (mul' (rev us) vs) = decode base us * decode base vs. + Proof. induction us using rev_ind; intros; simpl; try apply decode_nil. + + assert (length us + length vs < length base)%nat as inbounds. { + rewrite app_length in *; simpl in *. + rewrite plus_comm in *. + rewrite NPeano.Nat.add_1_r, <- plus_n_Sm in *. + auto. + } + ssimpl_list. rewrite add_rep. - rewrite IHus; clear IHus. + rewrite IHus by (rewrite le_trans; eauto); clear IHus. rewrite set_higher. rewrite mul_each_rep. - rewrite mul_bi_rep. + rewrite mul_bi_rep by auto. ring. Qed. - Lemma mul_rep : forall us vs, decode base (us #* vs) = decode base us * decode base vs. - apply mul'_rep. + Lemma mul_rep : forall us vs, + (length us + length vs <= length base)%nat -> + decode base (us #* vs) = decode base us * decode base vs. + Proof. + exact mul'_rep. Qed. End BaseSystem. -- cgit v1.2.3 From d02084f328a2f7253cfee94ffa01bb845827fd2c Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 15:21:07 -0400 Subject: slight refactoring of BaseSystem --- src/Galois/BaseSystem.v | 183 +++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 148 insertions(+), 35 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index ecd21b56e..4c50a193e 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,28 +1,57 @@ Require Import List. Require Import ZArith.ZArith ZArith.Zdiv. + Require Import Omega. + +Lemma nth_error_map : forall A B (f:A->B) xs i y, + nth_error (map f xs) i = Some y -> + exists x, nth_error xs i = Some x /\ f x = y. +Admitted. + +Lemma nth_error_seq : forall start len i, + nth_error (seq start len) i = + if lt_dec i len + then Some (start + i) + else None. +Admitted. + +Lemma nth_error_length_error : forall A (xs:list A) i, nth_error xs i = None -> + i >= length xs. +Admitted. Local Open Scope Z. -Module Type BaseCoefs. - (* lists coefficients of digits and the digits themselves always have the - * LEAST significant position first. *) - Definition coefs : Type := list Z. +Lemma pos_pow_nat_pos : forall x n, + Z.pos x ^ Z.of_nat n > 0. +Admitted. - Parameter base : coefs. - Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too *) +Module Type BaseCoefs. + (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *) + Parameter base : list Z. + Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too... *) Axiom base_good : - forall i j, + forall i j, (i+j < length base)%nat -> let b := nth_default 0 base in let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. End BaseCoefs. Module BaseSystem (Import B:BaseCoefs). + (** [BaseSystem] implements an constrained positional number system. + A wide variety of bases are supported: the base coefficients are not + required to be powers of 2, and it is NOT necessarily the case that + $b_{i+j} = b_j b_j$. Implementations of addition and multiplication are + provided, with focus on near-optimal multiplication performance on + non-trivial but small operands: maybe 10 32-bit integers or so. This + module does not handle carries automatically: if no restrictions are put + on the use of a [BaseSystem], each digit is unbounded. This has nothing + to do with modular arithmetic either. + *) Definition digits : Type := list Z. Definition accumulate p acc := fst p * snd p + acc. - Definition decode bs u := fold_right accumulate 0 (combine u bs). - Hint Unfold decode accumulate. + Definition decode' bs u := fold_right accumulate 0 (combine u bs). + Definition decode := decode' base. + Hint Unfold decode' accumulate. Fixpoint add (us vs:digits) : digits := match us,vs with @@ -30,15 +59,15 @@ Module BaseSystem (Import B:BaseCoefs). | _, nil => us | _, _ => vs end. - Local Infix ".+" := add (at level 50). + Infix ".+" := add (at level 50). - Lemma add_rep : forall bs us vs, decode bs (add us vs) = decode bs us + decode bs vs. + Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs. Proof. - unfold decode, accumulate. + unfold decode', accumulate. induction bs; destruct us; destruct vs; auto; simpl; try rewrite IHbs; ring. Qed. - Lemma decode_nil : forall bs, decode bs nil = 0. + Lemma decode_nil : forall bs, decode' bs nil = 0. auto. Qed. @@ -50,9 +79,9 @@ Module BaseSystem (Import B:BaseCoefs). end. Definition mul_each u := map (Z.mul u). - Lemma mul_each_rep : forall bs u vs, decode bs (mul_each u vs) = u * decode bs vs. + Lemma mul_each_rep : forall bs u vs, decode' bs (mul_each u vs) = u * decode' bs vs. Proof. - unfold decode, accumulate. + unfold decode', accumulate. induction bs; destruct vs; auto; simpl; try rewrite IHbs; ring. Qed. @@ -61,8 +90,8 @@ Module BaseSystem (Import B:BaseCoefs). (b(i) * b(j)) / b(i+j)%nat. Fixpoint zeros n := match n with O => nil | S n' => 0::zeros n' end. - Lemma zeros_rep : forall bs n, decode bs (zeros n) = 0. - unfold decode, accumulate. + Lemma zeros_rep : forall bs n, decode' bs (zeros n) = 0. + unfold decode', accumulate. induction bs; destruct n; auto; simpl; try rewrite IHbs; ring. Qed. Lemma length_zeros : forall n, length (zeros n) = n. @@ -97,20 +126,20 @@ Module BaseSystem (Import B:BaseCoefs). *) Lemma decode_single : forall n bs x, - decode bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. + decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. Proof. induction n; intros; simpl. - destruct bs; auto; unfold decode, accumulate, nth_default; simpl; ring. + destruct bs; auto; unfold decode', accumulate, nth_default; simpl; ring. destruct bs; simpl; auto. - unfold decode, accumulate, nth_default in *; simpl in *; auto. + unfold decode', accumulate, nth_default in *; simpl in *; auto. Qed. - Lemma peel_decode : forall xs ys x y, decode (x::xs) (y::ys) = x*y + decode xs ys. + Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys. intros. - unfold decode, accumulate, nth_default in *; simpl in *; ring_simplify; auto. + unfold decode', accumulate, nth_default in *; simpl in *; ring_simplify; auto. Qed. - Lemma decode_highzeros : forall xs bs n, decode bs (xs ++ zeros n) = decode bs xs. + Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs. induction xs; intros; simpl; try rewrite zeros_rep; auto. destruct bs; simpl; auto. repeat (rewrite peel_decode). @@ -119,9 +148,9 @@ Module BaseSystem (Import B:BaseCoefs). Lemma mul_bi_single : forall m n x, (n + m < length base)%nat -> - decode base (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. + decode (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. Proof. - unfold mul_bi. + unfold mul_bi, decode. destruct m; simpl; ssimpl_list; simpl; intros. { rewrite decode_single. unfold crosscoef; simpl. @@ -150,7 +179,7 @@ Module BaseSystem (Import B:BaseCoefs). rewrite decode_single. unfold crosscoef; simpl; ring_simplify. rewrite NPeano.Nat.add_1_r. - rewrite base_good. + rewrite base_good by auto. rewrite Z_div_mult. rewrite <- Z.mul_assoc. rewrite <- Z.mul_comm. @@ -158,7 +187,7 @@ Module BaseSystem (Import B:BaseCoefs). rewrite <- Z.mul_assoc. destruct (Z.eq_dec x 0); subst; try ring. rewrite Z.mul_cancel_l by auto. - rewrite <- base_good. + rewrite <- base_good by auto. ring. apply base_positive. @@ -173,7 +202,7 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Lemma set_higher : forall bs vs x, - decode bs (vs++x::nil) = decode bs vs + nth_default 0 bs (length vs) * x. + decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x. Proof. intros. rewrite set_higher'. @@ -194,12 +223,13 @@ Module BaseSystem (Import B:BaseCoefs). Lemma mul_bi_rep : forall i vs, (i + length vs < length base)%nat -> - decode base (mul_bi i vs) = decode base vs * nth_default 0 base i. + decode (mul_bi i vs) = decode vs * nth_default 0 base i. Proof. + unfold decode. induction vs using rev_ind; intros; simpl. { - unfold mul_bi. + unfold mul_bi, decode. ssimpl_list; rewrite zeros_rep; simpl. - unfold decode; simpl. + unfold decode'; simpl. ring. } { assert (i + length vs < length base)%nat as inbounds. { @@ -228,12 +258,13 @@ Module BaseSystem (Import B:BaseCoefs). | _ => nil end. Definition mul us := mul' (rev us). - Local Infix "#*" := mul (at level 40). + Infix "#*" := mul (at level 40). Lemma mul'_rep : forall us vs, (length us + length vs <= length base)%nat -> - decode base (mul' (rev us) vs) = decode base us * decode base vs. + decode (mul' (rev us) vs) = decode us * decode vs. Proof. + unfold decode. induction us using rev_ind; intros; simpl; try apply decode_nil. assert (length us + length vs < length base)%nat as inbounds. { @@ -248,14 +279,96 @@ Module BaseSystem (Import B:BaseCoefs). rewrite IHus by (rewrite le_trans; eauto); clear IHus. rewrite set_higher. rewrite mul_each_rep. - rewrite mul_bi_rep by auto. + rewrite mul_bi_rep by auto; unfold decode. ring. Qed. Lemma mul_rep : forall us vs, (length us + length vs <= length base)%nat -> - decode base (us #* vs) = decode base us * decode base vs. + decode (us #* vs) = decode us * decode vs. Proof. exact mul'_rep. Qed. End BaseSystem. + +Module Type PolynomialBaseParams. + Parameter b1 : positive. (* the value at which the polynomial is evaluated *) + Parameter baseLength : nat. (* 1 + degree of the polynomial *) +End PolynomialBaseParams. + +Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. + (** PolynomialBaseCoeffs generates base vectors for [BaseSystem] using the extra assumption that $b_{i+j} = b_j b_j$. *) + Definition bi i := (Zpos b1)^(Z.of_nat i). + Definition base := map bi (seq 0 baseLength). + + Lemma base_positive : forall b, In b base -> b > 0. + unfold base. + intros until 0; intro H. + rewrite in_map_iff in *. + destruct H; destruct H. + subst. + apply pos_pow_nat_pos. + Qed. + + Lemma base_good: + forall i j, (i + j < length base)%nat -> + let b := nth_default 0 base in + let r := (b i * b j) / b (i+j)%nat in + b i * b j = r * b (i+j)%nat. + Proof. + unfold base, nth_default. + intros; repeat progress (match goal with + | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros + | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H + | [ H: _ /\ _ |- _ ] => destruct H + | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H + | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst + | [ H: None = Some _ |- _ ] => inversion H + | [ H: Some _ = None |- _ ] => inversion H + | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H + end); autorewrite with list in *; try omega. + + clear. + unfold bi. + rewrite Nat2Z.inj_add, Zpower_exp by + (replace 0 with (Z.of_nat 0) by auto; rewrite <- Nat2Z.inj_ge; omega). + rewrite Z_div_same_full; try ring. + rewrite <- Z.neq_mul_0. + split; apply Z.pow_nonzero; try apply Zle_0_nat; try solve [intro H; inversion H]. + Qed. +End PolynomialBaseCoefs. + +Module BasePoly2Degree32Params <: PolynomialBaseParams. + Definition b1 := 2%positive. + Definition baseLength := 32%nat. +End BasePoly2Degree32Params. + +Import ListNotations. + +Module BaseSystemExample. + Module BasePoly2Degree32Coefs := PolynomialBaseCoefs BasePoly2Degree32Params. + Module BasePoly2Degree32 := BaseSystem BasePoly2Degree32Coefs. + Import BasePoly2Degree32. + + Example three_times_two : [1;1;0] #* [0;1;0] = [0;1;1;0;0]. + compute; reflexivity. + Qed. + + (* python -c "e = lambda x: '['+''.join(reversed(bin(x)[2:])).replace('1','1;').replace('0','0;')[:-1]+']'; print(e(19259)); print(e(41781))" *) + Definition a := [1;1;0;1;1;1;0;0;1;1;0;1;0;0;1]. + Definition b := [1;0;1;0;1;1;0;0;1;1;0;0;0;1;0;1]. + Example da : decode a = 19259. + compute. reflexivity. + Qed. + Example db : decode b = 41781. + compute. reflexivity. + Qed. + Example encoded_ab : + a #*b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1]. + compute. reflexivity. + Qed. + Example dab : decode (a #* b) = 804660279. + compute. reflexivity. + Qed. +End BaseSystemExample. -- cgit v1.2.3 From 277fbcc216245a32e11044c5794f57f68591bb42 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 18:07:45 -0400 Subject: nth_tac --- src/Galois/BaseSystem.v | 52 ++++++++++++++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 20 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 4c50a193e..b60a16fb2 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,22 +1,45 @@ Require Import List. Require Import ZArith.ZArith ZArith.Zdiv. - Require Import Omega. - -Lemma nth_error_map : forall A B (f:A->B) xs i y, +Require Import Omega. + +Ltac nth_tac' := + intros; simpl in *; unfold error,value in *; repeat progress (match goal with + | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros + | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) + | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ H: _ /\ _ |- _ ] => destruct H + | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst + | [ H: None = Some _ |- _ ] => inversion H + | [ H: Some _ = None |- _ ] => inversion H + | [ |- Some _ = Some _ ] => apply f_equal + end); eauto; try (autorewrite with list in *); try omega; eauto. +Lemma nth_error_map : forall A B (f:A->B) i xs y, nth_error (map f xs) i = Some y -> exists x, nth_error xs i = Some x /\ f x = y. -Admitted. +Proof. + induction i; destruct xs; nth_tac'. +Qed. -Lemma nth_error_seq : forall start len i, +Lemma nth_error_seq : forall i start len, nth_error (seq start len) i = if lt_dec i len then Some (start + i) else None. -Admitted. + induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. +Qed. -Lemma nth_error_length_error : forall A (xs:list A) i, nth_error xs i = None -> +Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None -> i >= length xs. -Admitted. +Proof. + induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. +Qed. + +Ltac nth_tac := + repeat progress (try nth_tac'; try (match goal with + | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H + | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H + | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H + end)). Local Open Scope Z. @@ -316,18 +339,7 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. Proof. - unfold base, nth_default. - intros; repeat progress (match goal with - | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros - | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H - | [ H: _ /\ _ |- _ ] => destruct H - | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H - | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) - | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst - | [ H: None = Some _ |- _ ] => inversion H - | [ H: Some _ = None |- _ ] => inversion H - | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H - end); autorewrite with list in *; try omega. + unfold base, nth_default; nth_tac. clear. unfold bi. -- cgit v1.2.3 From d655b90707449b7ebb2aa661fef6d947d9d88c58 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 18:23:02 -0400 Subject: pos_pow_nat_pos --- src/Galois/BaseSystem.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index b60a16fb2..036b9d5b1 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -45,7 +45,11 @@ Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. -Admitted. + do 2 (intros; induction n; subst; simpl in *; auto with zarith). + SearchAbout Pos.succ. + rewrite <- Pos.add_1_r, Zpower_pos_is_exp. + apply Zmult_gt_0_compat; auto; compute; auto. +Qed. Module Type BaseCoefs. (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *) -- cgit v1.2.3 From cdae9d225576146dc88902a466173170ee7e9dc1 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 28 Oct 2015 14:07:05 -0400 Subject: Tiny module-system tweaks in PointFormats --- .gitignore | 1 + src/Curves/PointFormats.v | 24 ++++++++++++++---------- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/.gitignore b/.gitignore index ae784f4a5..cec91e9a6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ +bedrock fiat *~ diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 7af310257..baa6bd2a7 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -78,8 +78,8 @@ Module PointFormats. End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (Import ta:TwistedA) (Import td:TwistedD). - Module M := CompleteTwistedEdwardsSpec ta td. - Import M. + Module Import Spec := CompleteTwistedEdwardsSpec ta td. + Lemma twistedAddCompletePlus : forall (P1 P2:point) (oc1:onCurve P1) (oc2:onCurve P2), let x1 := projX P1 in @@ -131,7 +131,7 @@ Module PointFormats. Module CompleteTwistedEdwardsSpecPointFormat (ta:TwistedA) (td:TwistedD) - <: (CompleteTwistedEdwardsPointFormat ta td). + <: CompleteTwistedEdwardsPointFormat ta td. Module Spec := CompleteTwistedEdwardsSpec ta td. Definition point := Spec.point. Definition mkPoint := Spec.mkPoint. @@ -178,16 +178,18 @@ Module PointFormats. End ta. Import ta. - Module M := CompleteTwistedEdwardsSpec ta td. + Module Spec := CompleteTwistedEdwardsSpec ta td. Module Format <: CompleteTwistedEdwardsPointFormat ta td. - Module Spec := CompleteTwistedEdwardsSpec ta td. + Module Import Facts := CompleteTwistedEdwardsFacts ta td. + (** [projective] represents a point on an elliptic curve using projective * Edwards coordinates for twisted edwards curves with a=-1 (see * * ) *) Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}. Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z). + Definition twistedToProjective (P : Spec.point) : projective := let x := Spec.projX P in let y := Spec.projY P in @@ -205,11 +207,6 @@ Module PointFormats. Lemma twistedProjectiveInv : forall P, projectiveToTwisted (twistedToProjective P) = P. Proof. - (* FIXME: this is copied from CompleteTwistedEdwardsFacts because I don't know how to get it to be in scope here *) - Ltac twisted := autounfold; intros; - repeat match goal with - | [ x : Spec.point |- _ ] => destruct x - end; simpl; repeat (ring || f_equal); field. twisted. Qed. @@ -246,6 +243,7 @@ Module PointFormats. Qed. Lemma twistedToExtendedValid : forall (P : Spec.point), extendedValid (twistedToExtended P). + Proof. autounfold. destruct P. simpl. @@ -255,6 +253,7 @@ Module PointFormats. Definition rep (P:point) (rP:Spec.point) : Prop := extendedToTwisted P = rP /\ extendedValid P. Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Spec.mkPoint x y). + Proof. split. apply twistedExtendedInv. apply twistedToExtendedValid. @@ -268,9 +267,11 @@ Module PointFormats. | [ x : rep ?a ?b |- _ ] => destruct x end). Lemma projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP. + Proof. rep. Qed. Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP. + Proof. rep. Qed. @@ -353,10 +354,13 @@ Module PointFormats. Lemma unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ -> P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ). + Proof. split; rep. apply unifiedAddToTwisted; auto. apply unifiedAddCon; auto. Qed. + + Module Spec := Spec. End Format. End Minus1Twisted. -- cgit v1.2.3 From 2dbf88adb2710ff9ef7cea115e5108f8009cea28 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 28 Oct 2015 14:56:44 -0400 Subject: Proof improvements in BaseSystem --- src/Galois/BaseSystem.v | 126 +++++++++++++++++++++++++++++++----------------- 1 file changed, 81 insertions(+), 45 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 036b9d5b1..55b7b66dd 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -48,7 +48,7 @@ Lemma pos_pow_nat_pos : forall x n, do 2 (intros; induction n; subst; simpl in *; auto with zarith). SearchAbout Pos.succ. rewrite <- Pos.add_1_r, Zpower_pos_is_exp. - apply Zmult_gt_0_compat; auto; compute; auto. + apply Zmult_gt_0_compat; auto; reflexivity. Qed. Module Type BaseCoefs. @@ -66,7 +66,7 @@ Module BaseSystem (Import B:BaseCoefs). (** [BaseSystem] implements an constrained positional number system. A wide variety of bases are supported: the base coefficients are not required to be powers of 2, and it is NOT necessarily the case that - $b_{i+j} = b_j b_j$. Implementations of addition and multiplication are + $b_{i+j} = b_i b_j$. Implementations of addition and multiplication are provided, with focus on near-optimal multiplication performance on non-trivial but small operands: maybe 10 32-bit integers or so. This module does not handle carries automatically: if no restrictions are put @@ -78,14 +78,14 @@ Module BaseSystem (Import B:BaseCoefs). Definition accumulate p acc := fst p * snd p + acc. Definition decode' bs u := fold_right accumulate 0 (combine u bs). Definition decode := decode' base. - Hint Unfold decode' accumulate. - - Fixpoint add (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => (u+v)::(add us' vs') - | _, nil => us - | _, _ => vs - end. + Hint Unfold accumulate. + + Fixpoint add (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => u+v :: add us' vs' + | _, nil => us + | _, _ => vs + end. Infix ".+" := add (at level 50). Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs. @@ -100,10 +100,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *) Fixpoint mul_geomseq (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs - | _, _ => nil - end. + match us,vs with + | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs + | _, _ => nil + end. Definition mul_each u := map (Z.mul u). Lemma mul_each_rep : forall bs u vs, decode' bs (mul_each u vs) = u * decode' bs vs. @@ -125,17 +125,37 @@ Module BaseSystem (Import B:BaseCoefs). induction n; simpl; auto. Qed. - Lemma app_zeros_zeros : forall n m, (zeros n ++ zeros m) = zeros (n + m). - Admitted. + Ltac boring := + simpl; intuition; + repeat match goal with + | [ H : _ |- _ ] => rewrite H; clear H + | _ => progress autounfold in * + | _ => progress try autorewrite with core + | _ => progress simpl in * + | _ => progress intuition + end; ring || eauto. + + Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m). + Proof. + induction n; boring. + Qed. - Lemma zeros_app0 : forall m, (zeros m ++ 0 :: nil) = zeros (S m). - Admitted. + Lemma zeros_app0 : forall m, zeros m ++ 0 :: nil = zeros (S m). + Proof. + induction m; boring. + Qed. + + Hint Rewrite zeros_app0. Lemma rev_zeros : forall n, rev (zeros n) = zeros n. - Admitted. + Proof. + induction n; boring. + Qed. Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. - Admitted. + Proof. + induction xs; boring. + Qed. (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) Fixpoint mul_bi' (i:nat) (vsr:digits) := @@ -146,36 +166,47 @@ Module BaseSystem (Import B:BaseCoefs). Definition mul_bi (i:nat) (vs:digits) : digits := zeros i ++ rev (mul_bi' i (rev vs)). + Infix ".*" := mul_bi (at level 40). + (* Definition mul_bi (i:nat) (vs:digits) : digits := let mkEntry := (fun (p:(nat*Z)) => let (j, v) := p in v * crosscoef i j) in zeros i ++ map mkEntry (@enumerate Z vs). *) + Hint Unfold nth_default. + + Hint Extern 1 (@eq Z _ _) => ring. + + Lemma decode'_cons : forall x1 x2 xs1 xs2, + decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2. + Proof. + unfold decode'; boring. + Qed. + + Hint Rewrite decode'_cons. + Lemma decode_single : forall n bs x, decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. Proof. - induction n; intros; simpl. - destruct bs; auto; unfold decode', accumulate, nth_default; simpl; ring. - destruct bs; simpl; auto. - unfold decode', accumulate, nth_default in *; simpl in *; auto. + induction n; destruct bs; boring. Qed. Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys. - intros. - unfold decode', accumulate, nth_default in *; simpl in *; ring_simplify; auto. + Proof. + boring. Qed. + Hint Rewrite zeros_rep peel_decode. + Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs. - induction xs; intros; simpl; try rewrite zeros_rep; auto. - destruct bs; simpl; auto. - repeat (rewrite peel_decode). - rewrite IHxs; auto. + Proof. + induction xs; destruct bs; boring. Qed. Lemma mul_bi_single : forall m n x, (n + m < length base)%nat -> - decode (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. + decode (n .* (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. Proof. unfold mul_bi, decode. destruct m; simpl; ssimpl_list; simpl; intros. { @@ -224,10 +255,9 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil). - induction vs; auto. - intros; simpl; rewrite IHvs; f_equal; ring. + induction vs; boring; f_equal; ring. Qed. - + Lemma set_higher : forall bs vs x, decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x. Proof. @@ -244,13 +274,13 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Lemma mul_bi_add : forall n us vs, - mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. + n .* (us .+ vs) = n .* us .+ n .* vs. Proof. Admitted. Lemma mul_bi_rep : forall i vs, (i + length vs < length base)%nat -> - decode (mul_bi i vs) = decode vs * nth_default 0 base i. + decode (i .* vs) = decode vs * nth_default 0 base i. Proof. unfold decode. induction vs using rev_ind; intros; simpl. { @@ -279,10 +309,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => - mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs - | _ => nil + match usr with + | u::usr' => + mul_each u (length usr' .* vs) .+ mul' usr' vs + | _ => nil end. Definition mul us := mul' (rev us). Infix "#*" := mul (at level 40). @@ -329,6 +359,7 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. Definition base := map bi (seq 0 baseLength). Lemma base_positive : forall b, In b base -> b > 0. + Proof. unfold base. intros until 0; intro H. rewrite in_map_iff in *. @@ -368,23 +399,28 @@ Module BaseSystemExample. Import BasePoly2Degree32. Example three_times_two : [1;1;0] #* [0;1;0] = [0;1;1;0;0]. - compute; reflexivity. + Proof. + reflexivity. Qed. (* python -c "e = lambda x: '['+''.join(reversed(bin(x)[2:])).replace('1','1;').replace('0','0;')[:-1]+']'; print(e(19259)); print(e(41781))" *) Definition a := [1;1;0;1;1;1;0;0;1;1;0;1;0;0;1]. Definition b := [1;0;1;0;1;1;0;0;1;1;0;0;0;1;0;1]. Example da : decode a = 19259. - compute. reflexivity. + Proof. + reflexivity. Qed. Example db : decode b = 41781. - compute. reflexivity. + Proof. + reflexivity. Qed. Example encoded_ab : a #*b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1]. - compute. reflexivity. + Proof. + reflexivity. Qed. Example dab : decode (a #* b) = 804660279. - compute. reflexivity. + Proof. + reflexivity. Qed. End BaseSystemExample. -- cgit v1.2.3 From a7a2d882691af1cddd729f1f871c467900b9ac4e Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Oct 2015 00:53:26 -0400 Subject: remove SearchAbouts --- src/Galois/BaseSystem.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 55b7b66dd..e818660e8 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -46,7 +46,6 @@ Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. do 2 (intros; induction n; subst; simpl in *; auto with zarith). - SearchAbout Pos.succ. rewrite <- Pos.add_1_r, Zpower_pos_is_exp. apply Zmult_gt_0_compat; auto; reflexivity. Qed. @@ -215,7 +214,6 @@ Module BaseSystem (Import B:BaseCoefs). rewrite plus_0_r. ring_simplify. replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. - SearchAbout Z.div. rewrite Z_div_mult; try ring. apply base_positive. -- cgit v1.2.3 From 2cb694b68c8d28b2049936f1c20349200eb121c2 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Oct 2015 00:54:22 -0400 Subject: remove resolved todo --- src/Curves/PointFormats.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index baa6bd2a7..8ab81e0a8 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -66,8 +66,6 @@ Module PointFormats. Parameter projY : point -> GF. Parameter unifiedAdd : point -> point -> point. - (* TODO: split module here? *) - Parameter rep : point -> Spec.point -> Prop. Local Notation "P '~=' rP" := (rep P rP) (at level 70). Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y. -- cgit v1.2.3 From 9882ffed11619425880c87fe11d2357569a58203 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 Oct 2015 20:14:52 -0400 Subject: BaseSystem to Util.ListUtil: separate out generic list lemmas --- _CoqProject | 1 + src/Galois/BaseSystem.v | 40 +--------------------------------------- src/Util/ListUtil.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 39 deletions(-) create mode 100644 src/Util/ListUtil.v diff --git a/_CoqProject b/_CoqProject index bbb167dc3..3b45e81b9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ -R fiat/src Fiat -R bedrock/Bedrock Bedrock src/Tactics/VerdiTactics.v +src/Util/ListUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v src/Galois/GaloisExamples.v diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index e818660e8..77428e549 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,46 +1,8 @@ Require Import List. +Require Import Util.ListUtil. Require Import ZArith.ZArith ZArith.Zdiv. Require Import Omega. -Ltac nth_tac' := - intros; simpl in *; unfold error,value in *; repeat progress (match goal with - | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros - | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) - | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) - | [ H: _ /\ _ |- _ ] => destruct H - | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst - | [ H: None = Some _ |- _ ] => inversion H - | [ H: Some _ = None |- _ ] => inversion H - | [ |- Some _ = Some _ ] => apply f_equal - end); eauto; try (autorewrite with list in *); try omega; eauto. -Lemma nth_error_map : forall A B (f:A->B) i xs y, - nth_error (map f xs) i = Some y -> - exists x, nth_error xs i = Some x /\ f x = y. -Proof. - induction i; destruct xs; nth_tac'. -Qed. - -Lemma nth_error_seq : forall i start len, - nth_error (seq start len) i = - if lt_dec i len - then Some (start + i) - else None. - induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. -Qed. - -Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None -> - i >= length xs. -Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. -Qed. - -Ltac nth_tac := - repeat progress (try nth_tac'; try (match goal with - | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H - | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H - | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H - end)). - Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v new file mode 100644 index 000000000..7c203a320 --- /dev/null +++ b/src/Util/ListUtil.v @@ -0,0 +1,49 @@ +Require Import List. +Require Import Omega. + +Ltac nth_tac' := + intros; simpl in *; unfold error,value in *; repeat progress (match goal with + | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros + | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) + | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ H: _ /\ _ |- _ ] => destruct H + | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst + | [ H: None = Some _ |- _ ] => inversion H + | [ H: Some _ = None |- _ ] => inversion H + | [ |- Some _ = Some _ ] => apply f_equal + end); eauto; try (autorewrite with list in *); try omega; eauto. +Lemma nth_error_map : forall A B (f:A->B) i xs y, + nth_error (map f xs) i = Some y -> + exists x, nth_error xs i = Some x /\ f x = y. +Proof. + induction i; destruct xs; nth_tac'. +Qed. + +Lemma nth_error_seq : forall i start len, + nth_error (seq start len) i = + if lt_dec i len + then Some (start + i) + else None. + induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. +Qed. + +Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None -> + i >= length xs. +Proof. + induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. +Qed. + +Ltac nth_tac := + repeat progress (try nth_tac'; try (match goal with + | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H + | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H + | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H + end)). + +Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. +Proof. + induction xs; simpl; repeat match goal with + | [ H : _ |- _ ] => rewrite H; clear H + | _ => progress intuition + end; eauto. +Qed. -- cgit v1.2.3 From 1d34b00840bcf77969412c0ffc9a194dde1291ef Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 Oct 2015 20:14:52 -0400 Subject: word bound propagation examples --- _CoqProject | 1 + src/Assembly/WordBounds.v | 122 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 123 insertions(+) create mode 100644 src/Assembly/WordBounds.v diff --git a/_CoqProject b/_CoqProject index 3b45e81b9..ca6ca21f9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,4 +11,5 @@ src/Galois/ComputationalGaloisField.v src/Galois/ZGaloisField.v src/Galois/BaseSystem.v src/Curves/PointFormats.v +src/Assembly/WordBounds.v src/Curves/Curve25519.v diff --git a/src/Assembly/WordBounds.v b/src/Assembly/WordBounds.v new file mode 100644 index 000000000..e05fcb1d4 --- /dev/null +++ b/src/Assembly/WordBounds.v @@ -0,0 +1,122 @@ +Require Import Bedrock.Word. +Import BinNums PArith.BinPos NArith.BinNat NArith.Ndigits. + +Definition wordUn (f : N -> N) {sz : nat} (x : word sz) := + NToWord sz (f (wordToN x)). +Definition wshr {l} n := @wordUn (fun x => N.shiftr x n) l. +Lemma wshr_test : (wordToN (wshr 3 (NToWord 32 (128- 19)))) = 13%N. + reflexivity. +Qed. + +Module WordBoundsExamples. + Definition u31 := word 31. + Definition U31 := NToWord 31. + Definition u64 := word 64. + Definition U64 := NToWord 64. + + Definition c2 : u64 := NToWord _ 2. + Definition c19_31 : u31 := NToWord _ 19. + Definition c19 : u64 := NToWord _ 19. + Definition c38 : u64 := NToWord _ 38. + Definition t25_31 : u31 := NToWord _ (Npos (2^25)). + Definition t26_31 : u31 := NToWord _ (Npos (2^26)). + Definition t25 : u64 := NToWord _ (Npos (2^25)). + Definition t26 : u64 := NToWord _ (Npos (2^26)). + Definition t27 : u64 := NToWord _ (Npos (2^26)). + Definition m25 : u64 := t25^-(NToWord _ 1). + Definition m26 : u64 := t26^-(NToWord _ 1). + Definition r25 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 25 hk, wand m25 hk). + Definition r26 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 26 hk, wand m26 hk). + Definition r25mod (hSk hk:u64) : (u64 * u64) := (hSk ^+ c19^*wshr 25 hk, wand m25 hk). + + Lemma simple_add_rep : forall (a b c d:N), + (a < Npos(2^29) -> b < Npos(2^29) -> c < Npos(2^29) -> d < Npos(2^29))%N -> + wordToN(U31 a ^+ U31 b ^+ U31 c ^+ U31 d) = (a + b + c + d)%N. + Admitted. + + Lemma simple_add_bound : forall (a b c d:u64), + a < t25 -> b < t25 -> c < t25 -> d < t25 -> + (a ^+ b ^+ c ^+ d) < t27. + Admitted. + + (* the bounds can as well be stated in N if the _rep lemma works. + I am not sure whether it is a better idea to propagate the bounds in word or + in N, though -- proving rep requires propagating bounds for the subexpressions. + *) + + Lemma simple_linear_rep : forall (a b:N), (a < Npos(2^25) + Npos(2^26) -> b < Npos(2^25))%N -> + wordToN((U31 a)^*c19_31 ^+ U31 b) = (a*19 + b)%N. + Admitted. + + Lemma simple_linear_bound : forall (a b:u31), a < t25_31 ^+ t26_31 -> b < t25_31 -> + a^*c19_31 ^+ b < (NToWord _ 1946157056). (* (2**26+2**25)*19 + 2**25 = 1946157056 *) + Admitted. + + Lemma simple_mul_carry_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26) -> c < Npos(2^26))%N -> + wordToN(wshr 26 (U64 a ^* U64 b) ^+ U64 c) = ((a*b)/(2^26) + c)%N. + Admitted. + + Lemma simple_mul_carry_bound : forall (a b c:u64), a < t26 -> b < t26 -> c < t26 -> + wshr 26 (a ^* b) ^+ c < t27. + Admitted. + + Lemma simple_mul_reduce_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26))%N -> + wordToN(wand m26 (U64 a ^* U64 b)) = ((a*b) mod (2^26) + c)%N. + Admitted. + + Lemma sandy2x_bound : forall + (* this example is transcribed by hand from section 2.2. + it is very representative of the bounds check / absence-of-overflow proofs we actually + want to do. However, given its size, presence of transcription errors is totally plausible. + A corresponding _rep proof will also necessary.*) + (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : u64) + (g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : u64), + f0 < t26 -> g0 < t26 -> + f1 < t25 -> g1 < t25 -> + f2 < t26 -> g2 < t26 -> + f3 < t25 -> g3 < t25 -> + f4 < t26 -> g4 < t26 -> + f5 < t25 -> g5 < t25 -> + f6 < t26 -> g6 < t26 -> + f7 < t25 -> g7 < t25 -> + f8 < t26 -> g8 < t26 -> + f9 < t25 -> g9 < t25 -> + + let h0 := f0^*g0 ^+ c38^*f1^*g9 ^+ c19^*f2^*g8 ^+ c38^*f3^*g7 ^+ c19^*f4^*g6 ^+ c38^*f5^*g5 ^+ c19^*f6^*g4 ^+ c38^*f7^*g3 ^+ c19^*f8^*g2 ^+ c38^*f9^*g1 in + let h1 := f0^*g1 ^+ f1^*g0 ^+ c19^*f2^*g9 ^+ c19^*f3^*g8 ^+ c19^*f4^*g7 ^+ c19^*f5^*g6 ^+ c19^*f6^*g5 ^+ c19^*f7^*g4 ^+ c19^*f8^*g3 ^+ c19^*f9^*g2 in + let h2 := f0^*g2 ^+ c2^* f1^*g1 ^+ f2^*g0 ^+ c38^*f3^*g9 ^+ c19^*f4^*g8 ^+ c38^*f5^*g7 ^+ c19^*f6^*g6 ^+ c38^*f7^*g5 ^+ c19^*f8^*g4 ^+ c38^*f9^*g3 in + let h3 := f0^*g3 ^+ f1^*g2 ^+ f2^*g1 ^+ f3^*g0 ^+ c19^*f4^*g9 ^+ c19^*f5^*g8 ^+ c19^*f6^*g7 ^+ c19^*f7^*g6 ^+ c19^*f8^*g5 ^+ c19^*f9^*g4 in + let h4 := f0^*g4 ^+ c2^* f1^*g3 ^+ f2^*g2 ^+ c2^* f3^*g1 ^+ f4^*g0 ^+ c38^*f5^*g9 ^+ c19^*f6^*g8 ^+ c38^*f7^*g7 ^+ c19^*f8^*g6 ^+ c38^*f9^*g5 in + let h5 := f0^*g5 ^+ f1^*g4 ^+ f2^*g3 ^+ f3^*g2 ^+ f4^*g1 ^+ f5^*g0 ^+ c19^*f6^*g9 ^+ c19^*f7^*g8 ^+ c19^*f8^*g7 ^+ c19^*f9^*g6 in + let h6 := f0^*g6 ^+ c2^* f1^*g5 ^+ f2^*g4 ^+ c2^* f3^*g3 ^+ f4^*g2 ^+ c2^* f5^*g1 ^+ f6^*g0 ^+ c38^*f7^*g9 ^+ c19^*f8^*g8 ^+ c38^*f9^*g7 in + let h7 := f0^*g7 ^+ f1^*g6 ^+ f2^*g5 ^+ f3^*g4 ^+ f4^*g3 ^+ f5^*g2 ^+ f6^*g1 ^+ f7^*g0 ^+ c19^*f8^*g9 ^+ c19^*f9^*g8 in + let h8 := f0^*g8 ^+ c2^* f1^*g7 ^+ f2^*g6 ^+ c2^* f3^*g5 ^+ f4^*g4 ^+ c2^* f5^*g3 ^+ f6^*g2 ^+ c2^* f7^*g1 ^+ f8^*g0 ^+ c38^*f9^*g9 in + let h9 := f0^*g9 ^+ f1^*g8 ^+ f2^*g7 ^+ f3^*g6 ^+ f4^*g5 ^+ f5^*g4 ^+ f6^*g3 ^+ f7^*g2 ^+ f8^*g1 ^+ f9^*g0 in + + let (h1_1, h0_1) := r26 h1 h0 in + let (h2_1, h1_2) := r25 h2 h1_1 in + let (h3_1, h2_2) := r26 h3 h2_1 in + let (h4_1, h3_2) := r25 h4 h3_1 in + + let (h6_1, h5_1) := r25 h6 h5 in + let (h7_1, h6_2) := r26 h7 h6_1 in + let (h8_1, h7_2) := r25 h8 h7_1 in + let (h9_1, h8_2) := r26 h9 h8_1 in + let (h0_2, h9_2) := r25mod h0_1 h9_1 in + let (h1_3, h0_2) := r26 h1_2 h0_1 in + + let (h5_2, h4_2) := r26 h5_1 h4_1 in + let (h6_2, h5_3) := r25 h6_1 h5_2 in + + h0_2 < t26 /\ + h1_3 < t27 /\ + h2_2 < t26 /\ + h3_2 < t25 /\ + h4_2 < t26 /\ + h5_3 < t25 /\ + h6_2 < t27 /\ + h7_2 < t25 /\ + h8_2 < t26 /\ + h9_2 < t25. + Admitted. +End WordBoundsExamples. -- cgit v1.2.3 From 6db9640e6ff581c8c16eac3f1bddb95dcc762492 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 30 Oct 2015 10:47:20 -0400 Subject: Beautified BinGF.splitWords --- _CoqProject | 2 +- src/Rep/BinGF.v | 82 +++++++++++++++++++++++++++++++++++---------------------- 2 files changed, 52 insertions(+), 32 deletions(-) diff --git a/_CoqProject b/_CoqProject index ca6ca21f9..7f2624ee8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,10 +5,10 @@ src/Tactics/VerdiTactics.v src/Util/ListUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v +src/Galois/ZGaloisField.v src/Galois/GaloisExamples.v src/Galois/AbstractGaloisField.v src/Galois/ComputationalGaloisField.v -src/Galois/ZGaloisField.v src/Galois/BaseSystem.v src/Curves/PointFormats.v src/Assembly/WordBounds.v diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v index a19ae788b..138277870 100644 --- a/src/Rep/BinGF.v +++ b/src/Rep/BinGF.v @@ -8,6 +8,8 @@ Require Import Eqdep_dec. Module Type BitSpec. Parameter wordSize: nat. Parameter numWords: nat. + + Axiom wordSize_pos : (wordSize > 0)%nat. End BitSpec. Module GFBits (M: Modulus) (Spec: BitSpec). @@ -20,45 +22,64 @@ Module GFBits (M: Modulus) (Spec: BitSpec). Definition BinGF := {lst: list (word wordSize) | length lst = numWords}. - Definition convertWordSize {a b: nat} (x: word a): a = b -> word b. - intro H; rewrite H in x; exact x. - Defined. - - Lemma convert_invertible: - forall (a b: nat) (x: word a) (H1: a = b) (H2: b = a), - convertWordSize (convertWordSize x H1) H2 = x. + Definition splitGt {n m} {H : (n > m)%nat} (w : word n) : word m * word (n - m). Proof. - intros; destruct H2; simpl. - replace H1 with (eq_refl b); simpl; intuition. - apply UIP_dec; exact eq_nat_dec. - Qed. + refine (let w' := match _ : (n = m + (n - m))%nat in _ = N return word N with + | eq_refl => w + end in + (split1 m (n - m) w', split2 m (n - m) w')); + abstract omega. + Defined. - Fixpoint splitWords' (sz: nat) (len: nat) (x: word sz): list (word wordSize). - induction len, (gt_dec sz wordSize). + Fixpoint copies {A} (x : A) (n : nat) : list A := + match n with + | O => nil + | S n' => x :: copies x n' + end. - - refine nil. + Definition splitWords' : forall (len : nat) {sz: nat} (x: word sz), list (word wordSize). + Proof. + refine (fix splitWords' (len : nat) {sz : nat} (w : word sz) {struct len} : list (word wordSize) := + match len with + | O => nil + | S len' => + if gt_dec sz wordSize + then let (w1, w2) := splitGt w in + w1 :: splitWords' len' w2 + else match _ in _ = N return list (word N) with + | eq_refl => zext w (wordSize - sz) :: copies (wzero _) len' + end + end)%nat; clear splitWords'; abstract omega. + Defined. - - refine nil. + Lemma length_cast : forall A (F : A -> Type) x1 x2 (pf : x1 = x2) x xs, + length (match pf in _ = X return list (F X) with + | eq_refl => x :: xs + end) = S (length xs). + Proof. + destruct pf; auto. + Qed. - - assert (sz = wordSize + (sz - wordSize))%nat. intuition. - assert (z := convertWordSize x H). - refine ( - cons (split1 wordSize (sz - wordSize) z) - (splitWords' (sz - wordSize)%nat len - (split2 wordSize (sz - wordSize) z))). + Lemma length_copies : forall A (x : A) n, length (copies x n) = n. + Proof. + induction n; simpl; auto. + Qed. - - assert (sz + (wordSize - sz) = wordSize)%nat. intuition. - assert (z := convertWordSize (zext x (wordSize - sz)) H). - refine (cons z nil). + Hint Rewrite length_cast length_copies. - Admitted. + Lemma length_splitWords' : forall len sz (w : word sz), length (splitWords' len w) = len. + Proof. + induction len; simpl; intuition; + match goal with + | [ |- context[match ?E with _ => _ end] ] => destruct E + end; simpl; try rewrite IHlen; autorewrite with core; reflexivity. + Qed. Definition splitWords {sz} (len: nat) (x: word sz): - {x: list (word wordSize) | length x = len}. - exists (splitWords' sz len x). - - induction len, (gt_dec sz wordSize). - Admitted. + {x: list (word wordSize) | length x = len}. + Proof. + exists (splitWords' len x); apply length_splitWords'. + Defined. Definition splitGF (x: GF) := splitWords numWords (NToWord (numWords * wordSize)%nat (Z.to_N (proj1_sig x))). @@ -116,4 +137,3 @@ Module GFBits (M: Modulus) (Spec: BitSpec). }. End GFBits. - -- cgit v1.2.3 From d2edf784f94d01a238f56e0ce4983739c43a77f1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 1 Nov 2015 21:25:38 -0500 Subject: set_nth --- src/Util/ListUtil.v | 39 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 7c203a320..5604ebcc3 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,11 +1,14 @@ Require Import List. Require Import Omega. +Require Import Arith.Peano_dec. Ltac nth_tac' := intros; simpl in *; unfold error,value in *; repeat progress (match goal with | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros - | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) - | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ |- context[(if lt_dec ?a ?b then _ else _) = _] ] => destruct (lt_dec a b) + | [ |- context[_ = (if lt_dec ?a ?b then _ else _)] ] => destruct (lt_dec a b) + | [ H: context[(if lt_dec ?a ?b then _ else _) = _] |- _ ] => destruct (lt_dec a b) + | [ H: context[_ = (if lt_dec ?a ?b then _ else _)] |- _ ] => destruct (lt_dec a b) | [ H: _ /\ _ |- _ ] => destruct H | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst | [ H: None = Some _ |- _ ] => inversion H @@ -47,3 +50,35 @@ Proof. | _ => progress intuition end; eauto. Qed. + +(* xs[n] := x *) +Fixpoint set_nth {T} n x (xs:list T) {struct n} := + match n with + | O => match xs with + | nil => nil + | x'::xs' => x::xs' + end + | S n' => match xs with + | nil => nil + | x'::xs' => x'::set_nth n' x xs' + end + end. + +Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) (x x':T), + nth_error (set_nth m x xs) n = + if eq_nat_dec n m + then (if lt_dec n (length xs) then Some x else None) + else nth_error xs n. +Proof. + induction m. + + destruct n, xs; auto. + + intros; destruct xs, n; auto. + simpl; unfold error; match goal with + [ |- None = if ?x then None else None ] => destruct x + end; auto. + + simpl nth_error; erewrite IHm by auto; clear IHm. + destruct (eq_nat_dec n m), (eq_nat_dec (S n) (S m)); nth_tac. +Qed. -- cgit v1.2.3