Skip to content

Phase 0 (#6656): software half of the incremental-update PoC -- static region, two compatible slots, sealed A -> B frontier #6677

Description

@gHashTag

Goal

Do the software/forge half of #6656 (parent EPIC #6655). It needs one static region, one reconfigurable slot with two compatible implementations, seals for each, and the A -> B step judged by specs/verified/frontier.t27 (#6673): the static region is reused, the slot is rebuilt. Hardware stays UNPROVEN.

Where we are

reuse.t27 (#6670, PR #6671) and frontier.t27 (#6673, PR #6674) define the rule. The repo has no partial-reconfiguration spec. The smallest clocked example is specs/ternary/clocked_counter.t27.

Boundary

Allowed: specs/verified/poc/** and the seals t27c seal --save writes for those specs (.trinity/seals/poc_PocStatic.json, a_PocSlot.json, b_PocSlot.json, poc_PocRun.json).
Out of bounds: the compiler, tri, specs/fpga/**, any bitstream, any device programming, any claim of a real partial-device update.

User Scenarios & Testing

  • Given slot A and slot B, when t27c gen-verilog runs on each, then the module PocSlot (...) header is byte-identical.
  • Given A -> B with the same toolchain, then the frontier reuses the static region and rebuilds the slot (REBUILD_SPEC).
  • Given a different toolchain, then nothing is reused.
  • Given the same injected test failure twice, then the same fingerprint, and the second sighting updates the issue rather than opening a new one.
  • Given no device evidence, then the hardware state is UNPROVEN.

Requirements

  • FR-001: Pure .t27; every observation is produced by t27c seal or t27c gen-verilog, not typed by hand.
  • FR-002: No hardware claim.

Success Criteria

  • t27c seal <spec> --verify prints all hashes MATCH for static_counter, a/slot, b/slot and run.
  • t27c gen + zig test passes for each of the four specs; run.t27 prints All 4 tests passed.
  • The module PocSlot ( ... ); blocks of the gen-verilog output for a/slot and b/slot differ by zero lines (diff exit 0).
  • spec_hash in a_PocSlot.json differs from b_PocSlot.json.
  • run.t27 asserts hw_state(true, false) == HW_UNPROVEN.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions