fix: constraint, trace and emulator defects found by a chip eval review - #111
Merged
Conversation
The loader walks segments 4 bytes at a time but stores 8-byte blocks, so a segment whose file-backed data ends in the low half of a block gets its BSS pass aimed at that same block. `BTreeMap::insert` replaces the whole entry, so those bytes were dropped and the committed `memory_image` no longer matched the ELF. `entry().or_insert(0)` creates the block only when absent, which is correct because the half each BSS iteration covers is already zero: a block that exists was built from a single 4-byte word. Triggered by `p_filesz mod 8` in 1..=4 with nonzero trailing bytes -- an ordinary `static mut u32` at a .data/BSS boundary is enough. The image of every ELF in this repo is unchanged, so no key material is affected.
`memory_image` stores 8-byte blocks while the segment loop walks 4 bytes at a time, and the two halves are merged by addition. That is sound only while each half is written once: two overlapping segments would silently sum two different values instead of one replacing the other. Ascending order is also the premise the BSS zero-fill relies on -- it is what makes "file-backed and BSS ranges are disjoint" hold across segments and not just within one. The ELF spec already requires PT_LOAD entries sorted on p_vaddr, so this rejects malformed input rather than restricting legitimate input. Every ELF in this repo still loads.
`Program::fetch` indexes the flat `instructions` vector as `(pc - pc_base) / 4`, but nothing checked that the executable segments it is built from are contiguous. A gap -- between two PF_X segments, or left by a BSS tail on one, since only file-backed words are pushed -- shifts every later instruction to the wrong address, and the preprocessed program table commits to that mapping. Each executable segment after the first must now begin exactly where the accumulated instruction stream ends. Ascending order is enforced by the previous commit, so the first executable segment is also the lowest, which is what `pc_base` must be; the old "lowest vaddr wins" scan is now redundant and gone. Every ELF in this repo still loads, with `pc_base` and instruction counts unchanged.
Two regions sit below `2^16` and neither can host a segment:
- `[0, NUM_REGISTERS)` is the register file. A segment there aliases a
register, which the emulator only catches with a `debug_assert!` that
compiles away in release -- the same builds that produce proofs.
- `[NUM_REGISTERS, 2^16)` is unreachable by any provable data access: the
memory chip's stack guard forces `addr[1] + addr[2] != 0`, so a load or
store below `2^16` has no satisfying trace.
Rejecting the segment at load time turns both into a deterministic parse
error instead of a release-mode aliasing bug or a proof that cannot be
produced.
The bound is exact, not conservative. Every ELF in this repo has its lowest
PT_LOAD at 0x10000 -- the linker's default image base for non-PIC links,
which is what applies here since ET_EXEC is already required. `-Ttext`
moves .text to 0x200800 but leaves the headers at the image base, so
raising this bound by one byte would reject all of them.
The preprocessed program table carries one row per instruction, so the
instruction count decides whether the program can be shaped at all.
Neither end was checked:
- An executable segment with no file-backed bytes leaves `pc_base` set
and the table empty, so every `Program::fetch` indexes out of bounds.
- `RiscvShapeConfig`'s `program_heights` tops out at `2^22` rows, so a
larger program has no shape to fit into; failing during shape
assignment is far from the cause.
Both are now parse errors. The largest ELF in this repo has 548,975
instructions, well inside the bound.
Every release crate inherits from `[workspace.package]`, so the root manifest is the only one that changes. `cargo update --workspace` keeps the root lock diff to the nine workspace members, and the bench-apps lock is updated for the four pico crates it pins by path; no other dependency moves.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Constraint, trace and emulator fixes from a review of chip
evalimplementations.Issue coverage
Closes #101 — all 13 listed defects are covered.
Closes #104 — Both issues are fixed here.
Closes #105 — the memory timestamp binding is included. The ECRecover hook hardening is not included and is not needed.