Cleanup and specs with Rust types

.gitignore

@@ -1,2 +1,4 @@
 Cargo.lock
 .vscode
+target/
+.DS_Store

Cargo.toml

@@ -1,12 +1,13 @@
 [workspace]
 members = [
-    "basic",
     "curve25519",
     "chacha20",
+    "chacha20-rust",
     "poly1305",
     "chacha20poly1305",
     "gimli",
     "sha256",
+    "sha256-rust",
     "sha3",
     "hmac",
     "hkdf",

chacha20-rust/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "chacha20"
+version = "0.1.0"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+edition = "2021"
+
+[dependencies]

chacha20-rust/out/Chacha20.Hacspec_helper.fst

@@ -0,0 +1,166 @@
+module Chacha20.Hacspec_helper
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let to_le_u32s_3 (bytes: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 3} =
+  let _:Prims.l_False =
+    match 3, Prims.op_Division (Core.Slice.len bytes) 4 with
+    | left_val, right_val ->
+      if Prims.l_Not (left_val = right_val)
+      then
+        let kind:Core.Panicking.assertKind_t = Core.Panicking.Eq in
+        Core.Panicking.assert_failed kind left_val right_val Core.Option.None
+  in
+  let out:Alloc.Boxed.box_t
+    (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 3})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0ul 3
+  in
+  let out:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 3} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({ start = 0; end = 3 }
+          ))
+      out
+      (fun i out ->
+          out.[ i ] <-
+            Core.Num.from_le_bytes (Core.Result.unwrap (Core.Convert.TryInto.try_into bytes.[ {
+                          start = 4 * i;
+                          end = 4 * i + 4
+                        } ])))
+  in
+  out
+
+let to_le_u32s_8 (bytes: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  let _:Prims.l_False =
+    match 8, Prims.op_Division (Core.Slice.len bytes) 4 with
+    | left_val, right_val ->
+      if Prims.l_Not (left_val = right_val)
+      then
+        let kind:Core.Panicking.assertKind_t = Core.Panicking.Eq in
+        Core.Panicking.assert_failed kind left_val right_val Core.Option.None
+  in
+  let out:Alloc.Boxed.box_t
+    (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0ul 8
+  in
+  let out:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({ start = 0; end = 8 }
+          ))
+      out
+      (fun i out ->
+          out.[ i ] <-
+            Core.Num.from_le_bytes (Core.Result.unwrap (Core.Convert.TryInto.try_into bytes.[ {
+                          start = 4 * i;
+                          end = 4 * i + 4
+                        } ])))
+  in
+  out
+
+let to_le_u32s_16 (bytes: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+  let _:Prims.l_False =
+    match 16, Prims.op_Division (Core.Slice.len bytes) 4 with
+    | left_val, right_val ->
+      if Prims.l_Not (left_val = right_val)
+      then
+        let kind:Core.Panicking.assertKind_t = Core.Panicking.Eq in
+        Core.Panicking.assert_failed kind left_val right_val Core.Option.None
+  in
+  let out:Alloc.Boxed.box_t
+    (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0ul 16
+  in
+  let out:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = 16
+            }))
+      out
+      (fun i out ->
+          out.[ i ] <-
+            Core.Num.from_le_bytes (Core.Result.unwrap (Core.Convert.TryInto.try_into bytes.[ {
+                          start = 4 * i;
+                          end = 4 * i + 4
+                        } ])))
+  in
+  out
+
+let u32s_to_le_bytes
+      (state: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let out:Alloc.Boxed.box_t
+    (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0uy 64
+  in
+  let out:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = Core.Slice.len (Hacspec.Lib.unsize state)
+            }))
+      out
+      (fun i out ->
+          let tmp:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 4} =
+            Core.Num.to_le_bytes (Core.Ops.Index.index state i)
+          in
+          Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+                    start = 0;
+                    end = 4
+                  }))
+            out
+            (fun j out -> out.[ i * 4 + j ] <- Core.Ops.Index.index tmp j))
+  in
+  out
+
+let xor_state
+      (state other: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = 16
+            }))
+      state
+      (fun i state ->
+          state.[ i ] <-
+            Hacspec_lib.^. (Core.Ops.Index.index state i) (Core.Ops.Index.index other i))
+  in
+  state
+
+let add_state
+      (state other: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = 16
+            }))
+      state
+      (fun i state ->
+          state.[ i ] <-
+            Core.Num.wrapping_add (Core.Ops.Index.index state i) (Core.Ops.Index.index other i))
+  in
+  state
+
+let update_array
+      (array: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+      (val: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let _:Prims.l_False =
+    if Prims.l_Not (Prims.op_GreaterThan 64 (Core.Slice.len val))
+    then Core.Panicking.panic "assertion failed: 64 >= val.len()"
+  in
+  let array:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = Core.Slice.len val
+            }))
+      array
+      (fun i array -> array.[ i ] <- Core.Ops.Index.index val i)
+  in
+  array

chacha20-rust/out/Chacha20.Hacspec_helper.v

@@ -0,0 +1,40 @@
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Require Import Super. (* as State *)
+
+(*Not implemented yet? todo(item)*)
+
+Definition to_le_u32s_3 (bytes : seq int8) : nseq int32 TODO: Int.to_string length :=
+  failure todo(term).
+
+Definition to_le_u32s_8 (bytes : seq int8) : nseq int32 TODO: Int.to_string length :=
+  failure todo(term).
+
+Definition to_le_u32s_16 (bytes : seq int8) : nseq int32 TODO: Int.to_string length :=
+  failure todo(term).
+
+Definition u32s_to_le_bytes (state : nseq int32 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let out := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let out := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(len (unsize state)))) out (fun i out =>
+      let tmp := (to_le_bytes (index state i)) : nseq int8 TODO: Int.to_string length in
+      fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 4))) out (fun j out =>
+        update_at out ((i.*(@repr WORDSIZE32 4)).+j) (index tmp j)))) : nseq int8 TODO: Int.to_string length in
+  out.
+
+Definition xor_state (state : nseq int32 TODO: Int.to_string length) (other : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 16))) state (fun i state =>
+      update_at state i ((index state i).^(index other i)))) : nseq int32 TODO: Int.to_string length in
+  state.
+
+Definition add_state (state : nseq int32 TODO: Int.to_string length) (other : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 16))) state (fun i state =>
+      update_at state i (wrapping_add (index state i) (index other i)))) : nseq int32 TODO: Int.to_string length in
+  state.
+
+Definition update_array (array : nseq int8 TODO: Int.to_string length) (val : seq int8) : nseq int8 TODO: Int.to_string length :=
+  failure todo(term).