Skip to content

Commit caa053c

Browse files
RobinJadoulerik-3milabs
RobinJadoul
and
erik-3milabs
authored
spec: SHA256 accelerator (#372)
* spec: First sha256 accelerator draft * Types checked * Update typst description * HWSLC -> HWSL * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * preliminary changes after review * fix out_e carry check * rotxor with 2 fewer columns * Correct count of bytes for out range checks * Explicit tables for SHA256_K * whoops * cosmetic + explanation * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Update spec/sha256.typ * Replace base_addr by entry in addr * review comments * structure * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Update spec/sha256.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec/sha256: rebase fixes --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Erik Takke <erik.takke@3milabs.tech>
1 parent 7b42e51 commit caa053c

9 files changed

Lines changed: 1180 additions & 0 deletions

File tree

‎spec/book.typ‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@
4242
("about_ecalls.typ", [About `ECALL`], <ecall>),
4343
("halt.typ", [`HALT` chip], <halt>),
4444
("commit.typ", [`COMMIT` chip], <commit>),
45+
("sha256.typ", [`SHA256` accelerator], <sha256>),
4546
))
4647
)
4748
)

‎spec/sha256.typ‎

Lines changed: 204 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
1+
#import "/book.typ": book-page, aside, rj
2+
#import "/src.typ": load_config, load_chip
3+
#import "/chip.typ": (
4+
render_chip_variable_table,
5+
total_nr_variables,
6+
total_nr_instantiated_columns,
7+
render_constraint_table,
8+
render_chip_assumptions,
9+
render_chip_padding_table,
10+
)
11+
12+
#let config = load_config()
13+
14+
#show: book-page("sha256.typ")
15+
16+
#let sha256chip = load_chip("src/sha256.toml", config)
17+
#let sha256msgschedchip = load_chip("src/sha256msgsched.toml", config)
18+
#let sha256roundchip = load_chip("src/sha256round.toml", config)
19+
#let rotxorchip = load_chip("src/rotxor.toml", config)
20+
#let sha256 = raw(sha256chip.name)
21+
#let sha256msgsched = raw(sha256msgschedchip.name)
22+
#let sha256round = raw(sha256roundchip.name)
23+
#let rotxor = raw(rotxorchip.name)
24+
25+
The following chips constitute an accelerator for the SHA256 compression function;
26+
other aspects of SHA256 hashing (such as repeated compression invocation,
27+
input padding and state initialization) fall outside the scope of this accelerator.
28+
29+
The base #sha256 chip provides the `ECALL` interface, interacts with memory and then delegates to the #sha256msgsched and #sha256round chips
30+
to perform the message schedule and the compression rounds, respectively.
31+
The `SHA256_M` interaction signature is used to represent the output of the message schedule.
32+
The `SHA256_K` interaction signature is used to represent the `k` constants.
33+
It could either be instantiated with a (short) precomputed table, or through hardcoded LogUp contributions in this chip.
34+
For this exposition, we choose the former option, and present a table further below.
35+
Additionally, we introduce a #rotxor chip to perform the common action of computing the XOR of three rotations (or shifts) of a word.
36+
37+
Most of the structure and variable naming follows the pseudocode of the wikipedia page#footnote(link("https://web.archive.org/web/20260320010021/https://en.wikipedia.org/wiki/SHA-2#Pseudocode")).
38+
39+
= #sha256 chip
40+
41+
== Columns
42+
#let nr_variables = total_nr_variables(sha256chip)
43+
#let nr_columns = total_nr_instantiated_columns(sha256chip, config)
44+
45+
The #sha256 chip leverages #nr_variables variables, spanning #nr_columns columns:
46+
#render_chip_variable_table(sha256chip, config)
47+
48+
== Constraints
49+
50+
The first responsibility of the chip is to read the current state and message chunk from memory,
51+
passed as arguments through pointers.
52+
Since the memory ranges could overlap, we read the chunk first (in @sha256:c:read_chunk, at timestamp `timestamp`), before reading and writing the state (in @sha256:c:read_state, at timestamp `timestamp + 1`).
53+
The addresses containing the state and the current chunk are passed in as arguments `A0 = x10` and `A1 = x11`, respectively.
54+
Note that following the SHA256 spec, this state and the chunks are read and written as big-endian.
55+
#render_constraint_table(sha256chip, config, groups: "memory")
56+
57+
Then we prepare the message schedule, by emitting the input chunk with multiplicities
58+
corresponding to the number of times it will be read during a compression evaluation.
59+
The #sha256msgsched chip itself is implicitly invoked by itself and #sha256round, setting the `amount`
60+
column appropriately for the number of times the `w` value is required.
61+
#render_constraint_table(sha256chip, config, groups: "sched")
62+
63+
And finally, we provide the boundaries for the #sha256round chip and the
64+
final addition of the compression to the old state.
65+
Observe that we embed the addition into the upper 32 bits of a double word,
66+
in order to satisfy and use the `ADD` chip.
67+
#render_constraint_table(sha256chip, config, groups: "compress")
68+
69+
In this VM, we assign syscall number -1 to the #sha256 accelerator.
70+
The chip therefore contributes the following interaction to the lookup-argument:
71+
#render_constraint_table(sha256chip, config, groups: "lookup")
72+
73+
== Padding
74+
75+
#render_chip_padding_table(sha256chip, config)
76+
77+
= #sha256msgsched chip
78+
79+
== Columns
80+
81+
#let nr_variables = total_nr_variables(sha256msgschedchip)
82+
#let nr_columns = total_nr_instantiated_columns(sha256msgschedchip, config)
83+
84+
The #sha256msgsched chip leverages #nr_variables variables, spanning #nr_columns columns:
85+
#render_chip_variable_table(sha256msgschedchip, config)
86+
87+
== Assumptions
88+
89+
#render_chip_assumptions(sha256msgschedchip, config)
90+
91+
== Constraints
92+
93+
First, we gather the dependencies from earlier in the message schedule.
94+
95+
#render_constraint_table(sha256msgschedchip, config, groups: "lookback")
96+
97+
Then, we calculate the result.
98+
It suffices to check that the carry of adding four range-checked words
99+
into a range-checked word is not too big, following the logic from @add.
100+
In this case, using the `IS_BYTE` constraint allows us to add multiple words together
101+
at the same time, without needing to store and range-check intermediate results.
102+
#render_constraint_table(sha256msgschedchip, config, groups: "calc")
103+
104+
Finally, we contribute to the LogUp.
105+
#render_constraint_table(sha256msgschedchip, config, groups: "output")
106+
107+
= #sha256round chip
108+
109+
== Columns
110+
111+
#let nr_variables = total_nr_variables(sha256roundchip)
112+
#let nr_columns = total_nr_instantiated_columns(sha256roundchip, config)
113+
114+
The #sha256round chip leverages #nr_variables variables, spanning #nr_columns columns:
115+
#render_chip_variable_table(sha256roundchip, config)
116+
117+
== Assumptions
118+
119+
#render_chip_assumptions(sha256roundchip, config)
120+
121+
== Constraints
122+
123+
First, we compute the necessary intermediate values.
124+
#let bitand = math.class("binary", math.amp)
125+
To compute `maj`, observe that $ (a bitand b) xor (a bitand c) xor (b bitand c) = (a bitand b) xor (c bitand (a xor b)), $
126+
by distribution.
127+
Additionally, since for this form, $(a bitand b)$ and $(a xor b)$ are disjoint, so are $(a bitand b)$ and $(c bitand (a xor b))$,
128+
and hence we can replace that top-level XOR with a field addition to compute $(a bitand b) + (c bitand (a xor b))$,
129+
needing fewer intermediate columns.
130+
Similarly, `ch` can be written as $(e bitand f) + ((2^32 - 1 - e) bitand g)$.
131+
#render_constraint_table(sha256roundchip, config, groups: "value")
132+
133+
Then we constrain the addition for the new state, constraining additions with the same `IS_BYTE` trick as before.
134+
#render_constraint_table(sha256roundchip, config, groups: "addition")
135+
136+
Finally, we chain the rounds together through the interactions.
137+
#render_constraint_table(sha256roundchip, config, groups: "output")
138+
139+
== Padding
140+
141+
#render_chip_padding_table(sha256roundchip, config)
142+
143+
= #rotxor chip
144+
145+
146+
This chip takes as input `a`, `r0`, `r1`, `r2` (4-bit values) and a bit `last_rot` to compute
147+
$
148+
cases(
149+
(a >>> (16 + r_0)) xor (a >>> (16 + r_0 - r_1)) xor (a >>> r_2) quad "if" #`last_rot`,
150+
(a >>> (16 + r_0)) xor (a >>> (16 + r_0 - r_1)) xor (a >> r_2) quad "if" #`!last_rot`
151+
),
152+
$
153+
where we let $>>>$ denote right rotation and $>>$ logical shift right.
154+
We choose this representation so that all shift amounts required fit into 4 bits,
155+
making the usage of `HWSL` more straightforward and avoid extra columns to represent more bits.
156+
157+
== Columns
158+
159+
#let nr_variables = total_nr_variables(rotxorchip)
160+
#let nr_columns = total_nr_instantiated_columns(rotxorchip, config)
161+
The #rotxor chip leverages #nr_variables variables, spanning #nr_columns columns:
162+
163+
#render_chip_variable_table(rotxorchip, config)
164+
165+
== Assumptions
166+
167+
Range checking for all elements is inherited from the bitwise lookups.
168+
We can safely assume that no `r_i` will be zero, and avoid extra work due to right rotation needing `16 - shift` as arguments to the `HWSL` interactions.
169+
#render_chip_assumptions(rotxorchip, config)
170+
171+
== Constraints
172+
173+
We first compute all rotations (or shifts) of `a`.
174+
`a1` is computed as a left rotation of `a0`, in order to not need
175+
additional columns to represent the full right-rotation amounts.
176+
#render_constraint_table(rotxorchip, config, groups: "shift")
177+
178+
Then the bitwise XOR of the results.
179+
#render_constraint_table(rotxorchip, config, groups: "xor")
180+
181+
And finally contribute to the lookup argument.
182+
#render_constraint_table(rotxorchip, config, groups: "output")
183+
184+
== Padding
185+
186+
#render_chip_padding_table(rotxorchip, config)
187+
188+
= Constant lookup
189+
190+
#let sha256_kchip = load_chip("src/sha256consts.toml", config)
191+
#let sha256_k = raw(sha256_kchip.name)
192+
193+
As mentioned, we provide the round constants through a short precomputed lookup table: #sha256_k.
194+
195+
#render_chip_variable_table(sha256_kchip, config)
196+
#render_constraint_table(sha256_kchip, config)
197+
198+
= Notes/optimizations
199+
- This could instead be designed following the #link("https://github.com/riscv/riscv-crypto")[RISC-V Crypto Scalar extension `Zknh`],
200+
for wider compatibility, but this design is likely to be more efficient.
201+
It is still possible, if desired, to expose #rotxor (or a selection of parameter instantiations thereof)
202+
as implementation for these primitives.
203+
- The message schedule could be exposed as its own ECALL instead, but the direct integration leads to better efficiency.
204+
- Some of these chips could be made narrower, at the cost of introducing some extra lookups and extra tables to compute and store intermediate results.

‎spec/src/config.toml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,22 @@ desc = """\
9191
The `Word` is the *most* significant digit.
9292
"""
9393

94+
[[variables.types]]
95+
label = "WordBL"
96+
subtypes = ["Byte", "Byte", "Byte", "Byte"]
97+
desc = """\
98+
Variable that can only assume values in the range $[0, 2^32)$. \\
99+
Represented as an array of four `Byte` variables.\
100+
"""
101+
102+
[[variables.types]]
103+
label = "WordHL"
104+
subtypes = ["Half", "Half"]
105+
desc = """\
106+
Variable that can only assume values in the range $[0, 2^32)$. \\
107+
Represented as an array of two `Half` variables.\
108+
"""
109+
94110
[[variables.types]]
95111
label = "QuadHL"
96112
subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"]

0 commit comments

Comments
 (0)