From b257b912ee9daaf3be4e6a098df2899aadb773a1 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 15:19:33 +0200 Subject: [PATCH 01/25] spec: math/code render mod expr --- spec/expr.typ | 47 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/spec/expr.typ b/spec/expr.typ index 2de0d6ba3..a383c1891 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -1,20 +1,26 @@ // Types and array types // ::= str -// | [str, int] +// | [, int] // Check that a type expression is structurally valid, without validating against a set of known base types #let check_array_type(typ) = { + while type(typ) == array { + assert(typ.len() == 2, message: "Array types must specify two parameters") + assert(type(typ.at(1)) == int, message: "Array types need to have a constant dimension") + typ = typ.at(0) + } assert(type(typ.at(0)) == str, message: "Array types need to have a regular type as base") - assert(type(typ.at(1)) == int, message: "Array types need to have a constant dimension") } // Render a type to code #let type_to_code(typ) = { - if type(typ) == array { - check_array_type(typ) - return raw(typ.at(0) + "[" + str(typ.at(1)) + "]") - } else if type(typ) == str { - return raw(typ) + let label = "" + while type(typ) == array { + label += "[" + str(typ.at(1)) + "]" + typ = typ.at(0) + } + if type(typ) == str { + return raw(typ + label) } else { assert(false, message: "Unknown format for type: " + repr(typ)) } @@ -54,12 +60,13 @@ "cast": 3, // cast "mul": 4, // * "div": 5, // / - "sum": 6, // Σ - "not": 7, // not - "sub": 8, // - - "add": 9, // + - "eq": 10, // = and := - "MAX": 11, // + "mod": 6, // % + "sum": 7, // Σ + "not": 8, // not + "sub": 9, // - + "add": 10, // + + "eq": 11, // = and := + "MAX": 12, // ) // Mutual recursion through a trick from https://github.com/typst/typst/issues/744 @@ -97,6 +104,13 @@ "not": (pp, rec, e) => cwrap(rec(PREC.not, 1) + ` - ` + rec(PREC.not, e.at(1)), pp < PREC.not), "+": (pp, rec, e) => cwrap(e.slice(1).map(rec.with(PREC.add)).join(` + `), pp < PREC.add), "sum": (pp, rec, e) => assert(false, message: "sum is unsupported in code."), + "mod": (pp, rec, e) => { + assert(e.len() == 3 and type(e.at(2)) == int, message: "Invalid mod expr: " + repr(e)) + cwrap( + rec(PREC.mod, e.at(1)) + `%` + rec(PREC.mod, e.at(2)), + pp <= PREC.mod + ) + }, "*": (pp, rec, e) => { if e.len() == 3 and type(e.at(1)) == int and type(e.at(2)) == str and e.at(2).len() == 1 { // multiplication of a constant with one-letter variable. @@ -165,6 +179,13 @@ pp <= PREC.sub ) }, + "mod": (pp, rec, e) => { + assert(e.len() == 3 and type(e.at(2)) == int, message: "Invalid mod expr: " + repr(e)) + mwrap( + $#rec(PREC.mod, e.at(1)) mod #rec(PREC.mod, e.at(2))$, + pp <= PREC.mod + ) + }, "*": (pp, rec, e) => { if e.len() == 3 and type(e.at(1)) == int and type(e.at(2)) == str and e.at(2).len() == 1 { // multiplication of a constant with one-letter variable. From 98a685c4c6ce674c91cf43181c65103fb4c36343 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 22:03:55 +0200 Subject: [PATCH 02/25] spec/type_check: add ModExpr --- spec/tooling/chip.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index d597d2274..f682601e2 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -255,6 +255,28 @@ def typecheck(self, env: Environment) -> Type: return t +@dataclass +class ModExpr: + elt: Expr + modulus: Expr + + def typecheck(self, env: Environment) -> Type: + elt = self.elt.typecheck(env) + modulus = self.modulus.typecheck(env) + + if isinstance(modulus, list) or not modulus.is_const(): + reporter.error(f"Invalid non-constant modulus: {self.modulus!r}") + modulus = modulus.get_const() + if modulus <= 0: + reporter.error(f"Invalid zero non-positive modulus: {self.modulus!r}") + + if elt.is_const(): + elt = elt.get_const() + return Range.const(elt % modulus) + else: + return Range(0, modulus-1) + + @dataclass class PowExpr: base: Expr @@ -343,6 +365,8 @@ def build_expr(config: Optional["Config"], data: object) -> Expr: return SubExpr( build_expr(config, head), [build_expr(config, s) for s in subs] ) + case ["mod", elt, modulus]: + return ModExpr(build_expr(config, elt), build_expr(config, modulus)) case ["^", base, exp]: return PowExpr(build_expr(config, base), build_expr(config, exp)) case ["sum", ["=", str(var), start], stop, terms]: From 64abef7589bfaf76c422fcdb15205f63dd18a034 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 11:46:14 +0200 Subject: [PATCH 03/25] spec: add multi-dimensional array support --- spec/chip.typ | 13 ++++++++----- spec/src.typ | 11 +++++------ 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index f3e0892f7..abb6b1b63 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -14,12 +14,15 @@ .map(pair => pair.at(1)) .flatten() .map(var => { - let (label, factor) = if type(var.type) == array { - (var.type.at(0), var.type.at(1)) - } else { - (var.type, 1) + let (factor, var_type) = (1, var.type) + while type(var_type) == array { + assert(var_type.len() == 2, message: "invalid var (sub)type length: " + repr(var.type)) + assert(type(var_type.at(1)) == int, message: "invalid var (sub)type length: " + repr(var.type)) + factor *= var_type.at(1) + var_type = var_type.at(0) } - config.variables.types.filter(type => type.label == label).first().subtypes.len() * factor + + config.variables.types.filter(type => type.label == var_type).first().subtypes.len() * factor }) .sum() } diff --git a/spec/src.typ b/spec/src.typ index 6328c4665..7d5f15979 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -104,14 +104,13 @@ let all_vars = chip.variables.values().flatten() let all_labels = config.variables.types.map(type => type.label); for var in all_vars { - let type_label = if type(var.type) == array { - var.type.at(0) - } else { - var.type + let type_label = var.type + while type(type_label) == array { + assert(type_label.len() == 2 and type(type_label.at(1)) == int, message: "invalid type: " + repr(var.type)) + type_label = type_label.at(0) } - // Check that all variable types are valid - assert(type_label in all_labels, message: "found invalid var type:" + repr(var.type)) + assert(type_label in all_labels, message: "found invalid var type: " + repr(var.type)) } } From 4bb8747149529104d4467d895d2672a5c5802666 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 11:46:25 +0200 Subject: [PATCH 04/25] spec/KECCAK: introduce v0 --- spec/book.typ | 1 + spec/chip.typ | 2 +- spec/keccak.typ | 65 +++++++++ spec/src/keccak.toml | 87 ++++++++++++ spec/src/keccak_round.toml | 265 +++++++++++++++++++++++++++++++++++++ 5 files changed, 419 insertions(+), 1 deletion(-) create mode 100644 spec/keccak.typ create mode 100644 spec/src/keccak.toml create mode 100644 spec/src/keccak_round.toml diff --git a/spec/book.typ b/spec/book.typ index 3de02e363..3b65642f9 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -43,6 +43,7 @@ ("halt.typ", [`HALT` chip], ), ("commit.typ", [`COMMIT` chip], ), ("sha256.typ", [`SHA256` accelerator], ), + ("keccak.typ", [`KECCAK` accelerator], ), )) ) ) diff --git a/spec/chip.typ b/spec/chip.typ index abb6b1b63..c6cce5073 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -293,7 +293,7 @@ } else if type(groups) == str { groups = (groups,) } - assert(groups.all(group => group in all_groups), message: "unknown group") + assert(groups.all(group => group in all_groups), message: "unknown group: " + repr(groups)) let selected_constraints = groups.map(g => ((g): chip.constraints.at(g))).join() // Find the group definition in the constraint_groups diff --git a/spec/keccak.typ b/spec/keccak.typ new file mode 100644 index 000000000..9dce69adf --- /dev/null +++ b/spec/keccak.typ @@ -0,0 +1,65 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_padding_table, +) + +#let config = load_config() +#let chip = load_chip("src/keccak.toml", config) + +#show: book-page(chip.name) +#let keccak = raw(chip.name) + +The #keccak chip applies the keccak permutation. + += Core chip +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #keccak chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_variable_table(chip, config) + +== Assumptions + +// #render_chip_assumptions(chip, config) + +== Constraints +In this VM, we assign syscall number -2 to the #keccak accelerator. +The chip therefore contributes the following interaction to the lookup-argument: +#render_constraint_table(chip, config, groups: "output") + +The address containing the state to be permuted are passed in as argument `A0 = x10`. +This address is read into `addr`, from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived. +The state is then read into `input_state`, while the `output_state` is written back to the indicated address. +#render_constraint_table(chip, config, groups: "mem") + +Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus. +#render_constraint_table(chip, config, groups: "round") + +== Padding + +The table can be padded to the next power of two with the following value assignments: + +// #render_chip_padding_table(chip, config) + += Round chip +#let round_chip = load_chip("src/keccak_round.toml", config) +#let keccak_rnd = raw(round_chip.name) + +== Columns +#let nr_variables = total_nr_variables(round_chip) +#let nr_columns = total_nr_instantiated_columns(round_chip, config) + +The #keccak_rnd chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_variable_table(round_chip, config) + + +== Constraints + +#render_constraint_table(round_chip, config) \ No newline at end of file diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml new file mode 100644 index 000000000..b47d987e9 --- /dev/null +++ b/spec/src/keccak.toml @@ -0,0 +1,87 @@ +name = "KECCAK" + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp at which the permutation is performed" + +[[variables.input]] +name = "addr" +type = "DWordBL" +desc = "memory address storing the first bit of the state" + +[[variables.input]] +name = "input_state" +type = [[["Byte", 8], 5], 5] +desc = "state at the start of executing the permutation" + +[[variables.output]] +name = "output_state" +type = [[["Byte", 8], 5], 5] +desc = "state after executing the permutation" + +[[variables.auxiliary]] +name = "state_ptr" +type = [["DWordHL", 5], 5] +desc = "memory addresses storing the entire state" + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 1], ["-", ["^", 2, 32], 2]]] +multiplicity = ["-", "μ"] + +[[constraint_groups]] +name = "mem" + +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 10], "DWordWL"], "addr", "timestamp", 1, 0, 0] +output = "addr" +multiplicity = "μ" + +[[constraints.mem]] +kind = "template" +tag = "ADD" +input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "x"], "y"]], "DWordWL"]] +output = ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"] +iters = [["x", 0, 4], ["y", 0, 4]] + +[[constraints.mem]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] +multiplicity = "μ" + +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [0, ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"], ["idx", ["idx", "output_state", "x"], "y"], "timestamp", 0, 0, 1] +output = ["idx", ["idx", "input_state", "x"], "y"] +iters = [["x", 0, 4], ["y", 0, 4]] +multiplicity = "μ" + +[[constraint_groups]] +name = "round" + +[[constraints.round]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", 0, "input_state"] +multiplicity = "μ" + +[[constraints.round]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", 24, "output_state"] +multiplicity = ["-", "μ"] diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml new file mode 100644 index 000000000..30c4c8faa --- /dev/null +++ b/spec/src/keccak_round.toml @@ -0,0 +1,265 @@ +name = "KECCAK_RND" + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp at which the permutation is performed" + + +[[variables.input]] +name = "round" +type = "BaseField" +desc = "index of the permutation round" + +[[variables.input]] +name = "A" +type = [[["Byte", 8], 5], 5] +desc = "state at the start of executing the permutation" + +[[variables.auxiliary]] +name = "Cxz" +type = [[["Byte", 8], 4], 5] +desc = "$:= xor_(i=0)^(y+1) #`A[x,i,z]`$" + +[[variables.auxiliary]] +name = "Cxz_sub_1" +type = [["Byte", 8], 5] +desc = "$:= #`Cxz[x,` 3 #`,` (#`z`-1) mod 5 #`]`$" + +[[variables.auxiliary]] +name = "Dxz" +type = [["Byte", 8], 5] +desc = "$:= #`Cxz[x,y,z]` xor #`Cxz[` (#`x` +1) mod 5, #`y`, (#`z`-1) mod 5 #`]`$" + +[[variables.auxiliary]] +name = "A'" +type = [[["Byte", 8], 5], 5] +desc = "$θ(#`A`)$" + +[[variables.auxiliary]] +name = "rot_left" +type = [[["Byte", 8], 5], 5] +desc = "todo" + +[[variables.auxiliary]] +name = "rot_right" +type = [[["Byte", 8], 5], 5] +desc = "todo" + +[[variables.auxiliary]] +name = "chi_ANDs" +type = [[["Byte", 8], 5], 5] +desc = "todo" + +[[variables.auxiliary]] +name = "chi" +type = [[["Byte", 8], 5], 5] +desc = "$χ(#`theta`)$ = θ(#`A`)" + +[[variables.auxiliary]] +name = "rc" +type = ["Byte", 8] +desc = "round constants" + +[[variables.auxiliary]] +name = "iota" +type = ["Byte", 8] +desc = "state after applying `ɩ`." + +[[variables.virtual]] +name = "out" +type = [[["Byte", 8], 5], 5] +desc = "state at the end of executing the permutation" +def = {polys=[ + {iters=[["x", 0], ["y", 0], ["z", 0, 7]], poly=["idx", "iota","z"]}, + {iters=[["x", 1, 5], ["y", 0], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 0], ["y", 1, 5], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 1, 5], ["y", 1, 5], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]} +]} + +[[variables.virtual]] +name = "rho" +type = [[["Byte", 8], 5], 5] +desc = "state after applying `ρ`" +def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[ + "+", + ["*", + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0]], + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 1], 8]], + ] + ], + ["*", + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0], + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 2], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 3], 8]], + ] + ], + ["*", + ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0]], + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 4], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 5], 8]], + ] + ], + ["*", + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 0], + ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1], + ["+", + ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 6], 8]], + ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 7], 8]], + ] + ], +]} + +[[variables.virtual]] +name = "pi" +type = [[["Byte", 8], 5], 5] +desc = "state after applying `π`" +def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=["idx", ["idx", ["idx", "rho", ["mod", ["+", "x", ["*", 3, "y"]], 5]], "x"], "z"]} + +[[variables.constant]] +name = "rnc" +type = [["Byte", 5], 5] +desc = "lower nibble of `ρ` constants" + +[[variables.constant]] +name = "rbc" +type = [[["Bit", 2], 5], 5] +desc = "top two bits of `ρ` constants" + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + +# Assumptions + + +# Constraints + +[[constraint_groups]] +name = "io" + +[[constraints.io]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", "round", "A"] +multiplicity = ["-", "μ"] + +[[constraints.io]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", ["+", "round", 1], "out"] +multiplicity = "μ" + +[[constraint_groups]] +name = "theta" + +[[constraints.theta]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "A", "x"], 0], "z"], ["idx", ["idx", ["idx", "A", "x"], 1], "z"]] +output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] +iters = [["x", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.theta]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "A", "x"], "y"], "z"]] +output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] +iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.theta]] +kind = "interaction" +tag = "ROT" +input = [["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordWL"], 1] +output = ["cast", ["idx", "Cxz_rot", "x"], "DWordWL"] +iter = ["x", 0, 4] +multiplicity = "μ" + +[[constraints.theta]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", ["idx", "Cxz_rot", "x"], "z"]] +iters = [["x", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.theta]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "Cxz", "x"], 3], "z"], ["idx", ["idx", "Cxz_rot", "x"], "z"]] +output = ["idx", ["idx", "Dxz", "x"], "z"] +iters = [["x", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.theta]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "A", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] +output = ["idx", ["idx", ["idx", "theta", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraint_groups]] +name = "rho" + +[[constraints.rho]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.rho]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.rho]] +kind = "interaction" +tag = "HWSL" +input = [["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"], ["idx", ["idx", "rc", "x"], "y"]] +output = ["arr", ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] +multiplicity = "μ" + +[[constraint_groups]] +name = "chi" + +[[constraints.chi]] +kind = "interaction" +tag = "AND_BYTE" +input = [["-", 255, ["idx", ["idx", ["idx", "pi", ["mod", ["+", "x", 1], 5]], "y"], "z"]], ["idx",["idx",["idx", "pi", ["mod", ["+", "x", 2], 5]], "y"], "z"]] +output = ["idx", ["idx", ["idx", "chi_ANDs", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraints.chi]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "rho", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] +output = ["idx", ["idx", ["idx", "chi", "x"], "y"], "z"] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +multiplicity = "μ" + +[[constraint_groups]] +name = "iota" + +[[constraints.iota]] +kind = "interaction" +tag = "XOR_BYTE" +input = [["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc", "z"]] +output = ["idx", "iota", "z"] +iter = ["z", 0, 7] +multiplicity = "μ" From f01563491a484eb2cf9d03a33fc94578724989f5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 20:56:47 +0200 Subject: [PATCH 05/25] spec/keccak: define padding --- spec/keccak.typ | 2 +- spec/src/keccak.toml | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 9dce69adf..fc8665230 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -46,7 +46,7 @@ Lastly, the input state is pushed to the Keccak-round function, while the output The table can be padded to the next power of two with the following value assignments: -// #render_chip_padding_table(chip, config) +#render_chip_padding_table(chip, config) = Round chip #let round_chip = load_chip("src/keccak_round.toml", config) diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index b47d987e9..008cf3100 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -4,31 +4,43 @@ name = "KECCAK" name = "timestamp" type = "DWordWL" desc = "timestamp at which the permutation is performed" +pad = 0 [[variables.input]] name = "addr" type = "DWordBL" desc = "memory address storing the first bit of the state" +pad = 0 [[variables.input]] name = "input_state" type = [[["Byte", 8], 5], 5] desc = "state at the start of executing the permutation" +pad = 0 [[variables.output]] name = "output_state" type = [[["Byte", 8], 5], 5] desc = "state after executing the permutation" +pad = 0 [[variables.auxiliary]] name = "state_ptr" type = [["DWordHL", 5], 5] desc = "memory addresses storing the entire state" +pad = ["*", 8, ["arr", + ["arr", 0, 1, 2, 3, 4], + ["arr", 5, 6, 7, 8, 9], + ["arr", 10, 11, 12, 13, 14], + ["arr", 15, 16, 17, 18, 19], + ["arr", 20, 21, 22, 23, 24] +]] [[variables.multiplicity]] name = "μ" type = "Bit" desc = "" +pad = 0 [[constraint_groups]] name = "output" From 4d6dd20a822eafd1ef8b91bbc87c88b8ece0ed0e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 31 Mar 2026 22:24:51 +0200 Subject: [PATCH 06/25] spec: support multidimensional array in signatures --- spec/signatures.typ | 35 ++++++++++++++++++----------------- spec/src.typ | 7 ++++--- 2 files changed, 22 insertions(+), 20 deletions(-) diff --git a/spec/signatures.typ b/spec/signatures.typ index 12d84f757..fc029b0db 100644 --- a/spec/signatures.typ +++ b/spec/signatures.typ @@ -6,6 +6,16 @@ #let config = load_config() #let signatures = load_signatures(config) +// Render a type +#let render_type(typ) = { + let res = `` + while type(typ) == array { + res += `[` + raw(str(typ.at(1))) + `]` + typ = typ.at(0) + } + raw(typ) + res +} + // Render a signature #let render_signature(sig) = { let (lb, rb) = if sig.kind == "interaction" { @@ -19,21 +29,11 @@ raw(cond) + ` => ` } else {``} - let input_str = sig.input.map(elt => { - if type(elt) == array { - raw(elt.at(0)) + `[` + raw(str(elt.at(1))) + `]` - } else { - raw(elt) - } - }).join(`, `) + let input_str = sig.input.map(render_type).join(`, `) let output = sig.at("output", default: none) let output_str = if output != none { - if type(output) == array { - raw(output.at(0)) + `[` + raw(str(output.at(1))) + `]` - } else { - raw(output) - } + `; ` + render_type(output) + `; ` } else {``} return [#cond_str#raw(sig.tag)#lb#output_str#input_str#rb] @@ -44,12 +44,13 @@ let vars = sig.input + if "output" in sig { (sig.output, )} else {()} return vars.map(v => { - let (label, factor) = if type(v) == array { - (v.at(0), v.at(1)) - } else { - (v, 1) + let factor = 1 + while type(v) == array { + factor *= v.at(1) + v = v.at(0) } - config.variables.types.filter(type => type.label == label).first().subtypes.len() * factor + let lbl = v + config.variables.types.filter(type => type.label == lbl).first().subtypes.len() * factor }) .sum() } diff --git a/spec/src.typ b/spec/src.typ index 7d5f15979..d553629ff 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -40,10 +40,11 @@ // Verify that `var` is a valid variable. let verify_variable(var) = { - if type(var) == array { - assert(var.at(0) in var_labels, message: "Invalid var type: " + repr(var)) + while type(var) == array { assert(type(var.at(1)) == int, message: "Invalid var type: " + repr(var)) - } else if type(var) == str { + var = var.at(0) + } + if type(var) == str { assert(var in var_labels, message: "Invalid var type: " + repr(var)) } else { assert(false, message: "Invalid var type: " + repr(var)) From d621096f68facb853267aac8e297a3b3a322653b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 09:19:02 +0200 Subject: [PATCH 07/25] spec/keccak: add signatures --- spec/src/signatures.toml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 33f97cebf..b04b3d561 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -211,3 +211,16 @@ tag = "ROTXOR" kind = "interaction" input = ["Word", "Byte", "Byte", "Byte", "Bit"] output = "Word" + +# Keccak communication between rounds +[[signatures]] +tag = "KECCAK" +kind = "interaction" +input = ["DWordWL", "BaseField", [[["Byte", 8], 5], 5]] + +# Keccak round constants +[[signatures]] +tag = "KECCAK_RC" +kind = "interaction" +input = ["BaseField"] +output = ["Byte", 8] From f27b9d9a74e75e720a922ca4dff477a869aa9394 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 14:56:07 +0200 Subject: [PATCH 08/25] spec/keccak: update core chip --- spec/keccak.typ | 25 +++++++++++++------------ spec/src/keccak.toml | 3 +++ 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index fc8665230..220ad0770 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -15,7 +15,14 @@ #show: book-page(chip.name) #let keccak = raw(chip.name) -The #keccak chip applies the keccak permutation. +The #keccak chip applies the keccak permutation $kappa$ to a given memory range. + +This permutation $kappa: FF_2^1600 -> FF_2^1600$ operates on 1600 bits and is composed of 24 applications of round-permutation $Lambda: FF_2^1600 times NN -> FF_2^1600$, where the additional parameter is the round constant. +$Lambda$ is defined as the composition $iota compose chi compose pi compose rho compose theta$, where only $iota$ depends on the round constant. +#footnote("More details on the KECCAK permutation: FIPS 202, NIST, " + link("https://csrc.nist.gov/pubs/fips/202/final")) + +The keccak accelerator comprises two chips: a core chip that interacts with the memory, and a round chip that applies the round permutation. + = Core chip == Columns @@ -25,27 +32,21 @@ The #keccak chip applies the keccak permutation. The #keccak chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: #render_chip_variable_table(chip, config) -== Assumptions - -// #render_chip_assumptions(chip, config) - == Constraints In this VM, we assign syscall number -2 to the #keccak accelerator. The chip therefore contributes the following interaction to the lookup-argument: #render_constraint_table(chip, config, groups: "output") -The address containing the state to be permuted are passed in as argument `A0 = x10`. -This address is read into `addr`, from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived. -The state is then read into `input_state`, while the `output_state` is written back to the indicated address. +The address containing the state to be permuted is passed in as argument `A0 = x10`. +The following constraints describe that this address is read into `addr` (@keccak:c:read_addr), from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr). +The state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccack:c:load_store_state). #render_constraint_table(chip, config, groups: "mem") -Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus. +Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus: #render_constraint_table(chip, config, groups: "round") == Padding - -The table can be padded to the next power of two with the following value assignments: - +The #keccak table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(chip, config) = Round chip diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 008cf3100..9b38c74a1 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -60,6 +60,7 @@ tag = "MEMW" input = [1, ["cast", ["*", 2, 10], "DWordWL"], "addr", "timestamp", 1, 0, 0] output = "addr" multiplicity = "μ" +ref = "keccak:c:read_addr" [[constraints.mem]] kind = "template" @@ -67,6 +68,7 @@ tag = "ADD" input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "x"], "y"]], "DWordWL"]] output = ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"] iters = [["x", 0, 4], ["y", 0, 4]] +ref = "keccak:c:state_ptr" [[constraints.mem]] kind = "interaction" @@ -82,6 +84,7 @@ input = [0, ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"], ["idx" output = ["idx", ["idx", "input_state", "x"], "y"] iters = [["x", 0, 4], ["y", 0, 4]] multiplicity = "μ" +ref = "keccack:c:load_store_state" [[constraint_groups]] name = "round" From 7341d6d73063755d5c9ecc5662bc85c4a1d18245 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 14:56:30 +0200 Subject: [PATCH 09/25] spec/keccak: update keccak_rnd description --- spec/keccak.typ | 32 ++++++++++- spec/src/keccak_round.toml | 108 ++++++++++++++++++++++++------------- 2 files changed, 102 insertions(+), 38 deletions(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 220ad0770..c54249918 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -61,6 +61,36 @@ The #keccak_rnd chip is comprised of #nr_variables variables that are expressed #render_chip_variable_table(round_chip, config) +#strong("Note on " + raw("rnc") + " and " + raw("rbc") + ".") +Rho rotates every lane by a rotation offset in $[0, 64)$. +These offsets are identical for every round. +#footnote("See FIPS 202, NIST, Table 2 on page 13 for the exact offsets (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") +We decompose each offset in three components: the lower nibble (4 bits) are represented by `rnc`, while the upper two bits are represented by as `Bit`s in `rbc`. +That is, $#`rho_offset[x][y]` = #`rnc[x][y]` + 16 dot #`rbc[x][y][0]` + 32 dot #`rbc[x][y][1]`$. + + == Constraints -#render_constraint_table(round_chip, config) \ No newline at end of file +The following constraints ensure that `theta` captures the state after applying the first subpermutation of the round-permutation: $theta$. +Note here that `Cxz_left` and `Cxz_right` do have to be range-checked; it cannot be assumed that this implicitly follows from @keccak:c:Dxz combined with `rotated_Cxz`'s definition. +#render_constraint_table(round_chip, config, groups: "theta") + +Next, we constrain that `rho` captures the state after applying subpermutation $rho$. +Note here as well that `rot_left` and `rot_right` do have to be range-checked; it cannot be assumed that this implicitly follows from later constraints. +#render_constraint_table(round_chip, config, groups: "rho") + +Observe that the lane-permutation performed by $pi$ is absorbed in `pi`'s definition. +The next permutation that is constrained in $chi$: +#render_constraint_table(round_chip, config, groups: "chi") + +Lastly, the round constants are added to one of the lanes in the state. +`iota` contains the updated lane. +In the definition of `out`, the output of `chi` and `iota` is combined to construct the output of the permutation. +#render_constraint_table(round_chip, config, groups: "iota") + +Lastly, the round chip contributes the following interactions to the lookup: +#render_constraint_table(round_chip, config, groups: "io") + +== Optimizations +- step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. +- $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 30c4c8faa..d59e44b46 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -12,49 +12,54 @@ type = "BaseField" desc = "index of the permutation round" [[variables.input]] -name = "A" +name = "start" type = [[["Byte", 8], 5], 5] desc = "state at the start of executing the permutation" [[variables.auxiliary]] name = "Cxz" type = [[["Byte", 8], 4], 5] -desc = "$:= xor_(i=0)^(y+1) #`A[x,i,z]`$" +desc = "$xor_(i=0)^(y+2) #`start[x,i,z]`$" [[variables.auxiliary]] -name = "Cxz_sub_1" +name = "Cxz_left" type = [["Byte", 8], 5] -desc = "$:= #`Cxz[x,` 3 #`,` (#`z`-1) mod 5 #`]`$" +desc = "the left-rotated component of `rotated_Cxz`" + +[[variables.auxiliary]] +name = "Cxz_right" +type = [["Byte", 8], 5] +desc = "the right-rotated component of `rotated_Cxz`" [[variables.auxiliary]] name = "Dxz" type = [["Byte", 8], 5] -desc = "$:= #`Cxz[x,y,z]` xor #`Cxz[` (#`x` +1) mod 5, #`y`, (#`z`-1) mod 5 #`]`$" +desc = "$#`Cxz[x,y,z]` xor #`rotated_Cxz[`\\(#`x` +1) mod 5#`,y,z]`$" [[variables.auxiliary]] -name = "A'" +name = "theta" type = [[["Byte", 8], 5], 5] -desc = "$θ(#`A`)$" +desc = "$theta(#`start`)$, the state after applying $theta$." [[variables.auxiliary]] name = "rot_left" type = [[["Byte", 8], 5], 5] -desc = "todo" +desc = "the left-rotated component of $#`theta[x,y]` <<< #`rnc`$" [[variables.auxiliary]] name = "rot_right" type = [[["Byte", 8], 5], 5] -desc = "todo" +desc = "the right-rotated component of $#`theta[x,y]` <<< #`rnc`$" [[variables.auxiliary]] name = "chi_ANDs" type = [[["Byte", 8], 5], 5] -desc = "todo" +desc = "$(#`pi[`\\(x+1) mod 5#`,y,z]` xor 255) times.o #`pi[`\\(x + 2) mod 5#`,y,z]`$" [[variables.auxiliary]] name = "chi" type = [[["Byte", 8], 5], 5] -desc = "$χ(#`theta`)$ = θ(#`A`)" +desc = "$(chi compose pi compose rho compose theta)(#`start`)$; the state after applying $chi$" [[variables.auxiliary]] name = "rc" @@ -64,7 +69,13 @@ desc = "round constants" [[variables.auxiliary]] name = "iota" type = ["Byte", 8] -desc = "state after applying `ɩ`." +desc = "state update following from step $iota$." + +[[variables.virtual]] +name = "rotated_Cxz" +type = [["Byte", 8], 5] +desc = "$#`Cxz[x,`3#`,z]` <<< 1$" +def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", "z", 1], 8]]]} [[variables.virtual]] name = "out" @@ -72,15 +83,15 @@ type = [[["Byte", 8], 5], 5] desc = "state at the end of executing the permutation" def = {polys=[ {iters=[["x", 0], ["y", 0], ["z", 0, 7]], poly=["idx", "iota","z"]}, - {iters=[["x", 1, 5], ["y", 0], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, - {iters=[["x", 0], ["y", 1, 5], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, - {iters=[["x", 1, 5], ["y", 1, 5], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]} + {iters=[["x", 1, 4], ["y", 0], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 0], ["y", 1, 4], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]}, + {iters=[["x", 1, 4], ["y", 1, 4], ["z", 0, 7]], poly=["idx",["idx",["idx","chi","x"],"y"],"z"]} ]} [[variables.virtual]] name = "rho" type = [[["Byte", 8], 5], 5] -desc = "state after applying `ρ`" +desc = "$(rho compose theta)(#`start`)$; the state state after applying $rho$" def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[ "+", ["*", @@ -120,7 +131,7 @@ def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[ [[variables.virtual]] name = "pi" type = [[["Byte", 8], 5], 5] -desc = "state after applying `π`" +desc = "$(pi compose rho compose theta)(#`start`)$; the state after applying $pi$" def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=["idx", ["idx", ["idx", "rho", ["mod", ["+", "x", ["*", 3, "y"]], 5]], "x"], "z"]} [[variables.constant]] @@ -150,7 +161,7 @@ name = "io" [[constraints.io]] kind = "interaction" tag = "KECCAK" -input = ["timestamp", "round", "A"] +input = ["timestamp", "round", "start"] multiplicity = ["-", "μ"] [[constraints.io]] @@ -159,13 +170,20 @@ tag = "KECCAK" input = ["timestamp", ["+", "round", 1], "out"] multiplicity = "μ" +[[constraints.io]] +kind = "interaction" +tag = "KECCAK_RC" +input = ["round"] +output = "rc" +multiplicity = ["-", "μ"] + [[constraint_groups]] name = "theta" [[constraints.theta]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "A", "x"], 0], "z"], ["idx", ["idx", ["idx", "A", "x"], 1], "z"]] +input = [["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["idx", ["idx", ["idx", "start", "x"], 1], "z"]] output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -173,38 +191,50 @@ multiplicity = "μ" [[constraints.theta]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "A", "x"], "y"], "z"]] +input = [["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["idx", ["idx", "start", "x"], "y"], "z"]] output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] multiplicity = "μ" [[constraints.theta]] kind = "interaction" -tag = "ROT" -input = [["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordWL"], 1] -output = ["cast", ["idx", "Cxz_rot", "x"], "DWordWL"] -iter = ["x", 0, 4] +tag = "HWSL" +input = [["idx", ["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordHL"], "z"], 1] +output = ["arr", ["idx", ["cast", ["idx", "Cxz_left", "x"], "DWordHL"], "z"], ["idx", ["cast", ["idx", "Cxz_right", "x"], "DWordHL"], "z"]] +iters = [["x", 0, 4], ["z", 0, 3]] +multiplicity = "μ" + +# Note: these IS_BYTE checks are necessary. +# Without them, it is possible to prove 0 <<< S evaluates to -1 by setting +# Cxz_left = [-1, 256, -1, 256, -1, 256, -1, 256] and +# Cxz_right = [ 1, -256, 1, -256, 1, -256, 1, -256] +[[constraints.theta]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", ["idx", "Cxz_left", "x"], "z"]] +iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" [[constraints.theta]] kind = "interaction" tag = "IS_BYTE" -input = [["idx", ["idx", "Cxz_rot", "x"], "z"]] +input = [["idx", ["idx", "Cxz_right", "x"], "z"]] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" [[constraints.theta]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "Cxz", "x"], 3], "z"], ["idx", ["idx", "Cxz_rot", "x"], "z"]] +input = [["idx", ["idx", ["idx", "Cxz", ["mod", ["-", "x", 1], 5]], 3], "z"], ["idx", ["idx", "rotated_Cxz", ["mod", ["+", "x", 1], 5]], "z"]] output = ["idx", ["idx", "Dxz", "x"], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" +ref = "keccak:c:Dxz" [[constraints.theta]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "A", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] +input = [["idx", ["idx", ["idx", "start", "x"], "y"], "z"], ["idx", ["idx", "Dxz", "x"], "z"]] output = ["idx", ["idx", ["idx", "theta", "x"], "y"], "z"] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -214,24 +244,28 @@ name = "rho" [[constraints.rho]] kind = "interaction" -tag = "IS_BYTE" -input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]] -iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] +tag = "HWSL" +input = [["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"], ["idx", ["idx", "rnc", "x"], "y"]] +output = ["arr", ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] multiplicity = "μ" +# Note: these IS_BYTE checks are necessary. +# Without them, it is possible to prove 0 <<< S evaluates to -1 by setting +# rot_left = [-1, 256, -1, 256, -1, 256, -1, 256] and +# rot_right = [ 1, -256, 1, -256, 1, -256, 1, -256] [[constraints.rho]] kind = "interaction" tag = "IS_BYTE" -input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]] +input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" [[constraints.rho]] kind = "interaction" -tag = "HWSL" -input = [["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"], ["idx", ["idx", "rc", "x"], "y"]] -output = ["arr", ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"]] -iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] +tag = "IS_BYTE" +input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]] +iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" [[constraint_groups]] @@ -248,7 +282,7 @@ multiplicity = "μ" [[constraints.chi]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "rho", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] +input = [["idx", ["idx", ["idx", "pi", "x"], "y"], "z"], ["idx",["idx",["idx", "chi_ANDs", "x"], "y"], "z"]] output = ["idx", ["idx", ["idx", "chi", "x"], "y"], "z"] iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]] multiplicity = "μ" @@ -259,7 +293,7 @@ name = "iota" [[constraints.iota]] kind = "interaction" tag = "XOR_BYTE" -input = [["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc", "z"]] +input = [["idx", ["idx", ["idx", "chi", 0], 0], "z"], ["idx","rc","z"]] output = ["idx", "iota", "z"] iter = ["z", 0, 7] multiplicity = "μ" From 9fc7cee3eb61a2f471fd23ead0e2f56d816c728b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 1 Apr 2026 15:03:01 +0200 Subject: [PATCH 10/25] spec/keccak: define round constant lookup --- spec/keccak.typ | 12 ++++++++++++ spec/src/keccak_rc.toml | 28 ++++++++++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 spec/src/keccak_rc.toml diff --git a/spec/keccak.typ b/spec/keccak.typ index c54249918..8ea3c8d1a 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -94,3 +94,15 @@ Lastly, the round chip contributes the following interactions to the lookup: == Optimizations - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. + += Round constant lookup +#let rc_chip = load_chip("src/keccak_rc.toml", config) +#let keccak_rc = raw(rc_chip.name) + +== Columns +#let nr_variables = total_nr_variables(rc_chip) +#let nr_columns = total_nr_instantiated_columns(rc_chip, config) + +We provide the round constants through a short precomputed lookup table: #keccak_rc. +#render_chip_variable_table(rc_chip, config) +#render_constraint_table(rc_chip, config) \ No newline at end of file diff --git a/spec/src/keccak_rc.toml b/spec/src/keccak_rc.toml new file mode 100644 index 000000000..6c03cd563 --- /dev/null +++ b/spec/src/keccak_rc.toml @@ -0,0 +1,28 @@ +name = "KECCAK_RC" + +[[variables.input]] +name = "round" +type = "BaseField" +desc = "" +precomputed = true + +[[variables.input]] +name = "RC" +type = ["Byte", 8] +desc = "round constants for the given `round`" +precomputed = true + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "" + +[[constraint_groups]] +name = "contributions" + +[[constraints.contributions]] +kind = "interaction" +tag = "KECCAK_RC" +input = ["round"] +output = "RC" +multiplicity = ["-", "μ"] \ No newline at end of file From 0f48a46439590584cdcf3d0e3b00ee4e0c26c591 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Thu, 2 Apr 2026 10:20:57 +0200 Subject: [PATCH 11/25] Apply suggestions from code review Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> --- spec/expr.typ | 4 ++-- spec/keccak.typ | 2 +- spec/src/keccak.toml | 2 +- spec/tooling/chip.py | 4 +++- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/spec/expr.typ b/spec/expr.typ index a383c1891..ada64e5f6 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -9,7 +9,7 @@ assert(type(typ.at(1)) == int, message: "Array types need to have a constant dimension") typ = typ.at(0) } - assert(type(typ.at(0)) == str, message: "Array types need to have a regular type as base") + assert(type(typ) == str, message: "Array types need to have a regular type as base") } // Render a type to code @@ -60,7 +60,7 @@ "cast": 3, // cast "mul": 4, // * "div": 5, // / - "mod": 6, // % + "mod": 6, // mod "sum": 7, // Σ "not": 8, // not "sub": 9, // - diff --git a/spec/keccak.typ b/spec/keccak.typ index 8ea3c8d1a..84f2f1031 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -39,7 +39,7 @@ The chip therefore contributes the following interaction to the lookup-argument: The address containing the state to be permuted is passed in as argument `A0 = x10`. The following constraints describe that this address is read into `addr` (@keccak:c:read_addr), from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr). -The state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccack:c:load_store_state). +The state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccak:c:load_store_state). #render_constraint_table(chip, config, groups: "mem") Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus: diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 9b38c74a1..d00161c8f 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -84,7 +84,7 @@ input = [0, ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"], ["idx" output = ["idx", ["idx", "input_state", "x"], "y"] iters = [["x", 0, 4], ["y", 0, 4]] multiplicity = "μ" -ref = "keccack:c:load_store_state" +ref = "keccak:c:load_store_state" [[constraint_groups]] name = "round" diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index f682601e2..66b4dcd49 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -266,9 +266,11 @@ def typecheck(self, env: Environment) -> Type: if isinstance(modulus, list) or not modulus.is_const(): reporter.error(f"Invalid non-constant modulus: {self.modulus!r}") + return Range.const(1) modulus = modulus.get_const() if modulus <= 0: - reporter.error(f"Invalid zero non-positive modulus: {self.modulus!r}") + reporter.error(f"Invalid non-positive modulus: {self.modulus!r}") + return Range(1) if elt.is_const(): elt = elt.get_const() From b5f44a9014f14b6886712b52e2ef73f157c46153 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 13 Apr 2026 15:56:53 +0200 Subject: [PATCH 12/25] spec/keccak: clarify "optimizations" header --- spec/keccak.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 84f2f1031..a22616f4e 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -91,7 +91,7 @@ In the definition of `out`, the output of `chi` and `iota` is combined to constr Lastly, the round chip contributes the following interactions to the lookup: #render_constraint_table(round_chip, config, groups: "io") -== Optimizations +== Notes/potential optimizations - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. From 286cfd0ad0cc711215273f105ea14a4cb5971144 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 13 Apr 2026 15:58:59 +0200 Subject: [PATCH 13/25] spec/keccak: list `state_ptr` simplification optimization --- spec/keccak.typ | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/keccak.typ b/spec/keccak.typ index a22616f4e..a5727cdd7 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -92,6 +92,7 @@ Lastly, the round chip contributes the following interactions to the lookup: #render_constraint_table(round_chip, config, groups: "io") == Notes/potential optimizations +- one does not have to repeat `addr` in `state_ptr`; this saves 4 columns and 4 `IS_HALF` checks. - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. From 47f0f479a6eb2d8332266900166abb4ec764243e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 14:38:17 +0200 Subject: [PATCH 14/25] spec/keccak: fix C3 --- spec/src/keccak.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index d00161c8f..b8f2d91c2 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -65,7 +65,7 @@ ref = "keccak:c:read_addr" [[constraints.mem]] kind = "template" tag = "ADD" -input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "x"], "y"]], "DWordWL"]] +input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "y"], "x"]], "DWordWL"]] output = ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"] iters = [["x", 0, 4], ["y", 0, 4]] ref = "keccak:c:state_ptr" From 6fe03e2c54f6ebd97fa30fb320f98c0366507e98 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 14:44:03 +0200 Subject: [PATCH 15/25] spec/keccak: fix missing EOF --- spec/src/keccak_rc.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/keccak_rc.toml b/spec/src/keccak_rc.toml index 6c03cd563..7844dfbee 100644 --- a/spec/src/keccak_rc.toml +++ b/spec/src/keccak_rc.toml @@ -25,4 +25,4 @@ kind = "interaction" tag = "KECCAK_RC" input = ["round"] output = "RC" -multiplicity = ["-", "μ"] \ No newline at end of file +multiplicity = ["-", "μ"] From 6b5824a6c789efb6274649d6153ad075bb4029d6 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 15:06:23 +0200 Subject: [PATCH 16/25] spec/keccak: list interaction counts --- spec/keccak.typ | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index a5727cdd7..99389aedb 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -1,6 +1,7 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( + compute_nr_interactions, render_chip_assumptions, render_chip_variable_table, total_nr_variables, @@ -28,8 +29,9 @@ The keccak accelerator comprises two chips: a core chip that interacts with the == Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) -The #keccak chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +The #keccak chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) == Constraints @@ -56,8 +58,9 @@ The #keccak table can be padded to the next power of two with the following valu == Columns #let nr_variables = total_nr_variables(round_chip) #let nr_columns = total_nr_instantiated_columns(round_chip, config) +#let nr_interactions = compute_nr_interactions(round_chip) -The #keccak_rnd chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +The #keccak_rnd chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(round_chip, config) From bcf18a6b2b4557bfe2430202d53db2bbe6c4cbfc Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 15:09:36 +0200 Subject: [PATCH 17/25] spec/keccak: list three-way XOR optimization idea --- spec/keccak.typ | 1 + spec/src/keccak_round.toml | 2 ++ 2 files changed, 3 insertions(+) diff --git a/spec/keccak.typ b/spec/keccak.typ index 99389aedb..c448da27f 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -98,6 +98,7 @@ Lastly, the round chip contributes the following interactions to the lookup: - one does not have to repeat `addr` in `state_ptr`; this saves 4 columns and 4 `IS_HALF` checks. - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. +- when executed in large volumnes, `KECCAK_RND` could benefit from having a three-way XOR lookup table. With this in place, the total number of interactions in @keccak:c:theta_cxz_start and @keccak:c:theta_cxz could be dropped from 160 to 80. = Round constant lookup #let rc_chip = load_chip("src/keccak_rc.toml", config) diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index d59e44b46..0dbe7d55f 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -187,6 +187,7 @@ input = [["idx", ["idx", ["idx", "start", "x"], 0], "z"], ["idx", ["idx", ["idx" output = ["idx", ["idx", ["idx", "Cxz", "x"], 0], "z"] iters = [["x", 0, 4], ["z", 0, 7]] multiplicity = "μ" +ref = "keccak:c:theta_cxz_start" [[constraints.theta]] kind = "interaction" @@ -195,6 +196,7 @@ input = [["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 2]], "z"], ["idx", ["id output = ["idx", ["idx", ["idx", "Cxz", "x"], ["-", "y", 1]], "z"] iters = [["x", 0, 4], ["y", 2, 4], ["z", 0, 7]] multiplicity = "μ" +ref = "keccak:c:theta_cxz" [[constraints.theta]] kind = "interaction" From b268e2c15040e6116157a438d08930ddb81d4340 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 15:12:09 +0200 Subject: [PATCH 18/25] spec/tooling: fix mod_expr default --- spec/tooling/chip.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 66b4dcd49..7f7ecca81 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -266,11 +266,11 @@ def typecheck(self, env: Environment) -> Type: if isinstance(modulus, list) or not modulus.is_const(): reporter.error(f"Invalid non-constant modulus: {self.modulus!r}") - return Range.const(1) + return Range.const(0) modulus = modulus.get_const() if modulus <= 0: reporter.error(f"Invalid non-positive modulus: {self.modulus!r}") - return Range(1) + return Range.const(0) if elt.is_const(): elt = elt.get_const() From 3e8e40cba50999c3b550ebb4def7264ee6147d50 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 15:13:39 +0200 Subject: [PATCH 19/25] spec: add spaces round `%` rendering --- spec/expr.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/expr.typ b/spec/expr.typ index ada64e5f6..20a55d753 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -107,7 +107,7 @@ "mod": (pp, rec, e) => { assert(e.len() == 3 and type(e.at(2)) == int, message: "Invalid mod expr: " + repr(e)) cwrap( - rec(PREC.mod, e.at(1)) + `%` + rec(PREC.mod, e.at(2)), + rec(PREC.mod, e.at(1)) + ` % ` + rec(PREC.mod, e.at(2)), pp <= PREC.mod ) }, From 3f11acedb80642fb739030d8a8261749d0d1b738 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 14 Apr 2026 15:17:26 +0200 Subject: [PATCH 20/25] spec: reuse `type_to_code` in `signatures.typ` --- spec/signatures.typ | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/spec/signatures.typ b/spec/signatures.typ index fc029b0db..2839a74c6 100644 --- a/spec/signatures.typ +++ b/spec/signatures.typ @@ -1,21 +1,12 @@ #import "/book.typ": book-page #import "/src.typ": load_signatures, load_config +#import "/expr.typ": type_to_code #show: book-page("signatures.typ") #let config = load_config() #let signatures = load_signatures(config) -// Render a type -#let render_type(typ) = { - let res = `` - while type(typ) == array { - res += `[` + raw(str(typ.at(1))) + `]` - typ = typ.at(0) - } - raw(typ) + res -} - // Render a signature #let render_signature(sig) = { let (lb, rb) = if sig.kind == "interaction" { @@ -29,11 +20,11 @@ raw(cond) + ` => ` } else {``} - let input_str = sig.input.map(render_type).join(`, `) + let input_str = sig.input.map(type_to_code).join(`, `) let output = sig.at("output", default: none) let output_str = if output != none { - render_type(output) + `; ` + type_to_code(output) + `; ` } else {``} return [#cond_str#raw(sig.tag)#lb#output_str#input_str#rb] From 09db346a3f96889632e82d68e548fc537a04bbcb Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 14 Apr 2026 15:21:44 +0200 Subject: [PATCH 21/25] Apply suggestions from code review Co-authored-by: Robin Jadoul --- spec/src/keccak_round.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 0dbe7d55f..548cb5151 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -34,7 +34,7 @@ desc = "the right-rotated component of `rotated_Cxz`" [[variables.auxiliary]] name = "Dxz" type = [["Byte", 8], 5] -desc = "$#`Cxz[x,y,z]` xor #`rotated_Cxz[`\\(#`x` +1) mod 5#`,y,z]`$" +desc = "$#`Cxz[`\\(#`x` - 1) mod 5#`,y,z]` xor #`rotated_Cxz[`\\(#`x` + 1) mod 5#`,y,z]`$" [[variables.auxiliary]] name = "theta" From dd7b6ece296a815377de24342425bda4102dac0c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 17 Apr 2026 09:46:21 +0200 Subject: [PATCH 22/25] spec/keccak: update three-way XOR optimization benefits --- spec/keccak.typ | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index c448da27f..99c2a44bf 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -98,7 +98,8 @@ Lastly, the round chip contributes the following interactions to the lookup: - one does not have to repeat `addr` in `state_ptr`; this saves 4 columns and 4 `IS_HALF` checks. - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions. -- when executed in large volumnes, `KECCAK_RND` could benefit from having a three-way XOR lookup table. With this in place, the total number of interactions in @keccak:c:theta_cxz_start and @keccak:c:theta_cxz could be dropped from 160 to 80. +- when executed in large volumnes, `KECCAK_RND` could benefit from having a three-way XOR lookup table. With this in place, the 80 interactions in @keccak:c:theta_cxz_start and @keccak:c:theta_cxz could be dropped. + Likewise, 80 columns could be removed from the chip (a \~5% savings). = Round constant lookup #let rc_chip = load_chip("src/keccak_rc.toml", config) From 4a8ca720178e6c673ed5d6acd7ab8888a1bcb9c8 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 17 Apr 2026 10:18:46 +0200 Subject: [PATCH 23/25] spec/ecall: reintroduce ecall-number overview --- spec/about_ecalls.typ | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index ef4203610..9b37d5f21 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -22,3 +22,13 @@ When `ECALL` is executed, it is assumed that: - the return value is written to `A0`, where `A0`-`A7` are symbolic names for the registers `x10`-`x17` #footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]). + += ECALL number overview + +We provide a list of supported ECALL numbers. +Negative numbers (represented as 2s complement 64-bit numbers), are used for our own custom accelerators/extensions. + +/ 64: `write` (@commit) +/ 93: `exit` (@halt) +/ -1: `SHA256` (@sha256) +/ -2: `KECCAK` (@keccak) \ No newline at end of file From d2463501f648178ba9a457a3119e334b53627a76 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 17 Apr 2026 10:22:37 +0200 Subject: [PATCH 24/25] spec/keccak: ref to sections in FIPS202 on state endianness --- spec/keccak.typ | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 99c2a44bf..0de903c6c 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -16,13 +16,15 @@ #show: book-page(chip.name) #let keccak = raw(chip.name) -The #keccak chip applies the keccak permutation $kappa$ to a given memory range. +The #keccak chip applies the keccak permutation $kappa$ to a given memory range; +other aspects of keccak hashing (such as repeated permutation invocation, +input padding and state initialization) fall outside the scope of this accelerator. This permutation $kappa: FF_2^1600 -> FF_2^1600$ operates on 1600 bits and is composed of 24 applications of round-permutation $Lambda: FF_2^1600 times NN -> FF_2^1600$, where the additional parameter is the round constant. $Lambda$ is defined as the composition $iota compose chi compose pi compose rho compose theta$, where only $iota$ depends on the round constant. #footnote("More details on the KECCAK permutation: FIPS 202, NIST, " + link("https://csrc.nist.gov/pubs/fips/202/final")) -The keccak accelerator comprises two chips: a core chip that interacts with the memory, and a round chip that applies the round permutation. +The keccak accelerator comprises two chips: a core chip that interacts with the memory --- loading the input and writing the output, and a round chip that applies the round permutation. = Core chip @@ -63,11 +65,17 @@ The #keccak table can be padded to the next power of two with the following valu The #keccak_rnd chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(round_chip, config) +#strong("Note on " + raw("start") + ".") +`start` contains the state to which the permutation should be applied. +It's three-dimensional array mimics the specification's three-dimensional state +#footnote("FIPS 202, NIST, Section 3.1 (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") +and orders the bits as prescribed. +#footnote("FIPS 202, NIST, Section B.1, Algorithm 10 (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") #strong("Note on " + raw("rnc") + " and " + raw("rbc") + ".") Rho rotates every lane by a rotation offset in $[0, 64)$. These offsets are identical for every round. -#footnote("See FIPS 202, NIST, Table 2 on page 13 for the exact offsets (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") +#footnote("FIPS 202, NIST, page 13, Table 2 (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") We decompose each offset in three components: the lower nibble (4 bits) are represented by `rnc`, while the upper two bits are represented by as `Bit`s in `rbc`. That is, $#`rho_offset[x][y]` = #`rnc[x][y]` + 16 dot #`rbc[x][y][0]` + 32 dot #`rbc[x][y][1]`$. From 976e7737fdfd5fabecf7a0797ef92ce729e0c4e6 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 17 Apr 2026 10:29:11 +0200 Subject: [PATCH 25/25] spec/keccak: fix typo --- spec/keccak.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/keccak.typ b/spec/keccak.typ index 0de903c6c..e6e16f43f 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -67,7 +67,7 @@ The #keccak_rnd chip is comprised of #nr_variables variables that are expressed #strong("Note on " + raw("start") + ".") `start` contains the state to which the permutation should be applied. -It's three-dimensional array mimics the specification's three-dimensional state +Its three-dimensional array mimics the specification's three-dimensional state #footnote("FIPS 202, NIST, Section 3.1 (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")") and orders the bits as prescribed. #footnote("FIPS 202, NIST, Section B.1, Algorithm 10 (" + link("https://csrc.nist.gov/pubs/fips/202/final") + ")")