Implement SHA3 transpose lemma

mamonet · Dec 25, 2023 · 2898867 · 2898867
1 parent 6f6c085
commit 2898867
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 4 deletions.
diff --git a/code/sha3/Hacl.Spec.SHA3.Lemmas.fst b/code/sha3/Hacl.Spec.SHA3.Lemmas.fst
@@ -33,3 +33,18 @@ let transpose_ws4_lemma_ij #m ws j i =
   transpose4x4_lemma vs;
   assert ((vec_v (transpose_ws4 ws).[i]).[j] == (vec_v vs.[j]).[j_sub]);
   assert ((vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i_sub * l + j]).[j_sub])
+
+val transpose_ws_lemma_ij:
+    #m:m_spec{is_supported m}
+  -> ws:ws_spec m
+  -> j:nat{j < lanes m}
+  -> i:nat{i < 32} ->
+  Lemma
+   (let l = lanes m in
+    ((ws_spec_v #m (transpose_ws ws)).[j]).[i] == (vec_v ws.[i / l * l + j]).[i % l])
+
+let transpose_ws_lemma_ij #m ws j i =
+  assert (((ws_spec_v #m (transpose_ws ws)).[j]).[i] == (vec_v (transpose_ws ws).[i]).[j]);
+  match lanes m with
+  | 1 -> ()
+  | 4 -> transpose_ws4_lemma_ij #m ws j i
diff --git a/code/sha3/Hacl.Spec.SHA3.Vec.fst b/code/sha3/Hacl.Spec.SHA3.Vec.fst
@@ -265,10 +265,19 @@ noextract
 let ws_spec (m:m_spec) = lseq (element_t m) 32
 
 noextract
-let ws_spec_v (#a:keccak_alg) (#m:m_spec) (st:ws_spec m) : lseq (lseq (word a) 32) (lanes m) =
-  createi #(lseq (word a) 32) (lanes m) (fun i ->
-    createi 32 (fun j ->
-      (vec_v st.[j]).[i]))
+let ws_spec_v (#m:m_spec) (st:ws_spec m) : lseq (lseq uint64 32) (lanes m) =
+  createi #(lseq uint64 32) (lanes m) (fun i ->
+    create32 (vec_v st.[0]).[i] (vec_v st.[1]).[i] (vec_v st.[2]).[i]
+             (vec_v st.[3]).[i] (vec_v st.[4]).[i] (vec_v st.[5]).[i]
+             (vec_v st.[6]).[i] (vec_v st.[7]).[i] (vec_v st.[8]).[i]
+             (vec_v st.[9]).[i] (vec_v st.[10]).[i] (vec_v st.[11]).[i]
+             (vec_v st.[12]).[i] (vec_v st.[13]).[i] (vec_v st.[14]).[i]
+             (vec_v st.[15]).[i] (vec_v st.[16]).[i] (vec_v st.[17]).[i]
+             (vec_v st.[18]).[i] (vec_v st.[19]).[i] (vec_v st.[20]).[i]
+             (vec_v st.[21]).[i] (vec_v st.[22]).[i] (vec_v st.[23]).[i]
+             (vec_v st.[24]).[i] (vec_v st.[25]).[i] (vec_v st.[26]).[i]
+             (vec_v st.[27]).[i] (vec_v st.[28]).[i] (vec_v st.[29]).[i]
+             (vec_v st.[30]).[i] (vec_v st.[31]).[i])
 
 noextract
 let multiseq (lanes:lanes_t) (len:nat) =