progressing

formosa-crypto · Dec 22, 2024 · 4e28880 · 4e28880
1 parent d9ac5f4
commit 4e28880
Showing 1 changed file with 68 additions and 5 deletions.
diff --git a/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec b/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec
@@ -21,9 +21,9 @@ lemma poly_to_bytes_stack_equiv _mem _pos _a :
     (to_list res{1}.`1) /\ res{1}.`2 = res{2}].
 move => Hpos;proc => /=.
 unroll for {1} ^while; unroll for{2} ^while.
-seq 40 40 : (Glob.mem{2} = _mem /\ rp{2} = (of_int _pos)%W64 /\ ={a,jqx16_p,qx16,t0,t1,t2,t3,t4,t5,t6,t7});  1: by conseq />;sim.
+seq 40 40 : (Glob.mem{2} = _mem /\ rp{2} = (of_int _pos)%W64 /\ ={a,jqx16_p,qx16,t0,t1,t2,t3,t4,t5,t6,t7,ttt});  1: by conseq />;sim.
 
-seq 7 7 : (rp{2} = (of_int _pos)%W64 /\ ={a, jqx16_p, qx16, t0, t1, t2, t3, t4, t5, t6, t7} /\
+seq 7 7 : (rp{2} = (of_int _pos)%W64 /\ ={a, jqx16_p, qx16, t0, t1, t2, t3, t4, t5, t6, t7,ttt} /\
    Glob.mem{2} = stores _mem _pos (take 192 (to_list rp{1}))).
 + auto => /> &1 &2. 
   rewrite /storeW256 !of_uintK !modz_small; 1..6: by auto => /#. 
@@ -32,7 +32,35 @@ seq 7 7 : (rp{2} = (of_int _pos)%W64 /\ ={a, jqx16_p, qx16, t0, t1, t2, t3, t4,
   case (_pos <= p && p < _pos + 192) => *; last by smt().
   rewrite nth_take 1,2:/# (nth_change_dfl witness W8.zero (Array384.to_list _)); 1: by rewrite size_to_list 1:/#.
   rewrite get_to_list initiE 1:/#.
-  admit.
+  case (_pos + 160 <= p && p < _pos + 192) => *.
+  + rewrite get8_set256_directE 1,2:/# ifT 1:/# (nth_map witness);1:  smt(size_iota).   by rewrite nth_iota /#.
+  case ( _pos + 128 <= p && p < _pos + 160) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#. 
+  case (_pos + 96 <= p && p < _pos + 128) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  case (_pos + 64 <= p && p < _pos + 96) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  case (_pos + 32 <= p && p < _pos + 64) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  + rewrite ifT 1:/#.     
+    rewrite /get8  /set256_direct initiE 1:/# /= ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.  
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1: /#.
+    by rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
 
 seq 35 35 : (#pre);  1: by conseq />;sim.
 auto => /> &1 &2.
@@ -42,8 +70,43 @@ rewrite !get_storesE !size_to_list !size_take 1:/# !size_to_list size_map !iotar
 case (_pos <= p && p < _pos + 384) => *; last by smt().
 rewrite (nth_change_dfl witness W8.zero (Array384.to_list _)); 1: by rewrite size_to_list 1:/#.
 rewrite get_to_list initiE 1:/#.
-admit.
-
+  case (_pos + 352 <= p && p < _pos + 384) => *.
+  + rewrite get8_set256_directE 1,2:/# ifT 1:/# (nth_map witness);1:  smt(size_iota).   by rewrite nth_iota /#.
+  case ( _pos + 320 <= p && p < _pos + 352) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#. 
+  case (_pos + 288 <= p && p < _pos + 320) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  case (_pos + 256 <= p && p < _pos + 288) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  case (_pos + 224 <= p && p < _pos + 256) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  case (_pos + 192 <= p && p < _pos + 224) => *.
+  + rewrite get8_set256_directE 1,2:/# ifF 1:/# (nth_map witness);1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.
+    rewrite /get8 initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifT /#.
+  + rewrite ifT 1:/#.     
+    rewrite /get8  /set256_direct initiE 1:/# /= ifF 1:/# nth_take 1,2:/# (nth_map witness) /=;1:  smt(size_iota)
+.   rewrite nth_iota 1: /#.  
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1:/#.
+    rewrite initiE 1:/# initiE 1:/# /= /set256_direct initiE 1:/# /= ifF 1: /#.
+    by rewrite initiE /#.
 qed.
 
 lemma polyvec_to_bytes_stack_equiv _mem _pos: