-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathBlake3.lean
154 lines (121 loc) · 5.48 KB
/
Blake3.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
/-! Bindings to the BLAKE3 hashing library. -/
theorem ByteArray.size_of_extract {hash : ByteArray} (hbe : b ≤ e) (h : e ≤ hash.data.size) :
(hash.extract b e).size = e - b := by
simp [ByteArray.size, ByteArray.extract, ByteArray.copySlice, ByteArray.empty, ByteArray.mkEmpty]
rw [Nat.add_comm, Nat.sub_add_cancel hbe, Nat.min_eq_left h]
namespace Blake3
/-- BLAKE3 constants -/
abbrev BLAKE3_OUT_LEN : Nat := 32
abbrev BLAKE3_KEY_LEN : Nat := 32
/-- A wrapper around `ByteArray` whose size is `BLAKE3_OUT_LEN` -/
def Blake3Hash : Type := { r : ByteArray // r.size = BLAKE3_OUT_LEN }
/-- A wrapper around `ByteArray` whose size is `BLAKE3_KEY_LEN` -/
def Blake3Key : Type := { r : ByteArray // r.size = BLAKE3_KEY_LEN }
def Blake3Key.ofBytes (bytes : ByteArray)
(h : bytes.size = BLAKE3_KEY_LEN := by rw [ByteArray.size]; rfl) : Blake3Key :=
⟨bytes, h⟩
instance : Inhabited Blake3Hash where
default := ⟨⟨#[
0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0
]⟩, by rw [ByteArray.size]; rfl⟩
private opaque HasherNonempty : NonemptyType
def Hasher : Type := HasherNonempty.type
instance : Nonempty Hasher := HasherNonempty.property
@[extern "lean_blake3_version"]
protected opaque internalVersion : Unit → String
/-- Version of the linked BLAKE3 implementation library. -/
def version : String := Blake3.internalVersion ()
namespace Hasher
/-- Initialize a hasher. -/
@[extern "lean_blake3_init"]
opaque init : Unit → Hasher
/-- Initialize a hasher using pseudo-random key -/
@[extern "lean_blake3_init_keyed"]
opaque initKeyed (key : @& Blake3Key) : Hasher
@[extern "lean_blake3_init_derive_key"]
opaque initDeriveKey (context : @& ByteArray) : Hasher
/-- Put more data into the hasher. This can be called several times. -/
@[extern "lean_blake3_hasher_update"]
opaque update (hasher : Hasher) (input : @& ByteArray) : Hasher
instance {length : USize} : Inhabited { r : ByteArray // r.size = length.toNat } where
default := ⟨
⟨⟨List.replicate length.toNat 0⟩⟩,
by simp only [ByteArray.size, List.toArray_replicate, Array.size_mkArray]
⟩
/-- Finalize the hasher and write the output to an array of a given length. -/
@[extern "lean_blake3_hasher_finalize"]
opaque finalize : (hasher : Hasher) → (length : USize) →
{r : ByteArray // r.size = length.toNat}
def finalizeWithLength (hasher : Hasher) (length : Nat)
(h : length % 2 ^ System.Platform.numBits = length := by native_decide) :
{ r : ByteArray // r.size = length } :=
let ⟨hash, h'⟩ := hasher.finalize length.toUSize
have hash_size_eq_len : hash.size = length := by
cases System.Platform.numBits_eq with
| inl h32 => rw [h32] at h; simp [h', h32]; exact h
| inr h64 => rw [h64] at h; simp [h', h64]; exact h
⟨hash, hash_size_eq_len⟩
end Hasher
/-- Hash a ByteArray -/
def hash (input : ByteArray) : Blake3Hash :=
let hasher := Hasher.init ()
let hasher := hasher.update input
hasher.finalizeWithLength BLAKE3_OUT_LEN
/-- Hash a ByteArray using keyed initializer -/
def hashKeyed (input : @& ByteArray) (key : @& Blake3Key) : Blake3Hash :=
let hasher := Hasher.initKeyed key
let hasher := hasher.update input
hasher.finalizeWithLength BLAKE3_OUT_LEN
/-- Hash a ByteArray using initializer parameterized by some context -/
def hashDeriveKey (input context : @& ByteArray) : Blake3Hash :=
let hasher := Hasher.initDeriveKey context
let hasher := hasher.update input
hasher.finalizeWithLength BLAKE3_OUT_LEN
structure Sponge where
hasher : Hasher
counter : Nat
namespace Sponge
abbrev ABSORB_MAX_BYTES := UInt32.size - 1
abbrev DEFAULT_REKEYING_STAGE := UInt16.size - 1
def init (label : String) (_h : ¬label.isEmpty := by decide) : Sponge :=
⟨Hasher.initDeriveKey label.toUTF8, 0⟩
def ratchet (sponge : Sponge) : Sponge :=
let key := sponge.hasher.finalizeWithLength BLAKE3_KEY_LEN
{ sponge with hasher := Hasher.initKeyed key, counter := 0 }
def absorb (sponge : Sponge) (bytes : ByteArray)
(_h : bytes.size < ABSORB_MAX_BYTES := by norm_cast) : Sponge :=
let highCounter := sponge.counter >= DEFAULT_REKEYING_STAGE
let sponge := if highCounter then sponge.ratchet else sponge
⟨sponge.hasher.update bytes, sponge.counter + 1⟩
def squeeze (sponge : Sponge) (length : USize)
(h_len_bound : 2 * BLAKE3_OUT_LEN + length.toNat < 2 ^ System.Platform.numBits :=
by native_decide) :
{ r : ByteArray // r.size = length.toNat } :=
let ⟨tmp, h⟩ := sponge.hasher.finalize (2 * BLAKE3_OUT_LEN.toUSize + length)
let b := (2 * BLAKE3_OUT_LEN)
let e := (2 * BLAKE3_OUT_LEN + length.toNat)
let y := tmp.extract b e
have sub_e_b_eq_length : e - b = length.toNat := by
simp only [b, e]
rw [Nat.add_comm _ length.toNat, Nat.add_sub_cancel]
have le_b_e : b ≤ e := by simp only [Nat.le_add_right, e, b]
have h_e_bound : e ≤ tmp.size := by
simp [e, h]
cases System.Platform.numBits_eq with
| inl h32 =>
have hbound : (2 * BLAKE3_OUT_LEN) + length.toNat < 2 ^ 32 := by
rwa [h32, Nat.pow_succ] at h_len_bound
rw [h32, BLAKE3_OUT_LEN]
simp only [Nat.mod_eq_of_lt hbound, Nat.le_refl]
| inr h64 =>
have hbound : (2 * BLAKE3_OUT_LEN) + length.toNat < 2 ^ 64 := by
rwa [h64, Nat.pow_succ] at h_len_bound
rw [h64, BLAKE3_OUT_LEN]
simp only [Nat.mod_eq_of_lt hbound, Nat.le_refl]
have size_of_extract := ByteArray.size_of_extract le_b_e h_e_bound
⟨y, by simp only [y, size_of_extract, sub_e_b_eq_length]⟩
end Sponge
end Blake3