diff --git a/Cargo.toml b/Cargo.toml index 7bdf689..323f25d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,6 +2,7 @@ members = [ "basic", "curve25519", + "curve25519-rust", "chacha20", "poly1305", "poly1305-rust", diff --git a/curve25519-rust/Cargo.toml b/curve25519-rust/Cargo.toml new file mode 100644 index 0000000..7b30c4a --- /dev/null +++ b/curve25519-rust/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "curve25519" +version = "0.1.0" +authors = ["Franziskus Kiefer "] +edition = "2021" + +[lib] +path = "src/curve25519.rs" + +[dependencies] +num-bigint = "0.4" +natmod = { path = "../natmod" } + +[dev-dependencies] +criterion = "0.4" +hex = "0.4" +rand = "0.8" diff --git a/curve25519-rust/out/Hacspec_curve25519.Edited.fst b/curve25519-rust/out/Hacspec_curve25519.Edited.fst new file mode 100644 index 0000000..5e78385 --- /dev/null +++ b/curve25519-rust/out/Hacspec_curve25519.Edited.fst @@ -0,0 +1,134 @@ +module Hacspec_curve25519 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open FStar.Mul +open Hacspec.Lib +open Hacspec_lib_tc + +unfold +type x25519FieldElement_t = + nat_mod 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed +unfold +type fieldCanvas_t = lseq pub_uint8 256 + +unfold +type scalar_t = nat_mod 0x8000000000000000000000000000000000000000000000000000000000000000 +unfold +type scalarCanvas_t = lseq pub_uint8 256 + +let point = (x25519FieldElement_t & x25519FieldElement_t) + +unfold +type x25519SerializedPoint_t = lseq uint8 32 + +unfold +type x25519SerializedScalar_t = lseq uint8 32 + +let mask_scalar (s: x25519SerializedScalar_t) : x25519SerializedScalar_t = + let k:x25519SerializedScalar_t = s in + let k:x25519SerializedScalar_t = k.[ 0l ] <- k.[ 0l ] &. Hacspec_lib_tc.secret 248uy in + let k:x25519SerializedScalar_t = k.[ 31l ] <- k.[ 31l ] &. Hacspec_lib_tc.secret 127uy in + k.[ 31l ] <- k.[ 31l ] |. Hacspec_lib_tc.secret 64uy + +let decode_scalar (s: x25519SerializedScalar_t) : scalar_t = + let k:x25519SerializedScalar_t = mask_scalar s in + from_byte_seq_le k + +let decode_point (u: x25519SerializedPoint_t) : (x25519FieldElement_t & x25519FieldElement_t) = + let u_:x25519SerializedPoint_t = u in + let u_:x25519SerializedPoint_t = u_.[ 31l ] <- u_.[ 31l ] &. Hacspec_lib_tc.secret 127uy in + from_byte_seq_le u_, from_literal (pub_u128 1) + +let encode_point (p: (x25519FieldElement_t & x25519FieldElement_t)) : x25519SerializedPoint_t = + let x, y:(x25519FieldElement_t & x25519FieldElement_t) = p in + let b:x25519FieldElement_t = x *. inv y in + Hacspec_lib_tc.update_start new_ ((to_byte_seq_le b) <: lseq uint8 32) + +let point_add_and_double + (q: (x25519FieldElement_t & x25519FieldElement_t)) + (np: + ((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t))) + : ((x25519FieldElement_t & x25519FieldElement_t) & (x25519FieldElement_t & x25519FieldElement_t) + ) = + let nq, nqp1:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + np + in + let x_1, _z_1:(x25519FieldElement_t & x25519FieldElement_t) = q in + let x_2, z_2:(x25519FieldElement_t & x25519FieldElement_t) = nq in + let x_3, z_3:(x25519FieldElement_t & x25519FieldElement_t) = nqp1 in + let a:x25519FieldElement_t = x_2 +. z_2 in + let aa:x25519FieldElement_t = pow a (pub_u128 2) in + let b:x25519FieldElement_t = x_2 -. z_2 in + let bb:x25519FieldElement_t = b *. b in + let e:x25519FieldElement_t = aa -. bb in + let c:x25519FieldElement_t = x_3 +. z_3 in + let d:x25519FieldElement_t = x_3 -. z_3 in + let da:x25519FieldElement_t = d *. a in + let cb:x25519FieldElement_t = c *. b in + let x_3:x25519FieldElement_t = pow (da +. cb) (pub_u128 2) in + let z_3:x25519FieldElement_t = x_1 *. pow (da -. cb) (pub_u128 2) in + let x_2:x25519FieldElement_t = aa *. bb in + let e121665:x25519FieldElement_t = from_literal (pub_u128 121665) in + let z_2:x25519FieldElement_t = e *. (aa +. e121665 *. e) in + FStar.Pervasives.Native.Mktuple2 x_2 z_2, FStar.Pervasives.Native.Mktuple2 x_3 z_3 + +let swap + (x: + ((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t))) + : ((x25519FieldElement_t & x25519FieldElement_t) & (x25519FieldElement_t & x25519FieldElement_t) + ) = + let x0, x1:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + x + in + x1, x0 + +let montgomery_ladder (k: scalar_t) (init: (x25519FieldElement_t & x25519FieldElement_t)) + : (x25519FieldElement_t & x25519FieldElement_t) = + let inf:(x25519FieldElement_t & x25519FieldElement_t) = + from_literal (pub_u128 1), from_literal (pub_u128 0) + in + let + (acc: + ((x25519FieldElement_t & x25519FieldElement_t) & (x25519FieldElement_t & x25519FieldElement_t))):( + (x25519FieldElement_t & x25519FieldElement_t) & (x25519FieldElement_t & x25519FieldElement_t)) = + inf, init + in + let acc:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + Hacspec.Lib.foldi 0 + 256 + (fun i acc -> + if bit k (255 - i) + then + let acc:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + swap acc + in + let acc:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + point_add_and_double init acc + in + swap acc + else point_add_and_double init acc) + acc + in + let out, _:((x25519FieldElement_t & x25519FieldElement_t) & + (x25519FieldElement_t & x25519FieldElement_t)) = + acc + in + out + +let x25519_scalarmult (s: x25519SerializedScalar_t) (p: x25519SerializedPoint_t) + : x25519SerializedPoint_t = + let s_:scalar_t = decode_scalar s in + let p_:(x25519FieldElement_t & x25519FieldElement_t) = decode_point p in + let r:(x25519FieldElement_t & x25519FieldElement_t) = montgomery_ladder s_ p_ in + encode_point r + +let x25519_secret_to_public (s: x25519SerializedScalar_t) : x25519SerializedPoint_t = + let base:x25519SerializedPoint_t = new_ in + let base:x25519SerializedPoint_t = base.[ 0l ] <- Hacspec_lib_tc.secret 9uy in + x25519_scalarmult s base diff --git a/curve25519-rust/proofs/fstar/extraction/Curve25519.Hacspec_helper.fst b/curve25519-rust/proofs/fstar/extraction/Curve25519.Hacspec_helper.fst new file mode 100644 index 0000000..4f1caf9 --- /dev/null +++ b/curve25519-rust/proofs/fstar/extraction/Curve25519.Hacspec_helper.fst @@ -0,0 +1,7 @@ +module Curve25519.Hacspec_helper +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + +let t_U8 = u8 + +let v_U8 (x: u8) : u8 = x \ No newline at end of file diff --git a/curve25519-rust/proofs/fstar/extraction/Curve25519.SCALAR_mod.fst b/curve25519-rust/proofs/fstar/extraction/Curve25519.SCALAR_mod.fst new file mode 100644 index 0000000..cb55048 --- /dev/null +++ b/curve25519-rust/proofs/fstar/extraction/Curve25519.SCALAR_mod.fst @@ -0,0 +1,75 @@ +module Curve25519.SCALAR_mod +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + +let v_SCALAR_MODULUS: array u8 32sz = + (let l = + [ + 128uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; + 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy + ] + in + assert_norm (List.Tot.length l == 32); + Rust_primitives.Hax.array_of_list l) + +let impl: Curve25519.Hacspec_helper.t_NatMod Curve25519.t_Scalar 32sz = + { + mODULUS + = + (fun -> + (let l = + [ + 128uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; + 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy + ] + in + assert_norm (List.Tot.length l == 32); + Rust_primitives.Hax.array_of_list l)); + mODULUS_STR = (fun -> "8000000000000000000000000000000000000000000000000000000000000000"); + zERO = (fun -> Rust_primitives.Hax.repeat 0uy 32sz); + new_ = (fun (value: array u8 32sz) -> { Curve25519.Scalar.f_value = value }); + value = fun (self: Curve25519.t_Scalar) -> Rust_primitives.unsize self.Curve25519.Scalar.f_value + } + +let impl: Core.Convert.t_AsRef Curve25519.t_Scalar (slice u8) = + { + as_ref + = + fun (self: Curve25519.t_Scalar) -> Rust_primitives.unsize self.Curve25519.Scalar.f_value + } + +(* +Last available AST for this item: + +/* TO DO */ + *) + +let impl: Core.Convert.t_Into Curve25519.t_Scalar (array u8 32sz) = + { into = fun (self: Curve25519.t_Scalar) -> self.Curve25519.Scalar.f_value } + +let impl: Core.Ops.Arith.t_Add Curve25519.t_Scalar Curve25519.t_Scalar = + { + output = Curve25519.t_Scalar; + add + = + fun (self: Curve25519.t_Scalar) (rhs: Curve25519.t_Scalar) -> + Curve25519.Hacspec_helper.NatMod.fadd self rhs + } + +let impl: Core.Ops.Arith.t_Mul Curve25519.t_Scalar Curve25519.t_Scalar = + { + output = Curve25519.t_Scalar; + mul + = + fun (self: Curve25519.t_Scalar) (rhs: Curve25519.t_Scalar) -> + Curve25519.Hacspec_helper.NatMod.fmul self rhs + } + +let impl: Core.Ops.Arith.t_Sub Curve25519.t_Scalar Curve25519.t_Scalar = + { + output = Curve25519.t_Scalar; + sub + = + fun (self: Curve25519.t_Scalar) (rhs: Curve25519.t_Scalar) -> + Curve25519.Hacspec_helper.NatMod.fsub self rhs + } \ No newline at end of file diff --git a/curve25519-rust/proofs/fstar/extraction/Curve25519.X25519FIELDELEMENT_mod.fst b/curve25519-rust/proofs/fstar/extraction/Curve25519.X25519FIELDELEMENT_mod.fst new file mode 100644 index 0000000..f492d8c --- /dev/null +++ b/curve25519-rust/proofs/fstar/extraction/Curve25519.X25519FIELDELEMENT_mod.fst @@ -0,0 +1,83 @@ +module Curve25519.X25519FIELDELEMENT_mod +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + +let v_X25519FIELDELEMENT_MODULUS: array u8 32sz = + (let l = + [ + 127uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; + 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; + 255uy; 255uy; 255uy; 255uy; 255uy; 237uy + ] + in + assert_norm (List.Tot.length l == 32); + Rust_primitives.Hax.array_of_list l) + +let impl: Curve25519.Hacspec_helper.t_NatMod Curve25519.t_X25519FieldElement 32sz = + { + mODULUS + = + (fun -> + (let l = + [ + 127uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; + 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; + 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 255uy; 237uy + ] + in + assert_norm (List.Tot.length l == 32); + Rust_primitives.Hax.array_of_list l)); + mODULUS_STR = (fun -> "7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed"); + zERO = (fun -> Rust_primitives.Hax.repeat 0uy 32sz); + new_ = (fun (value: array u8 32sz) -> { Curve25519.X25519FieldElement.f_value = value }); + value + = + fun (self: Curve25519.t_X25519FieldElement) -> + Rust_primitives.unsize self.Curve25519.X25519FieldElement.f_value + } + +let impl: Core.Convert.t_AsRef Curve25519.t_X25519FieldElement (slice u8) = + { + as_ref + = + fun (self: Curve25519.t_X25519FieldElement) -> + Rust_primitives.unsize self.Curve25519.X25519FieldElement.f_value + } + +(* +Last available AST for this item: + +/* TO DO */ + *) + +let impl: Core.Convert.t_Into Curve25519.t_X25519FieldElement (array u8 32sz) = + { + into = fun (self: Curve25519.t_X25519FieldElement) -> self.Curve25519.X25519FieldElement.f_value + } + +let impl: Core.Ops.Arith.t_Add Curve25519.t_X25519FieldElement Curve25519.t_X25519FieldElement = + { + output = Curve25519.t_X25519FieldElement; + add + = + fun (self: Curve25519.t_X25519FieldElement) (rhs: Curve25519.t_X25519FieldElement) -> + Curve25519.Hacspec_helper.NatMod.fadd self rhs + } + +let impl: Core.Ops.Arith.t_Mul Curve25519.t_X25519FieldElement Curve25519.t_X25519FieldElement = + { + output = Curve25519.t_X25519FieldElement; + mul + = + fun (self: Curve25519.t_X25519FieldElement) (rhs: Curve25519.t_X25519FieldElement) -> + Curve25519.Hacspec_helper.NatMod.fmul self rhs + } + +let impl: Core.Ops.Arith.t_Sub Curve25519.t_X25519FieldElement Curve25519.t_X25519FieldElement = + { + output = Curve25519.t_X25519FieldElement; + sub + = + fun (self: Curve25519.t_X25519FieldElement) (rhs: Curve25519.t_X25519FieldElement) -> + Curve25519.Hacspec_helper.NatMod.fsub self rhs + } \ No newline at end of file diff --git a/curve25519-rust/proofs/fstar/extraction/Curve25519.fst b/curve25519-rust/proofs/fstar/extraction/Curve25519.fst new file mode 100644 index 0000000..83e4a94 --- /dev/null +++ b/curve25519-rust/proofs/fstar/extraction/Curve25519.fst @@ -0,0 +1,152 @@ +module Curve25519 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + +type t_X25519FieldElement = { f_value:array u8 32sz } + +type t_Scalar = { f_value:array u8 32sz } + +let t_Point = (t_X25519FieldElement & t_X25519FieldElement) + +let t_X25519SerializedPoint = array u8 32sz + +let t_X25519SerializedScalar = array u8 32sz + +let mask_scalar (s: array u8 32sz) : array u8 32sz = + let k:array u8 32sz = s in + let k:array u8 32sz = + Rust_primitives.Hax.update_at k + 0sz + ((k.[ 0sz ] <: u8) &. (Curve25519.Hacspec_helper.v_U8 248uy <: u8) <: u8) + in + let k:array u8 32sz = + Rust_primitives.Hax.update_at k + 31sz + ((k.[ 31sz ] <: u8) &. (Curve25519.Hacspec_helper.v_U8 127uy <: u8) <: u8) + in + let k:array u8 32sz = + Rust_primitives.Hax.update_at k + 31sz + ((k.[ 31sz ] <: u8) |. (Curve25519.Hacspec_helper.v_U8 64uy <: u8) <: u8) + in + k + +let decode_scalar (s: array u8 32sz) : t_Scalar = + let k:array u8 32sz = mask_scalar s in + Curve25519.Hacspec_helper.NatMod.from_le_bytes (Rust_primitives.unsize k <: slice u8) + +let decode_point (u: array u8 32sz) : (t_X25519FieldElement & t_X25519FieldElement) = + let u:array u8 32sz = + Rust_primitives.Hax.update_at u + 31sz + ((u.[ 31sz ] <: u8) &. (Curve25519.Hacspec_helper.v_U8 127uy <: u8) <: u8) + in + Curve25519.Hacspec_helper.NatMod.from_le_bytes (Rust_primitives.unsize u <: slice u8), + Curve25519.Hacspec_helper.NatMod.from_u128 (pub_u128 1sz) + +let encode_point (p: (t_X25519FieldElement & t_X25519FieldElement)) : array u8 32sz = + let b = p._1 *. (Curve25519.Hacspec_helper.NatMod.inv p._2 <: t_X25519FieldElement) in + Curve25519.Hacspec_helper.NatMod.to_le_bytes b + +let point_add_and_double + (q: (t_X25519FieldElement & t_X25519FieldElement)) + (np: + ((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement))) + : ((t_X25519FieldElement & t_X25519FieldElement) & (t_X25519FieldElement & t_X25519FieldElement) + ) = + let nq, nqp1:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + np + in + let x_1_, v__z_1_:(t_X25519FieldElement & t_X25519FieldElement) = q in + let x_2_, z_2_:(t_X25519FieldElement & t_X25519FieldElement) = nq in + let x_3_, z_3_:(t_X25519FieldElement & t_X25519FieldElement) = nqp1 in + let a = x_2_ +. z_2_ in + let aa:t_X25519FieldElement = Curve25519.Hacspec_helper.NatMod.pow a (pub_u128 2sz) in + let b = x_2_ -. z_2_ in + let bb = b *. b in + let e = aa -. bb in + let c = x_3_ +. z_3_ in + let d = x_3_ -. z_3_ in + let da = d *. a in + let cb = c *. b in + let x_3_:t_X25519FieldElement = + Curve25519.Hacspec_helper.NatMod.pow (da +. cb <: _) (pub_u128 2sz) + in + let z_3_ = + x_1_ *. + (Curve25519.Hacspec_helper.NatMod.pow (da -. cb <: _) (pub_u128 2sz) <: t_X25519FieldElement) + in + let x_2_ = aa *. bb in + let e121665:t_X25519FieldElement = + Curve25519.Hacspec_helper.NatMod.from_u128 (pub_u128 121665sz) + in + let z_2_ = e *. (aa +. (e121665 *. e <: _) <: _) in + FStar.Pervasives.Native.Mktuple2 x_2_ z_2_, FStar.Pervasives.Native.Mktuple2 x_3_ z_3_ + +let swap + (x: + ((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement))) + : ((t_X25519FieldElement & t_X25519FieldElement) & (t_X25519FieldElement & t_X25519FieldElement) + ) = x._2, x._1 + +let montgomery_ladder (k: t_Scalar) (init: (t_X25519FieldElement & t_X25519FieldElement)) + : (t_X25519FieldElement & t_X25519FieldElement) = + let inf:(t_X25519FieldElement & t_X25519FieldElement) = + Curve25519.Hacspec_helper.NatMod.from_u128 (pub_u128 1sz), + Curve25519.Hacspec_helper.NatMod.from_u128 (pub_u128 0sz) + in + let + (acc: + ((t_X25519FieldElement & t_X25519FieldElement) & (t_X25519FieldElement & t_X25519FieldElement))):( + (t_X25519FieldElement & t_X25519FieldElement) & (t_X25519FieldElement & t_X25519FieldElement)) = + inf, init + in + let acc:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({ + Core.Ops.Range.Range.f_start = pub_u128 0sz; + Core.Ops.Range.Range.f_end = pub_u128 256sz + }) + <: + _) + acc + (fun acc i -> + if Curve25519.Hacspec_helper.NatMod.bit k (pub_u128 255sz -. i <: u128) <: bool + then + let acc:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + swap acc + in + let acc:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + point_add_and_double init acc + in + let acc:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + swap acc + in + acc + else + let acc:((t_X25519FieldElement & t_X25519FieldElement) & + (t_X25519FieldElement & t_X25519FieldElement)) = + point_add_and_double init acc + in + acc) + in + acc._1 + +let x25519_scalarmult (s p: array u8 32sz) : array u8 32sz = + let s:t_Scalar = decode_scalar s in + let p:(t_X25519FieldElement & t_X25519FieldElement) = decode_point p in + let r:(t_X25519FieldElement & t_X25519FieldElement) = montgomery_ladder s p in + encode_point r + +let x25519_secret_to_public (s: array u8 32sz) : array u8 32sz = + let base:array u8 32sz = Rust_primitives.Hax.repeat 0uy 32sz in + let base:array u8 32sz = + Rust_primitives.Hax.update_at base 0sz (Curve25519.Hacspec_helper.v_U8 9uy <: u8) + in + x25519_scalarmult s base \ No newline at end of file diff --git a/curve25519-rust/src/curve25519.rs b/curve25519-rust/src/curve25519.rs new file mode 100644 index 0000000..460ee15 --- /dev/null +++ b/curve25519-rust/src/curve25519.rs @@ -0,0 +1,102 @@ +//! x25519 as specified in https://www.rfc-editor.org/rfc/rfc7748 + +mod hacspec_helper; +use hacspec_helper::*; + +#[nat_mod("7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed", 32)] +pub struct X25519FieldElement {} + +#[nat_mod("8000000000000000000000000000000000000000000000000000000000000000", 32)] +pub struct Scalar {} + +pub type Point = (X25519FieldElement, X25519FieldElement); + +pub type X25519SerializedPoint = [U8; 32]; +pub type X25519SerializedScalar = [U8; 32]; + +fn mask_scalar(s: X25519SerializedScalar) -> X25519SerializedScalar { + let mut k = s; + k[0] = k[0] & U8(248); + k[31] = k[31] & U8(127); + k[31] = k[31] | U8(64); + k +} + +fn decode_scalar(s: X25519SerializedScalar) -> Scalar { + let k = mask_scalar(s); + Scalar::from_le_bytes(&k) +} + +fn decode_point(mut u: X25519SerializedPoint) -> Point { + u[31] = u[31] & U8(127); + ( + X25519FieldElement::from_le_bytes(&u), + X25519FieldElement::from_u128(1), + ) +} + +fn encode_point(p: Point) -> X25519SerializedPoint { + let b = p.0 * p.1.inv(); + b.to_le_bytes() +} + +fn point_add_and_double(q: Point, np: (Point, Point)) -> (Point, Point) { + let (nq, nqp1) = np; + let (x_1, _z_1) = q; + let (x_2, z_2) = nq; + let (x_3, z_3) = nqp1; + let a = x_2 + z_2; + let aa = a.pow(2); + let b = x_2 - z_2; + let bb = b * b; + let e = aa - bb; + let c = x_3 + z_3; + let d = x_3 - z_3; + let da = d * a; + let cb = c * b; + + let x_3 = (da + cb).pow(2); + let z_3 = x_1 * ((da - cb).pow(2)); + let x_2 = aa * bb; + let e121665 = X25519FieldElement::from_u128(121_665); + let z_2 = e * (aa + (e121665 * e)); + ((x_2, z_2), (x_3, z_3)) +} + +fn swap(x: (Point, Point)) -> (Point, Point) { + (x.1, x.0) +} + +fn montgomery_ladder(k: Scalar, init: Point) -> Point { + let inf = ( + X25519FieldElement::from_u128(1), + X25519FieldElement::from_u128(0), + ); + let mut acc: (Point, Point) = (inf, init); + for i in 0..256 { + if k.bit(255 - i) { + acc = swap(acc); + acc = point_add_and_double(init, acc); + acc = swap(acc); + } else { + acc = point_add_and_double(init, acc); + } + } + acc.0 +} + +pub fn x25519_scalarmult( + s: X25519SerializedScalar, + p: X25519SerializedPoint, +) -> X25519SerializedPoint { + let s = decode_scalar(s); + let p = decode_point(p); + let r = montgomery_ladder(s, p); + encode_point(r) +} + +pub fn x25519_secret_to_public(s: X25519SerializedScalar) -> X25519SerializedPoint { + let mut base = [0; 32]; + base[0] = U8(0x09u8); + x25519_scalarmult(s, base) +} diff --git a/curve25519-rust/src/hacspec_helper.rs b/curve25519-rust/src/hacspec_helper.rs new file mode 100644 index 0000000..4f26a28 --- /dev/null +++ b/curve25519-rust/src/hacspec_helper.rs @@ -0,0 +1,211 @@ +use std::convert::TryInto; + +/// This has to come from the lib. +pub use natmod::nat_mod; + +pub trait NatMod { + const MODULUS: [u8; LEN]; + const MODULUS_STR: &'static str; + const ZERO: [u8; LEN]; + + fn new(value: [u8; LEN]) -> Self; + fn value(&self) -> &[u8]; + + /// Sub self with `rhs` and return the result `self - rhs % MODULUS`. + fn fsub(self, rhs: Self) -> Self + where + Self: Sized, + { + let lhs = num_bigint::BigUint::from_bytes_be(self.value()); + let rhs = num_bigint::BigUint::from_bytes_be(rhs.value()); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + let res = if lhs < rhs { + modulus.clone() + lhs - rhs + } else { + lhs - rhs + }; + let res = res % modulus; + Self::from_bigint(res) + } + + /// Add self with `rhs` and return the result `self + rhs % MODULUS`. + fn fadd(self, rhs: Self) -> Self + where + Self: Sized, + { + let lhs = num_bigint::BigUint::from_bytes_be(self.value()); + let rhs = num_bigint::BigUint::from_bytes_be(rhs.value()); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + let res = (lhs + rhs) % modulus; + Self::from_bigint(res) + } + + /// Multiply self with `rhs` and return the result `self * rhs % MODULUS`. + fn fmul(self, rhs: Self) -> Self + where + Self: Sized, + { + let lhs = num_bigint::BigUint::from_bytes_be(self.value()); + let rhs = num_bigint::BigUint::from_bytes_be(rhs.value()); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + let res = (lhs * rhs) % modulus; + Self::from_bigint(res) + } + + /// `self ^ rhs % MODULUS`. + fn pow(self, rhs: u128) -> Self + where + Self: Sized, + { + let lhs = num_bigint::BigUint::from_bytes_be(self.value()); + let rhs = num_bigint::BigUint::from(rhs); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + let res = lhs.modpow(&rhs, &modulus); + Self::from_bigint(res) + } + + /// Invert self and return the result `self ^ -1 % MODULUS`. + fn inv(self) -> Self + where + Self: Sized, + { + let val = num_bigint::BigUint::from_bytes_be(self.value()); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + let m = &modulus - num_bigint::BigUint::from(2u32); + Self::from_bigint(val.modpow(&m, &modulus)) + } + + /// Zero element + fn zero() -> Self + where + Self: Sized, + { + Self::new(Self::ZERO) + } + + /// One element + fn one() -> Self + where + Self: Sized, + { + let out = Self::new(Self::ZERO); + out.fadd(Self::from_u128(1)) + } + + fn bit(&self, bit: u128) -> bool { + let val = num_bigint::BigUint::from_bytes_be(self.value()); + val.bit(bit.try_into().unwrap()) + } + + /// Returns 2 to the power of the argument + fn pow2(x: usize) -> Self + where + Self: Sized, + { + let res = num_bigint::BigUint::from(1u32) << x; + Self::from_bigint(res) + } + + /// Create a new [`#ident`] from a `u128` literal. + fn from_u128(literal: u128) -> Self + where + Self: Sized, + { + Self::from_bigint(num_bigint::BigUint::from(literal)) + } + + /// Create a new [`#ident`] from a little endian byte slice. + /// + /// This computes bytes % MODULUS + fn from_le_bytes(bytes: &[u8]) -> Self + where + Self: Sized, + { + let value = num_bigint::BigUint::from_bytes_le(bytes); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + Self::from_bigint(value % modulus) + } + + /// Create a new [`#ident`] from a little endian byte slice. + /// + /// This computes bytes % MODULUS + fn from_be_bytes(bytes: &[u8]) -> Self + where + Self: Sized, + { + let value = num_bigint::BigUint::from_bytes_be(bytes); + let modulus = num_bigint::BigUint::from_bytes_be(&Self::MODULUS); + Self::from_bigint(value % modulus) + } + + fn to_le_bytes(self) -> [u8; LEN] + where + Self: Sized, + { + Self::pad(&num_bigint::BigUint::from_bytes_be(self.value()).to_bytes_le()) + } + + fn to_be_bytes(self) -> [u8; LEN] + where + Self: Sized, + { + self.value().try_into().unwrap() + } + + /// Get hex string representation of this. + fn to_hex(&self) -> String { + let strs: Vec = self.value().iter().map(|b| format!("{:02x}", b)).collect(); + strs.join("") + } + + /// New from hex string + fn from_hex(hex: &str) -> Self + where + Self: Sized, + { + assert!(hex.len() % 2 == 0); + let l = hex.len() / 2; + assert!(l <= LEN); + let mut value = [0u8; LEN]; + let skip = LEN - l; + for i in 0..l { + value[skip + i] = u8::from_str_radix(&hex[2 * i..2 * i + 2], 16) + .expect("An unexpected error occurred."); + } + Self::new(value) + } + + fn pad(bytes: &[u8]) -> [u8; LEN] { + let mut value = [0u8; LEN]; + let upper = value.len(); + let lower = upper - bytes.len(); + value[lower..upper].copy_from_slice(&bytes); + value + } + + fn from_bigint(x: num_bigint::BigUint) -> Self + where + Self: Sized, + { + let max_value = Self::MODULUS; + assert!( + x <= num_bigint::BigUint::from_bytes_be(&max_value), + "{} is too large for type {}!", + x, + stringify!($ident) + ); + let repr = x.to_bytes_be(); + if repr.len() > LEN { + panic!("{} is too large for this type", x) + } + + Self::new(Self::pad(&repr)) + } +} + +// === Secret Integers + +pub type U8 = u8; +pub fn U8(x: u8) -> u8 { + x +} diff --git a/curve25519-rust/tests/test_curve25519.rs b/curve25519-rust/tests/test_curve25519.rs new file mode 100644 index 0000000..4fd2f45 --- /dev/null +++ b/curve25519-rust/tests/test_curve25519.rs @@ -0,0 +1,68 @@ +use std::convert::TryInto; + +use curve25519::*; + +fn ecdh(s: X25519SerializedScalar, u: X25519SerializedPoint, expected: X25519SerializedPoint) { + let r = x25519_scalarmult(s, u); + assert_eq!(expected, r); +} + +#[test] +fn test_kat1() { + let s = [ + 0xa5, 0x46, 0xe3, 0x6b, 0xf0, 0x52, 0x7c, 0x9d, 0x3b, 0x16, 0x15, 0x4b, 0x82, 0x46, 0x5e, + 0xdd, 0x62, 0x14, 0x4c, 0x0a, 0xc1, 0xfc, 0x5a, 0x18, 0x50, 0x6a, 0x22, 0x44, 0xba, 0x44, + 0x9a, 0xc4, + ]; + let u = [ + 0xe6, 0xdb, 0x68, 0x67, 0x58, 0x30, 0x30, 0xdb, 0x35, 0x94, 0xc1, 0xa4, 0x24, 0xb1, 0x5f, + 0x7c, 0x72, 0x66, 0x24, 0xec, 0x26, 0xb3, 0x35, 0x3b, 0x10, 0xa9, 0x03, 0xa6, 0xd0, 0xab, + 0x1c, 0x4c, + ]; + let expected = [ + 0xc3, 0xda, 0x55, 0x37, 0x9d, 0xe9, 0xc6, 0x90, 0x8e, 0x94, 0xea, 0x4d, 0xf2, 0x8d, 0x08, + 0x4f, 0x32, 0xec, 0xcf, 0x03, 0x49, 0x1c, 0x71, 0xf7, 0x54, 0xb4, 0x07, 0x55, 0x77, 0xa2, + 0x85, 0x52, + ]; + + ecdh(s, u, expected); +} + +const KAT: [(&str, &str, &str); 5] = [ + ( + "77076d0a7318a57d3c16c17251b26645df4c2f87ebc0992ab177fba51db92c2a", + "de9edb7d7b7dc1b4d35b61c2ece435373f8343c85b78674dadfc7e146f882b4f", + "4a5d9d5ba4ce2de1728e3bf480350f25e07e21c947d19e3376f09b3c1e161742", + ), + ( + "5dab087e624a8a4b79e17f8b83800ee66f3bb1292618b6fd1c2f8b27ff88e0eb", + "8520f0098930a754748b7ddcb43ef75a0dbf3a0d26381af4eba4a98eaa9b4e6a", + "4a5d9d5ba4ce2de1728e3bf480350f25e07e21c947d19e3376f09b3c1e161742", + ), + ( + "0100000000000000000000000000000000000000000000000000000000000000", + "2500000000000000000000000000000000000000000000000000000000000000", + "3c7777caf997b264416077665b4e229d0b9548dc0cd81998ddcdc5c8533c797f", + ), + ( + "0100000000000000000000000000000000000000000000000000000000000000", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "b32d1362c248d62fe62619cff04dd43db73ffc1b6308ede30b78d87380f1e834", + ), + ( + "a546e36bf0527c9d3b16154b82465edd62144c0ac1fc5a18506a2244ba449ac4", + "e6db6867583030db3594c1a424b15f7c726624ec26b3353b10a903a6d0ab1c4c", + "c3da55379de9c6908e94ea4df28d084f32eccf03491c71f754b4075577a28552", + ), +]; + +#[test] +fn test_kat3() { + for kat in KAT.iter() { + let s: [u8; 32] = hex::decode(kat.0).unwrap().try_into().unwrap(); + let u: [u8; 32] = hex::decode(kat.1).unwrap().try_into().unwrap(); + let expected: [u8; 32] = hex::decode(kat.2).unwrap().try_into().unwrap(); + + ecdh(s, u, expected); + } +} diff --git a/poly1305-rust/natmod/Cargo.toml b/natmod/Cargo.toml similarity index 100% rename from poly1305-rust/natmod/Cargo.toml rename to natmod/Cargo.toml diff --git a/natmod/proofs/fstar/extraction/Natmod.Nat_mod.fst b/natmod/proofs/fstar/extraction/Natmod.Nat_mod.fst new file mode 100644 index 0000000..2c9a10c --- /dev/null +++ b/natmod/proofs/fstar/extraction/Natmod.Nat_mod.fst @@ -0,0 +1,4 @@ +module Natmod.Nat_mod +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + diff --git a/natmod/proofs/fstar/extraction/Natmod.fst b/natmod/proofs/fstar/extraction/Natmod.fst new file mode 100644 index 0000000..5626425 --- /dev/null +++ b/natmod/proofs/fstar/extraction/Natmod.fst @@ -0,0 +1,725 @@ +module Natmod +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core + +type t_NatModAttr = { + f_mod_str:Alloc.String.t_String; + f_mod_bytes:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global; + f_int_size:usize +} + +let impl: Syn.Parse.t_Parse t_NatModAttr = + { + parse + = + fun (input: Syn.Parse.t_ParseBuffer) -> + let hoist1:Core.Result.t_Result t_NatModAttr Syn.Error.t_Error = + Core.Ops.Try_trait.FromResidual.from_residual (Syn.Parse.parse_under_impl_9 input) + in + let mod_str:Alloc.String.t_String = Syn.Lit.value_under_impl hoist1 in + let mod_bytes:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Core.Result.expect_under_impl (Hex.FromHex.from_hex mod_str) "Invalid hex String" + in + let _:Core.Result.t_Result t_NatModAttr Syn.Error.t_Error = + Core.Ops.Try_trait.FromResidual.from_residual (Syn.Parse.parse_under_impl_9 input) + in + let hoist2:Core.Result.t_Result t_NatModAttr Syn.Error.t_Error = + Core.Ops.Try_trait.FromResidual.from_residual (Syn.Parse.parse_under_impl_9 input) + in + let hoist3:Core.Result.t_Result usize Syn.Error.t_Error = + Syn.Lit.base10_parse_under_impl_4 hoist2 + in + let int_size:Core.Result.t_Result t_NatModAttr Syn.Error.t_Error = + Core.Ops.Try_trait.FromResidual.from_residual hoist3 + in + let _:never = + if ~.(Syn.Parse.is_empty_under_impl_9 input) + then + Core.Panicking.panic_fmt (Core.Fmt.new_v1_under_impl_2 (Rust_primitives.unsize (let l = + ["Left over tokens in attribute "] + in + assert_norm (List.Tot.length l == 1); + Rust_primitives.Hax.array_of_list l)) + (Rust_primitives.unsize (let l = [Core.Fmt.Rt.new_debug_under_impl_1 input] in + assert_norm (List.Tot.length l == 1); + Rust_primitives.Hax.array_of_list l))) + in + Core.Result.Result_Ok + ({ + Natmod.NatModAttr.f_mod_str = mod_str; + Natmod.NatModAttr.f_mod_bytes = mod_bytes; + Natmod.NatModAttr.f_int_size = int_size + }) + } + +let nat_mod (attr item: Proc_macro.t_TokenStream) : Proc_macro.t_TokenStream = + Rust_primitives.Hax.Control_flow_monad.Mexception.run (let* item_ast:Syn.Derive.t_DeriveInput = + match Syn.parse item with + | Core.Result.Result_Ok data -> Core.Ops.Control_flow.ControlFlow_Continue data + | Core.Result.Result_Err err -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Convert.From.from (Syn.Error.to_compile_error_under_impl + err)) + in + let ident:Proc_macro2.t_Ident = + Core.Clone.Clone.clone item_ast.Syn.Derive.DeriveInput.f_ident + in + let* args:t_NatModAttr = + match Syn.parse attr with + | Core.Result.Result_Ok data -> Core.Ops.Control_flow.ControlFlow_Continue data + | Core.Result.Result_Err err -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Convert.From.from (Syn.Error.to_compile_error_under_impl + err)) + in + Core.Ops.Control_flow.ControlFlow_Continue + (let num_bytes:usize = args.Natmod.NatModAttr.f_int_size in + let modulus:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = args.Natmod.NatModAttr.f_mod_bytes in + let modulus_string:Alloc.String.t_String = args.Natmod.NatModAttr.f_mod_str in + let padded_modulus:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Alloc.Vec.from_elem 0uy (num_bytes -. Alloc.Vec.len_under_impl_1 modulus) + in + let _:Prims.unit = + Rust_primitives.Hax.failure "" + "alloc::vec::append_under_impl_1(\n &mut (padded_modulus),\n &mut (deref(&mut (core::clone::Clone::clone(&(modulus))))),\n )" + + in + let mod_iter1:Core.Slice.Iter.t_Iter u8 = + Core.Slice.iter_under_impl (Core.Ops.Deref.Deref.deref padded_modulus) + in + let mod_iter2:Core.Slice.Iter.t_Iter u8 = + Core.Slice.iter_under_impl (Core.Ops.Deref.Deref.deref padded_modulus) + in + let res:Alloc.String.t_String = + Alloc.Fmt.format (Core.Fmt.new_v1_under_impl_2 (Rust_primitives.unsize (let l = + [""; "_MODULUS"] + in + assert_norm (List.Tot.length l == 2); + Rust_primitives.Hax.array_of_list l)) + (Rust_primitives.unsize (let l = + [ + Core.Fmt.Rt.new_display_under_impl_1 (Alloc.Str.to_uppercase_under_impl_5 ( + Core.Ops.Deref.Deref.deref (Alloc.String.ToString.to_string ident) + )) + ] + in + assert_norm (List.Tot.length l == 1); + Rust_primitives.Hax.array_of_list l))) + in + let const_name:Proc_macro2.t_Ident = + Proc_macro2.new_under_impl_31 (Core.Ops.Deref.Deref.deref res) + (Proc_macro2.span_under_impl_31 ident) + in + let res:Alloc.String.t_String = + Alloc.Fmt.format (Core.Fmt.new_v1_under_impl_2 (Rust_primitives.unsize (let l = + [""; "_MODULUS_STR"] + in + assert_norm (List.Tot.length l == 2); + Rust_primitives.Hax.array_of_list l)) + (Rust_primitives.unsize (let l = + [ + Core.Fmt.Rt.new_display_under_impl_1 (Alloc.Str.to_uppercase_under_impl_5 ( + Core.Ops.Deref.Deref.deref (Alloc.String.ToString.to_string ident) + )) + ] + in + assert_norm (List.Tot.length l == 1); + Rust_primitives.Hax.array_of_list l))) + in + let static_name:Proc_macro2.t_Ident = + Proc_macro2.new_under_impl_31 (Core.Ops.Deref.Deref.deref res) + (Proc_macro2.span_under_impl_31 ident) + in + let res:Alloc.String.t_String = + Alloc.Fmt.format (Core.Fmt.new_v1_under_impl_2 (Rust_primitives.unsize (let l = + [""; "_mod"] + in + assert_norm (List.Tot.length l == 2); + Rust_primitives.Hax.array_of_list l)) + (Rust_primitives.unsize (let l = + [ + Core.Fmt.Rt.new_display_under_impl_1 (Alloc.Str.to_uppercase_under_impl_5 ( + Core.Ops.Deref.Deref.deref (Alloc.String.ToString.to_string ident) + )) + ] + in + assert_norm (List.Tot.length l == 1); + Rust_primitives.Hax.array_of_list l))) + in + let mod_name:Proc_macro2.t_Ident = + Proc_macro2.new_under_impl_31 (Core.Ops.Deref.Deref.deref res) + (Proc_macro2.span_under_impl_31 ident) + in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_pound _s in + let hoist8:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "derive" in + let hoist5:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Clone" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Copy" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "PartialEq" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Eq" in + let hoist4:Proc_macro2.t_TokenStream = _s in + let hoist6:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist5 Proc_macro2.Delimiter_Parenthesis hoist4 + in + let _s:Proc_macro2.t_TokenStream = hoist6 in + let hoist7:Proc_macro2.t_TokenStream = _s in + let hoist9:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist8 Proc_macro2.Delimiter_Bracket hoist7 + in + let _s:Proc_macro2.t_TokenStream = hoist9 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#pub" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#struct" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist14:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let hoist11:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist10:Proc_macro2.t_TokenStream = _s in + let hoist12:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist11 Proc_macro2.Delimiter_Bracket hoist10 + in + let _s:Proc_macro2.t_TokenStream = hoist12 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let hoist13:Proc_macro2.t_TokenStream = _s in + let hoist15:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist14 Proc_macro2.Delimiter_Brace hoist13 + in + let _s:Proc_macro2.t_TokenStream = hoist15 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_pound _s in + let hoist20:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "allow" in + let hoist17:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "non_snake_case" in + let hoist16:Proc_macro2.t_TokenStream = _s in + let hoist18:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist17 Proc_macro2.Delimiter_Parenthesis hoist16 + in + let _s:Proc_macro2.t_TokenStream = hoist18 in + let hoist19:Proc_macro2.t_TokenStream = _s in + let hoist21:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist20 Proc_macro2.Delimiter_Bracket hoist19 + in + let _s:Proc_macro2.t_TokenStream = hoist21 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#mod" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens mod_name _s in + let hoist133:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#use" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "super" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_star _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#const" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens const_name _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let hoist23:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist22:Proc_macro2.t_TokenStream = _s in + let hoist24:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist23 Proc_macro2.Delimiter_Bracket hoist22 + in + let _s:Proc_macro2.t_TokenStream = hoist24 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let hoist27:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _i:usize = 0sz in + let has_iter:Quote.__private.t_ThereIsNoIteratorInRepetition = + Quote.__private.ThereIsNoIteratorInRepetition + in + let mod_iter1, i:(Core.Slice.Iter.t_Iter u8 & Quote.__private.t_HasIterator) = + Quote.__private.Ext.RepIteratorExt.quote_into_iter mod_iter1 + in + let has_iter = has_iter |. i in + let (_: Quote.__private.t_HasIterator):Quote.__private.t_HasIterator = has_iter in + let _i, _s, mod_iter1:(Prims.unit & Proc_macro2.t_TokenStream & Core.Slice.Iter.t_Iter u8) = + Rust_primitives.Hax.failure "" + "{\n (loop {\n |Tuple3(_i, _s, mod_iter1)| {\n (if true {\n {\n let Tuple2(todo_fresh_var, mod_iter1_temp): tuple2<\n core::option::Option,\n core::slice::iter::Iter,\n > = { core::iter::traits::iterator::Iterator::next(mod_iter1) };\n {\n let mod_iter1: core::slice::iter::Iter = { mod_iter1_temp };\n {\n let hoist25: core::option::Option =\n { todo_fresh_var };\n {\n let mod_iter1: quote::__private::RepInterp = {\n (match hoist25 {\n core::option::Option::Some(_x) => {\n quote::__private::RepInterp(_x)\n }\n core::option::Option::None => {\n rust_primitives::hax::failure(\n \"\",\n \"(break (Tuple0))\",\n )\n }\n })\n };\n {\n let _s: proc_macro2::TokenStream = {\n (if core::cmp::PartialOrd::gt(_i, 0) {\n {\n let _s: proc_macro2::TokenStream =\n { quote::__private::push_comma(_s) };\n _s\n }\n } else {\n _s\n })\n };\n {\n let Tuple0: tuple0 =\n { core::ops::arith::Add::add(_i, 1) };\n {\n let _i: tuple0 = { Tuple0 };\n {\n let _s: proc_macro2::TokenStream = {\n quote::to_tokens::ToTokens::to_tokens(\n mod_iter1, _s,\n )\n };\n Tuple3(_i, _s, mod_iter1)\n }\n }\n }\n }\n }\n }\n }\n }\n } else {\n {\n let _: tuple0 = { rust_primitives::hax::failure(\"\", \"(break (Tuple0))\") };\n Tuple3(_i, _s, mod_iter1)\n }\n })\n }\n })(Tuple3(_i, _s, mod_iter1))\n }" + + in + let hoist26:Proc_macro2.t_TokenStream = _s in + let hoist28:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist27 Proc_macro2.Delimiter_Bracket hoist26 + in + let _s:Proc_macro2.t_TokenStream = hoist28 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#static" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens static_name _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "str" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens modulus_string _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "NatMod" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lt _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_gt _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist64:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#const" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "MODULUS" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let hoist30:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist29:Proc_macro2.t_TokenStream = _s in + let hoist31:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist30 Proc_macro2.Delimiter_Bracket hoist29 + in + let _s:Proc_macro2.t_TokenStream = hoist31 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let hoist34:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _i:usize = 0sz in + let has_iter:Quote.__private.t_ThereIsNoIteratorInRepetition = + Quote.__private.ThereIsNoIteratorInRepetition + in + let mod_iter2, i:(Core.Slice.Iter.t_Iter u8 & Quote.__private.t_HasIterator) = + Quote.__private.Ext.RepIteratorExt.quote_into_iter mod_iter2 + in + let has_iter = has_iter |. i in + let (_: Quote.__private.t_HasIterator):Quote.__private.t_HasIterator = has_iter in + let _i, _s, mod_iter2:(Prims.unit & Proc_macro2.t_TokenStream & Core.Slice.Iter.t_Iter u8) = + Rust_primitives.Hax.failure "" + "{\n (loop {\n |Tuple3(_i, _s, mod_iter2)| {\n (if true {\n {\n let Tuple2(todo_fresh_var, mod_iter2_temp): tuple2<\n core::option::Option,\n core::slice::iter::Iter,\n > = { core::iter::traits::iterator::Iterator::next(mod_iter2) };\n {\n let mod_iter2: core::slice::iter::Iter = { mod_iter2_temp };\n {\n let hoist32: core::option::Option =\n { todo_fresh_var };\n {\n let mod_iter2: quote::__private::RepInterp = {\n (match hoist32 {\n core::option::Option::Some(_x) => {\n quote::__private::RepInterp(_x)\n }\n core::option::Option::None => {\n rust_primitives::hax::failure(\n \"\",\n \"(break (Tuple0))\",\n )\n }\n })\n };\n {\n let _s: proc_macro2::TokenStream = {\n (if core::cmp::PartialOrd::gt(_i, 0) {\n {\n let _s: proc_macro2::TokenStream =\n { quote::__private::push_comma(_s) };\n _s\n }\n } else {\n _s\n })\n };\n {\n let Tuple0: tuple0 =\n { core::ops::arith::Add::add(_i, 1) };\n {\n let _i: tuple0 = { Tuple0 };\n {\n let _s: proc_macro2::TokenStream = {\n quote::to_tokens::ToTokens::to_tokens(\n mod_iter2, _s,\n )\n };\n Tuple3(_i, _s, mod_iter2)\n }\n }\n }\n }\n }\n }\n }\n }\n } else {\n {\n let _: tuple0 = { rust_primitives::hax::failure(\"\", \"(break (Tuple0))\") };\n Tuple3(_i, _s, mod_iter2)\n }\n })\n }\n })(Tuple3(_i, _s, mod_iter2))\n }" + + in + let hoist33:Proc_macro2.t_TokenStream = _s in + let hoist35:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist34 Proc_macro2.Delimiter_Bracket hoist33 + in + let _s:Proc_macro2.t_TokenStream = hoist35 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#const" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "MODULUS_STR" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lifetime _s "'static" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "str" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens modulus_string _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#const" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "ZERO" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let hoist37:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist36:Proc_macro2.t_TokenStream = _s in + let hoist38:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist37 Proc_macro2.Delimiter_Bracket hoist36 + in + let _s:Proc_macro2.t_TokenStream = hoist38 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let hoist40:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.parse _s "0u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist39:Proc_macro2.t_TokenStream = _s in + let hoist41:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist40 Proc_macro2.Delimiter_Bracket hoist39 + in + let _s:Proc_macro2.t_TokenStream = hoist41 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "new" in + let hoist46:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let hoist43:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist42:Proc_macro2.t_TokenStream = _s in + let hoist44:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist43 Proc_macro2.Delimiter_Bracket hoist42 + in + let _s:Proc_macro2.t_TokenStream = hoist44 in + let hoist45:Proc_macro2.t_TokenStream = _s in + let hoist47:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist46 Proc_macro2.Delimiter_Parenthesis hoist45 + in + let _s:Proc_macro2.t_TokenStream = hoist47 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let hoist52:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let hoist49:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let hoist48:Proc_macro2.t_TokenStream = _s in + let hoist50:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist49 Proc_macro2.Delimiter_Brace hoist48 + in + let _s:Proc_macro2.t_TokenStream = hoist50 in + let hoist51:Proc_macro2.t_TokenStream = _s in + let hoist53:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist52 Proc_macro2.Delimiter_Brace hoist51 + in + let _s:Proc_macro2.t_TokenStream = hoist53 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let hoist55:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let hoist54:Proc_macro2.t_TokenStream = _s in + let hoist56:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist55 Proc_macro2.Delimiter_Parenthesis hoist54 + in + let _s:Proc_macro2.t_TokenStream = hoist56 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let hoist58:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let hoist57:Proc_macro2.t_TokenStream = _s in + let hoist59:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist58 Proc_macro2.Delimiter_Bracket hoist57 + in + let _s:Proc_macro2.t_TokenStream = hoist59 in + let hoist61:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let hoist60:Proc_macro2.t_TokenStream = _s in + let hoist62:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist61 Proc_macro2.Delimiter_Brace hoist60 + in + let _s:Proc_macro2.t_TokenStream = hoist62 in + let hoist63:Proc_macro2.t_TokenStream = _s in + let hoist65:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist64 Proc_macro2.Delimiter_Brace hoist63 + in + let _s:Proc_macro2.t_TokenStream = hoist65 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "convert" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "AsRef" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lt _s in + let hoist67:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let hoist66:Proc_macro2.t_TokenStream = _s in + let hoist68:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist67 Proc_macro2.Delimiter_Bracket hoist66 + in + let _s:Proc_macro2.t_TokenStream = hoist68 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_gt _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist79:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "as_ref" in + let hoist70:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let hoist69:Proc_macro2.t_TokenStream = _s in + let hoist71:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist70 Proc_macro2.Delimiter_Parenthesis hoist69 + in + let _s:Proc_macro2.t_TokenStream = hoist71 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let hoist73:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let hoist72:Proc_macro2.t_TokenStream = _s in + let hoist74:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist73 Proc_macro2.Delimiter_Bracket hoist72 + in + let _s:Proc_macro2.t_TokenStream = hoist74 in + let hoist76:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let hoist75:Proc_macro2.t_TokenStream = _s in + let hoist77:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist76 Proc_macro2.Delimiter_Brace hoist75 + in + let _s:Proc_macro2.t_TokenStream = hoist77 in + let hoist78:Proc_macro2.t_TokenStream = _s in + let hoist80:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist79 Proc_macro2.Delimiter_Brace hoist78 + in + let _s:Proc_macro2.t_TokenStream = hoist80 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fmt" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Display" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist91:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fmt" in + let hoist82:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "f" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_and _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#mut" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fmt" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Formatter" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lt _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lifetime _s "'_" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_gt _s in + let hoist81:Proc_macro2.t_TokenStream = _s in + let hoist83:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist82 Proc_macro2.Delimiter_Parenthesis hoist81 + in + let _s:Proc_macro2.t_TokenStream = hoist83 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fmt" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Result" in + let hoist88:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "write" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_bang _s in + let hoist85:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "f" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.parse _s "\"{}\"" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "to_hex" in + let _s:Proc_macro2.t_TokenStream = + Quote.__private.push_group _s Proc_macro2.Delimiter_Parenthesis Proc_macro2.new_under_impl + in + let hoist84:Proc_macro2.t_TokenStream = _s in + let hoist86:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist85 Proc_macro2.Delimiter_Parenthesis hoist84 + in + let _s:Proc_macro2.t_TokenStream = hoist86 in + let hoist87:Proc_macro2.t_TokenStream = _s in + let hoist89:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist88 Proc_macro2.Delimiter_Brace hoist87 + in + let _s:Proc_macro2.t_TokenStream = hoist89 in + let hoist90:Proc_macro2.t_TokenStream = _s in + let hoist92:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist91 Proc_macro2.Delimiter_Brace hoist90 + in + let _s:Proc_macro2.t_TokenStream = hoist92 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Into" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_lt _s in + let hoist94:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist93:Proc_macro2.t_TokenStream = _s in + let hoist95:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist94 Proc_macro2.Delimiter_Bracket hoist93 + in + let _s:Proc_macro2.t_TokenStream = hoist95 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_gt _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist106:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "into" in + let hoist97:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let hoist96:Proc_macro2.t_TokenStream = _s in + let hoist98:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist97 Proc_macro2.Delimiter_Parenthesis hoist96 + in + let _s:Proc_macro2.t_TokenStream = hoist98 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let hoist100:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "u8" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens num_bytes _s in + let hoist99:Proc_macro2.t_TokenStream = _s in + let hoist101:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist100 Proc_macro2.Delimiter_Bracket hoist99 + in + let _s:Proc_macro2.t_TokenStream = hoist101 in + let hoist103:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "value" in + let hoist102:Proc_macro2.t_TokenStream = _s in + let hoist104:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist103 Proc_macro2.Delimiter_Brace hoist102 + in + let _s:Proc_macro2.t_TokenStream = hoist104 in + let hoist105:Proc_macro2.t_TokenStream = _s in + let hoist107:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist106 Proc_macro2.Delimiter_Brace hoist105 + in + let _s:Proc_macro2.t_TokenStream = hoist107 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "ops" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Add" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist118:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#type" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Output" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "add" in + let hoist109:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "rhs" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let hoist108:Proc_macro2.t_TokenStream = _s in + let hoist110:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist109 Proc_macro2.Delimiter_Parenthesis hoist108 + in + let _s:Proc_macro2.t_TokenStream = hoist110 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Output" in + let hoist115:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fadd" in + let hoist112:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "rhs" in + let hoist111:Proc_macro2.t_TokenStream = _s in + let hoist113:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist112 Proc_macro2.Delimiter_Parenthesis hoist111 + in + let _s:Proc_macro2.t_TokenStream = hoist113 in + let hoist114:Proc_macro2.t_TokenStream = _s in + let hoist116:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist115 Proc_macro2.Delimiter_Brace hoist114 + in + let _s:Proc_macro2.t_TokenStream = hoist116 in + let hoist117:Proc_macro2.t_TokenStream = _s in + let hoist119:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist118 Proc_macro2.Delimiter_Brace hoist117 + in + let _s:Proc_macro2.t_TokenStream = hoist119 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#impl" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "core" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "ops" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Mul" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#for" in + let _s:Proc_macro2.t_TokenStream = Quote.To_tokens.ToTokens.to_tokens ident _s in + let hoist130:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#type" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Output" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_eq _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_semi _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "r#fn" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "mul" in + let hoist121:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_comma _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "rhs" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let hoist120:Proc_macro2.t_TokenStream = _s in + let hoist122:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist121 Proc_macro2.Delimiter_Parenthesis hoist120 + in + let _s:Proc_macro2.t_TokenStream = hoist122 in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_rarrow _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_colon2 _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "Output" in + let hoist127:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "self" in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_dot _s in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "fmul" in + let hoist124:Proc_macro2.t_TokenStream = _s in + let _s:Proc_macro2.t_TokenStream = Proc_macro2.new_under_impl in + let _s:Proc_macro2.t_TokenStream = Quote.__private.push_ident _s "rhs" in + let hoist123:Proc_macro2.t_TokenStream = _s in + let hoist125:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist124 Proc_macro2.Delimiter_Parenthesis hoist123 + in + let _s:Proc_macro2.t_TokenStream = hoist125 in + let hoist126:Proc_macro2.t_TokenStream = _s in + let hoist128:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist127 Proc_macro2.Delimiter_Brace hoist126 + in + let _s:Proc_macro2.t_TokenStream = hoist128 in + let hoist129:Proc_macro2.t_TokenStream = _s in + let hoist131:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist130 Proc_macro2.Delimiter_Brace hoist129 + in + let _s:Proc_macro2.t_TokenStream = hoist131 in + let hoist132:Proc_macro2.t_TokenStream = _s in + let hoist134:Proc_macro2.t_TokenStream = + Quote.__private.push_group hoist133 Proc_macro2.Delimiter_Brace hoist132 + in + let _s:Proc_macro2.t_TokenStream = hoist134 in + let out_struct:Proc_macro2.t_TokenStream = _s in + Core.Convert.Into.into out_struct)) + +let v___: Prims.unit = () \ No newline at end of file diff --git a/poly1305-rust/natmod/src/lib.rs b/natmod/src/lib.rs similarity index 93% rename from poly1305-rust/natmod/src/lib.rs rename to natmod/src/lib.rs index 404a421..cafe644 100644 --- a/poly1305-rust/natmod/src/lib.rs +++ b/natmod/src/lib.rs @@ -63,7 +63,7 @@ pub fn nat_mod(attr: TokenStream, item: TokenStream) -> TokenStream { ); let out_struct = quote! { - #[derive(Clone, Copy, PartialEq, Eq)] + #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct #ident { value: [u8; #num_bytes], } @@ -119,7 +119,6 @@ pub fn nat_mod(attr: TokenStream, item: TokenStream) -> TokenStream { } } - impl core::ops::Mul for #ident { type Output = Self; @@ -127,6 +126,14 @@ pub fn nat_mod(attr: TokenStream, item: TokenStream) -> TokenStream { self.fmul(rhs) } } + + impl core::ops::Sub for #ident { + type Output = Self; + + fn sub(self, rhs: Self) -> Self::Output { + self.fsub(rhs) + } + } } }; diff --git a/poly1305-rust/natmod/tests/poly1305.rs b/natmod/tests/poly1305.rs similarity index 98% rename from poly1305-rust/natmod/tests/poly1305.rs rename to natmod/tests/poly1305.rs index 4e27590..1667478 100644 --- a/poly1305-rust/natmod/tests/poly1305.rs +++ b/natmod/tests/poly1305.rs @@ -10,6 +10,13 @@ pub trait NatMod { fn new(value: [u8; LEN]) -> Self; fn value(&self) -> &[u8]; + fn fsub(self, rhs: Self) -> Self + where + Self: Sized, + { + todo!() + } + /// Add self with `rhs` and return the result `self + rhs % MODULUS`. fn fadd(self, rhs: Self) -> Self where diff --git a/poly1305-rust/Cargo.toml b/poly1305-rust/Cargo.toml index 0ea01a0..b1a907e 100644 --- a/poly1305-rust/Cargo.toml +++ b/poly1305-rust/Cargo.toml @@ -13,7 +13,7 @@ path = "src/poly1305.rs" [dependencies] num-bigint = "0.4" -natmod = { path = "./natmod" } +natmod = { path = "../natmod" } [dev-dependencies] serde_json = "1.0" diff --git a/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst b/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst index e5516bc..ee355e6 100644 --- a/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst +++ b/poly1305-rust/proofs/fstar/extraction/Poly1305.FIELDELEMENT_mod.fst @@ -65,4 +65,13 @@ let impl: Core.Ops.Arith.t_Mul Poly1305.t_FieldElement Poly1305.t_FieldElement = = fun (self: Poly1305.t_FieldElement) (rhs: Poly1305.t_FieldElement) -> Poly1305.Hacspec_helper.NatMod.fmul self rhs + } + +let impl: Core.Ops.Arith.t_Sub Poly1305.t_FieldElement Poly1305.t_FieldElement = + { + output = Poly1305.t_FieldElement; + sub + = + fun (self: Poly1305.t_FieldElement) (rhs: Poly1305.t_FieldElement) -> + Poly1305.Hacspec_helper.NatMod.fsub self rhs } \ No newline at end of file diff --git a/poly1305-rust/proofs/fstar/extraction/Poly1305.fst b/poly1305-rust/proofs/fstar/extraction/Poly1305.fst index 8905cd3..45fe530 100644 --- a/poly1305-rust/proofs/fstar/extraction/Poly1305.fst +++ b/poly1305-rust/proofs/fstar/extraction/Poly1305.fst @@ -28,19 +28,27 @@ let poly1305_encode_r (b: array u8 16sz) : t_FieldElement = Poly1305.Hacspec_helper.NatMod.from_u128 n let poly1305_encode_block (b: array u8 16sz) : _ = - let f:t_FieldElement = Poly1305.Hacspec_helper.NatMod.from_le_bytes (Rust_primitives.unsize b) in - f +. Poly1305.Hacspec_helper.NatMod.pow2 128sz + let f:t_FieldElement = + Poly1305.Hacspec_helper.NatMod.from_le_bytes (Rust_primitives.unsize b <: slice u8) + in + f +. (Poly1305.Hacspec_helper.NatMod.pow2 128sz <: t_FieldElement) let poly1305_encode_last (pad_len: usize) (b: slice u8) : _ = let f:t_FieldElement = Poly1305.Hacspec_helper.NatMod.from_le_bytes b in - f +. Poly1305.Hacspec_helper.NatMod.pow2 (8sz *. pad_len) + f +. (Poly1305.Hacspec_helper.NatMod.pow2 (8sz *. pad_len <: usize) <: t_FieldElement) let poly1305_init (key: array u8 32sz) : t_PolyState = let r:t_FieldElement = - poly1305_encode_r (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into key.[ { - Core.Ops.Range.Range.f_start = 0sz; - Core.Ops.Range.Range.f_end = 16sz - } ])) + poly1305_encode_r (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into (key.[ { + Core.Ops.Range.Range.f_start = 0sz; + Core.Ops.Range.Range.f_end = 16sz + } ] + <: + slice u8) + <: + Core.Result.t_Result (array u8 16sz) _) + <: + array u8 16sz) in { Poly1305.PolyState.f_acc = Poly1305.Hacspec_helper.NatMod.zero; @@ -54,7 +62,8 @@ let poly1305_update_block (b: array u8 16sz) (st: t_PolyState) : t_PolyState = st with Poly1305.PolyState.f_acc = - (poly1305_encode_block b +. st.Poly1305.PolyState.f_acc) *. st.Poly1305.PolyState.f_r + ((poly1305_encode_block b <: t_FieldElement) +. st.Poly1305.PolyState.f_acc <: _) *. + st.Poly1305.PolyState.f_r } in st @@ -63,26 +72,35 @@ let poly1305_update_blocks (m: slice u8) (st: t_PolyState) : t_PolyState = let st:t_PolyState = Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter (Core.Slice.chunks_exact_under_impl m - v_BLOCKSIZE)) + v_BLOCKSIZE + <: + Core.Slice.Iter.t_ChunksExact u8) + <: + _) st (fun st chunk -> - poly1305_update_block (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into chunk) - ) - st) + poly1305_update_block (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into chunk + <: + Core.Result.t_Result (array u8 16sz) _) + <: + array u8 16sz) + st + <: + t_PolyState) in st let poly1305_update_last (pad_len: usize) (b: slice u8) (st: t_PolyState) : t_PolyState = let st:t_PolyState = st in let st:t_PolyState = - if Core.Slice.len_under_impl b <>. 0sz + if (Core.Slice.len_under_impl b <: usize) <>. 0sz then let st:t_PolyState = { st with Poly1305.PolyState.f_acc = - (poly1305_encode_last pad_len b +. st.Poly1305.PolyState.f_acc) *. + ((poly1305_encode_last pad_len b <: t_FieldElement) +. st.Poly1305.PolyState.f_acc <: _) *. st.Poly1305.PolyState.f_r } in @@ -94,24 +112,38 @@ let poly1305_update_last (pad_len: usize) (b: slice u8) (st: t_PolyState) : t_Po let poly1305_update (m: slice u8) (st: t_PolyState) : t_PolyState = let st:t_PolyState = poly1305_update_blocks m st in let last:slice u8 = - Core.Slice.Iter.remainder_under_impl_87 (Core.Slice.chunks_exact_under_impl m v_BLOCKSIZE) + Core.Slice.Iter.remainder_under_impl_87 (Core.Slice.chunks_exact_under_impl m v_BLOCKSIZE + <: + Core.Slice.Iter.t_ChunksExact u8) in - poly1305_update_last (Core.Slice.len_under_impl last) last st + poly1305_update_last (Core.Slice.len_under_impl last <: usize) last st let poly1305_finish (st: t_PolyState) : array u8 16sz = let n:u128 = Core.Num.from_le_bytes_under_impl_10 (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into - st.Poly1305.PolyState.f_key.[ { - Core.Ops.Range.Range.f_start = 16sz; - Core.Ops.Range.Range.f_end = 32sz - } ])) + (st.Poly1305.PolyState.f_key.[ { + Core.Ops.Range.Range.f_start = 16sz; + Core.Ops.Range.Range.f_end = 32sz + } ] + <: + slice u8) + <: + Core.Result.t_Result (array u8 16sz) _) + <: + array u8 16sz) in let aby:array u8 17sz = Poly1305.Hacspec_helper.NatMod.to_le_bytes st.Poly1305.PolyState.f_acc in let a:u128 = Core.Num.from_le_bytes_under_impl_10 (Core.Result.unwrap_under_impl (Core.Convert.TryInto.try_into - aby.[ { Core.Ops.Range.Range.f_start = 0sz; Core.Ops.Range.Range.f_end = 16sz } ])) + (aby.[ { Core.Ops.Range.Range.f_start = 0sz; Core.Ops.Range.Range.f_end = 16sz } ] + <: + slice u8) + <: + Core.Result.t_Result (array u8 16sz) _) + <: + array u8 16sz) in - Core.Num.to_le_bytes_under_impl_10 (Core.Num.wrapping_add_under_impl_10 a n) + Core.Num.to_le_bytes_under_impl_10 (Core.Num.wrapping_add_under_impl_10 a n <: u128) let poly1305 (m: slice u8) (key: array u8 32sz) : array u8 16sz = let st:t_PolyState = poly1305_init key in diff --git a/poly1305-rust/src/hacspec_helper.rs b/poly1305-rust/src/hacspec_helper.rs index 445bd57..015fb02 100644 --- a/poly1305-rust/src/hacspec_helper.rs +++ b/poly1305-rust/src/hacspec_helper.rs @@ -8,6 +8,13 @@ pub trait NatMod { fn new(value: [u8; LEN]) -> Self; fn value(&self) -> &[u8]; + fn fsub(self, _rhs: Self) -> Self + where + Self: Sized, + { + todo!() + } + /// Add self with `rhs` and return the result `self + rhs % MODULUS`. fn fadd(self, rhs: Self) -> Self where