8000 Cleanup and specs with Rust types by franziskuskiefer · Pull Request #3 · hacspec/specs · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Cleanup and specs with Rust types #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Cleanup and specs with Rust types #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
24681fc
add sha256 with rust types and exports
franziskuskiefer Jun 12, 2023
20f3d31
chacha20 spec with Rust types
franziskuskiefer Jun 12, 2023
fc57d60
hmac with rust and traits
franziskuskiefer Jun 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,4 @@
Cargo.lock
.vscode
target/
.DS_Store
4 changes: 3 additions & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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",
Expand Down
7 changes: 7 additions & 0 deletions chacha20-rust/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "chacha20"
version = "0.1.0"
authors = ["Franziskus Kiefer <franziskuskiefer@gmail.com>"]
edition = "2021"

[dependencies]
166 changes: 166 additions & 0 deletions chacha20-rust/out/Chacha20.Hacspec_helper.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
40 changes: 40 additions & 0 deletions chacha20-rust/out/Chacha20.Hacspec_helper.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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).
Loading
0