Skip to content

feat(verified): PoC static region + two compatible slots, sealed A -> B frontier (#6656) - #6678

Merged
gHashTag merged 1 commit into
claude/verified-frontier-6655from
claude/verified-poc-6656
Oct 6, 2026
Merged

gHashTag merged 1 commit into
claude/verified-frontier-6655from
claude/verified-poc-6656

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 6, 2026

Copy link
Copy Markdown
Owner

Closes #6677
Refs #6656, #6655. Stacked on #6674, which is stacked on #6671.

What

This is the software and forge half of the Phase 0 MVP. Everything is under specs/verified/poc/:

File Role
static_counter.t27 (PocStatic) Static region, a clocked 8-bit counter
a/slot.t27, b/slot.t27 (PocSlot) Two implementations of one slot. Same module and same on_comb(x: u8) -> u8. A passes the input through; B inverts it.
run.t27 (PocRun, use verified::frontier;) The A -> B step, judged by the frontier rule

Evidence

Run on the Railway lab with master t27c 1c0299f59 and zig 0.16.0. Every observation comes from a tool:

  • t27c seal --verify reports all hashes MATCH for all four specs.
  • The module PocSlot (...) headers from gen-verilog for A and B are byte-identical (diff exit 0): clk, rst_n, en, x[7:0], ready, result[7:0].
  • The seals differ. spec_hash is c0f23686... for A and 64be0a9d... for B; gen_hash_verilog is 895d022b... and ce531941....
  • run.t27 passes 4 of 4 tests:
    • static region REUSE, slot REBUILD_SPEC;
    • a new toolchain reuses nothing;
    • the injected failure (B's test edited from 250 to 251, run twice, same assertion both times) gets one fingerprint;
    • hw_state(true, false) == HW_UNPROVEN.

What this does NOT show

  • No device was programmed. No bitstream was built, and nothing was loaded into a partial region. Hardware is UNPROVEN.
  • The lab has no yosys or iverilog, so there was no synthesis or simulation either.
  • "Static reused" here means the static spec's seal is unchanged and nothing links it to the slot. Nothing was measured as kept running across a reconfiguration.
  • Feeding seals into frontier.t27 is still done by reading them. A tri command that reads the seals itself would be the next child; it needs the toolchain identity in the seal, which is a compiler change.

🤖 Generated with Claude Code

… B frontier (#6656)

specs/verified/poc/: static_counter.t27 (static region, clocked counter),
a/slot.t27 and b/slot.t27 (two implementations of module PocSlot with the
same on_comb signature), run.t27 (the A -> B step judged by frontier.t27).

Evidence from master t27c 1c0299f + zig 0.16.0 on the Railway lab:
seal --verify all hashes MATCH for all four; gen-verilog `module PocSlot`
headers of A and B byte-identical; A and B spec_hash differ; run.t27 4/4:
static REUSE, slot REBUILD_SPEC, new toolchain reuses nothing, injected
failure has one fingerprint, hardware UNPROVEN. No device was programmed.

Closes #6677
Refs #6656, #6655

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant