current

proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec

@@ -1883,31 +1883,12 @@ bind op [W32.t & W16.t] W2u16.truncateu16 "truncate".
 realize bvtruncateP by admit.
 
 
-op lane_func_compress10(x : W16.t) : W10.t = truncate64_10 (
-   sll_64 (((sll_64 (W4u16.zeroextu64 x) (W64.of_int 10)) + W64.of_int 1665) * (W64.of_int 1290167)) (W64.of_int 32)). 
-
 bind op [W16.t & W32.t] sigextu32 "sextend".
 realize bvsextendP by admit.
 
 bind op [W32.t & W8.t] W4u8.truncateu8 "truncate".
 realize bvtruncateP by admit. 
 
-op sra_32 (w1 w2 : W32.t) : W32.t =
-  w1 `|>>` (truncateu8 w2).
-
-bind op [W32.t] sra_32 "ashr".
-realize bvashrP by admit.
-
-op lane_func_reduce(c : W16.t) : W16.t =  
-    let t = (sigextu32 c) in
-    let t = (t * (W32.of_int 20159)) in
-    let t = (sra_32 t (W32.of_int 26)) in
-    let t = (t * (W32.of_int 3329)) in
-    let r = (truncateu16 t) in
-       (r - (truncateu16 t)).
-
-op lane_polyvec_redcomp10(w : W16.t) : W10.t = lane_func_compress10 (lane_func_reduce w).
-
 bind circuit VPBROADCAST_8u32 "VPBROADCAST_8u32".
 bind circuit VPBROADCAST_4u64 "VPBROADCAST_4u64".
 
@@ -1927,11 +1908,27 @@ bind circuit VPEXTR_32 "VEXTRACTI32_256".
 
 bind circuit W4u32.VPEXTR_32 "VEXTRACTI32_128".
 
-
 bind op [W256.t & W128.t] truncateu128 "truncate".
 realize bvtruncateP by admit.
 
-op lane (w: W16.t) = w.
+op sra_32 (w1 w2 : W32.t) : W32.t =
+  w1 `|>>` (truncateu8 w2).
+
+bind op [W32.t] sra_32 "ashr".
+realize bvashrP by admit.
+
+op lane_func_reduce(c : W16.t) : W16.t =  
+    let t = ((sigextu32 c) * (W32.of_int 20159)) in
+    let t = (sra_32 t (W32.of_int 26)) in
+    let t = (t * (W32.of_int 3329)) in
+       (c - (truncateu16 t)).
+
+op lane_func_compress10(x : W16.t) : W10.t = truncate64_10 (
+   sll_64 (((sll_64 (W4u16.zeroextu64 x) (W64.of_int 10)) + W64.of_int 1665) * (W64.of_int 1290167)) (W64.of_int 32)). 
+
+op lane_polyvec_redcomp10(w : W16.t) : W10.t = lane_func_compress10 (lane_func_reduce w).
+
+op lane(w : W16.t) : W16.t = w.
 op pcond (w: W16.t) = true.
 
 lemma blah (_bp : W16.t Array768.t) : hoare [ AuxPolyVecCompress10.avx2 : true ==> false].
@@ -1961,25 +1958,17 @@ proc change 37 : (sliceget32_8_256 pvc_shufbidx_s 0). by admit.
 
 proc change ^while{4}.1 : (sliceget768_16_256 a i). by admit.
 
-print set128_direct.
-
 proc change ^while{4}.25 : (init_960_8 (fun j => (sliceset960_8_128 rp (i * 20) lo).[j])). by admit.
 proc change ^while{4}.26 : (init_960_8 (fun j => (sliceset960_8_32 rp (i * 20 + 16) (VPEXTR_32 hi W8.zero)).[j])). 
 by admit.
 
-
-
-
 cfold 38.
 unroll for 39.
 cfold 38. unroll for 24. cfold 23.
 unroll for 16. cfold 15. unroll for 8. cfold 7.
 
-seq 590 : true.
-
-bdep 16 10 [_bp] [bp] [ap] lane_polyvec_redcomp10 pcond.
+bdep 16 16 [_bp] [bp] [ap] lane pcond.
 
-print get256_direct.
 qed.
 
 (* MAP REDUCE GOAL *)