Fully proof Hacl.Spec.Gf128.FieldNI.fst module

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 =

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

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;
+  }

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)

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 =

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,15 +563,130 @@ 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:
     x1:vec128 -> x2:vec128 -> x3:vec128 -> x4:vec128
   -> 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)

specs/Spec.GF128.fst

@@ -8,17 +8,20 @@ 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
 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

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 =
+  ()