Feat: Ecall/Halt

[kunxian-xia]

Fixes #125.

• Ecall instruction config
• Ecall/Halt circuit.
• Added public input in the prover framework and allows the circuit builder to access public inputs.

[naure]

This does not check the exit_code.

The VM looks for the exit code in register x10 / a0 and requires it to be 0 for success.

VMState.ecall()

While non-zero values are an error, and they cannot be proven. E.g. panic is halt(1).

ceno_rt panic

There are two options:

1. Read the register CENO_PLATFORM.reg_arg0() with success value 0.
   … OR …
2. redefine halt to halt_success. In ceno_rt, call it only for success, not for panic:

pub fn halt(exit_code: u32) -> ! {
    if exit_code == 0 {
        // SUCCESS
        unsafe {
            asm!(
                // Set the ecall code HALT_SUCCESS.
                "li t0, 0x0",
            );
            riscv::asm::ecall();
        }
    }
    #[allow(clippy::empty_loop)]
    loop {}
}

[naure]

We define PC=0 as invalid, and no other instruction can execute after that. I would document this requirement right here as follows:

assert!(!CENO_PLATFORM.can_execute(0), "PC=0 means the program is terminated.");

[hero78119]

nitpick: we can define 0 as constant EXIT_PC to improve the readibility

[matthiasgoergens]

If you want PC=0 to be invalid, I would suggest also adding 0x0000_0000 in the first 32 bits of memory. Just for consistency. (32 bits of all zeroes is Risc-V's way of specifying a guaranteed invalid instruction in every version of the instruction set.)

[kunxian-xia]

As for exit_code, I plan to add it in the 2-tuple of global state (pc, ts) . That is,

• the global state becomes a three-tuple (pc, ts, exit_code).
• the global state is initialized to be (pc=PC_START, ts=0, exit_code=0); and only ecall/halt instruction will change exit_code to some non-zero value read from X10 register.

[naure]

That incurs a cost on every instruction then. There should be a better way.

For instance, initialize by writing state (pc_start, ts_start), and require a write of (pc=0, ts) to exist.

Or require the HaltCircuit to exist with exactly one instance.

[kunxian-xia]

That incurs a cost on every instruction then. There should be a better way.

The cost is negligible as we stores the rlc not the 3-tuple (or old 2-tuple).

[kunxian-xia]

For instance, initialize by writing state (pc_start, ts_start), and require a write of (pc=0, ts) to exist.

The problem with this approach is that we need to add a lookup record for program table. But we don't know that ecall/halt instruction's index/pc in the program.

[kunxian-xia]

As a desired feature of zkvm prover/verifier: we should skip generating opcode proof if the number of instances = 1. #288.

[naure]

How do you plan on checking the presence of the code in the state? However that works, it could check that (pc=0, ts=0) or whatever special value. Same as checking (pc, ts, code=1).

[naure]

That is not part of this PR though, right? That would be issue #127

[naure]

Regarding non-zero exit codes: this does not need to be supported by the zkVM circuits. It is just impossible to generate a proof for an execution that did not terminate correctly.

[naure]

That works now with the exit code!

[kunxian-xia]

Regarding non-zero exit codes: this does not need to be supported by the zkVM circuits. It is just impossible to generate a proof for an execution that did not terminate correctly.

No. For computation that ends with error we can detect it by exit_code. But for program that failed by misaligned memory address, that might be hard to prove.

[naure]

The cost is negligible as we stores the rlc not the 3-tuple (or old 2-tuple).

That is a lot of extended multiplications in the prover and verifier. I’d be interested to learn how much those weight though.

[kunxian-xia]

We assert that the value read from register x10 is equal to exit_code in the public inputs.

[hero78119]

awesome job!! 🔥 just left reviews with few questions

[hero78119]

nitpick: we can define 0 as constant EXIT_PC to improve the readibility

[hero78119]

A side topic: would we plan to separate public input into 2 kinds, one are hinted from prover, and the others are set from verifier directly? For those hinted from prover, we can have mark #[serde(skip)] to make proof size smaller

[matthiasgoergens]

A few notes on design:

Do we have use for exit codes that go beyond success / failure?

If not, we might want to consider using unimpl to abort execution. unimpl is the mnemonic for the instruction that consists of all 32 bits of 0. Fortunately, we don't actually have to add anything to the constraints: we already need constraints that forbid jumping to an illegal instruction.

For successful exit, ecall might be fine, but you can also consider using ebreak. That way, if you want to run your guest program hooked up to a debugger like gdb via (a slightly hacked up) qemu, for simple programs is will automatically do the right thing: fail for unimpl and halt for ebreak.

Making debugging simpler is one of the big lessons we learned from previously working on Mozak's zkVM.

Overloading ecall less, and using alternative means, might make our guest programs slightly more robust, as an attacker would have to work harder to change eg an IO system call into a successful exit. Or to change a program abort into an IO call or a successful exit.

[hero78119]

LGTM and nice job! +1 for resolving other pending issues in later PR