docs: trusted-code assumptions

cs/src/machine/decoder/decode_optimized_must_handle_csr.rs

@@ -238,9 +238,10 @@
         // chunk3 = (i_insn + s_insn) * sign_bit + b_insn * imm11 + j_insn * rs2_low
         // chunk4 = (i_insn + s_insn + b_insn) * sign_bit * 0b1111 + (u_insn + j_insn) * (rs1_low << 3 + funct3)
         // chunk5 = {
         //      j_insn * (sign_bit * 0xfff0 + rs1_high) + u_insn * insn_high +
-        //      (1 - j_insn - b_insn) * sign_bit * 0xffff
+        //      (1 - j_insn - u_insn) * sign_bit * 0xffff
         // }
+
 
         // chunks 0..4 are used for linear constraint later on to form imm_low
         let chunks_defining_constraints: [Constraint<F>; 5] = [

cs/src/machine/ops/mul_div.rs

@@ -306,7 +306,7 @@ impl<
                 // default value is as-is it was divisor == 0
 
                 let quotient = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::constant(u32::MAX);
-                let remainder = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::constant(0);
+                let remainder = divident_unsigned.clone();
 
                 let masked_divisor = <CS::WitnessPlacer as WitnessTypeSet<F>>::U32::select(
                     &divisor_is_non_zero,

docs/delegation_circuits.md

@@ -20,6 +20,14 @@ Currently, in our system, we have three delegation circuits implemented:
 
 ---
 
+### Trusted-code guarantees
+
+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.
+
+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.
+
+---
+
 ### BLAKE2 single round
 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.