Add proofs for Ind_cpa functions

cryspen · Oct 14, 2024 · 6f11eac · 6f11eac
1 parent 5ef4ee0
commit 6f11eac
Show file tree

Hide file tree

Showing 22 changed files with 872 additions and 239 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
           result == Spec.Utils.v_PRF v_LEN input)
 
 val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
-    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+      (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+      (ensures
+        fun result ->
+          let result:t_Array (t_Array u8 v_LEN) v_K = result in
+          result == Spec.Utils.v_PRFxN v_K v_LEN input)
 
 /// The state.
 /// It\'s only used for SHAKE128.
@@ -73,15 +78,17 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd256Hash v_K =
     f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
     f_PRFxN_pre
     =
-    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) -> true);
+    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->
+        v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
     f_PRFxN_post
     =
     (fun
         (v_LEN: usize)
         (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
         (out: t_Array (t_Array u8 v_LEN) v_K)
         ->
-        true);
+        (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+        out == Spec.Utils.v_PRFxN v_K v_LEN input);
     f_PRFxN
     =
     (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
           result == Spec.Utils.v_PRF v_LEN input)
 
 val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
-    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+      (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+      (ensures
+        fun result ->
+          let result:t_Array (t_Array u8 v_LEN) v_K = result in
+          result == Spec.Utils.v_PRFxN v_K v_LEN input)
 
 /// The state.
 /// It\'s only used for SHAKE128.
@@ -73,15 +78,17 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd128Hash v_K =
     f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
     f_PRFxN_pre
     =
-    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) -> true);
+    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->
+        v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
     f_PRFxN_post
     =
     (fun
         (v_LEN: usize)
         (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
         (out: t_Array (t_Array u8 v_LEN) v_K)
         ->
-        true);
+        (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+        out == Spec.Utils.v_PRFxN v_K v_LEN input);
     f_PRFxN
     =
     (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
           result == Spec.Utils.v_PRF v_LEN input)
 
 val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
-    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+      (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+      (ensures
+        fun result ->
+          let result:t_Array (t_Array u8 v_LEN) v_K = result in
+          result == Spec.Utils.v_PRFxN v_K v_LEN input)
 
 /// The state.
 /// It\'s only used for SHAKE128.
@@ -73,15 +78,17 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash (t_PortableHash v_K
     f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
     f_PRFxN_pre
     =
-    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) -> true);
+    (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->
+        v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
     f_PRFxN_post
     =
     (fun
         (v_LEN: usize)
         (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K)
         (out: t_Array (t_Array u8 v_LEN) v_K)
         ->
-        true);
+        (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+        out == Spec.Utils.v_PRFxN v_K v_LEN input);
     f_PRFxN
     =
     (fun (v_LEN: usize) (input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K) ->

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti
@@ -30,12 +30,16 @@ class t_Hash (v_Self: Type0) (v_K: usize) = {
   f_PRF:v_LEN: usize -> x0: t_Slice u8
     -> Prims.Pure (t_Array u8 v_LEN) (f_PRF_pre v_LEN x0) (fun result -> f_PRF_post v_LEN x0 result);
   f_PRFxN_pre:v_LEN: usize -> input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K
-    -> pred: Type0{true ==> pred};
+    -> pred: Type0{v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4) ==> pred};
   f_PRFxN_post:
       v_LEN: usize ->
-      t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K ->
-      t_Array (t_Array u8 v_LEN) v_K
-    -> Type0;
+      input: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K ->
+      result: t_Array (t_Array u8 v_LEN) v_K
+    -> pred:
+      Type0
+        { pred ==>
+          (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+          result == Spec.Utils.v_PRFxN v_K v_LEN input };
   f_PRFxN:v_LEN: usize -> x0: t_Array (t_Array u8 (Rust_primitives.mk_usize 33)) v_K
     -> Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
         (f_PRFxN_pre v_LEN x0)