diff --git a/files/Hard Reset.md b/files/Hard Reset.md index 19fed897..8ac80c15 100644 --- a/files/Hard Reset.md +++ b/files/Hard Reset.md @@ -13,103 +13,6 @@ --- -## Phase 2 — Canonical Layout + Verifier Contract (JVM-like Control Flow) - -### PR-04 (5 pts) — Rewrite layout to compute instruction boundaries via decoder (no heuristics) - -**Briefing** - -Layout must be computed canonically using the decoder, not guessed via ad-hoc stepping. - -**Target** - -`prometeu_bytecode::layout` becomes the only authority for: - -* function ranges `[start, end)` -* function length -* valid instruction boundaries -* pc→function lookup - -**Scope** - -* Implement layout computation by scanning bytes with the canonical decoder. -* Provide APIs: - - * `function_range(func_idx) -> (start, end)` - * `function_len(func_idx)` - * `is_boundary(func_idx, rel_pc)` or `is_boundary_abs(abs_pc)` - * `lookup_function_by_pc(abs_pc)` - -**Requirements Checklist** - -* [ ] No “clamp_jump_target” or tolerant APIs remain. -* [ ] Layout derived only via decoder. - -**Completion Tests** - -* [ ] Unit tests: boundaries for a known bytecode sequence. -* [ ] Fuzz/table tests: random instruction sequences produce monotonic ranges and valid boundaries. - ---- - -### PR-05 (3 pts) — Verifier hard reset: branches are function-relative only - -**Briefing** - -The verifier must not guess absolute vs relative. One encoding only. - -**Target** - -Branches use `immediate = target_rel_to_function_start`, with `target == func_len` allowed. - -**Scope** - -* Replace any dual-format logic. -* Validation: - - * `target_rel <= func_len` - * if `target_rel == func_len`: OK (end-exclusive) - * else target must be an instruction boundary -* All boundary checks must come from `layout`. - -**Requirements Checklist** - -* [ ] No heuristics. -* [ ] Verifier depends only on layout + decoder. - -**Completion Tests** - -* [ ] JumpToEnd accepted. -* [ ] JumpToMidInstruction rejected. -* [ ] JumpOutsideFunction rejected. - ---- - -### PR-06 (3 pts) — Linker hard reset: never relocate intra-function branches - -**Briefing** - -Linker must not rewrite local control-flow. - -**Target** - -Remove any relocation/patching for `Jmp`/`JmpIf*`. - -**Scope** - -* Delete branch relocation logic. -* Ensure only symbol/table/call relocations remain. - -**Requirements Checklist** - -* [ ] Linker does not inspect/patch branch immediates. - -**Completion Tests** - -* [ ] Link-order invariance test (A+B vs B+A) passes for intra-function branches. - ---- - ## Phase 3 — JVM-like Symbol Identity: Signature-based Overload & Constant-Pool Mindset ### PR-07 (5 pts) — Introduce Signature interning (`SigId`) and descriptor canonicalization diff --git a/test-cartridges/canonical/golden/program.pbc b/test-cartridges/canonical/golden/program.pbc index 3646ac85..5a70490d 100644 Binary files a/test-cartridges/canonical/golden/program.pbc and b/test-cartridges/canonical/golden/program.pbc differ