Remove lemma_create_index_vec_w1 from Lib.IntVector

mamonet · May 25, 2024 · d024ebd · d024ebd
1 parent b115aec
commit d024ebd
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 9 deletions.
diff --git a/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst b/code/gf128/Hacl.Spec.GF128.PolyLemmas.fst
@@ -27,14 +27,13 @@ let lemma_of_to_uint_128 a =
   lemma_equal a (of_uint 128 (to_uint 128 a))
 
 let lemma_to_of_vec128 q =
-  lemma_create_index_vec_w1 q
+  eq_intro (create 1 (index (vec_v q) 0)) (vec_v q)
 
 let lemma_of_to_vec128 a =
   ()
 
 let lemma_vec128_zero () =
   lemma_bitwise_all ();
-  Vale.Arch.TypesNative.lemma_zero_nth 128;
   lemma_equal P.zero (of_uint 128 0);
   ()
 

diff --git a/lib/Lib.IntVector.fst b/lib/Lib.IntVector.fst
@@ -30,8 +30,6 @@ let lemma_of_vec_t #t #w f = admit()
 
 let lemma_of_vec_v_t #t #w f = admit()
 
-let lemma_create_index_vec_w1 #t f = admit()
-
 let vecv_extensionality #t #w f1 f2 = admit()
 
 let reveal_vec_v_1 #t f = admit()

diff --git a/lib/Lib.IntVector.fsti b/lib/Lib.IntVector.fsti
@@ -32,11 +32,6 @@ val lemma_of_vec_v_t: #t:v_inttype -> #w:width -> f:vec_v_t t w -> Lemma
   (ensures vec_v (vec_t_v f) == f)
   [SMTPat (vec_v #t #w (vec_t_v #t #w f))]
 
-val lemma_create_index_vec_w1: #t:v_inttype -> f:vec_t t 1 -> Lemma
-  (ensures
-    (let x:uint_t t SEC = mk_int (v (index (vec_v f) 0)) in
-    create 1 x == vec_v f))
-
 val vecv_extensionality: #t:v_inttype -> #w:width -> f1:vec_t t w -> f2:vec_t t w -> Lemma
   (requires vec_v f1 == vec_v f2)
   (ensures f1 == f2)