From ad6e5bf2a14b759d060b5ae5cc7797e1d069e6ef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 31 Oct 2016 15:55:58 -0400 Subject: Make it so that changing the list of wire bounds doesn't break the build --- src/Specific/GF25519BoundedCommon.v | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index 29bc1af5d..648a27f55 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -110,9 +110,11 @@ Proof. apply (word_to_unbounded_word x); reflexivity. Defined. Definition bounds : list (Z * Z) := Eval compute in [b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26]. -Definition wire_digit_bounds : list (Z * Z) +Definition wire_digit_bounds_exp : list Z := Eval compute in - List.repeat (0, 2^32-1)%Z 7 ++ ((0,2^31-1)%Z :: nil). + List.repeat 32 7 ++ [31]. +Definition wire_digit_bounds : list (Z * Z) + := Eval compute in List.map (fun e => (0,2^e-1)%Z) wire_digit_bounds_exp. Local Opaque word64. Definition fe25519W := Eval cbv (*-[word64]*) in (tuple word64 (length limb_widths)). @@ -193,9 +195,16 @@ Definition fe25519 := let sanity := eq_refl : length bounds = length limb_widths in (word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26)%type. Definition wire_digits := - Eval cbv [fst snd Tuple.tuple Tuple.tuple'] in - (unbounded_word 32 * unbounded_word 32 * unbounded_word 32 * unbounded_word 32 - * unbounded_word 32 * unbounded_word 32 * unbounded_word 32 * unbounded_word 31)%type. + Eval cbv [list_rect wire_digit_bounds_exp List.rev List.app] in + list_rect + (fun _ => _) unit + (fun e xs es + => let t := unbounded_word e in + match xs with + | nil => t + | _::_ => (es * t)%type + end) + (List.rev wire_digit_bounds_exp). Definition proj1_fe25519W (x : fe25519) : fe25519W := let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in (proj_word x0, proj_word x1, proj_word x2, proj_word x3, proj_word x4, -- cgit v1.2.3