From 54bb7895d16c719400c7730a3049f2295aec9d91 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 15:10:14 -0500 Subject: Connect [is_bounded] to [bounded_by] This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519. --- src/Specific/GF25519BoundedCommon.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Specific') diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index 35f54601c..f9ee444dc 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -543,6 +543,24 @@ Proof. abstract (rewrite wire_digitsW_word64ize_id; apply is_bounded_proj1_wire_digits). Defined. +Lemma is_bounded_to_nth_default x (H : is_bounded x = true) + : forall n : nat, + (n < length limb_widths)%nat + -> (0 <= nth_default 0 (Tuple.to_list length_fe25519 x) n <= + snd (b_of (nth_default (-1) limb_widths n)))%Z. +Proof. + hnf in x; destruct_head' prod. + unfold_is_bounded_in H; destruct_head' and. + Z.ltb_to_lt. + unfold nth_default; simpl. + intros. + repeat match goal with + | [ |- context[nth_error _ ?x] ] + => is_var x; destruct x; simpl + end; + omega. +Qed. + (* END precomputation *) (* Precompute constants *) -- cgit v1.2.3