spec: COMMIT chip

[erik-3milabs]

In addition to introducing the COMMIT chip, this PR also updates the way footnotes are numbered, by wrapping numbers with square brackets. This is to prevent footnotes as being interpreted as exponents.

[erik-3milabs]

Currently, it is possible to have a 2^64-length recursion by starting an ECALL[64] with count = 0.
We could prevent this from happening, but doing so would probably add a column. Is this a problem we really want to prevent?

[greptile-apps]

Greptile Overview

Greptile Summary

Introduced the COMMIT chip specification that handles writing to stdout via RISC-V system call 64 (sys_write), implementing a recursive byte-by-byte commit mechanism. Updated footnote numbering format from superscript to square brackets [1] to prevent misinterpretation as mathematical exponents.

Major Changes:

• Added new COMMIT chip with recursive design that processes buffer writes one byte at a time
• Defined chip variables including address, count, first, last, and recursion tracking
• Implemented constraints for reading register values (x10-x12), memory interactions, and recursive calls via CNB (Commit Next Byte) tag
• Added "About ECALL" section documenting RISC-V system call ABI conventions
• Updated footnote numbering format to [1] style across the specification

Issues Found:

• Three syntax/grammar errors in spec/ecall.typ (incorrect function signature, duplicate word, missing word)

Confidence Score: 4/5

• Safe to merge after fixing minor syntax/grammar issues in documentation
• The core logic and constraint definitions in the COMMIT chip appear sound and well-structured. The recursive design is properly constrained with first/last flags and appropriate multiplicity tracking. However, documentation contains three syntax errors that should be corrected before merge
• spec/ecall.typ needs attention for syntax corrections (lines 97, 110, 123)

Important Files Changed

Filename	Overview
spec/ebook.typ	Added footnote numbering format with square brackets to prevent misinterpretation as exponents
spec/ecall.typ	Added About ECALL section and complete COMMIT chip documentation with syntax and grammar issues
spec/src/commit.toml	New TOML configuration defining the COMMIT chip with variables, constraints, and recursion logic

Sequence Diagram

sequenceDiagram
    participant CPU
    participant COMMIT as COMMIT Chip
    participant Memory
    participant Stdout

    Note over CPU,COMMIT: ECALL with syscall 64 (sys_write)
    CPU->>COMMIT: ECALL(timestamp=T, syscall=64, first=1)
    
    Note over COMMIT: Read register values
    COMMIT->>Memory: Read x10 (fd, expect 1)
    Memory-->>COMMIT: fd=1
    COMMIT->>Memory: Read x11 (address)
    Memory-->>COMMIT: address=A
    COMMIT->>Memory: Read x12 (count)
    Memory-->>COMMIT: count=N
    
    Note over COMMIT: Write count back to x10
    COMMIT->>Memory: Write x10=N
    
    Note over COMMIT: Recursive commit loop
    loop For each byte (count > 0)
        COMMIT->>Memory: Read byte at address
        Memory-->>COMMIT: value=V
        COMMIT->>Stdout: COMMIT(index, value)
        
        Note over COMMIT: Compute next iteration
        COMMIT->>COMMIT: address_incr = address + 1
        COMMIT->>COMMIT: count_decr = count - 1
        
        alt count_decr > 0
            Note over COMMIT: Recursive call (first=0)
            COMMIT->>COMMIT: CNB(timestamp, address_incr, count_decr)
        else count_decr == 0
            Note over COMMIT: Set last=1, stop recursion
        end
    end
    
    COMMIT-->>CPU: Return (count written to A0)

Loading

[greptile-apps]

_{3 files reviewed, 3 comments}

_{Edit Code Review Agent Settings | Greptile}

[RobinJadoul]

Currently, it is possible to have a 2^64-length recursion by starting an ECALL[64] with count = 0.
We could prevent this from happening, but doing so would probably add a column. Is this a problem we really want to prevent?

I think a write with count = 0 is a valid thing to do, and this would render it unprovable.
From man 2 write:

If count is zero and fd refers to a regular file, then write() may return a failure status if one of the errors below is detected. If no errors are detected, or error detection is not performed, 0 will be returned without causing any other effect. If count is zero and fd refers to a file other than a regular file, the results are not specified.

What about turning last into end, representing count = 0, where we enforce μ = 0 => end = 1 and performing both CNB and COMMIT with multiplicity 1 - end?

[RobinJadoul]

Nice, seems like this should work.
I'm thinking that we may not really need μ, as first and end may be enough.
You get a weird thing about the ZERO for end needing a multiplicity depending on end, but it could still work out due to interaction balancing.

[erik-3milabs]

@greptileai

[RobinJadoul]

A couple ideas for potential optimizations, but maybe we should just go for "works" for now, and work towards something better with the kernel.
I'd still write down our assumptions to be explicit, but otherwise this should be fine.

I'm starting to think now of "overcommitting" and having the ECALL return some "out of space" error, but let's maybe keep this for when we do a kernel-centric redesign.
For now, we don't need full genericity.

[RobinJadoul]

We could save an interaction by turning this into !end => count_decr = -1; which would require a full 2^64 extra commits to reach the next possibility to end and balance the logup sum otherwise.
That would even be impossible to prove due to addresses being read twice at the same timestamp.
If we replace count by a BaseField, this argument would weaken to only p extra "iterations" being impossible to prove.

[erik-3milabs]

How would that work? What about committing a sequence of 8 bytes. The first seven bytes will have end = 0, but we definitely don't want count_decr = -1 in those cases.

Perhaps you're misinterpreting what count_decr means? Note that count_decr := count - 1; it is not the value by which we decrease count, i.e., next_count := count - count_decr or smth.

[RobinJadoul]

I may have flipped the condition. The idea was that one direction of the ZERO implication didn't matter as much because it makes the overall system unprovable due to size

[erik-3milabs]

I think we would need end => count = 0; one cannot set the flag when count != 0, and if you "forget" when it is 0, you have to another round of 2^64 commits. Great observation!

[RobinJadoul]

We could get rid of this at the cost of one extra column for count as basefield that is populated conditionally from CNB or recomposed from the DWordWL count that came from the register.

[erik-3milabs]

am I correct in understanding that this proposal hinges on the assumption that count < p?

[RobinJadoul]

Hmm, yeah, that would also have to add an LT enforced with multiplicity first, I suppose