Skip to content

Commit 72b4d0c

Browse files
authored
docs: trusted-code assumptions (#174)
## What ❔ - Document the trusted-code assumptions for all delegation circuits in docs/delegation_circuits.md, clarifying why zero control masks are allowed in the proving circuit, how the simulator enforces stricter behavior during development, and why this is safe for current M-mode firmware. - Fix unsigned DIV/REM witness fallback in cs/src/machine/ops/mul_div.rs so that the default remainder for divisor=0 mirrors the dividend ## Why ❔ Delegation circuits share the same trusted-code surface as the base machine. The new documentation explains the security model for external operators, the difference between simulator/runtime behavior, and the role of trusted firmware. This prevents confusion when reading circuit code or comparing simulator panics with circuit permissiveness. ## Is this a breaking change? - [ ] Yes - [x] No ## Checklist - [x] PR title corresponds to the body of PR (we generate changelog entries from PRs). - [ ] Tests for the changes have been added / updated. - [x] Documentation comments have been added / updated. - [x] Code has been formatted.
1 parent f6c8269 commit 72b4d0c

File tree

8 files changed

+15
-7
lines changed

8 files changed

+15
-7
lines changed

circuit_defs/machine_without_signed_mul_div/generated/witness_generation_fn.cuh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ SHR(u32, 22, 19, 16)
581581
FROM(u16, 23, 22)
582582
IF(0, SET_WITNESS_PLACE(19, 23))
583583
REM(u32, 25, 15, 17)
584-
SELECT(u32, 26, 11, 25, 9)
584+
SELECT(u32, 26, 11, 25, 15)
585585
FROM(u16, 27, 26)
586586
IF(0, SET_WITNESS_PLACE(20, 27))
587587
SHR(u32, 29, 26, 16)

circuit_defs/machine_without_signed_mul_div/generated/witness_generation_fn.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1106,7 +1106,7 @@ fn eval_fn_31<
11061106
W::U16::select(&v_0, &v_23, &witness_proxy.get_witness_place_u16(19usize)),
11071107
);
11081108
let v_25 = W::U32::div_rem_assume_nonzero_divisor(&v_15, &v_17).1;
1109-
let v_26 = WitnessComputationCore::select(&v_11, &v_25, &v_9);
1109+
let v_26 = WitnessComputationCore::select(&v_11, &v_25, &v_15);
11101110
let v_27 = v_26.truncate();
11111111
witness_proxy.set_witness_place_u16(
11121112
20usize,

circuit_defs/machine_without_signed_mul_div/verifier/src/generated/witness_generation_fn.cuh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ SHR(u32, 22, 19, 16)
581581
FROM(u16, 23, 22)
582582
IF(0, SET_WITNESS_PLACE(19, 23))
583583
REM(u32, 25, 15, 17)
584-
SELECT(u32, 26, 11, 25, 9)
584+
SELECT(u32, 26, 11, 25, 15)
585585
FROM(u16, 27, 26)
586586
IF(0, SET_WITNESS_PLACE(20, 27))
587587
SHR(u32, 29, 26, 16)

circuit_defs/machine_without_signed_mul_div/verifier/src/generated/witness_generation_fn.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1106,7 +1106,7 @@ fn eval_fn_31<
11061106
W::U16::select(&v_0, &v_23, &witness_proxy.get_witness_place_u16(19usize)),
11071107
);
11081108
let v_25 = W::U32::div_rem_assume_nonzero_divisor(&v_15, &v_17).1;
1109-
let v_26 = WitnessComputationCore::select(&v_11, &v_25, &v_9);
1109+
let v_26 = WitnessComputationCore::select(&v_11, &v_25, &v_15);
11101110
let v_27 = v_26.truncate();
11111111
witness_proxy.set_witness_place_u16(
11121112
20usize,

cs/src/machine/decoder/decode_optimized_must_handle_csr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -239,7 +239,7 @@ impl OptimizedDecoder {
239239
// chunk4 = (i_insn + s_insn + b_insn) * sign_bit * 0b1111 + (u_insn + j_insn) * (rs1_low << 3 + funct3)
240240
// chunk5 = {
241241
// j_insn * (sign_bit * 0xfff0 + rs1_high) + u_insn * insn_high +
242-
// (1 - j_insn - b_insn) * sign_bit * 0xffff
242+
// (1 - j_insn - u_insn) * sign_bit * 0xffff
243243
// }
244244

245245
// chunks 0..4 are used for linear constraint later on to form imm_low

cs/src/machine/ops/mul_div.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -306,7 +306,7 @@ impl<
306306
// default value is as-is it was divisor == 0
307307

308308
let quotient = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::constant(u32::MAX);
309-
let remainder = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::constant(0);
309+
let remainder = divident_unsigned.clone();
310310

311311
let masked_divisor = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::select(
312312
&divisor_is_non_zero,

docs/delegation_circuits.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,14 @@ Currently, in our system, we have three delegation circuits implemented:
2020

2121
---
2222

23+
### Trusted-code guarantees
24+
25+
All delegations rely on the same **trusted-code** assumption as the base machine: Airbender currently proves only M-mode firmware that has been audited and compiled specifically for the circuit. Because we know the bytecode never emits illegal combinations, the circuits stay permissive about edge selectors such as `control_mask = 0` or a zero `round_bitmask`. We still flag these during development—the simulator panics on zero masks so authors catch mistakes but the proving circuit accepts them, since the production binaries never hit those paths.
26+
27+
This does not create an exploit. Forcing a zero mask merely yields a proof that nothing happened (all-zero accesses, all-zero outputs), comparable to calling an Ethereum precompile with empty calldata—valid, yet useless. Real faults such as divide-by-zero, overflow, or invalid opcodes already render the constraint system unsatisfiable, so a malicious witness can’t smuggle work past the verifier. When we expand to user-mode/untrusted programs, we will revisit these guards and add stricter checks in-circuit.
28+
29+
---
30+
2331
### BLAKE2 single round
2432
A fast cryptographic hash function built from add/xor/rotate G rounds over 32-bit words, it achieves high performance on CPUs and GPUs, keeping Merkle commitments and recursion fast. The function is circuit-friendly, as its operations decompose into simple XOR/bitwise lookups and additions, making it efficient as a delegation circuit, and it produces compact 256-bit outputs suitable for commitments.
2533

tools/generator/output/machine_without_signed_mul_div_witness_generation_fn.cuh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ SHR(u32, 22, 19, 16)
581581
FROM(u16, 23, 22)
582582
IF(0, SET_WITNESS_PLACE(19, 23))
583583
REM(u32, 25, 15, 17)
584-
SELECT(u32, 26, 11, 25, 9)
584+
SELECT(u32, 26, 11, 25, 15)
585585
FROM(u16, 27, 26)
586586
IF(0, SET_WITNESS_PLACE(20, 27))
587587
SHR(u32, 29, 26, 16)

0 commit comments

Comments
 (0)