diff --git a/.gitignore b/.gitignore
index 67c81c9..48c4419 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 Cargo.lock
 .vscode
+target/
+.DS_Store
diff --git a/Cargo.toml b/Cargo.toml
index b207749..5faaa44 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,14 +1,16 @@
 [workspace]
 members = [
-    "basic",
     "curve25519",
     "chacha20",
+    "chacha20-rust",
     "poly1305",
     "chacha20poly1305",
     "gimli",
     "sha256",
+    "sha256-rust",
     "sha3",
     "hmac",
+    "hmac-rust",
     "hkdf",
     "p256",
     "bls12-381",
diff --git a/chacha20-rust/Cargo.toml b/chacha20-rust/Cargo.toml
new file mode 100644
index 0000000..9a31d54
--- /dev/null
+++ b/chacha20-rust/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "chacha20"
+version = "0.1.0"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+edition = "2021"
+
+[dependencies]
diff --git a/chacha20-rust/out/Chacha20.Hacspec_helper.fst b/chacha20-rust/out/Chacha20.Hacspec_helper.fst
new file mode 100644
index 0000000..982add2
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/chacha20-rust/out/Chacha20.Hacspec_helper.v b/chacha20-rust/out/Chacha20.Hacspec_helper.v
new file mode 100644
index 0000000..516cb94
--- /dev/null
+++ b/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).
diff --git a/chacha20-rust/out/Chacha20.fst b/chacha20-rust/out/Chacha20.fst
new file mode 100644
index 0000000..e7fbcf1
--- /dev/null
+++ b/chacha20-rust/out/Chacha20.fst
@@ -0,0 +1,224 @@
+module Chacha20
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let state = x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}
+
+let block = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}
+
+let chaChaIV = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}
+
+let chaChaKey = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}
+
+let chacha20_line
+      (a b d: uint_size)
+      (s: UInt32.t)
+      (m: (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} = m in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    state.[ a ] <-
+      Core.Num.wrapping_add (Core.Ops.Index.index state a) (Core.Ops.Index.index state b)
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    state.[ d ] <- Hacspec_lib.^. (Core.Ops.Index.index state d) (Core.Ops.Index.index state a)
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    state.[ d ] <- Core.Num.rotate_left (Core.Ops.Index.index state d) s
+  in
+  state
+
+let chacha20_quarter_round
+      (a b c d: uint_size)
+      (state: (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} =
+    chacha20_line a b d 16ul state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_line c d b 12ul state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_line a b d 8ul state
+  in
+  chacha20_line c d b 7ul state
+
+let chacha20_double_round
+      (state: (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} =
+    chacha20_quarter_round 0 4 8 12 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 1 5 9 13 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 2 6 10 14 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 3 7 11 15 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 0 5 10 15 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 1 6 11 12 state
+  in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_quarter_round 2 7 8 13 state
+  in
+  chacha20_quarter_round 3 4 9 14 state
+
+let chacha20_rounds
+      (state: (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 st:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} = state in
+  let st: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 = 0l;
+              end = 10l
+            }))
+      st
+      (fun _i st -> chacha20_double_round st)
+  in
+  st
+
+let chacha20_core
+      (ctr: UInt32.t)
+      (st0: (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} = st0 in
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    state.[ 12 ] <- Core.Ops.Index.index state 12 + ctr
+  in
+  let k:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_rounds state
+  in
+  Chacha20.Hacspec_helper.add_state state k
+
+let chacha20_init
+      (key: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}))
+      (iv: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}))
+      (ctr: UInt32.t)
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+  let (key_u32: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8})):x:
+  Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    Chacha20.Hacspec_helper.to_le_u32s_8 (Hacspec.Lib.unsize key)
+  in
+  let (iv_u32: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 3})):x:
+  Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 3} =
+    Chacha20.Hacspec_helper.to_le_u32s_3 (Hacspec.Lib.unsize iv)
+  in
+  [
+    1634760805ul; 857760878ul; 2036477234ul; 1797285236ul; Core.Ops.Index.index key_u32 0;
+    Core.Ops.Index.index key_u32 1; Core.Ops.Index.index key_u32 2; Core.Ops.Index.index key_u32 3;
+    Core.Ops.Index.index key_u32 4; Core.Ops.Index.index key_u32 5; Core.Ops.Index.index key_u32 6;
+    Core.Ops.Index.index key_u32 7; ctr; Core.Ops.Index.index iv_u32 0;
+    Core.Ops.Index.index iv_u32 1; Core.Ops.Index.index iv_u32 2
+  ]
+
+let chacha20_key_block
+      (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 state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_core 0ul state
+  in
+  Chacha20.Hacspec_helper.u32s_to_le_bytes state
+
+let chacha20_key_block0
+      (key: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}))
+      (iv: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}))
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_init key iv 0ul
+  in
+  chacha20_key_block state
+
+let chacha20_encrypt_block
+      (st0: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+      (ctr: UInt32.t)
+      (plain: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let st:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_core ctr st0
+  in
+  let (pl: (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} =
+    Chacha20.Hacspec_helper.to_le_u32s_16 (Hacspec.Lib.unsize plain)
+  in
+  let encrypted:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    Chacha20.Hacspec_helper.xor_state st pl
+  in
+  Chacha20.Hacspec_helper.u32s_to_le_bytes encrypted
+
+let chacha20_encrypt_last
+      (st0: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+      (ctr: UInt32.t)
+      (plain: FStar.Seq.seq UInt8.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let (b: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})):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 b:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    Chacha20.Hacspec_helper.update_array b plain
+  in
+  let b:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    chacha20_encrypt_block st0 ctr b
+  in
+  Alloc.Slice.to_vec b.[ { end = Core.Slice.len plain } ]
+
+let chacha20_update
+      (st0: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16}))
+      (m: FStar.Seq.seq UInt8.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let blocks_out:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t = Alloc.Vec.new_ in
+  let num_blocks:uint_size = Prims.op_Division (Core.Slice.len m) 64 in
+  let remainder_len:uint_size = Prims.op_Modulus (Core.Slice.len m) 64 in
+  let blocks_out:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = num_blocks
+            }))
+      blocks_out
+      (fun i blocks_out ->
+          let b:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+            chacha20_encrypt_block st0
+              (cast i)
+              (Core.Result.unwrap (Core.Convert.TryInto.try_into m.[ {
+                          start = 64 * i;
+                          end = 64 * i + 64
+                        } ]))
+          in
+          let blocks_out:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+            Alloc.Vec.extend_from_slice blocks_out (Hacspec.Lib.unsize b)
+          in
+          blocks_out)
+  in
+  let blocks_out:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    if remainder_len <> 0
+    then
+      let b:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+        chacha20_encrypt_last st0 (cast num_blocks) m.[ { start = 64 * num_blocks } ]
+      in
+      let blocks_out:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+        Alloc.Vec.extend_from_slice blocks_out (Core.Ops.Deref.Deref.deref b)
+      in
+      blocks_out
+    else blocks_out
+  in
+  blocks_out
+
+let chacha20
+      (m: FStar.Seq.seq UInt8.t)
+      (key: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}))
+      (iv: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}))
+      (ctr: UInt32.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let state:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 16} =
+    chacha20_init key iv ctr
+  in
+  chacha20_update state m
\ No newline at end of file
diff --git a/chacha20-rust/out/Chacha20.v b/chacha20-rust/out/Chacha20.v
new file mode 100644
index 0000000..3a83975
--- /dev/null
+++ b/chacha20-rust/out/Chacha20.v
@@ -0,0 +1,117 @@
+(* 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.
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+Require Import Hacspec_helper.
+
+Notation State_t := (nseq int32 TODO: Int.to_string length).
+
+Notation Block_t := (nseq int8 TODO: Int.to_string length).
+
+Notation ChaChaIV_t := (nseq int8 TODO: Int.to_string length).
+
+Notation ChaChaKey_t := (nseq int8 TODO: Int.to_string length).
+
+Definition chacha20_line (a : uint_size) (b : uint_size) (d : uint_size) (s : int32) (m : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (m) : nseq int32 TODO: Int.to_string length in
+  let state := (update_at state a (wrapping_add (index state a) (index state b))) : nseq int32 TODO: Int.to_string length in
+  let state := (update_at state d ((index state d).^(index state a))) : nseq int32 TODO: Int.to_string length in
+  let state := (update_at state d (rotate_left (index state d) s)) : nseq int32 TODO: Int.to_string length in
+  state.
+
+Definition chacha20_quarter_round (a : uint_size) (b : uint_size) (c : uint_size) (d : uint_size) (state : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (chacha20_line a b d (@repr WORDSIZE32 16) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_line c d b (@repr WORDSIZE32 12) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_line a b d (@repr WORDSIZE32 8) state) : nseq int32 TODO: Int.to_string length in
+  chacha20_line c d b (@repr WORDSIZE32 7) state.
+
+Definition chacha20_double_round (state : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 0) (@repr WORDSIZE32 4) (@repr WORDSIZE32 8) (@repr WORDSIZE32 12) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 1) (@repr WORDSIZE32 5) (@repr WORDSIZE32 9) (@repr WORDSIZE32 13) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 2) (@repr WORDSIZE32 6) (@repr WORDSIZE32 10) (@repr WORDSIZE32 14) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 3) (@repr WORDSIZE32 7) (@repr WORDSIZE32 11) (@repr WORDSIZE32 15) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 0) (@repr WORDSIZE32 5) (@repr WORDSIZE32 10) (@repr WORDSIZE32 15) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 1) (@repr WORDSIZE32 6) (@repr WORDSIZE32 11) (@repr WORDSIZE32 12) state) : nseq int32 TODO: Int.to_string length in
+  let state := (chacha20_quarter_round (@repr WORDSIZE32 2) (@repr WORDSIZE32 7) (@repr WORDSIZE32 8) (@repr WORDSIZE32 13) state) : nseq int32 TODO: Int.to_string length in
+  chacha20_quarter_round (@repr WORDSIZE32 3) (@repr WORDSIZE32 4) (@repr WORDSIZE32 9) (@repr WORDSIZE32 14) state.
+
+Definition chacha20_rounds (state : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let st := (state) : nseq int32 TODO: Int.to_string length in
+  let st := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 10))) st (fun _i st =>
+      chacha20_double_round st)) : nseq int32 TODO: Int.to_string length in
+  st.
+
+Definition chacha20_core (ctr : int32) (st0 : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let state := (st0) : nseq int32 TODO: Int.to_string length in
+  let state := (update_at state (@repr WORDSIZE32 12) ((index state (@repr WORDSIZE32 12)).+ctr)) : nseq int32 TODO: Int.to_string length in
+  let k := (chacha20_rounds state) : nseq int32 TODO: Int.to_string length in
+  add_state state k.
+
+Definition chacha20_init (key : nseq int8 TODO: Int.to_string length) (iv : nseq int8 TODO: Int.to_string length) (ctr : int32) : nseq int32 TODO: Int.to_string length :=
+  let key_u32 := (to_le_u32s_8 (unsize key)) : nseq int32 TODO: Int.to_string length in
+  let iv_u32 := (to_le_u32s_3 (unsize iv)) : nseq int32 TODO: Int.to_string length in
+  array_from_list [(@repr WORDSIZE32 1634760805);
+    (@repr WORDSIZE32 857760878);
+    (@repr WORDSIZE32 2036477234);
+    (@repr WORDSIZE32 1797285236);
+    index key_u32 (@repr WORDSIZE32 0);
+    index key_u32 (@repr WORDSIZE32 1);
+    index key_u32 (@repr WORDSIZE32 2);
+    index key_u32 (@repr WORDSIZE32 3);
+    index key_u32 (@repr WORDSIZE32 4);
+    index key_u32 (@repr WORDSIZE32 5);
+    index key_u32 (@repr WORDSIZE32 6);
+    index key_u32 (@repr WORDSIZE32 7);
+    ctr;
+    index iv_u32 (@repr WORDSIZE32 0);
+    index iv_u32 (@repr WORDSIZE32 1);
+    index iv_u32 (@repr WORDSIZE32 2)].
+
+Definition chacha20_key_block (state : nseq int32 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let state := (chacha20_core (@repr WORDSIZE32 0) state) : nseq int32 TODO: Int.to_string length in
+  u32s_to_le_bytes state.
+
+Definition chacha20_key_block0 (key : nseq int8 TODO: Int.to_string length) (iv : nseq int8 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let state := (chacha20_init key iv (@repr WORDSIZE32 0)) : nseq int32 TODO: Int.to_string length in
+  chacha20_key_block state.
+
+Definition chacha20_encrypt_block (st0 : nseq int32 TODO: Int.to_string length) (ctr : int32) (plain : nseq int8 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let st := (chacha20_core ctr st0) : nseq int32 TODO: Int.to_string length in
+  let pl := (to_le_u32s_16 (unsize plain)) : nseq int32 TODO: Int.to_string length in
+  let encrypted := (xor_state st pl) : nseq int32 TODO: Int.to_string length in
+  u32s_to_le_bytes encrypted.
+
+Definition chacha20_encrypt_last (st0 : nseq int32 TODO: Int.to_string length) (ctr : int32) (plain : seq int8) : Vec_t (int8) (Global_t) :=
+  let b := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let b := (update_array b plain) : nseq int8 TODO: Int.to_string length in
+  let b := (chacha20_encrypt_block st0 ctr b) : nseq int8 TODO: Int.to_string length in
+  to_vec (b.[(Build_RangeTo_t (len plain))]).
+
+Definition chacha20_update (st0 : nseq int32 TODO: Int.to_string length) (m : seq int8) : Vec_t (int8) (Global_t) :=
+  let blocks_out := (new) : Vec_t (int8) (Global_t) in
+  let num_blocks := ((len m)./(@repr WORDSIZE32 64)) : uint_size in
+  let remainder_len := ((len m).%(@repr WORDSIZE32 64)) : uint_size in
+  let blocks_out := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)num_blocks)) blocks_out (fun i blocks_out =>
+      let b := (chacha20_encrypt_block st0 (cast i) (unwrap (try_into (m.[(Build_Range_t ((@repr WORDSIZE32 64).*i)(((@repr WORDSIZE32 64).*i).+(@repr WORDSIZE32 64)))])))) : nseq int8 TODO: Int.to_string length in
+      let blocks_out := (extend_from_slice blocks_out (unsize b)) : Vec_t (int8) (Global_t) in
+      blocks_out)) : Vec_t (int8) (Global_t) in
+  let blocks_out := (if
+      remainder_len<>(@repr WORDSIZE32 0)
+    then
+      let b := (chacha20_encrypt_last st0 (cast num_blocks) (m.[(Build_RangeFrom_t ((@repr WORDSIZE32 64).*num_blocks))])) : Vec_t (int8) (Global_t) in
+      let blocks_out := (extend_from_slice blocks_out (deref b)) : Vec_t (int8) (Global_t) in
+      blocks_out
+    else
+      blocks_out) : Vec_t (int8) (Global_t) in
+  blocks_out.
+
+Definition chacha20 (m : seq int8) (key : nseq int8 TODO: Int.to_string length) (iv : nseq int8 TODO: Int.to_string length) (ctr : int32) : Vec_t (int8) (Global_t) :=
+  let state := (chacha20_init key iv ctr) : nseq int32 TODO: Int.to_string length in
+  chacha20_update state m.
diff --git a/chacha20-rust/src/hacspec_helper.rs b/chacha20-rust/src/hacspec_helper.rs
new file mode 100644
index 0000000..a3a4b0a
--- /dev/null
+++ b/chacha20-rust/src/hacspec_helper.rs
@@ -0,0 +1,62 @@
+use super::State;
+
+// pub(super) fn to_le_u32s<const L: usize>(bytes: &[u8]) -> [u32; L] {
+//     assert_eq!(L, bytes.len() / 4);
+//     let mut out = [0; L];
+//     for (i, block) in bytes.chunks(4).enumerate() {
+//         out[i] = u32::from_le_bytes(block.try_into().unwrap());
+//     }
+//     out
+// }
+
+macro_rules! to_le_u32s_impl {
+    ($name:ident,$l:literal) => {
+        pub(super) fn $name(bytes: &[u8]) -> [u32; $l] {
+            assert_eq!($l, bytes.len() / 4);
+            let mut out = [0; $l];
+            // for (i, block) in bytes.chunks(4).enumerate() {
+            for i in 0..$l {
+                out[i] = u32::from_le_bytes(bytes[4 * i..4 * i + 4].try_into().unwrap());
+            }
+            out
+        }
+    };
+}
+to_le_u32s_impl!(to_le_u32s_3, 3);
+to_le_u32s_impl!(to_le_u32s_8, 8);
+to_le_u32s_impl!(to_le_u32s_16, 16);
+
+pub(super) fn u32s_to_le_bytes(state: &[u32; 16]) -> [u8; 64] {
+    // <const L: usize>
+    let mut out = [0; 64];
+    for i in 0..state.len() {
+        let tmp = state[i].to_le_bytes();
+        for j in 0..4 {
+            out[i * 4 + j] = tmp[j];
+        }
+    }
+    out
+}
+
+pub(super) fn xor_state(mut state: State, other: State) -> State {
+    for i in 0..16 {
+        state[i] = state[i] ^ other[i];
+    }
+    state
+}
+
+pub(super) fn add_state(mut state: State, other: State) -> State {
+    for i in 0..16 {
+        state[i] = state[i].wrapping_add(other[i]);
+    }
+    state
+}
+
+pub(super) fn update_array(mut array: [u8; 64], val: &[u8]) -> [u8; 64] {
+    // <const L: usize>
+    assert!(64 >= val.len());
+    for i in 0..val.len() {
+        array[i] = val[i];
+    }
+    array
+}
diff --git a/chacha20-rust/src/lib.rs b/chacha20-rust/src/lib.rs
new file mode 100644
index 0000000..8a70c2b
--- /dev/null
+++ b/chacha20-rust/src/lib.rs
@@ -0,0 +1,123 @@
+mod hacspec_helper;
+use hacspec_helper::*;
+
+type State = [u32; 16];
+type Block = [u8; 64];
+type ChaChaIV = [u8; 12];
+type ChaChaKey = [u8; 32];
+
+fn chacha20_line(a: usize, b: usize, d: usize, s: u32, m: State) -> State {
+    let mut state = m;
+    state[a] = state[a].wrapping_add(state[b]);
+    state[d] = state[d] ^ state[a];
+    state[d] = state[d].rotate_left(s);
+    state
+}
+
+pub fn chacha20_quarter_round(a: usize, b: usize, c: usize, d: usize, state: State) -> State {
+    let state = chacha20_line(a, b, d, 16, state);
+    let state = chacha20_line(c, d, b, 12, state);
+    let state = chacha20_line(a, b, d, 8, state);
+    chacha20_line(c, d, b, 7, state)
+}
+
+fn chacha20_double_round(state: State) -> State {
+    let state = chacha20_quarter_round(0, 4, 8, 12, state);
+    let state = chacha20_quarter_round(1, 5, 9, 13, state);
+    let state = chacha20_quarter_round(2, 6, 10, 14, state);
+    let state = chacha20_quarter_round(3, 7, 11, 15, state);
+
+    let state = chacha20_quarter_round(0, 5, 10, 15, state);
+    let state = chacha20_quarter_round(1, 6, 11, 12, state);
+    let state = chacha20_quarter_round(2, 7, 8, 13, state);
+    chacha20_quarter_round(3, 4, 9, 14, state)
+}
+
+pub fn chacha20_rounds(state: State) -> State {
+    let mut st = state;
+    for _i in 0..10 {
+        st = chacha20_double_round(st);
+    }
+    st
+}
+
+pub fn chacha20_core(ctr: u32, st0: State) -> State {
+    let mut state = st0;
+    state[12] = state[12] + ctr;
+    let k = chacha20_rounds(state);
+    add_state(state, k)
+}
+
+pub fn chacha20_init(key: &ChaChaKey, iv: &ChaChaIV, ctr: u32) -> State {
+    let key_u32: [u32; 8] = to_le_u32s_8(key);
+    let iv_u32: [u32; 3] = to_le_u32s_3(iv);
+    [
+        0x6170_7865,
+        0x3320_646e,
+        0x7962_2d32,
+        0x6b20_6574,
+        key_u32[0],
+        key_u32[1],
+        key_u32[2],
+        key_u32[3],
+        key_u32[4],
+        key_u32[5],
+        key_u32[6],
+        key_u32[7],
+        ctr,
+        iv_u32[0],
+        iv_u32[1],
+        iv_u32[2],
+    ]
+}
+
+pub fn chacha20_key_block(state: State) -> Block {
+    let state = chacha20_core(0u32, state);
+    u32s_to_le_bytes(&state)
+}
+
+pub fn chacha20_key_block0(key: &ChaChaKey, iv: &ChaChaIV) -> Block {
+    let state = chacha20_init(key, iv, 0u32);
+    chacha20_key_block(state)
+}
+
+pub fn chacha20_encrypt_block(st0: State, ctr: u32, plain: &Block) -> Block {
+    let st = chacha20_core(ctr, st0);
+    let pl: State = to_le_u32s_16(plain);
+    let encrypted = xor_state(st, pl);
+    u32s_to_le_bytes(&encrypted)
+}
+
+pub fn chacha20_encrypt_last(st0: State, ctr: u32, plain: &[u8]) -> Vec<u8> {
+    let mut b: Block = [0; 64];
+    b = update_array(b, plain);
+    b = chacha20_encrypt_block(st0, ctr, &b);
+    b[..plain.len()].to_vec()
+}
+
+pub fn chacha20_update(st0: State, m: &[u8]) -> Vec<u8> {
+    let mut blocks_out = Vec::new();
+    let num_blocks = m.len() / 64;
+    let remainder_len = m.len() % 64;
+    // for (i, msg_block) in m.chunks(64).enumerate() {
+    for i in 0..num_blocks {
+        // if msg_block.len() != 64 {
+        // } else {
+        // Full block
+        let b =
+            chacha20_encrypt_block(st0, i as u32, &m[64 * i..(64 * i + 64)].try_into().unwrap());
+        blocks_out.extend_from_slice(&b);
+        // }
+    }
+    if remainder_len != 0 {
+        // Last block
+        let b = chacha20_encrypt_last(st0, num_blocks as u32, &m[64 * num_blocks..]);
+        blocks_out.extend_from_slice(&b);
+    }
+    blocks_out
+}
+
+pub fn chacha20(m: &[u8], key: &ChaChaKey, iv: &ChaChaIV, ctr: u32) -> Vec<u8> {
+    let state = chacha20_init(key, iv, ctr);
+    chacha20_update(state, m)
+}
diff --git a/chacha20-rust/tests/kat.rs b/chacha20-rust/tests/kat.rs
new file mode 100644
index 0000000..b5a15ec
--- /dev/null
+++ b/chacha20-rust/tests/kat.rs
@@ -0,0 +1,139 @@
+use chacha20::chacha20;
+
+pub type ChaChaIV = [u8; 12];
+pub type ChaChaKey = [u8; 32];
+
+fn kat_test(m: Vec<u8>, key: ChaChaKey, iv: ChaChaIV, exp_cipher: Vec<u8>) {
+    let out = chacha20(&m, &key, &iv, 1u32);
+    assert_eq!(exp_cipher, out);
+
+    let decrypted = chacha20(&out, &key, &iv, 1u32);
+    assert_eq!(m, decrypted);
+}
+
+#[test]
+fn test_kat() {
+    let key = [
+        0x80, 0x81, 0x82, 0x83, 0x84, 0x85, 0x86, 0x87, 0x88, 0x89, 0x8a, 0x8b, 0x8c, 0x8d, 0x8e,
+        0x8f, 0x90, 0x91, 0x92, 0x93, 0x94, 0x95, 0x96, 0x97, 0x98, 0x99, 0x9a, 0x9b, 0x9c, 0x9d,
+        0x9e, 0x9f,
+    ];
+    let iv = [
+        0x07, 0x00, 0x00, 0x00, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47,
+    ];
+    let m = vec![
+        0x4c, 0x61, 0x64, 0x69, 0x65, 0x73, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x47, 0x65, 0x6e, 0x74,
+        0x6c, 0x65, 0x6d, 0x65, 0x6e, 0x20, 0x6f, 0x66, 0x20, 0x74, 0x68, 0x65, 0x20, 0x63, 0x6c,
+        0x61, 0x73, 0x73, 0x20, 0x6f, 0x66, 0x20, 0x27, 0x39, 0x39, 0x3a, 0x20, 0x49, 0x66, 0x20,
+        0x49, 0x20, 0x63, 0x6f, 0x75, 0x6c, 0x64, 0x20, 0x6f, 0x66, 0x66, 0x65, 0x72, 0x20, 0x79,
+        0x6f, 0x75, 0x20, 0x6f, 0x6e, 0x6c, 0x79, 0x20, 0x6f, 0x6e, 0x65, 0x20, 0x74, 0x69, 0x70,
+        0x20, 0x66, 0x6f, 0x72, 0x20, 0x74, 0x68, 0x65, 0x20, 0x66, 0x75, 0x74, 0x75, 0x72, 0x65,
+        0x2c, 0x20, 0x73, 0x75, 0x6e, 0x73, 0x63, 0x72, 0x65, 0x65, 0x6e, 0x20, 0x77, 0x6f, 0x75,
+        0x6c, 0x64, 0x20, 0x62, 0x65, 0x20, 0x69, 0x74, 0x2e,
+    ];
+    let exp_cipher = vec![
+        0xd3, 0x1a, 0x8d, 0x34, 0x64, 0x8e, 0x60, 0xdb, 0x7b, 0x86, 0xaf, 0xbc, 0x53, 0xef, 0x7e,
+        0xc2, 0xa4, 0xad, 0xed, 0x51, 0x29, 0x6e, 0x08, 0xfe, 0xa9, 0xe2, 0xb5, 0xa7, 0x36, 0xee,
+        0x62, 0xd6, 0x3d, 0xbe, 0xa4, 0x5e, 0x8c, 0xa9, 0x67, 0x12, 0x82, 0xfa, 0xfb, 0x69, 0xda,
+        0x92, 0x72, 0x8b, 0x1a, 0x71, 0xde, 0x0a, 0x9e, 0x06, 0x0b, 0x29, 0x05, 0xd6, 0xa5, 0xb6,
+        0x7e, 0xcd, 0x3b, 0x36, 0x92, 0xdd, 0xbd, 0x7f, 0x2d, 0x77, 0x8b, 0x8c, 0x98, 0x03, 0xae,
+        0xe3, 0x28, 0x09, 0x1b, 0x58, 0xfa, 0xb3, 0x24, 0xe4, 0xfa, 0xd6, 0x75, 0x94, 0x55, 0x85,
+        0x80, 0x8b, 0x48, 0x31, 0xd7, 0xbc, 0x3f, 0xf4, 0xde, 0xf0, 0x8e, 0x4b, 0x7a, 0x9d, 0xe5,
+        0x76, 0xd2, 0x65, 0x86, 0xce, 0xc6, 0x4b, 0x61, 0x16,
+    ];
+    kat_test(m, key, iv, exp_cipher);
+
+    let key = [
+        0x8c, 0x4e, 0xfa, 0x63, 0x37, 0x96, 0x89, 0xd5, 0x90, 0xa8, 0xcb, 0xcf, 0xe1, 0x59, 0x42,
+        0xf8, 0xc1, 0xce, 0xe5, 0xaf, 0xa5, 0xf7, 0x52, 0xf7, 0xc3, 0xf0, 0x92, 0xa8, 0x41, 0x93,
+        0xa6, 0x89,
+    ];
+    let iv = [
+        0xbc, 0xf, 0x85, 0xee, 0x55, 0xa, 0x45, 0x6f, 0x16, 0xa7, 0x35, 0xb6,
+    ];
+    let m = vec![
+        204, 17, 211, 86, 205, 3, 143, 149, 232, 65, 249, 176, 134, 19, 51, 245, 33, 247, 187, 39,
+        120, 111, 226, 96, 68, 224, 250, 140, 18, 23, 174, 109, 149, 193, 10, 5, 167, 22, 19, 129,
+        17, 172, 51, 202, 186, 21, 6, 141, 39, 108, 186, 72, 39, 100, 193, 30, 104, 79, 48, 185,
+        169, 209, 200, 3, 13, 163, 231, 189, 171, 136, 188, 95, 55, 49, 109, 64, 186, 116, 233,
+        184, 56, 190, 71, 41, 250, 237, 235, 86, 23, 123, 226, 228, 35, 127, 176, 10, 49, 230, 129,
+        226, 237, 144, 29, 197, 161, 96, 129, 200, 66, 205, 187, 155, 34, 133, 250, 84, 14, 51,
+        242, 189, 46, 228, 61, 170, 192, 93, 214, 35, 206, 224, 157, 14, 249, 97, 40, 134, 103,
+        194, 168, 191, 159, 249, 127, 85, 83, 223, 166, 145, 98, 60, 85, 129, 209, 67, 119, 189,
+        67, 56, 55, 106, 48, 255, 198, 76, 192, 233, 56, 236, 98, 228, 219, 213, 206, 185, 25, 125,
+        189, 112, 160, 113, 183, 90, 71, 15, 80, 46, 143, 110, 112, 234, 214, 218, 24, 232, 196,
+        229, 62, 176, 17, 61, 92, 172, 224, 29, 225, 151, 141, 143, 126, 235, 195, 179, 186, 244,
+        250, 165, 106, 17, 255, 145, 27, 166, 250, 29, 149, 212, 55, 214, 158, 104, 82, 74, 246,
+        167, 216, 132, 218, 121, 4, 167, 73, 67, 145, 173, 245, 40, 158, 72, 71, 167, 53, 176, 27,
+        136, 165, 222, 115, 63, 241, 144, 198, 3, 81, 22, 58, 128, 38, 198, 100, 40, 36, 136, 194,
+        216, 150, 182, 94, 194, 235, 97, 212, 195, 112, 255, 158, 243, 154, 102, 56, 105, 25, 72,
+        80, 106, 123, 84, 162, 102, 161, 8, 58, 194, 160, 111, 247, 22, 129, 212, 140, 111, 80,
+        168, 203, 126, 222, 231, 82, 98, 63, 194, 253, 127, 127, 25, 208, 14, 252, 199, 107, 88,
+        38, 82, 57, 67, 13, 173, 208, 75, 182, 222, 89, 70, 27, 28, 21, 17, 97, 122, 184, 122, 27,
+        230, 219, 56, 135, 146, 204, 36, 211, 92, 113, 196, 121, 14, 212, 64, 211, 3, 122, 47, 217,
+        186, 209, 254, 221, 126, 172, 235, 198, 198, 52, 118, 19, 192, 150, 148, 224, 250, 173,
+        139, 121, 101, 231, 13, 101, 22, 168, 223, 118, 254, 161, 216, 110, 246, 67, 64, 249, 252,
+        55, 54, 95, 52, 72, 206, 68, 35, 36, 120, 52, 126, 233, 38, 3, 27, 11, 89, 242, 17, 168,
+        32, 197, 21, 121, 187, 77, 193, 107, 204, 151, 76, 187, 196, 162, 149, 93, 43, 39, 165,
+        171, 45, 154, 186, 89, 170, 11, 60, 119, 30, 183, 0, 29, 154, 114, 227, 77, 207, 140, 232,
+        18, 117, 3, 49, 229, 150, 125, 201, 100, 191, 44, 20, 35, 142, 216, 219, 38, 133, 166, 247,
+        26, 129, 69, 90, 140, 20, 70, 97, 49, 143, 7, 214, 61, 2, 65, 133, 36, 116, 140, 78, 68,
+        29, 138, 89, 83, 162, 117, 48, 52, 247, 108, 118, 183, 48, 125, 45, 53, 192, 235, 198, 30,
+        159, 113, 131, 182, 22, 185, 47, 174, 155, 179, 39, 235, 248, 188, 117, 181, 233, 8, 153,
+        224, 107, 115, 226, 77, 22, 38, 190, 143, 50, 151, 171, 80, 137, 229, 209, 131, 130, 232,
+        147, 142, 227, 225, 86, 56, 230, 12, 236, 180, 121, 119, 89, 55, 231, 158, 222, 131, 173,
+        255, 24, 41, 49, 196, 145, 137, 240, 71, 244, 165, 16, 84, 19, 218, 103, 26, 212, 221, 140,
+        154, 59, 87, 86, 254, 200, 81, 20, 250, 20, 173, 95, 33, 185, 106, 170, 39, 55, 249, 33,
+        192, 79, 5, 27, 92, 126, 245, 10, 215, 11, 43, 240, 120, 16, 167, 251, 80, 79, 16, 215,
+        154, 28, 131, 8, 121, 124, 189, 178, 190, 194, 246, 196, 35, 155, 36, 74, 175, 231, 78,
+        230, 212, 130, 13, 240, 137, 255, 103, 224, 163, 209, 164, 252, 7, 16, 205, 198, 155, 107,
+        255, 9, 26, 176, 69, 47, 58, 17, 198, 134, 241, 242, 2, 98, 48, 131, 58, 52, 122, 10, 96,
+        45, 39, 231, 146, 89, 207, 187, 96, 84, 207, 157, 89, 166, 169, 236, 140, 165, 205, 87,
+        111, 142, 142, 49, 12, 18, 218, 196, 168, 239, 111, 86, 192, 199, 237, 65, 91, 177, 113,
+        206, 133, 165, 51, 177, 49, 55, 127, 47, 14, 121, 250, 30, 107, 243, 99, 109, 195, 110, 62,
+        20, 112, 100, 205, 220, 51, 69, 151, 206, 114, 186, 6, 1, 243,
+    ];
+    let exp_cipher = vec![
+        223, 158, 69, 247, 207, 28, 32, 247, 233, 67, 87, 239, 80, 204, 82, 219, 90, 49, 36, 247,
+        188, 12, 201, 188, 19, 16, 249, 172, 149, 48, 185, 193, 205, 81, 162, 184, 194, 29, 198,
+        129, 72, 30, 148, 5, 127, 254, 175, 179, 229, 228, 26, 157, 127, 67, 88, 85, 240, 197, 250,
+        135, 43, 230, 0, 140, 178, 229, 204, 62, 247, 160, 98, 24, 192, 253, 194, 86, 162, 196,
+        216, 177, 7, 32, 220, 97, 252, 127, 236, 194, 131, 230, 229, 37, 222, 145, 142, 96, 87, 99,
+        206, 218, 149, 223, 164, 92, 65, 178, 73, 240, 146, 227, 168, 244, 163, 11, 237, 205, 132,
+        236, 150, 253, 140, 20, 232, 68, 177, 232, 224, 19, 254, 63, 58, 105, 53, 146, 164, 5, 151,
+        188, 55, 7, 39, 137, 12, 169, 49, 209, 20, 80, 199, 134, 31, 170, 254, 177, 67, 119, 216,
+        57, 170, 76, 37, 226, 93, 9, 65, 61, 62, 169, 67, 230, 241, 209, 164, 240, 81, 100, 13,
+        228, 24, 212, 86, 69, 48, 182, 160, 106, 151, 144, 173, 173, 173, 91, 155, 9, 156, 138,
+        182, 6, 211, 221, 221, 250, 148, 175, 189, 222, 79, 142, 31, 198, 146, 194, 4, 250, 19, 8,
+        5, 28, 15, 9, 95, 66, 122, 234, 138, 205, 107, 0, 202, 236, 143, 197, 126, 164, 77, 159,
+        172, 180, 144, 68, 211, 76, 146, 83, 92, 56, 68, 164, 0, 145, 243, 106, 71, 233, 182, 118,
+        138, 193, 179, 0, 249, 162, 210, 56, 157, 210, 161, 158, 129, 112, 82, 253, 98, 148, 70,
+        247, 93, 234, 218, 200, 137, 245, 191, 196, 157, 204, 239, 148, 253, 103, 98, 99, 28, 131,
+        78, 194, 122, 201, 171, 106, 20, 16, 150, 80, 138, 202, 29, 171, 173, 57, 98, 55, 49, 211,
+        99, 74, 160, 255, 83, 213, 55, 141, 22, 58, 121, 220, 86, 159, 148, 178, 220, 245, 243, 36,
+        53, 126, 31, 224, 188, 220, 133, 63, 99, 108, 103, 93, 134, 210, 57, 114, 228, 127, 226,
+        182, 106, 98, 113, 107, 131, 15, 222, 1, 129, 21, 169, 179, 168, 102, 42, 156, 92, 6, 237,
+        16, 13, 213, 75, 44, 155, 15, 86, 12, 148, 236, 168, 124, 131, 127, 59, 212, 145, 224, 46,
+        226, 170, 254, 210, 8, 237, 7, 247, 57, 146, 170, 220, 97, 24, 172, 34, 128, 233, 62, 238,
+        90, 249, 38, 244, 211, 95, 80, 57, 199, 75, 123, 130, 240, 89, 251, 58, 223, 205, 116, 105,
+        153, 116, 120, 165, 121, 140, 9, 191, 13, 247, 10, 236, 51, 65, 210, 243, 255, 234, 90,
+        254, 111, 15, 50, 91, 143, 221, 78, 248, 40, 232, 43, 255, 5, 160, 65, 77, 57, 36, 91, 77,
+        124, 50, 93, 70, 105, 195, 8, 248, 184, 204, 56, 173, 5, 131, 177, 162, 222, 103, 218, 194,
+        42, 227, 64, 3, 105, 74, 86, 47, 26, 164, 31, 71, 26, 234, 83, 51, 230, 27, 214, 78, 117,
+        248, 75, 226, 140, 181, 144, 74, 161, 201, 178, 243, 210, 157, 121, 176, 23, 156, 192, 126,
+        100, 121, 79, 0, 24, 100, 36, 116, 127, 226, 233, 240, 84, 197, 88, 107, 151, 105, 106, 64,
+        195, 79, 52, 168, 185, 30, 19, 98, 90, 213, 9, 202, 106, 46, 114, 58, 229, 84, 220, 105,
+        225, 65, 139, 175, 0, 250, 31, 76, 73, 33, 17, 245, 23, 213, 74, 255, 52, 148, 242, 217,
+        98, 67, 243, 59, 117, 103, 133, 119, 164, 4, 231, 1, 26, 6, 22, 157, 134, 104, 137, 49,
+        172, 89, 95, 137, 37, 141, 91, 14, 132, 109, 215, 214, 136, 224, 175, 40, 11, 31, 128, 67,
+        255, 29, 78, 70, 204, 36, 194, 16, 218, 200, 77, 150, 72, 167, 22, 47, 72, 199, 88, 109,
+        151, 177, 11, 114, 11, 176, 174, 20, 65, 182, 80, 28, 131, 39, 234, 181, 226, 169, 9, 154,
+        97, 248, 57, 91, 133, 52, 0, 75, 211, 171, 106, 84, 179, 14, 134, 13, 238, 157, 123, 36,
+        190, 69, 232, 85, 4, 125, 86, 69, 64, 230, 162, 139, 187, 189, 210, 58, 212, 74, 74, 122,
+        52, 61, 237, 152, 75, 38, 92, 222, 119, 138, 202, 98, 36, 20, 35, 50, 22, 234, 40, 206,
+        147, 146, 243, 204, 19, 44, 227, 82, 169, 91, 238, 179, 118, 18, 70, 166, 163, 30, 156,
+        191, 179, 183, 83, 252, 252, 238, 207, 70, 81, 219, 48, 86, 226, 243, 94, 179, 251, 22,
+        107, 146, 133, 165, 37, 138,
+    ];
+    kat_test(m, key, iv, exp_cipher);
+}
diff --git a/hmac-rust/Cargo.toml b/hmac-rust/Cargo.toml
new file mode 100644
index 0000000..308ce42
--- /dev/null
+++ b/hmac-rust/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "hmac"
+version = "0.1.0"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+edition = "2021"
+
+[lib]
+path = "src/hmac.rs"
+
+[dependencies]
+sha256 = { path = "../sha256-rust" }
+
+[dev-dependencies]
+hex = "0.4"
diff --git a/hmac-rust/out/Hmac.Hacspec_helper.fst b/hmac-rust/out/Hmac.Hacspec_helper.fst
new file mode 100644
index 0000000..99a5d7d
--- /dev/null
+++ b/hmac-rust/out/Hmac.Hacspec_helper.fst
@@ -0,0 +1,21 @@
+module Hmac.Hacspec_helper
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let xor_slice (this: Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t) (other: FStar.Seq.seq UInt8.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let _:Prims.l_False =
+    if Prims.l_Not (Alloc.Vec.len this = Core.Slice.len other)
+    then Core.Panicking.panic "assertion failed: this.len() == other.len()"
+  in
+  let this:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = Alloc.Vec.len this
+            }))
+      this
+      (fun i this -> this.[ i ] <- Hacspec_lib.^. this.[ i ] (Core.Ops.Index.index other i))
+  in
+  this
\ No newline at end of file
diff --git a/hmac-rust/out/Hmac.Hacspec_helper.v b/hmac-rust/out/Hmac.Hacspec_helper.v
new file mode 100644
index 0000000..de7476a
--- /dev/null
+++ b/hmac-rust/out/Hmac.Hacspec_helper.v
@@ -0,0 +1,9 @@
+(* 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.
+
+Definition xor_slice (this : Vec_t (int8) (Global_t)) (other : seq int8) : Vec_t (int8) (Global_t) :=
+  failure todo(term).
diff --git a/hmac-rust/out/Hmac.fst b/hmac-rust/out/Hmac.fst
new file mode 100644
index 0000000..fc7799f
--- /dev/null
+++ b/hmac-rust/out/Hmac.fst
@@ -0,0 +1,82 @@
+module Hmac
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+class hash (self: Type) = {
+  bLOCK_LEN:uint_size;
+  hASH_LEN:uint_size;
+  hash:FStar.Seq.seq UInt8.t -> Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t
+}
+
+type sha256_t = {  }
+
+let impl: Hash sha256_t =
+  {
+    bLOCK_LEN = (fun  -> 64);
+    hASH_LEN = (fun  -> 32);
+    hash
+    =
+    fun (bytes: FStar.Seq.seq UInt8.t) ->
+      Alloc.Slice.to_vec (Hacspec.Lib.unsize (Sha256.sha256 bytes))
+  }
+
+let o_pad
+      (#h: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __0: Core.Marker.sized_t h)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __1: hash_t h)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t = Alloc.Vec.from_elem 92uy Hmac.Hash.bLOCK_LEN
+
+let i_pad
+      (#h: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __0: Core.Marker.sized_t h)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __1: hash_t h)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t = Alloc.Vec.from_elem 54uy Hmac.Hash.bLOCK_LEN
+
+let k_block
+      (#h: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __0: Core.Marker.sized_t h)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __1: hash_t h)
+      (k: FStar.Seq.seq UInt8.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let k:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    if Prims.op_GreaterThanOrEqual (Core.Slice.len k) Hmac.Hash.bLOCK_LEN
+    then Hmac.Hash.hash k
+    else Alloc.Slice.to_vec k
+  in
+  let block:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Alloc.Vec.from_elem 0uy Hmac.Hash.bLOCK_LEN
+  in
+  let block:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = Alloc.Vec.len k
+            }))
+      block
+      (fun i block -> block.[ i ] <- k.[ i ])
+  in
+  block
+
+let hmac
+      (#h: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __0: Core.Marker.sized_t h)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] __1: hash_t h)
+      (k txt: FStar.Seq.seq UInt8.t)
+    : Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+  let k_block:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t = k_block k in
+  let h_in:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Hmac.Hacspec_helper.xor_slice (Core.Clone.Clone.clone k_block)
+      (Core.Ops.Deref.Deref.deref i_pad)
+  in
+  let h_in:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t = Alloc.Vec.extend_from_slice h_in txt in
+  let h_inner:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+    Sha256.hash (Core.Ops.Deref.Deref.deref h_in)
+  in
+  let h_in:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Hmac.Hacspec_helper.xor_slice k_block (Core.Ops.Deref.Deref.deref o_pad)
+  in
+  let h_in:Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t =
+    Alloc.Vec.extend_from_slice h_in (Hacspec.Lib.unsize h_inner)
+  in
+  Alloc.Slice.to_vec (Hacspec.Lib.unsize (Sha256.hash (Core.Ops.Deref.Deref.deref h_in)))
\ No newline at end of file
diff --git a/hmac-rust/out/Hmac.v b/hmac-rust/out/Hmac.v
new file mode 100644
index 0000000..f2719e1
--- /dev/null
+++ b/hmac-rust/out/Hmac.v
@@ -0,0 +1,56 @@
+(* 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.
+
+(*Not implemented yet? todo(item)*)
+
+Require Import Sha256.
+
+(*Not implemented yet? todo(item)*)
+
+Require Import Hacspec_helper.
+
+Class Hash Self := {
+  BLOCK_LEN:uint_size ;
+  HASH_LEN:uint_size ;
+  hash:seq int8 -> Vec_t (int8) (Global_t) ;
+}.
+
+Record Sha256_tSha256 : Type :={
+}.
+
+Instance Sha256_t_Hash : Hash Sha256_t := {
+  BLOCK_LEN := (@repr WORDSIZE32 64);
+  HASH_LEN := (@repr WORDSIZE32 32);
+  hash (bytes : seq int8) := to_vec (unsize (sha256 bytes));
+}.
+
+Definition o_pad : Vec_t (int8) (Global_t) :=
+  from_elem (@repr WORDSIZE8 92) BLOCK_LEN.
+
+Definition i_pad : Vec_t (int8) (Global_t) :=
+  from_elem (@repr WORDSIZE8 54) BLOCK_LEN.
+
+Definition k_block (k : seq int8) : Vec_t (int8) (Global_t) :=
+  let k := (if
+      (len k)>.?BLOCK_LEN
+    then
+      hash k
+    else
+      to_vec k) : Vec_t (int8) (Global_t) in
+  let block := (from_elem (@repr WORDSIZE8 0) BLOCK_LEN) : Vec_t (int8) (Global_t) in
+  let block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(len k))) block (fun i block =>
+      update_at block i (k.[i]))) : Vec_t (int8) (Global_t) in
+  block.
+
+Definition hmac (k : seq int8) (txt : seq int8) : Vec_t (int8) (Global_t) :=
+  let k_block := (k_block k) : Vec_t (int8) (Global_t) in
+  let h_in := (xor_slice (clone k_block) (deref i_pad)) : Vec_t (int8) (Global_t) in
+  let h_in := (extend_from_slice h_in txt) : Vec_t (int8) (Global_t) in
+  let h_inner := (hash (deref h_in)) : nseq int8 TODO: Int.to_string length in
+  let h_in := (xor_slice k_block (deref o_pad)) : Vec_t (int8) (Global_t) in
+  let h_in := (extend_from_slice h_in (unsize h_inner)) : Vec_t (int8) (Global_t) in
+  to_vec (unsize (hash (deref h_in))).
diff --git a/hmac-rust/out/Sha256.fst b/hmac-rust/out/Sha256.fst
new file mode 100644
index 0000000..8b3e500
--- /dev/null
+++ b/hmac-rust/out/Sha256.fst
@@ -0,0 +1,325 @@
+module Sha256
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let bLOCK_SIZE: uint_size = 64
+
+let lEN_SIZE: uint_size = 8
+
+let k_SIZE: uint_size = 64
+
+let hASH_SIZE: uint_size = Prims.op_Division 256 8
+
+let block = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}
+
+let opTableType = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}
+
+let sha256Digest = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}
+
+let roundConstantsTable =
+  x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}
+
+let hash = x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}
+
+let ch (x y z: UInt32.t) : UInt32.t =
+  Hacspec_lib.^. (Hacspec_lib.&. x y) (Hacspec_lib.&. (Prims.l_Not x) z)
+
+let maj (x y z: UInt32.t) : UInt32.t =
+  Hacspec_lib.^. (Hacspec_lib.&. x y) (Hacspec_lib.^. (Hacspec_lib.&. x z) (Hacspec_lib.&. y z))
+
+let oP_TABLE: x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12} =
+  [2uy; 13uy; 22uy; 6uy; 11uy; 25uy; 7uy; 18uy; 3uy; 17uy; 19uy; 10uy]
+
+let k_TABLE: x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  [
+    1116352408ul; 1899447441ul; 3049323471ul; 3921009573ul; 961987163ul; 1508970993ul; 2453635748ul;
+    2870763221ul; 3624381080ul; 310598401ul; 607225278ul; 1426881987ul; 1925078388ul; 2162078206ul;
+    2614888103ul; 3248222580ul; 3835390401ul; 4022224774ul; 264347078ul; 604807628ul; 770255983ul;
+    1249150122ul; 1555081692ul; 1996064986ul; 2554220882ul; 2821834349ul; 2952996808ul; 3210313671ul;
+    3336571891ul; 3584528711ul; 113926993ul; 338241895ul; 666307205ul; 773529912ul; 1294757372ul;
+    1396182291ul; 1695183700ul; 1986661051ul; 2177026350ul; 2456956037ul; 2730485921ul; 2820302411ul;
+    3259730800ul; 3345764771ul; 3516065817ul; 3600352804ul; 4094571909ul; 275423344ul; 430227734ul;
+    506948616ul; 659060556ul; 883997877ul; 958139571ul; 1322822218ul; 1537002063ul; 1747873779ul;
+    1955562222ul; 2024104815ul; 2227730452ul; 2361852424ul; 2428436474ul; 2756734187ul; 3204031479ul;
+    3329325298ul
+  ]
+
+let hASH_INIT: x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  [
+    1779033703ul;
+    3144134277ul;
+    1013904242ul;
+    2773480762ul;
+    1359893119ul;
+    2600822924ul;
+    528734635ul;
+    1541459225ul
+  ]
+
+let sigma (x: UInt32.t) (i op: uint_size) : UInt32.t =
+  let (tmp: UInt32.t):UInt32.t =
+    Core.Num.rotate_right x (Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i + 2)))
+  in
+  let tmp:UInt32.t =
+    if op = 0 then Hacspec_lib.>>. x (Core.Ops.Index.index oP_TABLE (3 * i + 2)) else tmp
+  in
+  let rot_val_1:UInt32.t = Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i)) in
+  let rot_val_2:UInt32.t = Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i + 1)) in
+  Hacspec_lib.^. (Hacspec_lib.^. (Core.Num.rotate_right x rot_val_1)
+        (Core.Num.rotate_right x rot_val_2))
+    tmp
+
+let to_be_u32s
+      (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+    : Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+  let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+    Alloc.Vec.with_capacity (Prims.op_Division bLOCK_SIZE 4)
+  in
+  let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks (Hacspec.Lib.unsize
+                  block)
+              4))
+      out
+      (fun block_chunk out ->
+          let block_chunk_array:UInt32.t =
+            Core.Num.from_be_bytes (Core.Result.unwrap (Core.Convert.TryInto.try_into block_chunk))
+          in
+          let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+            Alloc.Vec.push out block_chunk_array
+          in
+          out)
+  in
+  out
+
+let schedule (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let b:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t = to_be_u32s block in
+  let s:Alloc.Boxed.box_t
+    (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0ul 64
+  in
+  let s:x: Prims.list UInt32.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 = k_SIZE
+            }))
+      s
+      (fun i s ->
+          if Prims.op_LessThan i 16
+          then
+            let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+              s.[ i ] <- b.[ i ]
+            in
+            s
+          else
+            let t16:UInt32.t = Core.Ops.Index.index s (i - 16) in
+            let t15:UInt32.t = Core.Ops.Index.index s (i - 15) in
+            let t7:UInt32.t = Core.Ops.Index.index s (i - 7) in
+            let t2:UInt32.t = Core.Ops.Index.index s (i - 2) in
+            let s1:UInt32.t = sigma t2 3 0 in
+            let s0:UInt32.t = sigma t15 2 0 in
+            let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+              s.[ i ] <-
+                Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add s1 t7) s0) t16
+            in
+            s)
+  in
+  s
+
+let shuffle
+      (ws: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+      (hashi: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} = hashi in
+  let h: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 = k_SIZE
+            }))
+      h
+      (fun i h ->
+          let a0:UInt32.t = Core.Ops.Index.index h 0 in
+          let b0:UInt32.t = Core.Ops.Index.index h 1 in
+          let c0:UInt32.t = Core.Ops.Index.index h 2 in
+          let d0:UInt32.t = Core.Ops.Index.index h 3 in
+          let e0:UInt32.t = Core.Ops.Index.index h 4 in
+          let f0:UInt32.t = Core.Ops.Index.index h 5 in
+          let g0:UInt32.t = Core.Ops.Index.index h 6 in
+          let (h0: UInt32.t):UInt32.t = Core.Ops.Index.index h 7 in
+          let t1:UInt32.t =
+            Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add
+                          h0
+                          (sigma e0 1 1))
+                      (ch e0 f0 g0))
+                  (Core.Ops.Index.index k_TABLE i))
+              (Core.Ops.Index.index ws i)
+          in
+          let t2:UInt32.t = Core.Num.wrapping_add (sigma a0 0 1) (maj a0 b0 c0) in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 0 ] <- Core.Num.wrapping_add t1 t2
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 1 ] <- a0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 2 ] <- b0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 3 ] <- c0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 4 ] <- Core.Num.wrapping_add d0 t1
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 5 ] <- e0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 6 ] <- f0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 7 ] <- g0
+          in
+          h)
+  in
+  h
+
+let compress
+      (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+      (h_in: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    schedule block
+  in
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    shuffle s h_in
+  in
+  let h: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 }
+          ))
+      h
+      (fun i h ->
+          h.[ i ] <- Core.Num.wrapping_add (Core.Ops.Index.index h i) (Core.Ops.Index.index h_in i))
+  in
+  h
+
+let u32s_to_be_bytes
+      (state: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+  let (out: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32})):Alloc.Boxed.box_t
+    (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0uy 32
+  in
+  let out:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = lEN_SIZE
+            }))
+      out
+      (fun i out ->
+          let tmp:UInt32.t = Core.Ops.Index.index state i in
+          let tmp:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 4} =
+            Core.Num.to_be_bytes tmp
+          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 hash (msg: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} = hASH_INIT in
+  let (last_block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})):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 last_block_len:uint_size = 0 in
+  let h, last_block, last_block_len:(x:
+    Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} &
+    x:
+    Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} &
+    uint_size) =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks msg
+              bLOCK_SIZE))
+      (h, last_block, last_block_len)
+      (fun block (h, last_block, last_block_len) ->
+          if Prims.op_LessThan (Core.Slice.len block) bLOCK_SIZE
+          then
+            let last_block: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 block
+                      }))
+                last_block
+                (fun i last_block -> last_block.[ i ] <- Core.Ops.Index.index block i)
+            in
+            let last_block_len:uint_size = Core.Slice.len block in
+            h, last_block, last_block_len
+          else
+            let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+              compress (Core.Result.unwrap (Core.Convert.TryInto.try_into block)) h
+            in
+            h, last_block, last_block_len)
+  in
+  let last_block:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    last_block.[ last_block_len ] <- 128uy
+  in
+  let len_bist:UInt64.t = cast (Core.Slice.len msg * 8) in
+  let len_bist_bytes:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    Core.Num.to_be_bytes len_bist
+  in
+  let h, last_block:(x:
+    Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} &
+    x:
+    Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}) =
+    if Prims.op_LessThan last_block_len (bLOCK_SIZE - lEN_SIZE)
+    then
+      let last_block: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 = lEN_SIZE
+                }))
+          last_block
+          (fun i last_block ->
+              last_block.[ bLOCK_SIZE - lEN_SIZE + i ] <- Core.Ops.Index.index len_bist_bytes i)
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress last_block h
+      in
+      h, last_block
+    else
+      let (pad_block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})):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 pad_block: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 = lEN_SIZE
+                }))
+          pad_block
+          (fun i pad_block ->
+              pad_block.[ bLOCK_SIZE - lEN_SIZE + i ] <- Core.Ops.Index.index len_bist_bytes i)
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress last_block h
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress pad_block h
+      in
+      h, last_block
+  in
+  u32s_to_be_bytes h
+
+let sha256 (msg: FStar.Seq.seq UInt8.t)
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} = hash msg
\ No newline at end of file
diff --git a/hmac-rust/out/Sha256.v b/hmac-rust/out/Sha256.v
new file mode 100644
index 0000000..21310df
--- /dev/null
+++ b/hmac-rust/out/Sha256.v
@@ -0,0 +1,245 @@
+(* 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.
+
+(*Not implemented yet? todo(item)*)
+
+Require Import Std. (* as TryInto *)
+
+Definition BLOCK_SIZE : uint_size :=
+  (@repr WORDSIZE32 64).
+
+Definition LEN_SIZE : uint_size :=
+  (@repr WORDSIZE32 8).
+
+Definition K_SIZE : uint_size :=
+  (@repr WORDSIZE32 64).
+
+Definition HASH_SIZE : uint_size :=
+  (@repr WORDSIZE32 256)./(@repr WORDSIZE32 8).
+
+Notation Block_t := (nseq int8 TODO: Int.to_string length).
+
+Notation OpTableType_t := (nseq int8 TODO: Int.to_string length).
+
+Notation Sha256Digest_t := (nseq int8 TODO: Int.to_string length).
+
+Notation RoundConstantsTable_t := (nseq int32 TODO: Int.to_string length).
+
+Notation Hash_t := (nseq int32 TODO: Int.to_string length).
+
+Definition ch (x : int32) (y : int32) (z : int32) : int32 :=
+  (x.&y).^(((TODO: UnOp) x).&z).
+
+Definition maj (x : int32) (y : int32) (z : int32) : int32 :=
+  (x.&y).^((x.&z).^(y.&z)).
+
+Definition OP_TABLE : nseq int8 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE8 2);
+    (@repr WORDSIZE8 13);
+    (@repr WORDSIZE8 22);
+    (@repr WORDSIZE8 6);
+    (@repr WORDSIZE8 11);
+    (@repr WORDSIZE8 25);
+    (@repr WORDSIZE8 7);
+    (@repr WORDSIZE8 18);
+    (@repr WORDSIZE8 3);
+    (@repr WORDSIZE8 17);
+    (@repr WORDSIZE8 19);
+    (@repr WORDSIZE8 10)].
+
+Definition K_TABLE : nseq int32 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE32 1116352408);
+    (@repr WORDSIZE32 1899447441);
+    (@repr WORDSIZE32 3049323471);
+    (@repr WORDSIZE32 3921009573);
+    (@repr WORDSIZE32 961987163);
+    (@repr WORDSIZE32 1508970993);
+    (@repr WORDSIZE32 2453635748);
+    (@repr WORDSIZE32 2870763221);
+    (@repr WORDSIZE32 3624381080);
+    (@repr WORDSIZE32 310598401);
+    (@repr WORDSIZE32 607225278);
+    (@repr WORDSIZE32 1426881987);
+    (@repr WORDSIZE32 1925078388);
+    (@repr WORDSIZE32 2162078206);
+    (@repr WORDSIZE32 2614888103);
+    (@repr WORDSIZE32 3248222580);
+    (@repr WORDSIZE32 3835390401);
+    (@repr WORDSIZE32 4022224774);
+    (@repr WORDSIZE32 264347078);
+    (@repr WORDSIZE32 604807628);
+    (@repr WORDSIZE32 770255983);
+    (@repr WORDSIZE32 1249150122);
+    (@repr WORDSIZE32 1555081692);
+    (@repr WORDSIZE32 1996064986);
+    (@repr WORDSIZE32 2554220882);
+    (@repr WORDSIZE32 2821834349);
+    (@repr WORDSIZE32 2952996808);
+    (@repr WORDSIZE32 3210313671);
+    (@repr WORDSIZE32 3336571891);
+    (@repr WORDSIZE32 3584528711);
+    (@repr WORDSIZE32 113926993);
+    (@repr WORDSIZE32 338241895);
+    (@repr WORDSIZE32 666307205);
+    (@repr WORDSIZE32 773529912);
+    (@repr WORDSIZE32 1294757372);
+    (@repr WORDSIZE32 1396182291);
+    (@repr WORDSIZE32 1695183700);
+    (@repr WORDSIZE32 1986661051);
+    (@repr WORDSIZE32 2177026350);
+    (@repr WORDSIZE32 2456956037);
+    (@repr WORDSIZE32 2730485921);
+    (@repr WORDSIZE32 2820302411);
+    (@repr WORDSIZE32 3259730800);
+    (@repr WORDSIZE32 3345764771);
+    (@repr WORDSIZE32 3516065817);
+    (@repr WORDSIZE32 3600352804);
+    (@repr WORDSIZE32 4094571909);
+    (@repr WORDSIZE32 275423344);
+    (@repr WORDSIZE32 430227734);
+    (@repr WORDSIZE32 506948616);
+    (@repr WORDSIZE32 659060556);
+    (@repr WORDSIZE32 883997877);
+    (@repr WORDSIZE32 958139571);
+    (@repr WORDSIZE32 1322822218);
+    (@repr WORDSIZE32 1537002063);
+    (@repr WORDSIZE32 1747873779);
+    (@repr WORDSIZE32 1955562222);
+    (@repr WORDSIZE32 2024104815);
+    (@repr WORDSIZE32 2227730452);
+    (@repr WORDSIZE32 2361852424);
+    (@repr WORDSIZE32 2428436474);
+    (@repr WORDSIZE32 2756734187);
+    (@repr WORDSIZE32 3204031479);
+    (@repr WORDSIZE32 3329325298)].
+
+Definition HASH_INIT : nseq int32 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE32 1779033703);
+    (@repr WORDSIZE32 3144134277);
+    (@repr WORDSIZE32 1013904242);
+    (@repr WORDSIZE32 2773480762);
+    (@repr WORDSIZE32 1359893119);
+    (@repr WORDSIZE32 2600822924);
+    (@repr WORDSIZE32 528734635);
+    (@repr WORDSIZE32 1541459225)].
+
+Definition sigma (x : int32) (i : uint_size) (op : uint_size) : int32 :=
+  let tmp := (rotate_right x (into (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 2))))) : int32 in
+  let tmp := (if
+      op=.?(@repr WORDSIZE32 0)
+    then
+      x shift_right (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 2)))
+    else
+      tmp) : int32 in
+  let rot_val_1 := (into (index OP_TABLE ((@repr WORDSIZE32 3).*i))) : int32 in
+  let rot_val_2 := (into (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 1)))) : int32 in
+  ((rotate_right x rot_val_1).^(rotate_right x rot_val_2)).^tmp.
+
+Definition to_be_u32s (block : nseq int8 TODO: Int.to_string length) : Vec_t (int32) (Global_t) :=
+  let out := (with_capacity (BLOCK_SIZE./(@repr WORDSIZE32 4))) : Vec_t (int32) (Global_t) in
+  let out := (fold (into_iter (chunks (unsize block) (@repr WORDSIZE32 4))) out (fun block_chunk out =>
+      let block_chunk_array := (from_be_bytes (unwrap (try_into block_chunk))) : int32 in
+      let out := (push out block_chunk_array) : Vec_t (int32) (Global_t) in
+      out)) : Vec_t (int32) (Global_t) in
+  out.
+
+Definition schedule (block : nseq int8 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let b := (to_be_u32s block) : Vec_t (int32) (Global_t) in
+  let s := (repeat (@repr WORDSIZE32 0) (@repr WORDSIZE32 64)) : Box_t (nseq int32 TODO: Int.to_string length) (Global_t) in
+  let s := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)K_SIZE)) s (fun i s =>
+      if
+        i<.?(@repr WORDSIZE32 16)
+      then
+        let s := (update_at s i (b.[i])) : nseq int32 TODO: Int.to_string length in
+        s
+      else
+        let t16 := (index s (i.-(@repr WORDSIZE32 16))) : int32 in
+        let t15 := (index s (i.-(@repr WORDSIZE32 15))) : int32 in
+        let t7 := (index s (i.-(@repr WORDSIZE32 7))) : int32 in
+        let t2 := (index s (i.-(@repr WORDSIZE32 2))) : int32 in
+        let s1 := (sigma t2 (@repr WORDSIZE32 3) (@repr WORDSIZE32 0)) : int32 in
+        let s0 := (sigma t15 (@repr WORDSIZE32 2) (@repr WORDSIZE32 0)) : int32 in
+        let s := (update_at s i (wrapping_add (wrapping_add (wrapping_add s1 t7) s0) t16)) : nseq int32 TODO: Int.to_string length in
+        s)) : nseq int32 TODO: Int.to_string length in
+  s.
+
+Definition shuffle (ws : nseq int32 TODO: Int.to_string length) (hashi : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let h := (hashi) : nseq int32 TODO: Int.to_string length in
+  let h := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)K_SIZE)) h (fun i h =>
+      let a0 := (index h (@repr WORDSIZE32 0)) : int32 in
+      let b0 := (index h (@repr WORDSIZE32 1)) : int32 in
+      let c0 := (index h (@repr WORDSIZE32 2)) : int32 in
+      let d0 := (index h (@repr WORDSIZE32 3)) : int32 in
+      let e0 := (index h (@repr WORDSIZE32 4)) : int32 in
+      let f0 := (index h (@repr WORDSIZE32 5)) : int32 in
+      let g0 := (index h (@repr WORDSIZE32 6)) : int32 in
+      let h0 := (index h (@repr WORDSIZE32 7)) : int32 in
+      let t1 := (wrapping_add (wrapping_add (wrapping_add (wrapping_add h0 (sigma e0 (@repr WORDSIZE32 1) (@repr WORDSIZE32 1))) (ch e0 f0 g0)) (index K_TABLE i)) (index ws i)) : int32 in
+      let t2 := (wrapping_add (sigma a0 (@repr WORDSIZE32 0) (@repr WORDSIZE32 1)) (maj a0 b0 c0)) : int32 in
+      let h := (update_at h (@repr WORDSIZE32 0) (wrapping_add t1 t2)) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 1) a0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 2) b0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 3) c0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 4) (wrapping_add d0 t1)) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 5) e0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 6) f0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 7) g0) : nseq int32 TODO: Int.to_string length in
+      h)) : nseq int32 TODO: Int.to_string length in
+  h.
+
+Definition compress (block : nseq int8 TODO: Int.to_string length) (h_in : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let s := (schedule block) : nseq int32 TODO: Int.to_string length in
+  let h := (shuffle s h_in) : nseq int32 TODO: Int.to_string length in
+  let h := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 8))) h (fun i h =>
+      update_at h i (wrapping_add (index h i) (index h_in i)))) : nseq int32 TODO: Int.to_string length in
+  h.
+
+Definition u32s_to_be_bytes (state : nseq int32 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let out := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 32)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let out := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) out (fun i out =>
+      let tmp := (index state i) : int32 in
+      let tmp := (to_be_bytes tmp) : 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 hash (msg : seq int8) : nseq int8 TODO: Int.to_string length :=
+  let h := (HASH_INIT) : nseq int32 TODO: Int.to_string length in
+  let last_block := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let last_block_len := ((@repr WORDSIZE32 0)) : uint_size in
+  let '(h,last_block,last_block_len) := (fold (into_iter (chunks msg BLOCK_SIZE)) (h,last_block,last_block_len) (fun block '(h,last_block,last_block_len) =>
+      if
+        (len block)<.?BLOCK_SIZE
+      then
+        let last_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(len block))) last_block (fun i last_block =>
+            update_at last_block i (index block i))) : nseq int8 TODO: Int.to_string length in
+        let last_block_len := (len block) : uint_size in
+        (h,last_block,last_block_len)
+      else
+        let h := (compress (unwrap (try_into block)) h) : nseq int32 TODO: Int.to_string length in
+        (h,last_block,last_block_len))) : (nseq int32 TODO: Int.to_string length × nseq int8 TODO: Int.to_string length × uint_size) in
+  let last_block := (update_at last_block last_block_len (@repr WORDSIZE8 128)) : nseq int8 TODO: Int.to_string length in
+  let len_bist := (cast ((len msg).*(@repr WORDSIZE32 8))) : int64 in
+  let len_bist_bytes := (to_be_bytes len_bist) : nseq int8 TODO: Int.to_string length in
+  let '(h,last_block) := (if
+      last_block_len<.?(BLOCK_SIZE.-LEN_SIZE)
+    then
+      let last_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) last_block (fun i last_block =>
+          update_at last_block ((BLOCK_SIZE.-LEN_SIZE).+i) (index len_bist_bytes i))) : nseq int8 TODO: Int.to_string length in
+      let h := (compress last_block h) : nseq int32 TODO: Int.to_string length in
+      (h,last_block)
+    else
+      let pad_block := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+      let pad_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) pad_block (fun i pad_block =>
+          update_at pad_block ((BLOCK_SIZE.-LEN_SIZE).+i) (index len_bist_bytes i))) : nseq int8 TODO: Int.to_string length in
+      let h := (compress last_block h) : nseq int32 TODO: Int.to_string length in
+      let h := (compress pad_block h) : nseq int32 TODO: Int.to_string length in
+      (h,last_block)) : (nseq int32 TODO: Int.to_string length × nseq int8 TODO: Int.to_string length) in
+  u32s_to_be_bytes h.
+
+Definition sha256 (msg : seq int8) : nseq int8 TODO: Int.to_string length :=
+  hash msg.
diff --git a/hmac-rust/src/hacspec_helper.rs b/hmac-rust/src/hacspec_helper.rs
new file mode 100644
index 0000000..ecceca6
--- /dev/null
+++ b/hmac-rust/src/hacspec_helper.rs
@@ -0,0 +1,16 @@
+pub(super) fn xor_slice(mut this: Vec<u8>, other: &[u8]) -> Vec<u8> {
+    assert!(this.len() == other.len());
+
+    // error[CE0008]: (Diagnostics.Context.Phase (Reject ArbitraryLhs)): ExplicitRejection { reason: "unknown reason" }
+    //  --> hmac-rust/src/hacspec_helper.rs:5:9
+    //   |
+    // 5 |         *x = *x ^ *o;
+    //   |
+    // for (x, o) in this.iter_mut().zip(other.iter()) {
+    //     *x = *x ^ *o;
+    // }
+    for i in 0..this.len() {
+        this[i] = this[i] ^ other[i];
+    }
+    this
+}
diff --git a/hmac-rust/src/hmac.rs b/hmac-rust/src/hmac.rs
new file mode 100644
index 0000000..c8f0e10
--- /dev/null
+++ b/hmac-rust/src/hmac.rs
@@ -0,0 +1,63 @@
+use sha256::*;
+
+mod hacspec_helper;
+use hacspec_helper::*;
+
+/// Hash trait
+pub trait Hash {
+    const BLOCK_LEN: usize;
+    const HASH_LEN: usize;
+
+    fn hash(bytes: &[u8]) -> Vec<u8>;
+}
+
+/// SHA 256 struct for the [`Hash`] trait.
+pub struct Sha256 {}
+
+impl Hash for Sha256 {
+    const BLOCK_LEN: usize = 64;
+    const HASH_LEN: usize = 32;
+
+    fn hash(bytes: &[u8]) -> Vec<u8> {
+        sha256::sha256(bytes).to_vec()
+    }
+}
+
+// === HMAC ===
+
+fn o_pad<H: Hash>() -> Vec<u8> {
+    vec![0x5c; H::BLOCK_LEN]
+}
+
+fn i_pad<H: Hash>() -> Vec<u8> {
+    vec![0x36; H::BLOCK_LEN]
+}
+
+fn k_block<H: Hash>(k: &[u8]) -> Vec<u8> {
+    let k = if k.len() > H::BLOCK_LEN {
+        H::hash(k)
+    } else {
+        k.to_vec()
+    };
+    let mut block = vec![0u8; H::BLOCK_LEN];
+    for i in 0..k.len() {
+        block[i] = k[i];
+    }
+    block
+}
+
+// H(K XOR opad, H(K XOR ipad, text))
+pub fn hmac<H: Hash>(k: &[u8], txt: &[u8]) -> Vec<u8> {
+    // Applications that use keys longer than B bytes will first hash the key
+    // using H and then use the resultant L byte string as the actual key to HMAC
+    let k_block = k_block::<H>(k);
+
+    let mut h_in = xor_slice(k_block.clone(), &i_pad::<H>());
+    h_in.extend_from_slice(txt);
+    let h_inner = hash(&h_in);
+
+    let mut h_in = xor_slice(k_block, &o_pad::<H>());
+    h_in.extend_from_slice(&h_inner);
+
+    hash(&h_in).to_vec()
+}
diff --git a/hmac-rust/tests/test_hmac.rs b/hmac-rust/tests/test_hmac.rs
new file mode 100644
index 0000000..d7a5274
--- /dev/null
+++ b/hmac-rust/tests/test_hmac.rs
@@ -0,0 +1,47 @@
+use hmac::*;
+
+struct HMACTestVectors<'a> {
+    key: &'a str,
+    txt: &'a str,
+    expected: &'a str,
+}
+
+// https://tools.ietf.org/html/rfc4231
+const HMAC_KAT: [HMACTestVectors; 5] = [
+    HMACTestVectors {
+        key: "0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b",
+        txt: "4869205468657265",
+        expected: "b0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7",
+    },
+    HMACTestVectors {
+        key: "4a656665",
+        txt: "7768617420646f2079612077616e7420666f72206e6f7468696e673f",
+        expected: "5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843",
+    },
+    HMACTestVectors {
+        key: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
+        txt: "dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd",
+        expected: "773ea91e36800e46854db8ebd09181a72959098b3ef8c122d9635514ced565fe",
+    },
+    HMACTestVectors {
+        key: "0102030405060708090a0b0c0d0e0f10111213141516171819",
+        txt: "cdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcd",
+        expected: "82558a389a443c0ea4cc819899f2083a85f0faa3e578f8077a2e3ff46729665b",
+    },
+    HMACTestVectors {
+        key: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
+        txt: "54657374205573696e67204c6172676572205468616e20426c6f636b2d53697a65204b6579202d2048617368204b6579204669727374",
+        expected: "60e431591ee0b67f0d8a26aacbf5b77f8e0bc6213728c5140546040f0ee37f54",
+    }
+];
+
+#[test]
+fn test_hmac_kat() {
+    for kat in HMAC_KAT.iter() {
+        let hmac = hmac::<hmac::Sha256>(
+            &hex::decode(kat.key).unwrap(),
+            &hex::decode(kat.txt).unwrap(),
+        );
+        assert_eq!(hex::decode(kat.expected).unwrap(), hmac);
+    }
+}
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
deleted file mode 100644
index 0a765b4..0000000
--- a/rust-toolchain.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[toolchain]
-channel = "nightly-2022-12-06"
-components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]
diff --git a/sha256-rust/.gitignore b/sha256-rust/.gitignore
new file mode 100644
index 0000000..2c96eb1
--- /dev/null
+++ b/sha256-rust/.gitignore
@@ -0,0 +1,2 @@
+target/
+Cargo.lock
diff --git a/sha256-rust/Cargo.toml b/sha256-rust/Cargo.toml
new file mode 100644
index 0000000..94fc74c
--- /dev/null
+++ b/sha256-rust/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "sha256"
+version = "0.1.0"
+authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
+edition = "2021"
+
+[lib]
+path = "src/sha256.rs"
+
+[dependencies]
diff --git a/sha256-rust/out/Sha256.fst b/sha256-rust/out/Sha256.fst
new file mode 100644
index 0000000..d9909fd
--- /dev/null
+++ b/sha256-rust/out/Sha256.fst
@@ -0,0 +1,326 @@
+module Sha256
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open FStar.Mul
+open Hacspec.Lib
+open Hacspec_lib_tc
+
+let bLOCK_SIZE: uint_size = 64
+
+let lEN_SIZE: uint_size = 8
+
+let k_SIZE: uint_size = 64
+
+let hASH_SIZE: uint_size = Prims.op_Division 256 8
+
+let block = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}
+
+let opTableType = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12}
+
+let sha256Digest = x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32}
+
+let roundConstantsTable =
+  x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}
+
+let hash = x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}
+
+let ch (x y z: UInt32.t) : UInt32.t =
+  Hacspec_lib.^. (Hacspec_lib.&. x y) (Hacspec_lib.&. (Prims.l_Not x) z)
+
+let maj (x y z: UInt32.t) : UInt32.t =
+  Hacspec_lib.^. (Hacspec_lib.&. x y) (Hacspec_lib.^. (Hacspec_lib.&. x z) (Hacspec_lib.&. y z))
+
+let oP_TABLE: x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 12} =
+  [2uy; 13uy; 22uy; 6uy; 11uy; 25uy; 7uy; 18uy; 3uy; 17uy; 19uy; 10uy]
+
+let k_TABLE: x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  [
+    1116352408ul; 1899447441ul; 3049323471ul; 3921009573ul; 961987163ul; 1508970993ul; 2453635748ul;
+    2870763221ul; 3624381080ul; 310598401ul; 607225278ul; 1426881987ul; 1925078388ul; 2162078206ul;
+    2614888103ul; 3248222580ul; 3835390401ul; 4022224774ul; 264347078ul; 604807628ul; 770255983ul;
+    1249150122ul; 1555081692ul; 1996064986ul; 2554220882ul; 2821834349ul; 2952996808ul; 3210313671ul;
+    3336571891ul; 3584528711ul; 113926993ul; 338241895ul; 666307205ul; 773529912ul; 1294757372ul;
+    1396182291ul; 1695183700ul; 1986661051ul; 2177026350ul; 2456956037ul; 2730485921ul; 2820302411ul;
+    3259730800ul; 3345764771ul; 3516065817ul; 3600352804ul; 4094571909ul; 275423344ul; 430227734ul;
+    506948616ul; 659060556ul; 883997877ul; 958139571ul; 1322822218ul; 1537002063ul; 1747873779ul;
+    1955562222ul; 2024104815ul; 2227730452ul; 2361852424ul; 2428436474ul; 2756734187ul; 3204031479ul;
+    3329325298ul
+  ]
+
+let hASH_INIT: x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  [
+    1779033703ul;
+    3144134277ul;
+    1013904242ul;
+    2773480762ul;
+    1359893119ul;
+    2600822924ul;
+    528734635ul;
+    1541459225ul
+  ]
+
+let sigma (x: UInt32.t) (i op: uint_size) : UInt32.t =
+  let (tmp: UInt32.t):UInt32.t =
+    Core.Num.rotate_right x (Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i + 2)))
+  in
+  let tmp:UInt32.t =
+    if op = 0 then Hacspec_lib.>>. x (Core.Ops.Index.index oP_TABLE (3 * i + 2)) else tmp
+  in
+  let rot_val_1:UInt32.t = Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i)) in
+  let rot_val_2:UInt32.t = Core.Convert.Into.into (Core.Ops.Index.index oP_TABLE (3 * i + 1)) in
+  Hacspec_lib.^. (Hacspec_lib.^. (Core.Num.rotate_right x rot_val_1)
+        (Core.Num.rotate_right x rot_val_2))
+    tmp
+
+let to_be_u32s
+      (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+    : Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+  let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+    Alloc.Vec.with_capacity (Prims.op_Division bLOCK_SIZE 4)
+  in
+  let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks (Hacspec.Lib.unsize
+                  block)
+              4))
+      out
+      (fun block_chunk out ->
+          let block_chunk_array:UInt32.t =
+            Core.Num.from_be_bytes (Core.Result.unwrap (Core.Convert.TryInto.try_into block_chunk))
+          in
+          let out:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t =
+            Alloc.Vec.push out block_chunk_array
+          in
+          out)
+  in
+  out
+
+let schedule (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+  let b:Alloc.Vec.vec_t UInt32.t Alloc.Alloc.global_t = to_be_u32s block in
+  let s:Alloc.Boxed.box_t
+    (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0ul 64
+  in
+  let s:x: Prims.list UInt32.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 = k_SIZE
+            }))
+      s
+      (fun i s ->
+          if Prims.op_LessThan i 16
+          then
+            let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+              s.[ i ] <- b.[ i ]
+            in
+            s
+          else
+            let t16:UInt32.t = Core.Ops.Index.index s (i - 16) in
+            let t15:UInt32.t = Core.Ops.Index.index s (i - 15) in
+            let t7:UInt32.t = Core.Ops.Index.index s (i - 7) in
+            let t2:UInt32.t = Core.Ops.Index.index s (i - 2) in
+            let s1:UInt32.t = sigma t2 3 0 in
+            let s0:UInt32.t = sigma t15 2 0 in
+            let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+              s.[ i ] <-
+                Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add s1 t7) s0) t16
+            in
+            s)
+  in
+  s
+
+let shuffle
+      (ws: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+      (hashi: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} = hashi in
+  let h: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 = k_SIZE
+            }))
+      h
+      (fun i h ->
+          let a0:UInt32.t = Core.Ops.Index.index h 0 in
+          let b0:UInt32.t = Core.Ops.Index.index h 1 in
+          let c0:UInt32.t = Core.Ops.Index.index h 2 in
+          let d0:UInt32.t = Core.Ops.Index.index h 3 in
+          let e0:UInt32.t = Core.Ops.Index.index h 4 in
+          let f0:UInt32.t = Core.Ops.Index.index h 5 in
+          let g0:UInt32.t = Core.Ops.Index.index h 6 in
+          let (h0: UInt32.t):UInt32.t = Core.Ops.Index.index h 7 in
+          let t1:UInt32.t =
+            Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add (Core.Num.wrapping_add
+                          h0
+                          (sigma e0 1 1))
+                      (ch e0 f0 g0))
+                  (Core.Ops.Index.index k_TABLE i))
+              (Core.Ops.Index.index ws i)
+          in
+          let t2:UInt32.t = Core.Num.wrapping_add (sigma a0 0 1) (maj a0 b0 c0) in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 0 ] <- Core.Num.wrapping_add t1 t2
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 1 ] <- a0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 2 ] <- b0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 3 ] <- c0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 4 ] <- Core.Num.wrapping_add d0 t1
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 5 ] <- e0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 6 ] <- f0
+          in
+          let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+            h.[ 7 ] <- g0
+          in
+          h)
+  in
+  h
+
+let compress
+      (block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}))
+      (h_in: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+  let s:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    schedule block
+  in
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    shuffle s h_in
+  in
+  let h: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 }
+          ))
+      h
+      (fun i h ->
+          h.[ i ] <- Core.Num.wrapping_add (Core.Ops.Index.index h i) (Core.Ops.Index.index h_in i))
+  in
+  h
+
+let u32s_to_be_bytes
+      (state: (x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8}))
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+  let (out: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32})):Alloc.Boxed.box_t
+    (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32})
+    Alloc.Alloc.global_t =
+    Hacspec.Lib.repeat 0uy 32
+  in
+  let out:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
+              start = 0;
+              end = lEN_SIZE
+            }))
+      out
+      (fun i out ->
+          let tmp:UInt32.t = Core.Ops.Index.index state i in
+          let tmp:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 4} =
+            Core.Num.to_be_bytes tmp
+          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 hash (msg: Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t)
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} =
+  let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} = hASH_INIT in
+  let (last_block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})):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 last_block_len:uint_size = 0 in
+  let h, last_block, last_block_len:(x:
+    Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} &
+    x:
+    Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} &
+    uint_size) =
+    Core.Iter.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks (Core.Ops.Deref.Deref.deref
+                  msg)
+              bLOCK_SIZE))
+      (h, last_block, last_block_len)
+      (fun block (h, last_block, last_block_len) ->
+          if Prims.op_LessThan (Core.Slice.len block) bLOCK_SIZE
+          then
+            let last_block: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 block
+                      }))
+                last_block
+                (fun i last_block -> last_block.[ i ] <- Core.Ops.Index.index block i)
+            in
+            let last_block_len:uint_size = Core.Slice.len block in
+            h, last_block, last_block_len
+          else
+            let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+              compress (Core.Result.unwrap (Core.Convert.TryInto.try_into block)) h
+            in
+            h, last_block, last_block_len)
+  in
+  let last_block:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64} =
+    last_block.[ last_block_len ] <- 128uy
+  in
+  let len_bist:UInt64.t = cast (Alloc.Vec.len msg * 8) in
+  let len_bist_bytes:x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+    Core.Num.to_be_bytes len_bist
+  in
+  let h, last_block:(x:
+    Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} &
+    x:
+    Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64}) =
+    if Prims.op_LessThan last_block_len (bLOCK_SIZE - lEN_SIZE)
+    then
+      let last_block: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 = lEN_SIZE
+                }))
+          last_block
+          (fun i last_block ->
+              last_block.[ bLOCK_SIZE - lEN_SIZE + i ] <- Core.Ops.Index.index len_bist_bytes i)
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress last_block h
+      in
+      h, last_block
+    else
+      let (pad_block: (x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 64})):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 pad_block: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 = lEN_SIZE
+                }))
+          pad_block
+          (fun i pad_block ->
+              pad_block.[ bLOCK_SIZE - lEN_SIZE + i ] <- Core.Ops.Index.index len_bist_bytes i)
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress last_block h
+      in
+      let h:x: Prims.list UInt32.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 8} =
+        compress pad_block h
+      in
+      h, last_block
+  in
+  u32s_to_be_bytes h
+
+let sha256 (msg: Alloc.Vec.vec_t UInt8.t Alloc.Alloc.global_t)
+    : x: Prims.list UInt8.t {Prims.op_Equality (FStar.List.Tot.Base.length x) 32} = hash msg
\ No newline at end of file
diff --git a/sha256-rust/out/Sha256.v b/sha256-rust/out/Sha256.v
new file mode 100644
index 0000000..6a7a825
--- /dev/null
+++ b/sha256-rust/out/Sha256.v
@@ -0,0 +1,245 @@
+(* 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.
+
+(*Not implemented yet? todo(item)*)
+
+Require Import Std. (* as TryInto *)
+
+Definition BLOCK_SIZE : uint_size :=
+  (@repr WORDSIZE32 64).
+
+Definition LEN_SIZE : uint_size :=
+  (@repr WORDSIZE32 8).
+
+Definition K_SIZE : uint_size :=
+  (@repr WORDSIZE32 64).
+
+Definition HASH_SIZE : uint_size :=
+  (@repr WORDSIZE32 256)./(@repr WORDSIZE32 8).
+
+Notation Block_t := (nseq int8 TODO: Int.to_string length).
+
+Notation OpTableType_t := (nseq int8 TODO: Int.to_string length).
+
+Notation Sha256Digest_t := (nseq int8 TODO: Int.to_string length).
+
+Notation RoundConstantsTable_t := (nseq int32 TODO: Int.to_string length).
+
+Notation Hash_t := (nseq int32 TODO: Int.to_string length).
+
+Definition ch (x : int32) (y : int32) (z : int32) : int32 :=
+  (x.&y).^(((TODO: UnOp) x).&z).
+
+Definition maj (x : int32) (y : int32) (z : int32) : int32 :=
+  (x.&y).^((x.&z).^(y.&z)).
+
+Definition OP_TABLE : nseq int8 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE8 2);
+    (@repr WORDSIZE8 13);
+    (@repr WORDSIZE8 22);
+    (@repr WORDSIZE8 6);
+    (@repr WORDSIZE8 11);
+    (@repr WORDSIZE8 25);
+    (@repr WORDSIZE8 7);
+    (@repr WORDSIZE8 18);
+    (@repr WORDSIZE8 3);
+    (@repr WORDSIZE8 17);
+    (@repr WORDSIZE8 19);
+    (@repr WORDSIZE8 10)].
+
+Definition K_TABLE : nseq int32 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE32 1116352408);
+    (@repr WORDSIZE32 1899447441);
+    (@repr WORDSIZE32 3049323471);
+    (@repr WORDSIZE32 3921009573);
+    (@repr WORDSIZE32 961987163);
+    (@repr WORDSIZE32 1508970993);
+    (@repr WORDSIZE32 2453635748);
+    (@repr WORDSIZE32 2870763221);
+    (@repr WORDSIZE32 3624381080);
+    (@repr WORDSIZE32 310598401);
+    (@repr WORDSIZE32 607225278);
+    (@repr WORDSIZE32 1426881987);
+    (@repr WORDSIZE32 1925078388);
+    (@repr WORDSIZE32 2162078206);
+    (@repr WORDSIZE32 2614888103);
+    (@repr WORDSIZE32 3248222580);
+    (@repr WORDSIZE32 3835390401);
+    (@repr WORDSIZE32 4022224774);
+    (@repr WORDSIZE32 264347078);
+    (@repr WORDSIZE32 604807628);
+    (@repr WORDSIZE32 770255983);
+    (@repr WORDSIZE32 1249150122);
+    (@repr WORDSIZE32 1555081692);
+    (@repr WORDSIZE32 1996064986);
+    (@repr WORDSIZE32 2554220882);
+    (@repr WORDSIZE32 2821834349);
+    (@repr WORDSIZE32 2952996808);
+    (@repr WORDSIZE32 3210313671);
+    (@repr WORDSIZE32 3336571891);
+    (@repr WORDSIZE32 3584528711);
+    (@repr WORDSIZE32 113926993);
+    (@repr WORDSIZE32 338241895);
+    (@repr WORDSIZE32 666307205);
+    (@repr WORDSIZE32 773529912);
+    (@repr WORDSIZE32 1294757372);
+    (@repr WORDSIZE32 1396182291);
+    (@repr WORDSIZE32 1695183700);
+    (@repr WORDSIZE32 1986661051);
+    (@repr WORDSIZE32 2177026350);
+    (@repr WORDSIZE32 2456956037);
+    (@repr WORDSIZE32 2730485921);
+    (@repr WORDSIZE32 2820302411);
+    (@repr WORDSIZE32 3259730800);
+    (@repr WORDSIZE32 3345764771);
+    (@repr WORDSIZE32 3516065817);
+    (@repr WORDSIZE32 3600352804);
+    (@repr WORDSIZE32 4094571909);
+    (@repr WORDSIZE32 275423344);
+    (@repr WORDSIZE32 430227734);
+    (@repr WORDSIZE32 506948616);
+    (@repr WORDSIZE32 659060556);
+    (@repr WORDSIZE32 883997877);
+    (@repr WORDSIZE32 958139571);
+    (@repr WORDSIZE32 1322822218);
+    (@repr WORDSIZE32 1537002063);
+    (@repr WORDSIZE32 1747873779);
+    (@repr WORDSIZE32 1955562222);
+    (@repr WORDSIZE32 2024104815);
+    (@repr WORDSIZE32 2227730452);
+    (@repr WORDSIZE32 2361852424);
+    (@repr WORDSIZE32 2428436474);
+    (@repr WORDSIZE32 2756734187);
+    (@repr WORDSIZE32 3204031479);
+    (@repr WORDSIZE32 3329325298)].
+
+Definition HASH_INIT : nseq int32 TODO: Int.to_string length :=
+  array_from_list [(@repr WORDSIZE32 1779033703);
+    (@repr WORDSIZE32 3144134277);
+    (@repr WORDSIZE32 1013904242);
+    (@repr WORDSIZE32 2773480762);
+    (@repr WORDSIZE32 1359893119);
+    (@repr WORDSIZE32 2600822924);
+    (@repr WORDSIZE32 528734635);
+    (@repr WORDSIZE32 1541459225)].
+
+Definition sigma (x : int32) (i : uint_size) (op : uint_size) : int32 :=
+  let tmp := (rotate_right x (into (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 2))))) : int32 in
+  let tmp := (if
+      op=.?(@repr WORDSIZE32 0)
+    then
+      x shift_right (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 2)))
+    else
+      tmp) : int32 in
+  let rot_val_1 := (into (index OP_TABLE ((@repr WORDSIZE32 3).*i))) : int32 in
+  let rot_val_2 := (into (index OP_TABLE (((@repr WORDSIZE32 3).*i).+(@repr WORDSIZE32 1)))) : int32 in
+  ((rotate_right x rot_val_1).^(rotate_right x rot_val_2)).^tmp.
+
+Definition to_be_u32s (block : nseq int8 TODO: Int.to_string length) : Vec_t (int32) (Global_t) :=
+  let out := (with_capacity (BLOCK_SIZE./(@repr WORDSIZE32 4))) : Vec_t (int32) (Global_t) in
+  let out := (fold (into_iter (chunks (unsize block) (@repr WORDSIZE32 4))) out (fun block_chunk out =>
+      let block_chunk_array := (from_be_bytes (unwrap (try_into block_chunk))) : int32 in
+      let out := (push out block_chunk_array) : Vec_t (int32) (Global_t) in
+      out)) : Vec_t (int32) (Global_t) in
+  out.
+
+Definition schedule (block : nseq int8 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let b := (to_be_u32s block) : Vec_t (int32) (Global_t) in
+  let s := (repeat (@repr WORDSIZE32 0) (@repr WORDSIZE32 64)) : Box_t (nseq int32 TODO: Int.to_string length) (Global_t) in
+  let s := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)K_SIZE)) s (fun i s =>
+      if
+        i<.?(@repr WORDSIZE32 16)
+      then
+        let s := (update_at s i (b.[i])) : nseq int32 TODO: Int.to_string length in
+        s
+      else
+        let t16 := (index s (i.-(@repr WORDSIZE32 16))) : int32 in
+        let t15 := (index s (i.-(@repr WORDSIZE32 15))) : int32 in
+        let t7 := (index s (i.-(@repr WORDSIZE32 7))) : int32 in
+        let t2 := (index s (i.-(@repr WORDSIZE32 2))) : int32 in
+        let s1 := (sigma t2 (@repr WORDSIZE32 3) (@repr WORDSIZE32 0)) : int32 in
+        let s0 := (sigma t15 (@repr WORDSIZE32 2) (@repr WORDSIZE32 0)) : int32 in
+        let s := (update_at s i (wrapping_add (wrapping_add (wrapping_add s1 t7) s0) t16)) : nseq int32 TODO: Int.to_string length in
+        s)) : nseq int32 TODO: Int.to_string length in
+  s.
+
+Definition shuffle (ws : nseq int32 TODO: Int.to_string length) (hashi : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let h := (hashi) : nseq int32 TODO: Int.to_string length in
+  let h := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)K_SIZE)) h (fun i h =>
+      let a0 := (index h (@repr WORDSIZE32 0)) : int32 in
+      let b0 := (index h (@repr WORDSIZE32 1)) : int32 in
+      let c0 := (index h (@repr WORDSIZE32 2)) : int32 in
+      let d0 := (index h (@repr WORDSIZE32 3)) : int32 in
+      let e0 := (index h (@repr WORDSIZE32 4)) : int32 in
+      let f0 := (index h (@repr WORDSIZE32 5)) : int32 in
+      let g0 := (index h (@repr WORDSIZE32 6)) : int32 in
+      let h0 := (index h (@repr WORDSIZE32 7)) : int32 in
+      let t1 := (wrapping_add (wrapping_add (wrapping_add (wrapping_add h0 (sigma e0 (@repr WORDSIZE32 1) (@repr WORDSIZE32 1))) (ch e0 f0 g0)) (index K_TABLE i)) (index ws i)) : int32 in
+      let t2 := (wrapping_add (sigma a0 (@repr WORDSIZE32 0) (@repr WORDSIZE32 1)) (maj a0 b0 c0)) : int32 in
+      let h := (update_at h (@repr WORDSIZE32 0) (wrapping_add t1 t2)) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 1) a0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 2) b0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 3) c0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 4) (wrapping_add d0 t1)) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 5) e0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 6) f0) : nseq int32 TODO: Int.to_string length in
+      let h := (update_at h (@repr WORDSIZE32 7) g0) : nseq int32 TODO: Int.to_string length in
+      h)) : nseq int32 TODO: Int.to_string length in
+  h.
+
+Definition compress (block : nseq int8 TODO: Int.to_string length) (h_in : nseq int32 TODO: Int.to_string length) : nseq int32 TODO: Int.to_string length :=
+  let s := (schedule block) : nseq int32 TODO: Int.to_string length in
+  let h := (shuffle s h_in) : nseq int32 TODO: Int.to_string length in
+  let h := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(@repr WORDSIZE32 8))) h (fun i h =>
+      update_at h i (wrapping_add (index h i) (index h_in i)))) : nseq int32 TODO: Int.to_string length in
+  h.
+
+Definition u32s_to_be_bytes (state : nseq int32 TODO: Int.to_string length) : nseq int8 TODO: Int.to_string length :=
+  let out := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 32)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let out := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) out (fun i out =>
+      let tmp := (index state i) : int32 in
+      let tmp := (to_be_bytes tmp) : 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 hash (msg : Vec_t (int8) (Global_t)) : nseq int8 TODO: Int.to_string length :=
+  let h := (HASH_INIT) : nseq int32 TODO: Int.to_string length in
+  let last_block := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+  let last_block_len := ((@repr WORDSIZE32 0)) : uint_size in
+  let '(h,last_block,last_block_len) := (fold (into_iter (chunks (deref msg) BLOCK_SIZE)) (h,last_block,last_block_len) (fun block '(h,last_block,last_block_len) =>
+      if
+        (len block)<.?BLOCK_SIZE
+      then
+        let last_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)(len block))) last_block (fun i last_block =>
+            update_at last_block i (index block i))) : nseq int8 TODO: Int.to_string length in
+        let last_block_len := (len block) : uint_size in
+        (h,last_block,last_block_len)
+      else
+        let h := (compress (unwrap (try_into block)) h) : nseq int32 TODO: Int.to_string length in
+        (h,last_block,last_block_len))) : (nseq int32 TODO: Int.to_string length × nseq int8 TODO: Int.to_string length × uint_size) in
+  let last_block := (update_at last_block last_block_len (@repr WORDSIZE8 128)) : nseq int8 TODO: Int.to_string length in
+  let len_bist := (cast ((len msg).*(@repr WORDSIZE32 8))) : int64 in
+  let len_bist_bytes := (to_be_bytes len_bist) : nseq int8 TODO: Int.to_string length in
+  let '(h,last_block) := (if
+      last_block_len<.?(BLOCK_SIZE.-LEN_SIZE)
+    then
+      let last_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) last_block (fun i last_block =>
+          update_at last_block ((BLOCK_SIZE.-LEN_SIZE).+i) (index len_bist_bytes i))) : nseq int8 TODO: Int.to_string length in
+      let h := (compress last_block h) : nseq int32 TODO: Int.to_string length in
+      (h,last_block)
+    else
+      let pad_block := (repeat (@repr WORDSIZE8 0) (@repr WORDSIZE32 64)) : Box_t (nseq int8 TODO: Int.to_string length) (Global_t) in
+      let pad_block := (fold (into_iter (Build_Range_t (@repr WORDSIZE32 0)LEN_SIZE)) pad_block (fun i pad_block =>
+          update_at pad_block ((BLOCK_SIZE.-LEN_SIZE).+i) (index len_bist_bytes i))) : nseq int8 TODO: Int.to_string length in
+      let h := (compress last_block h) : nseq int32 TODO: Int.to_string length in
+      let h := (compress pad_block h) : nseq int32 TODO: Int.to_string length in
+      (h,last_block)) : (nseq int32 TODO: Int.to_string length × nseq int8 TODO: Int.to_string length) in
+  u32s_to_be_bytes h.
+
+Definition sha256 (msg : Vec_t (int8) (Global_t)) : nseq int8 TODO: Int.to_string length :=
+  hash msg.
diff --git a/sha256-rust/src/sha256.rs b/sha256-rust/src/sha256.rs
new file mode 100644
index 0000000..3673d42
--- /dev/null
+++ b/sha256-rust/src/sha256.rs
@@ -0,0 +1,180 @@
+use std::convert::TryInto;
+
+const BLOCK_SIZE: usize = 64;
+const LEN_SIZE: usize = 8;
+pub const K_SIZE: usize = 64;
+pub const HASH_SIZE: usize = 256 / 8;
+
+pub type Block = [u8; BLOCK_SIZE];
+pub type OpTableType = [u8; 12];
+pub type Sha256Digest = [u8; HASH_SIZE];
+pub type RoundConstantsTable = [u32; K_SIZE];
+pub type Hash = [u32; LEN_SIZE];
+
+pub fn ch(x: u32, y: u32, z: u32) -> u32 {
+    (x & y) ^ ((!x) & z)
+}
+
+pub fn maj(x: u32, y: u32, z: u32) -> u32 {
+    (x & y) ^ ((x & z) ^ (y & z))
+}
+
+const OP_TABLE: OpTableType = [2, 13, 22, 6, 11, 25, 7, 18, 3, 17, 19, 10];
+
+#[rustfmt::skip]
+const K_TABLE: RoundConstantsTable = [
+        0x428a_2f98u32, 0x7137_4491u32, 0xb5c0_fbcfu32, 0xe9b5_dba5u32, 0x3956_c25bu32,
+        0x59f1_11f1u32, 0x923f_82a4u32, 0xab1c_5ed5u32, 0xd807_aa98u32, 0x1283_5b01u32,
+        0x2431_85beu32, 0x550c_7dc3u32, 0x72be_5d74u32, 0x80de_b1feu32, 0x9bdc_06a7u32,
+        0xc19b_f174u32, 0xe49b_69c1u32, 0xefbe_4786u32, 0x0fc1_9dc6u32, 0x240c_a1ccu32,
+        0x2de9_2c6fu32, 0x4a74_84aau32, 0x5cb0_a9dcu32, 0x76f9_88dau32, 0x983e_5152u32,
+        0xa831_c66du32, 0xb003_27c8u32, 0xbf59_7fc7u32, 0xc6e0_0bf3u32, 0xd5a7_9147u32,
+        0x06ca_6351u32, 0x1429_2967u32, 0x27b7_0a85u32, 0x2e1b_2138u32, 0x4d2c_6dfcu32,
+        0x5338_0d13u32, 0x650a_7354u32, 0x766a_0abbu32, 0x81c2_c92eu32, 0x9272_2c85u32,
+        0xa2bf_e8a1u32, 0xa81a_664bu32, 0xc24b_8b70u32, 0xc76c_51a3u32, 0xd192_e819u32,
+        0xd699_0624u32, 0xf40e_3585u32, 0x106a_a070u32, 0x19a4_c116u32, 0x1e37_6c08u32,
+        0x2748_774cu32, 0x34b0_bcb5u32, 0x391c_0cb3u32, 0x4ed8_aa4au32, 0x5b9c_ca4fu32,
+        0x682e_6ff3u32, 0x748f_82eeu32, 0x78a5_636fu32, 0x84c8_7814u32, 0x8cc7_0208u32,
+        0x90be_fffau32, 0xa450_6cebu32, 0xbef9_a3f7u32, 0xc671_78f2u32
+    ];
+
+const HASH_INIT: Hash = [
+    0x6a09e667u32,
+    0xbb67ae85u32,
+    0x3c6ef372u32,
+    0xa54ff53au32,
+    0x510e527fu32,
+    0x9b05688cu32,
+    0x1f83d9abu32,
+    0x5be0cd19u32,
+];
+
+pub fn sigma(x: u32, i: usize, op: usize) -> u32 {
+    let mut tmp: u32 = x.rotate_right(OP_TABLE[3 * i + 2].into());
+    if op == 0 {
+        tmp = x >> OP_TABLE[3 * i + 2]
+    }
+    let rot_val_1 = OP_TABLE[3 * i].into();
+    let rot_val_2 = OP_TABLE[3 * i + 1].into();
+    x.rotate_right(rot_val_1) ^ x.rotate_right(rot_val_2) ^ tmp
+}
+
+fn to_be_u32s(block: Block) -> Vec<u32> {
+    let mut out = Vec::with_capacity(BLOCK_SIZE / 4);
+    for block_chunk in block.chunks(4) {
+        let block_chunk_array = u32::from_be_bytes(block_chunk.try_into().unwrap());
+        out.push(block_chunk_array);
+    }
+
+    out
+}
+
+pub fn schedule(block: Block) -> RoundConstantsTable {
+    let b = to_be_u32s(block);
+    let mut s = [0; K_SIZE];
+    for i in 0..K_SIZE {
+        if i < 16 {
+            s[i] = b[i];
+        } else {
+            let t16 = s[i - 16];
+            let t15 = s[i - 15];
+            let t7 = s[i - 7];
+            let t2 = s[i - 2];
+            let s1 = sigma(t2, 3, 0);
+            let s0 = sigma(t15, 2, 0);
+            s[i] = s1.wrapping_add(t7).wrapping_add(s0).wrapping_add(t16);
+        }
+    }
+    s
+}
+
+pub fn shuffle(ws: RoundConstantsTable, hashi: Hash) -> Hash {
+    let mut h = hashi;
+    for i in 0..K_SIZE {
+        let a0 = h[0];
+        let b0 = h[1];
+        let c0 = h[2];
+        let d0 = h[3];
+        let e0 = h[4];
+        let f0 = h[5];
+        let g0 = h[6];
+        let h0: u32 = h[7];
+
+        let t1 = h0
+            .wrapping_add(sigma(e0, 1, 1))
+            .wrapping_add(ch(e0, f0, g0))
+            .wrapping_add(K_TABLE[i])
+            .wrapping_add(ws[i]);
+        let t2 = sigma(a0, 0, 1).wrapping_add(maj(a0, b0, c0));
+
+        h[0] = t1.wrapping_add(t2);
+        h[1] = a0;
+        h[2] = b0;
+        h[3] = c0;
+        h[4] = d0.wrapping_add(t1);
+        h[5] = e0;
+        h[6] = f0;
+        h[7] = g0;
+    }
+    h
+}
+
+pub fn compress(block: Block, h_in: Hash) -> Hash {
+    let s = schedule(block);
+    let mut h = shuffle(s, h_in);
+    for i in 0..8 {
+        h[i] = h[i].wrapping_add(h_in[i]);
+    }
+    h
+}
+
+fn u32s_to_be_bytes(state: Hash) -> Sha256Digest {
+    let mut out: Sha256Digest = [0u8; HASH_SIZE];
+    for i in 0..LEN_SIZE {
+        let tmp = state[i];
+        let tmp = tmp.to_be_bytes();
+        for j in 0..4 {
+            out[i * 4 + j] = tmp[j];
+        }
+    }
+    out
+}
+
+pub fn hash(msg: &[u8]) -> Sha256Digest {
+    let mut h = HASH_INIT;
+    let mut last_block: Block = [0; BLOCK_SIZE];
+    let mut last_block_len = 0;
+    for block in msg.chunks(BLOCK_SIZE) {
+        if block.len() < BLOCK_SIZE {
+            for i in 0..block.len() {
+                last_block[i] = block[i];
+            }
+            last_block_len = block.len();
+        } else {
+            h = compress(block.try_into().unwrap(), h);
+        }
+    }
+
+    last_block[last_block_len] = 0x80;
+    let len_bist = (msg.len() * 8) as u64;
+    let len_bist_bytes = len_bist.to_be_bytes();
+    if last_block_len < BLOCK_SIZE - LEN_SIZE {
+        for i in 0..LEN_SIZE {
+            last_block[BLOCK_SIZE - LEN_SIZE + i] = len_bist_bytes[i];
+        }
+        h = compress(last_block, h);
+    } else {
+        let mut pad_block: Block = [0; BLOCK_SIZE];
+        for i in 0..LEN_SIZE {
+            pad_block[BLOCK_SIZE - LEN_SIZE + i] = len_bist_bytes[i];
+        }
+        h = compress(last_block, h);
+        h = compress(pad_block, h);
+    }
+
+    u32s_to_be_bytes(h)
+}
+
+pub fn sha256(msg: &[u8]) -> Sha256Digest {
+    hash(msg)
+}
diff --git a/sha256-rust/tests/test_sha256.rs b/sha256-rust/tests/test_sha256.rs
new file mode 100644
index 0000000..0b5a2a9
--- /dev/null
+++ b/sha256-rust/tests/test_sha256.rs
@@ -0,0 +1,41 @@
+use std::num::ParseIntError;
+
+use sha256::*;
+
+fn hex_string_to_vec(s: &str) -> Vec<u8> {
+    debug_assert!(s.len() % core::mem::size_of::<u8>() == 0);
+    let b: Result<Vec<u8>, ParseIntError> = (0..s.len())
+        .step_by(2)
+        .map(|i| u8::from_str_radix(&s[i..i + 2], 16).map(<u8>::from))
+        .collect();
+    b.expect("Error parsing hex string")
+}
+
+#[test]
+fn test_sha256_kat() {
+    let msg = hex_string_to_vec("686163737065632072756c6573");
+    let expected_256 =
+        hex_string_to_vec("b37db5ed72c97da3b2579537afbc3261ed3d5a56f57b3d8e5c1019ae35929964");
+    let digest = hash(&msg);
+    println!("{:?}", expected_256);
+    println!("{:x?}", digest);
+    assert_eq!(expected_256, digest);
+
+    let msg = hex_string_to_vec("6861637370656320697320612070726f706f73616c20666f722061206e65772073706563696669636174696f6e206c616e677561676520666f722063727970746f207072696d69746976657320746861742069732073756363696e63742c2074686174206973206561737920746f207265616420616e6420696d706c656d656e742c20616e642074686174206c656e647320697473656c6620746f20666f726d616c20766572696669636174696f6e2e");
+    let expected_256 =
+        hex_string_to_vec("348ef044446d56e05210361af5a258588ad31765f446bf4cb3b67125a187a64a");
+    let digest = hash(&msg);
+    println!("{:?}", expected_256);
+    println!("{:x?}", digest);
+    assert_eq!(expected_256, digest);
+}
+
+#[test]
+fn empty_input() {
+    const SHA256_EMPTY: Sha256Digest = [
+        0xe3, 0xb0, 0xc4, 0x42, 0x98, 0xfc, 0x1c, 0x14, 0x9a, 0xfb, 0xf4, 0xc8, 0x99, 0x6f, 0xb9,
+        0x24, 0x27, 0xae, 0x41, 0xe4, 0x64, 0x9b, 0x93, 0x4c, 0xa4, 0x95, 0x99, 0x1b, 0x78, 0x52,
+        0xb8, 0x55,
+    ];
+    assert_eq!(hash(&vec![]), SHA256_EMPTY);
+}