HashSigs RHDL privacy-sanitized source narrative Evidence record: production-verifier-source-finite Repository-relative source: crates/wots-rhdl/VERIFIER_TOP_EVIDENCE.md Cryptographic subject/source commit: 892b7e62ed45e766033a382ba46b89ad0d18599b Cryptographic source dirty: no Pre-sanitization narrative SHA-256: b1477af52001d0b29dba4f0341ff31e3d0386351498f74d8f1222f5282da7537 Narrative checkout commit: 3810cf837ea79ca005f4ab227b0b5c2134fe6ad1 Narrative checkout dirty: no Sanitization substitutions: private build-host label: 1 -> [remote-build-host] This public projection is not byte-identical when substitutions are listed. The digest identifies the pre-sanitization narrative bytes read by this documentation build. It does not assert that those bytes existed at the cryptographic subject commit. --- sanitized narrative --- # Three-cluster SHA-256 verifier-top evidence Status: Rust/RHDL source and behavioral simulation evidence. The separately linked modular hierarchy has a capped source-descriptor gate; this is not synthesis, timing, route, or hardware evidence. ## Implemented hierarchy [`VerifierTop`](src/verify/top.rs) is generic over the same `CompressionLaneComponent` used by the signer cluster. It contains exactly three ordinary [`VerifierCluster`](src/verify/cluster.rs) children. Each cluster contains four verifier contexts and one exact-64-cycle compression lane, giving 12 physical verifier contexts and three independent lane issue slots. The hierarchy rule is deliberate: the top replicates complete ordinary cluster parents, never an unresolved external leaf. The available build aliases are: - `Sha256VerifierTop`: three inline RHDL SHA-256 lanes for source simulation; - `ModularSha256VerifierTop`: three separately linked lane leaves behind one replicated ordinary-cluster prototype. Both aliases implement the SHA-256 performance profile. They are not compatible with the separately typed `LEGACY_KECCAK` key/signature domain. ## Admission and identity Beat zero strictly targets the cluster named by the registered rotating cursor; child ready never participates in valid selection. If that target is busy, the top holds a one-hot offer there even when another cluster is ready. This bounded head-of-line stall is the deliberate cost of a ready-independent hierarchy. After accepted beat zero, the cursor rotates and the selected cluster, physical context, and assigned generation are captured as one internal identity. The top then locks that cluster for exactly 35 accepted beats and advances its own fixed beat counter; untrusted `last` never releases ownership. The top presents `stream_valid` and the exact payload to one selected cluster independently of that cluster's `stream_ready`. A stalled active-frame offer is held at the registered owner without advancing either frame counter. Acceptance is the common top/child event: ```text top.stream_accepted == selected cluster.stream_accepted == selected cluster input stream_valid && selected cluster.stream_ready ``` No unselected cluster ever sees input valid. An unaccepted valid offer causes no child state transition or cursor advance. A beat-zero accepted on a fault-containment edge still records its job ID, cluster, context, and generation before registered poison begins drainage. The implementation muxes stream ready, context, and generation as separate scalar fields; it never selects the whole cluster output aggregate into the admission path. The three cluster inputs are likewise complete direct literals. One-hot stream-valid depends only on the registered target/owner and top-local gates; one-hot result-ready depends only on the independent result selector. A focused collision gate proves an accepted offer to cluster 0 can coexist with a result grant to cluster 2, while a clean-versus-current-fault pair proves fault changes the grant vector but not any cluster stream-valid bit or common payload. ## Result merge The three cluster result slots feed a rotating fair one-entry top slot. A top slot may transfer and be replaced on the same edge. While stalled, its payload and source-cluster identity remain stable. The first visible global fatal edge has strict result precedence: - no retained result transfers; - no child result is captured or released; - a retained clean completion preserves its job/source identity and is converted to `verified = false, error = TRANSPORT`; - an existing nonzero per-job error is preserved. After global poison, the `drain_armed` register waits one complete abort-settle cycle before selection. Selection then depends only on registered child `result_valid`, not payload data that could feed the child's release wire. Capture defensively converts an unexpected clean payload to an identified transport error and preserves every existing nonzero error. ## Fault-containment timeline A child response rejection depends on observing the exact physical response. Feeding that current observation back through admission would create `response -> rejection -> credit -> child frame_start -> rejection`. The tested cycle cut keeps result fatality immediate while honoring already-advertised stream credit: | Cycle | Contract | |---|---| | `c` | One cluster exposes the first fault. Top fault/diagnostics and first-cause snapshots are immediate. Result transfer/capture is suppressed and a clean top slot is converted. At most one already-credited stream beat may be accepted; if so it is reported and delivered to exactly one selected cluster with full identity. Top poison D is set. | | `c+1` | Registered top poison removes global stream credit and sends neither a cluster input beat nor a child-result grant. `external_abort` is broadcast to all three clusters and `drain_armed` remains false. The command changes only each still-clean peer's poison, frame-clear, and diagnostic D state; all peer outputs remain independent of it. At most one lane launch, one routed return, and one internal result capture for already-accepted work may advance in each peer. | | `c+2` | Registered peer-cluster poison asserts every public cluster fault, exposes the peer external-abort diagnostics, reaches contexts/transport, and blocks every later lane launch and response route. Identified partial/full jobs convert to retained transport errors. Top child-result drainage is armed. | | later | Every accepted full or partial job drains exactly once as a nonzero error; no new admission or lane launch occurs until shared reset. | Thus `fault && stream_accepted` is legal only on the original containment edge. Global stream credit is absent from `c+1`; once peer poison is registered at `c+2`, every cluster lane launch and routed return remains false until reset. The first-cause state is stable while poisoned: - a three-bit origin-cluster mask; - one 16-bit diagnostic snapshot for each cluster; and - a top-local diagnostic mask for cluster origin, ownership mismatch, and invalid admission/result cursors. Peer abort diagnostics cannot overwrite that snapshot. ## Behavioral gates All commands are run serially in the isolated verifier-top worktree. ```text cargo test -j1 -p wots-rhdl --lib --test verify_cluster --test verify_top -- --test-threads=1 ``` Result: 16 library tests, 9 cluster integration tests, and 3 active top integration tests passed; the resource-intensive modular descriptor test was explicitly ignored in this batch. Coverage includes: - strict registered-cursor beat-zero targeting, including a target stall while another cluster is ready, plus ready-independent active-frame offers and exact top/child acceptance equality through scalar-only stream muxes; - simultaneous independent stream, result-grant, and response fields at both hierarchy boundaries, with clean/fault and offer/no-offer toggle checks; - beat-zero and mid-frame containment-edge acceptance with exact child delivery, identity preservation, immediate result suppression, and next-cycle poison; - fair locked allocation across all 12 contexts and generation increment on reuse; - deterministic result backpressure and elastic replacement; - one injected local lane fault, stable first-cause snapshots, output-independent peer-abort transition with bounded internal progress, zero physical effects after registered peer poison, and exactly-once `TRANSPORT` completion for every accepted full or partial job; and - reset-only recovery. ```text ulimit -v 6291456 CARGO_BUILD_JOBS=1 cargo test --locked -j1 -p wots-rhdl --test verify_top_full \ production_sha256_verifier_top_saturates_twelve_worst_case_jobs_exactly \ -- --ignored --exact --nocapture --test-threads=1 ``` This gate uses the actual inline RHDL full-compression lane in all three clusters. It resets a sacrificial mid-flight operation, admits 12 oracle-valid worst-case frames, enforces deterministic result stalls, and checks all accepted-request/routed-response accounting, identities, exact SHA work, and quiescence. Result: 1 exact ignored test passed in 110.12 seconds. The final finite source trace was: ```text admissions 245..=630 (386 cycles) SHA issues 282..=5565 (5284 cycles, 12480 accepted) routed returns 12480 deliveries 5256..=5632 (377 cycles) first result held 9 cycles total modeled cycles 5778 ``` Thus all `12 * 1,040 = 12,480` worst-case SHA tasks were accepted and exactly 12,480 returns were routed before quiescence. These are source-simulation cycle counters, not emitted-RTL equivalence, throughput, timing, or hardware evidence. ```text ulimit -v 6291456 CARGO_BUILD_JOBS=1 cargo test --release --locked -j1 -p wots-rhdl --test verify_top \ modular_sha256_verifier_top_is_an_unresolved_direct_child_skeleton \ -- --ignored --exact --nocapture --test-threads=1 ``` This capped gate constructs the complete modular source descriptor and inspects its unchecked unresolved skeleton. It requires one replicated ordinary cluster prototype, three cluster instances, one unresolved compression-lane leaf inside that prototype, and no locally emitted definition for the external leaf. Its final immutable source hashes were: ```text cluster.rs 30414d5c7c9eea6e779b35611532dbe3c8716a951a62fe2d7de0f3e379cc13bc top.rs c41589afd328bc1fd48667bf4c1108ffaa7789710753b1087765fdc3a2664a44 verify_top.rs a35efe2df1de6db3841b2c418fa3da6e1942d00838fe2e1a8fd8da1afab55e68 ``` Result: 1 exact ignored test passed in 64.41 seconds in the release profile under the 6 GiB virtual-memory cap. The expected unresolved-leaf checked-accessor failure reported `sha256_compression_lane` at all three cluster references; the unchecked skeleton then satisfied the exact prototype, instance, leaf, and missing-local-definition assertions. This is successful modular source descriptor evidence, not linked RTL, synthesis, timing, route, or hardware evidence. The last pre-cut attempt failed after 242.73 seconds with exit 101, below the 6 GiB cap, due to an RHDL `NetLoopError` between `contexts[3].response_rejected` and `responses[3].valid`. That negative result motivated the explicit containment-edge admission boundary above; it was not a memory-cap failure and is not reported as successful RTL evidence. A later pre-final attempt proved that response-rejection loop absent, but failed after 524.73 seconds with exit 101 on a distinct peer-drain SCC: `cluster.external_abort -> cluster.result.error -> top result eligibility -> cluster.result_ready`. It also remained below the cap (approximately 5.25 GiB VSZ and 3.25 GiB RSS when sampled). The final source removes payload data from the poisoned ready/grant decision and defensively fail-closes the payload only after selection. This intermediate failure is likewise negative diagnostic evidence, not a successful descriptor claim. The first attempt after that data/control separation failed after 544.85 seconds with exit 101 on the remaining public-status echo SCC: `top cluster_fault -> registered-abort command aggregate -> peer cluster_fault`. The previous payload/error SCC was absent. Sampled high-water memory remained below the cap (`VmPeak` 5,259,896 kB; `VmHWM` 4,599,300 kB). Removing only the same-edge public fault echo proved insufficient: the later release-profile gate identified the remaining command-to-datapath path documented below. Two subsequent debug-profile descriptor processes were terminated externally with exit 143 after approximately six minutes. Neither printed an RHDL result, both remained below the 6 GiB cap. The first sampled `VmPeak` 5,248,888 kB and `VmHWM` 4,429,916 kB; the second sampled `VmPeak` 3,621,872 kB and `VmHWM` 2,684,360 kB. They are infrastructure-inconclusive runs, not successful or negative lowering evidence. The same capped gate in the release profile then produced a definitive RHDL `NetLoopError` after 67.00 seconds. Its remaining SCC was `peer cluster fault -> child response rejection/valid -> cluster stream accepted/ready -> peer external_abort -> peer cluster fault`. The final source therefore makes `external_abort` transition-only: it records local D state but has no command-edge effect on any cluster output. Registered peer poison contains the cluster on the following cycle. A subsequent release-profile diagnostic after that abort cut failed after 68.51 seconds with another `NetLoopError` while remaining below the cap (`VmPeak` 5,317,936 kB; `VmHWM` 4,660,476 kB). A test-only lint cleanup overlapped this run's startup, so it is not accepted as final descriptor provenance. Its named SCC nevertheless exposed the remaining protocol path: `cluster fault -> child response rejection/response valid -> cluster stream accepted -> selected cluster stream_valid -> cluster fault`. The current source removes both structural causes. Beat-zero valid is a one-hot offer selected only from the registered normalized admission cursor; active-frame valid uses only the registered owner; neither observes child ready. Acceptance alone observes the scalar selected-ready field. Ready, context, and generation are separately muxed scalars rather than a selected whole-cluster aggregate. The next frozen strict-cursor/scalar-mux release gate still failed after 67.60 seconds with the same named SCC, below the cap. Source-range mapping localized the remaining edges to dynamically mutated child-input aggregates: top `cluster_inputs[selected].stream_valid` shared construction with fault-dependent dynamic `result_ready`, and cluster `context_inputs[selected].stream_valid` shared construction with context result grants and routed responses. The current source removes both mutation blocks. It computes independent scalar one-hots and constructs three complete cluster-input literals plus four complete context-input literals with constant field indices. ## Evidence limits and remaining work - Behavioral simulation and descriptor construction do not establish emitted RTL equivalence for the inline top. - An unresolved modular skeleton is a linkage artifact, not proof that a linked lane netlist synthesizes or routes. - No resource, frequency, initiation-interval, signatures-per-second, power, or U280 claim is inferred from source geometry or cycle accounting. - Synthesis, post-synthesis timing/resources, implementation, route, and hardware execution require separate [remote-build-host] evidence under the repository's evidence-tier rules.