From 31fda83e1eca1a5df25bcad736475152b9a6fca7 Mon Sep 17 00:00:00 2001 From: mamonet Date: Wed, 22 May 2024 22:24:41 +0300 Subject: [PATCH] Fully proof Hacl.Spec.Gf128.FieldNI.fst module --- code/gf128/Hacl.Impl.Gf128.FieldNI.fst | 6 +- code/gf128/Hacl.Impl.Gf128.Fields.fst | 6 +- .../Hacl.Spec.GF128.PolyLemmas_helpers.fst | 68 +++++++++ .../Hacl.Spec.GF128.PolyLemmas_helpers.fsti | 17 +++ code/gf128/Hacl.Spec.GF128.Vec.fst | 12 +- code/gf128/Hacl.Spec.Gf128.FieldNI.fst | 129 +++++++++++++++++- specs/Spec.GF128.fst | 7 +- vale/code/lib/math/Vale.Math.Poly2.Galois.fst | 6 + .../code/lib/math/Vale.Math.Poly2.Galois.fsti | 11 ++ 9 files changed, 243 insertions(+), 19 deletions(-) diff --git a/code/gf128/Hacl.Impl.Gf128.FieldNI.fst b/code/gf128/Hacl.Impl.Gf128.FieldNI.fst index 8bb88966c4..99bd69e165 100644 --- a/code/gf128/Hacl.Impl.Gf128.FieldNI.fst +++ b/code/gf128/Hacl.Impl.Gf128.FieldNI.fst @@ -26,7 +26,7 @@ include Hacl.Spec.Gf128.FieldNI inline_for_extraction noextract let vec128_zero = vec_zero U128 1 noextract -let zero = GF.zero #S.gf128 +let zero = GF.zero #S.gf128_le let felem = lbuffer vec128 1ul let felem4 = lbuffer vec128 4ul @@ -164,7 +164,7 @@ val fadd: Stack unit (requires fun h -> live h x /\ live h y) (ensures fun h0 _ h1 -> modifies1 x h0 h1 /\ - feval h1 x == GF.fadd #S.gf128 (feval h0 x) (feval h0 y)) + feval h1 x == GF.fadd #S.gf128_le (feval h0 x) (feval h0 y)) [@CInline] let fadd x y = @@ -198,7 +198,7 @@ val fmul: Stack unit (requires fun h -> live h x /\ live h y) (ensures fun h0 _ h1 -> modifies1 x h0 h1 /\ - feval h1 x == GF.fmul_be #S.gf128 (feval h0 x) (feval h0 y)) + feval h1 x == GF.reverse (GF.fmul #S.gf128_le (GF.reverse (feval h0 x)) (GF.reverse (feval h0 y)))) [@ CInline] let fmul x y = diff --git a/code/gf128/Hacl.Impl.Gf128.Fields.fst b/code/gf128/Hacl.Impl.Gf128.Fields.fst index 42846a9ac7..02d9f1a0db 100644 --- a/code/gf128/Hacl.Impl.Gf128.Fields.fst +++ b/code/gf128/Hacl.Impl.Gf128.Fields.fst @@ -74,7 +74,7 @@ let feval4 #s h e = | NI -> Hacl.Impl.Gf128.FieldNI.feval4 h e noextract -let zero = GF.zero #S.gf128 +let zero = GF.zero #S.gf128_le noextract @@ -222,7 +222,7 @@ val fadd: Stack unit (requires fun h -> live h x /\ live h y /\ eq_or_disjoint x y) (ensures fun h0 _ h1 -> modifies1 x h0 h1 /\ - feval h1 x == GF.fadd #S.gf128 (feval h0 x) (feval h0 y)) + feval h1 x == GF.fadd #S.gf128_le (feval h0 x) (feval h0 y)) let fadd #s x y = match s with @@ -252,7 +252,7 @@ val fmul: Stack unit (requires fun h -> live h x /\ live h y /\ eq_or_disjoint x y) (ensures fun h0 _ h1 -> modifies1 x h0 h1 /\ - feval h1 x == GF.fmul_be #S.gf128 (feval h0 x) (feval h0 y)) + feval h1 x == GF.reverse (GF.fmul #S.gf128_le (GF.reverse (feval h0 x)) (GF.reverse (feval h0 y)))) let fmul #s x y = match s with diff --git a/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fst b/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fst index 35b7d4085c..a38cebb07e 100644 --- a/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fst +++ b/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fst @@ -664,3 +664,71 @@ let lemma_add_helper_m a b c d p = lemma_add_associate p (a +. b) c; lemma_add_associate p (a +. b +. c) d; lemma_add_commute p (a +. b +. c +. d) + +let lemma_mul_reduce_helper1 x1 x2 x3 x4 y1 y2 y3 y4 = + let x1_r = reverse x1 127 in + let x2_r = reverse x2 127 in + let x3_r = reverse x3 127 in + let x4_r = reverse x4 127 in + let y1_r = reverse y1 127 in + let y2_r = reverse y2 127 in + let y3_r = reverse y3 127 in + let y4_r = reverse y4 127 in + calc (==) { + shift ((x1 *. y1) +. (x2 *. y2) +. (x3 *. y3) +. (x4 *. y4)) 1; + == {lemma_shift_is_mul ((x1 *. y1) +. + (x2 *. y2) +. (x3 *. y3) +. (x4 *. y4)) 1} + ((x1 *. y1) +. (x2 *. y2) +. (x3 *. y3) +. (x4 *. y4)) *. monomial 1; + == {lemma_mul_distribute_left ((x1 *. y1) +. (x2 *. y2) +. (x3 *. y3)) + (x4 *. y4) (monomial 1)} + ((x1 *. y1) +. (x2 *. y2) +. (x3 *. y3)) *. monomial 1 +. + (x4 *. y4) *. monomial 1; + == {lemma_mul_distribute_left ((x1 *. y1) +. (x2 *. y2)) + (x3 *. y3) (monomial 1)} + ((x1 *. y1) +. (x2 *. y2)) *. monomial 1 +. (x3 *. y3) *. monomial 1 +. + (x4 *. y4) *. monomial 1; + == {lemma_mul_distribute_left (x1 *. y1) (x2 *. y2) (monomial 1)} + (x1 *. y1) *. monomial 1 +. (x2 *. y2) *. monomial 1 +. + (x3 *. y3) *. monomial 1 +. (x4 *. y4) *. monomial 1; + == {lemma_shift_is_mul (x1 *. y1) 1; + lemma_shift_is_mul (x2 *. y2) 1; + lemma_shift_is_mul (x3 *. y3) 1; + lemma_shift_is_mul (x4 *. y4) 1} + shift (x1 *. y1) 1 +. shift (x2 *. y2) 1 +. + shift (x3 *. y3) 1 +. shift (x4 *. y4) 1; + == {lemma_mul_reverse_shift_1 x1_r y1_r 127; + lemma_mul_reverse_shift_1 x2_r y2_r 127; + lemma_mul_reverse_shift_1 x3_r y3_r 127; + lemma_mul_reverse_shift_1 x4_r y4_r 127} + reverse (x1_r *. y1_r) 255 +. reverse (x2_r *. y2_r) 255 +. + reverse (x3_r *. y3_r) 255 +. reverse (x4_r *. y4_r) 255; + == {lemma_add_reverse (x1_r *. y1_r) (x2_r *. y2_r) 255} + reverse ((x1_r *. y1_r) +. (x2_r *. y2_r)) 255 +. + reverse (x3_r *. y3_r) 255 +. reverse (x4_r *. y4_r) 255; + == {lemma_add_reverse ((x1_r *. y1_r) +. (x2_r *. y2_r)) (x3_r *. y3_r) 255} + reverse ((x1_r *. y1_r) +. (x2_r *. y2_r) +. (x3_r *. y3_r)) 255 +. + reverse (x4_r *. y4_r) 255; + == {lemma_add_reverse ((x1_r *. y1_r) +. (x2_r *. y2_r) +. (x3_r *. y3_r)) + (x4_r *. y4_r) 255} + reverse ((x1_r *. y1_r) +. (x2_r *. y2_r) +. (x3_r *. y3_r) +. (x4_r *. y4_r)) 255; + } + +let lemma_mul_reduce_helper2 z1 z2 z3 z4 g = + calc (==) { + (z1 +. z2 +. z3 +. z4) %. g; + == {lemma_mod_distribute (z1 +. z2 +. z3) z4 g} + (z1 +. z2 +. z3) %. g +. z4 %. g; + == {lemma_mod_distribute (z1 +. z2) z3 g} + (z1 +. z2) %. g +. z3 %. g +. z4 %. g; + == {lemma_mod_distribute z1 z2 g} + z1 %. g +. z2 %. g +. z3 %. g +. z4 %. g; + }; + calc (==) { + reverse (z1 %. g +. z2 %. g +. z3 %. g +. z4 %. g) 127; + == {lemma_add_reverse (z1 %. g +. z2 %. g +. z3 %. g) (z4 %. g) 127} + reverse (z1 %. g +. z2 %. g +. z3 %. g) 127 +. reverse (z4 %. g) 127; + == {lemma_add_reverse (z1 %. g +. z2 %. g) (z3 %. g) 127} + reverse (z1 %. g +. z2 %. g) 127 +. reverse (z3 %. g) 127 +. reverse (z4 %. g) 127; + == {lemma_add_reverse (z1 %. g) (z2 %. g) 127} + reverse (z1 %. g) 127 +. reverse (z2 %. g) 127 +. reverse (z3 %. g) 127 +. reverse (z4 %. g) 127; + } diff --git a/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fsti b/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fsti index e44ca1d9de..8a00beeec6 100644 --- a/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fsti +++ b/code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fsti @@ -162,3 +162,20 @@ val lemma_gf128_mul_4 (a0 b0 c0 d0 a1 b1 c1 d1 a2 b2 c2 d2 a3 b3 c3 d3:poly) : val lemma_add_helper_m (a b c d p:poly) : Lemma (ensures (p +. a +. b +. c +. d == (a +. b +. c +. d) +. p)) + +val lemma_mul_reduce_helper1 (x1 x2 x3 x4 y1 y2 y3 y4:poly) : Lemma + (requires degree x1 < 128 /\ degree x2 < 128 /\ degree x3 < 128 /\ + degree x4 < 128 /\ degree y1 < 128 /\ degree y2 < 128 /\ + degree y3 < 128 /\ degree y4 < 128) + (ensures reverse (shift ((x1 *. y1) +. + (x2 *. y2) +. (x3 *. y3) +. (x4 *. y4)) 1) 255 == + ((reverse x1 127) *. (reverse y1 127)) +. + ((reverse x2 127) *. (reverse y2 127)) +. + ((reverse x3 127) *. (reverse y3 127)) +. + ((reverse x4 127) *. (reverse y4 127))) + +val lemma_mul_reduce_helper2 (z1 z2 z3 z4 g:poly) : Lemma + (requires degree g == 128) + (ensures reverse ((z1 +. z2 +. z3 +. z4) %. g) 127 == + reverse (z1 %. g) 127 +. reverse (z2 %. g) 127 +. + reverse (z3 %. g) 127 +. reverse (z4 %. g) 127) diff --git a/code/gf128/Hacl.Spec.GF128.Vec.fst b/code/gf128/Hacl.Spec.GF128.Vec.fst index 1335b23fe0..8763b481f5 100644 --- a/code/gf128/Hacl.Spec.GF128.Vec.fst +++ b/code/gf128/Hacl.Spec.GF128.Vec.fst @@ -17,14 +17,14 @@ type gf128_spec = let _: squash (inversion gf128_spec) = allow_inversion gf128_spec -let elem = Scalar.elem -let gf128 = Scalar.gf128 +let elem = Scalar.elem_le +let gf128 = Scalar.gf128_le let elem2 = lseq elem 2 let elem4 = lseq elem 4 let fadd4 (a:elem4) (b:elem4) : elem4 = map2 fadd a b -let fmul4 (a:elem4) (b:elem4) : elem4 = map2 fmul_be a b +let fmul4 (a:elem4) (b:elem4) : elem4 = map2 (fun x y -> reverse (fmul (reverse x) (reverse y))) a b let load_elem4 (b:lbytes 64) : elem4 = let b1 = load_felem_be #gf128 (sub b 0 16) in @@ -43,9 +43,9 @@ let normalize4 (pre:elem4) (acc:elem4) : elem = fadd (fadd (fadd a.[0] a.[1]) a.[2]) a.[3] let load_precompute_r (r:elem) : elem4 = - let r2 = r `fmul_be` r in - let r3 = r `fmul_be` r2 in - let r4 = r `fmul_be` r3 in + let r2 = reverse (reverse r `fmul` reverse r) in + let r3 = reverse (reverse r `fmul` reverse r2) in + let r4 =reverse (reverse r `fmul` reverse r3) in create4 r4 r3 r2 r let gf128_update4_add_mul (pre:elem4) (b:lbytes 64) (acc:elem) : Tot elem = diff --git a/code/gf128/Hacl.Spec.Gf128.FieldNI.fst b/code/gf128/Hacl.Spec.Gf128.FieldNI.fst index 3041b6a646..09da428715 100644 --- a/code/gf128/Hacl.Spec.Gf128.FieldNI.fst +++ b/code/gf128/Hacl.Spec.Gf128.FieldNI.fst @@ -11,6 +11,7 @@ open Vale.Math.Poly2 open Vale.Math.Poly2.Lemmas open Vale.AES.GF128 open Vale.AES.GHash_BE +open Vale.Math.Poly2.Galois open Hacl.Spec.GF128.Poly_s open Hacl.Spec.GF128.PolyLemmas @@ -19,6 +20,7 @@ open Hacl.Spec.GF128.PolyLemmas_helpers module S = Spec.GF128 module GF = Spec.GaloisField module Vec = Hacl.Spec.GF128.Vec +module B = Vale.Math.Poly2.Bits_s #set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0" @@ -56,7 +58,8 @@ let clmul_wide (x:vec128) (y:vec128) : Tot (vec128 & vec128) = val lemma_clmul_wide (x:vec128) (y:vec128) : Lemma (ensures ( let (hi, lo) = clmul_wide x y in - mul (of_vec128 x) (of_vec128 y) == add (shift (of_vec128 hi) 128) (of_vec128 lo) + mul (of_vec128 x) (of_vec128 y) == add (shift (of_vec128 hi) 128) (of_vec128 lo) /\ + degree (of_vec128 hi) <= 126 )) let lemma_clmul_wide x y = @@ -165,7 +168,8 @@ val lemma_clmul_wide4 (mul (of_vec128 x2) (of_vec128 y2))) (mul (of_vec128 x3) (of_vec128 y3))) (mul (of_vec128 x4) (of_vec128 y4)) == - add (shift (of_vec128 hi) 128) (of_vec128 lo) + add (shift (of_vec128 hi) 128) (of_vec128 lo) /\ + degree (of_vec128 hi) <= 126 )) let lemma_clmul_wide4 x1 x2 x3 x4 y1 y2 y3 y4 = @@ -559,10 +563,74 @@ let lemma_gf128_reduce h l = assert (lo == reverse (mod x (add nn gf128_low)) 127); //OBSERVE () +let gf128_irred_elem_le = fun (i:nat) -> i = 127 || i = 126 || i = 125 || i = 120 + +let gf128_irred_elem_le_lemma (i:nat{i < 128}) : Lemma + (UInt.nth #128 (v S.gf128_le.irred) i == gf128_irred_elem_le i) = + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 0 == true); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 1 == false); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 2 == false); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 3 == false); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 4 == false); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 5 == true); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 6 == true); + assert_norm (UInt.nth #8 (v S.gf128_le.irred) 7 == true); + + assert_norm ((v S.gf128_le.irred) % pow2 8 == (v S.gf128_le.irred)); + UInt.slice_right_lemma #128 (UInt.to_vec (v S.gf128_le.irred)) 8; + assert (UInt.from_vec #8 (Seq.slice (UInt.to_vec #128 (v S.gf128_le.irred)) 120 128) = (v S.gf128_le.irred) % pow2 8); + assert (Seq.slice (UInt.to_vec #128 (v S.gf128_le.irred)) 120 128 = UInt.to_vec #8 (v S.gf128_le.irred)); + + assert_norm ((v S.gf128_le.irred) / pow2 8 == 0); + UInt.slice_left_lemma #128 (UInt.to_vec (v S.gf128_le.irred)) 120; + assert (UInt.from_vec #120 (Seq.slice (UInt.to_vec #128 (v S.gf128_le.irred)) 0 120) = (v S.gf128_le.irred) / pow2 8); + assert (Seq.slice (UInt.to_vec #128 (v S.gf128_le.irred)) 0 120 = UInt.to_vec #120 0); + let aux_zero (n:nat{n < 120}) : Lemma (UInt.nth #128 (v S.gf128_le.irred) n == false) = + UInt.zero_to_vec_lemma #120 n in + + Classical.forall_intro aux_zero; + assert (UInt.nth #128 (v S.gf128_le.irred) i == gf128_irred_elem_le i) + +let lemma_gf128_irred_le (_:unit) : Lemma + (B.of_uint 128 (v S.gf128_le.irred) == gf128_low) + = + let aux (i:nat{i < 128}) : Lemma (UInt.nth #128 (v S.gf128_le.irred) i == gf128_irred_elem_le i) = + gf128_irred_elem_le_lemma i in + + Classical.forall_intro aux; + lemma_index_all (); + lemma_reverse_define_all (); + lemma_equal (of_seq (UInt.to_vec #128 (v S.gf128_le.irred))) (of_fun 128 gf128_irred_elem_le); + lemma_equal (reverse (of_fun 128 gf128_irred_elem_le) 127) gf128_low + val gf128_clmul_wide_reduce_lemma: x:vec128 -> y:vec128 -> Lemma (let (hi, lo) = clmul_wide x y in - to_elem (gf128_reduce hi lo) == GF.fmul_be #S.gf128 (to_elem x) (to_elem y)) -let gf128_clmul_wide_reduce_lemma x y = admit() + to_elem (gf128_reduce hi lo) == + GF.reverse (GF.fmul #S.gf128_le (GF.reverse (to_elem x)) (GF.reverse (to_elem y)))) +let gf128_clmul_wide_reduce_lemma x y = + lemma_clmul_wide x y; + let (hi, lo) = clmul_wide x y in + assert (mul (of_vec128 x) (of_vec128 y) == + add (shift (of_vec128 hi) 128) (of_vec128 lo)); + lemma_gf128_reduce hi lo; + lemma_shift_is_mul (of_vec128 hi) 128; + let mm = monomial 128 in + let g = add mm gf128_low in + let a = shift (mul (of_vec128 x) (of_vec128 y)) 1 in + let z = reverse a 255 in + assert (gf128_reduce hi lo == to_vec128 (reverse (mod z g) 127)); + let x_r = reverse (of_vec128 x) 127 in + let y_r = reverse (of_vec128 y) 127 in + lemma_mul_reverse_shift_1 x_r y_r 127; + assert (z == mul x_r y_r); + lemma_gf128_irred_le (); + assert (irred_poly S.gf128_le == g); + assert (to_poly (GF.fmul (to_felem S.gf128_le x_r) (to_felem S.gf128_le y_r)) == mod z g); + lemma_reverse S.gf128_le (GF.fmul (to_felem S.gf128_le x_r) (to_felem S.gf128_le y_r)); + assert (GF.reverse (GF.fmul (to_felem S.gf128_le x_r) (to_felem S.gf128_le y_r)) == + to_felem S.gf128_le (reverse (mod z g) 127)); + lemma_reverse S.gf128_le (to_elem x); + lemma_reverse S.gf128_le (to_elem y) val gf128_clmul_wide4_reduce_lemma: @@ -570,4 +638,55 @@ val gf128_clmul_wide4_reduce_lemma: -> y1:vec128 -> y2:vec128 -> y3:vec128 -> y4:vec128 -> Lemma (let (hi, lo) = clmul_wide4 x1 x2 x3 x4 y1 y2 y3 y4 in to_elem (gf128_reduce hi lo) == Vec.normalize4 (to_elem4 y1 y2 y3 y4) (to_elem4 x1 x2 x3 x4)) -let gf128_clmul_wide4_reduce_lemma x1 x2 x3 x4 y1 y2 y3 y4 = admit() +let gf128_clmul_wide4_reduce_lemma x1 x2 x3 x4 y1 y2 y3 y4 = + lemma_clmul_wide4 x1 x2 x3 x4 y1 y2 y3 y4; + let (hi, lo) = clmul_wide4 x1 x2 x3 x4 y1 y2 y3 y4 in + assert (add (add (add + (mul (of_vec128 x1) (of_vec128 y1)) + (mul (of_vec128 x2) (of_vec128 y2))) + (mul (of_vec128 x3) (of_vec128 y3))) + (mul (of_vec128 x4) (of_vec128 y4)) == + add (shift (of_vec128 hi) 128) (of_vec128 lo)); + lemma_gf128_reduce hi lo; + lemma_shift_is_mul (of_vec128 hi) 128; + let mm = monomial 128 in + let g = add mm gf128_low in + let a = shift (add (add (add + (mul (of_vec128 x1) (of_vec128 y1)) + (mul (of_vec128 x2) (of_vec128 y2))) + (mul (of_vec128 x3) (of_vec128 y3))) + (mul (of_vec128 x4) (of_vec128 y4))) 1 in + let z = reverse a 255 in + assert (gf128_reduce hi lo == to_vec128 (reverse (mod z g) 127)); + lemma_mul_reduce_helper1 (of_vec128 x1) (of_vec128 x2) (of_vec128 x3) + (of_vec128 x4) (of_vec128 y1) (of_vec128 y2) (of_vec128 y3) (of_vec128 y4); + let x1_r = reverse (of_vec128 x1) 127 in + let x2_r = reverse (of_vec128 x2) 127 in + let x3_r = reverse (of_vec128 x3) 127 in + let x4_r = reverse (of_vec128 x4) 127 in + let y1_r = reverse (of_vec128 y1) 127 in + let y2_r = reverse (of_vec128 y2) 127 in + let y3_r = reverse (of_vec128 y3) 127 in + let y4_r = reverse (of_vec128 y4) 127 in + assert (z == add (add (add (mul x1_r y1_r) (mul x2_r y2_r)) + (mul x3_r y3_r)) (mul x4_r y4_r)); + lemma_gf128_irred_le (); + assert (irred_poly S.gf128_le == g); + lemma_mul_reduce_helper2 (mul x1_r y1_r) (mul x2_r y2_r) + (mul x3_r y3_r) (mul x4_r y4_r) g; + assert (reverse (mod z g) 127 == add (add (add (reverse (mod (mul x1_r y1_r) g) 127) + (reverse (mod (mul x2_r y2_r) g) 127)) (reverse (mod (mul x3_r y3_r) g) 127)) + (reverse (mod (mul x4_r y4_r) g) 127)); + assert (reverse (mod z g) 127 == to_poly (GF.fadd (GF.fadd (GF.fadd + (GF.reverse (GF.fmul (to_felem S.gf128_le x1_r) (to_felem S.gf128_le y1_r))) + (GF.reverse (GF.fmul (to_felem S.gf128_le x2_r) (to_felem S.gf128_le y2_r)))) + (GF.reverse (GF.fmul (to_felem S.gf128_le x3_r) (to_felem S.gf128_le y3_r)))) + (GF.reverse (GF.fmul (to_felem S.gf128_le x4_r) (to_felem S.gf128_le y4_r))))); + lemma_reverse S.gf128_le (to_elem x1); + lemma_reverse S.gf128_le (to_elem x2); + lemma_reverse S.gf128_le (to_elem x3); + lemma_reverse S.gf128_le (to_elem x4); + lemma_reverse S.gf128_le (to_elem y1); + lemma_reverse S.gf128_le (to_elem y2); + lemma_reverse S.gf128_le (to_elem y3); + lemma_reverse S.gf128_le (to_elem y4) diff --git a/specs/Spec.GF128.fst b/specs/Spec.GF128.fst index 9110739783..d604df9d9f 100644 --- a/specs/Spec.GF128.fst +++ b/specs/Spec.GF128.fst @@ -8,10 +8,9 @@ open Lib.ByteSequence open Spec.GaloisField //GF128 Field: to load bits in little-endian order set the parameters as follows -//let irred = u128 0x87 //let load_elem (b:lbytes 16) : elem = load_felem_le #gf128 b //let store_elem (e:elem) : lbytes 16 = store_felem_le #gf128 e -//and use `fmul` instead of `fmul_be` +//and use `gf128_le/fmul` instead of `gf128/fmul_be` let irred = mk_int #U128 #SEC 0xE1000000000000000000000000000000 let gf128 = gf U128 irred @@ -19,6 +18,10 @@ let elem = felem gf128 let load_elem (b:lbytes 16) : elem = load_felem_be #gf128 b let store_elem (e:elem) : lbytes 16 = store_felem_be #gf128 e +let irred_le = mk_int #U128 #SEC 0x87 +let gf128_le = gf U128 irred_le +let elem_le = felem gf128_le + (* GCM types and specs *) let size_block : size_nat = 16 let size_key : size_nat = 16 diff --git a/vale/code/lib/math/Vale.Math.Poly2.Galois.fst b/vale/code/lib/math/Vale.Math.Poly2.Galois.fst index 8eb831b631..5a2b0242ba 100644 --- a/vale/code/lib/math/Vale.Math.Poly2.Galois.fst +++ b/vale/code/lib/math/Vale.Math.Poly2.Galois.fst @@ -812,3 +812,9 @@ let lemma_reverse f e = lemma_f_reverse f e; lemma_s_g_reverse f e; lemma_s_reverse (to_poly e) (I.bits f.t - 1) + +let lemma_poly_of_uint f e = + () + +let lemma_poly_to_uint f a = + () diff --git a/vale/code/lib/math/Vale.Math.Poly2.Galois.fsti b/vale/code/lib/math/Vale.Math.Poly2.Galois.fsti index 3a01e98bd9..12c8a5e0d8 100644 --- a/vale/code/lib/math/Vale.Math.Poly2.Galois.fsti +++ b/vale/code/lib/math/Vale.Math.Poly2.Galois.fsti @@ -3,6 +3,7 @@ open FStar.Mul module I = Lib.IntTypes module G = Spec.GaloisField module P = Vale.Math.Poly2_s +module B = Vale.Math.Poly2.Bits_s open Vale.Math.Poly2_s open Vale.Math.Poly2 open FStar.Seq @@ -88,3 +89,13 @@ val lemma_reverse (f:G.field) (e:G.felem f) : Lemma (requires True) (ensures to_poly (G.reverse e) == reverse (to_poly e) (I.bits f.t - 1)) [SMTPat (to_poly (G.reverse e))] + +val lemma_poly_of_uint (f:G.field) (e:G.felem f) : Lemma + (requires True) + (ensures to_poly e == B.of_uint (I.bits f.t) (I.uint_v e)) + [SMTPat (to_poly e)] + +val lemma_poly_to_uint (f:G.field) (a:poly) : Lemma + (requires True) + (ensures to_felem f a == I.uint (B.to_uint (I.bits f.t) a)) + [SMTPat (to_felem f a)]