VERILOG-ROWS-0: prove compositional target emission with the board interlock by briansrls · Pull Request #8147 · gunb-ai/gunbc

briansrls · 2026-08-11T19:27:28Z

What this delivers

A board article that is admitted as a whole, projected to two languages through their own target authorities, and executed by real tools — Icarus Verilog simulated the emitted interlock, ngspice solved the emitted deck.

1. Verilog emits through the generic fold, with no compiler branch

The product-local Verilog printer is deleted. src/v2/extdeps/languages/verilog.dag owns the lexer, the ten formal productions, the layout transforms and the identifier admission; the product maps intent onto the target AST and nothing else. Relation rows are derived (derive_grammar_relation_row_node), not hand-authored, and backward selection is unique-structural-match on the emitted node.

A substrate asymmetry closed on the way: fixed_token_spelling_from_model now consults the emit-transform map, which previously only bound tokens did.

The first byte-exact green was a fixture echo — it replayed the exemplar's row regardless of input. The perturbation control caught it; the row is now derived from the program being emitted, and the control stays enrolled.

2. Nothing projects an unadmitted board

AdmittedBoardPowerInterfaceArticle is sole_constructor; admit_board_article is its only mint. Both production entry points take it. Proven by mutation: a cross-module literal is refused with sole_constructor type 'AdmittedBoardPowerInterfaceArticle' cannot be constructed outside its defining module.

Admission collects all causes rather than first-wins (a first-wins fold reports one defect per edit cycle, ordered by authoring accident). Twelve causes, each with a discriminating RED asserting exactly one cause and which one, plus a coherent positive control and a two-defects-two-causes claim.

3. A resistor rated in nanofarads has no constructor

Kind and value were two independently writable fields whose agreement nothing enforced. They are now one coproduct, so the invalid state has no representation rather than being refused after the fact.

4. The SPICE format module owns every byte

The product's element letters, reference node, field spacing and k/n suffixes are gone; it builds a SpiceNetlist and calls spice_emit. Three defects in that target module fell out and are fixed:

The constructor contributed nothing to the emitted bytes. The element letter arrived inside the name's spelling, so Resistor { name: c1 } emitted C1 ... and simulated as a capacitor. The letter now derives from the constructor.
The emitter was a fixture. spice_ident_spelling was a five-entry table (r1/c1/v1/n1/n2); anything else answered Absent, which spice_emit rendered as the empty string. Names carry their own spelling now, and admission refuses rather than sanitizing.
Scale suffixes are target-owned (SpiceScaleSuffix), so a magnitude cannot be spelled by a product.

The #8129 deck oracle and the pre-existing ngspice golden are byte-identical after all of it.

5. Real tools accepted the emitted bytes

Both artifacts were emitted from the .dag (gunbc run), not transcribed:

Icarus Verilog 11.0 compiled the module and simulated all four input combinations: permit only when conditioned-good holds and no fault is present; reset releases only behind permit.
ngspice-39 solved the operating point: pg_raw at 12 V, source current −1.2 mA. That figure is the discriminating one — a bare 10 would have solved cleanly and reported 1.2 A, so the run confirms the k suffix was read as kilo.

product.compute_board.simulation_receipt records each run with its tool subject and reported version. What it does not claim: nothing re-executes a simulator. The honesty mechanism is the enrolled witness beside it, which asserts the recorded artifact is byte-identical to what the projection emits today — so a stale receipt fails rather than continuing to vouch for an artifact nobody emits. Re-execution on a cadence is the next rung and is named, not claimed.

extdeps.simulators.icarus_verilog lands as its own subject with a runtime binding, parallel to ngspice. The self-host frontier rows for both SPICE and Verilog are regenerated to say what actually ran.

6. The firmware contract names the signals it rides on

PlatformFirmwareContract carried four prose strings, one of which said "board interlock asserts reset_release" about a signal the article declares. Preconditions now carry a typed PreconditionEstablishment: a board signal, a platform component, or an explicit "not this article's" (which is a claim, not an omission). Admission refuses a precondition naming an undeclared signal, and — the subtler one — a precondition established by an input, where the board would be claiming to establish a condition it only observes. Neither defect had a representation before.

Five platform firmware roles replace the single string. Three resolve to cited upstream subjects fetched live (Trusted Firmware-A, TianoCore EDK II, OpenBMC); two answer UpstreamNotModelledHere with a reason, because "nobody has cited this yet" and "there is nothing to cite" are different states and an Optional would fuse them.

A §3 fork surfaced and is recorded rather than papered over: std.bmc already carries OpenBmc as an enum arm naming the very project this module cites.

Rung, stated honestly

Structurally impossible: projecting an unadmitted article; a component whose kind disagrees with its value's dimension; a SPICE element whose emitted letter disagrees with its constructor.
Mechanically preventable: every admission cause; identifier admissibility; the receipt-to-emission join.
Observed once, not guaranteed: the two simulator runs. Named as such; the cadence that would raise them is the declared next trigger.

Not in scope

Geometry, placement, routing, manufacturing bytes, Altra contact ingestion. Byte-level reparse of emitted Verilog is not executable — v2.compiler.ingest starts at a ParseTree and nothing in .dag lexes text. That is a substrate gap, declared rather than worked around; the token spine is read back to the same emitted node instead.

First increment of the compositional-emission proof: the lexical vocabulary and the formal productions the interlock module needs, authored as grammar rather than as a printer. WHY THIS SHAPE. Rows are DERIVED from formal productions plus an exemplar (derive_grammar_relation_row_node), not hand-authored token lists, so the authored artifact is the grammar and emission is its backward reading. The template is TypeScript's PR3 target, which already exercises every mechanism this needs: grammar_formal_terminal for concrete tokens, grammar_formal_terminal_bound for bound names, and grammar_formal_nonterminal_occurrence for composition — plus two productions sharing one lhs, which is how alternation and optionality are expressed. COMPOSITION IS THE POINT, so the productions are recursive where a fixture would have been flat. The port list is right-recursive rather than three hard-coded slots, so two ports and four ports are the same grammar; expressions nest through expr_primary -> expr_unary -> expr_conjunction so a negation inside a conjunction derives from structure. A row whose token list happened to spell the whole module would only be the hand serializer moved into data, which is explicitly not the deliverable. Verified: compiles with ZERO new diagnostics. Baseline and this head both report the same 33 pre-existing annotation diagnostics in unrelated test files, so the comparison is against a measured baseline rather than an absent one. Not yet done, and this commit claims none of it: the exemplar emitted nodes, the translation-rules wiring, the product mapping from DigitalControlIntent, byte equality, bounded reparse, and the perturbation/reorder/ambiguity controls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-08-11T19:29:29Z

Finding: alternation requires structural difference — the `direction` productions as committed are unselectable

Reading formal_production_unique_lhs_exact_match (src/v2/std/grammar.dag): productions sharing an lhs are selected by unique structural match against the emitted node, and several matches yield grammar_relation_row_backward_selection_ambiguous.

Concrete terminals contribute no child to the emitted node. So these two, as committed in bc5a2ecc4a:

direction → kw_input
direction → kw_output

both emit an empty Conj, match indistinguishably, and would refuse as ambiguous. This is a defect in this PR, not in the substrate.

TypeScript's pr3_typed_params_opt alternation works because its alternatives differ in child count (empty vs one nonterminal occurrence). I generalized from "two productions may share an lhs" without checking what makes them selectable.

Fix direction: carry the direction as a bound terminal whose spelling supplies input/output, rather than as alternation between two concrete-only productions. That needs a single lexical class covering both keywords, since KeywordPattern takes one literal text. Not landing it half-done.

Silver lining: the spec's required control — "introduce a second relation that claims the same emitted shape; the generic path must return its existing ambiguity diagnostic rather than selecting whichever row appears first" — is already implemented in the substrate and will pass without new work. The refusal is grammar_relation_row_backward_selection_ambiguous.

This is the kind of constraint the spike exists to surface, and it argues the spike was correctly scoped as its own PR rather than bundled behind the article-admission work.

— sent from zesty-heron-736

…a spelling Fixes the defect flagged on this PR: `direction -> kw_input` and `direction -> kw_output` were unselectable. Productions sharing an lhs are selected by UNIQUE STRUCTURAL MATCH against the emitted node (formal_production_unique_lhs_exact_match), and a concrete terminal contributes NO child to that node. Both alternatives therefore emit an empty Conj, match indistinguishably, and refuse as grammar_relation_row_backward_selection_ambiguous. TypeScript's params_opt alternation works only because its alternatives differ in child count — empty versus one nonterminal occurrence. So alternation expresses OPTIONALITY and SHAPE, never a choice between two spellings. A spelling choice is a binding. Direction is now one bound terminal over a single lexical class that spans both keywords via ChoicePattern, which also means the one production reparses either direction rather than needing a variant per keyword. The constraint is recorded beside the productions rather than in a commit message alone, because the next author reaching for alternation will reach for it the same way I did. Verified: compiles with zero new diagnostics against the same measured baseline (33 pre-existing annotation diagnostics in unrelated test files, unchanged). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-08-12T00:10:39Z

Fixed in e947c46d2c, so the branch surface no longer carries the defect.

Direction is now a single bound terminal over one lexical class spanning both keywords (ChoicePattern), rather than an alternation between two concrete-only productions. That also means the one production reparses either direction instead of needing a variant per keyword.

The general rule this establishes, recorded beside the productions rather than only here: alternation expresses optionality and shape, never a choice between two spellings. A spelling choice is a binding. The next author reaching for alternation will reach for it the way I did, so the constraint belongs in the file.

Compiles with zero new diagnostics against the same measured baseline (33 pre-existing annotation diagnostics in unrelated test files, unchanged).

Still draft — exemplar nodes, rules wiring, byte equality, reparse and the product mapping remain.

— sent from zesty-heron-736

…ctable Three corrections, all resolved by execution rather than by asking. SELECTABILITY. Every alternative now differs by CHILD COUNT, which is what the backward selector actually compares. The earlier expr chain had `expr_unary -> expr_primary` and `expr_unary -> ~ expr_unary` both carrying one child, which is the same defect the direction pair had; conjunction against disjunction would have been worse, identical in both count and kind. Operators are therefore BOUND terminals over operator token classes: one expr production per arity — 1 child for a signal reference, 2 for a unary application, 3 for a binary one — and the operator spelling is a binding, exactly as direction is. That collapses conjunction and disjunction into one production instead of two that could never be told apart. Port and assignment lists keep their one-versus-cons alternation, which is selectable because the arities differ. LAYOUT HAD NO SOURCE AT ALL. target_text_seq concatenates exactly, and a fixed token's spelling is its lexeme, so the committed grammar would have emitted `moduleboard_power_interlock(`. The transform map that could have said otherwise was consulted for BOUND tokens only. That asymmetry is the defect, and it is target-neutral: a transform describes how a TOKEN CLASS renders, and nothing in that depends on whether the lexeme arrived from a binding or from the lexer. So the fixed arm consults the same map rather than growing a second layout mechanism beside it. Tokens stay lexically atomic — `(` still lexes as `(` — so reparse is unaffected and layout is target-owned rather than smuggled into a lexeme. Every existing target sets the map empty and is byte-identical by construction. Verified rather than assumed: semantic_decl_serialize_parity_test 7/7 green, which pins emitted bytes against goldens through the changed path. Whole-module compile shows the same 33 pre-existing annotation diagnostics as baseline. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

target_text_seq concatenates exactly, so every space and newline in an emitted module is declared in verilog_emit_layout_transforms or does not exist. None of it may return to product.compute_board, which is the point of the exercise. The header and expression parentheses are separate token classes because a transform is keyed by token class, and one paren class cannot render " (\n" around a port list and "(" inside an expression. The #8129 oracle needs both. Splitting the class is what makes the layout expressible; the two classes lex the same literal, which is a REPARSE question rather than an emission one and is tracked as such. Hand-assembling the profile against the oracle reproduces it exactly, including the parenthesised binary expressions and the two-space assign indent. That is arithmetic on paper, not an executed emission; the emission is next. Compiles at the 33-diagnostic baseline.

One slot per variable position, because ARITY is what backward selection compares. The expression forms carry one, two and three slots rather than sharing a shape and relying on a discriminant nothing compares: a signal reference carries its name, a unary application its operator and operand, a binary one its operand, operator and operand. Concrete punctuation contributes no slot, which is why the parentheses and keywords are invisible in these constructors and live entirely in the layout profile — the same fact read from the other side. Compiles at the 33-diagnostic baseline.

The binding symbol in a derived row comes from the EMITTED atom (FormalBindingConjSlotEmittedAtom reads node_atom_identity_optional on the slot), not from the production's binding symbol — the production only says WHICH slot is bound. Verified by reading the derivation rather than assumed, because the whole port list depends on it: it is what lets four ports share one production and still carry four different names. That also lets one signal atom serve as a port name, an assignment target and an expression reference at once. Those are the same identity spelled the same way, so forking them would have been three names for one thing. Rows are DERIVED from a production plus the exemplar, never authored as token lists — an authored token list would be the product-local printer wearing a different hat. A CONTROL ON THE EVIDENCE ITSELF. An import edit silently failed to apply and the module still reported the 33-diagnostic baseline, which made "compiles clean" suspect for every increment so far. Planting a reference to a function that does not exist moved the count to 34 with a located diagnostic, so the compile does check and the earlier claims stand. The names were resolving as bare cross-module references; they are now imported explicitly, because DESIGN's import-strip thread records that bare resolution succeeds by pool-membership coincidence rather than by the reference binding its target.

… fixture echo OUTCOME A: the generic target path composes a bounded Verilog module with no Verilog branch in the compiler. The module frame, the recursive port list, the nested expressions and every space and newline derive from the target's productions and layout profile. TWO MECHANISM FACTS COST MOST OF THE WORK, both settled by execution. A bound terminal only takes its binding from the emitted slot when its binding symbol is ^grammar_free_name_slot or ^grammar_lexeme_stamp_slot — that is what formal_binding_is_emitted_atom_from_slot tests. Custom binding symbols take the ExactBinding arm, which expects no emitted slot, so every production silently failed to match its own exemplar and derivation answered grammar_relation_production_not_found. grammar_formal_terminal_free is the constructor that means what this needed. AND THE FIRST GREEN WAS A FIXTURE ECHO. Row derivation walks the emitted tree and INLINES every nested nonterminal's tokens, so a derived row already carries the whole program's token sequence and serialization replays it. Passing a DIFFERENT module to a model holding the exemplar's row re-emitted the exemplar: byte-exact, entirely insensitive to its input. The perturbation control is what caught it — the positive control alone was green throughout and would have shipped a fixture as a compiler. So emission derives its row from the program being emitted. The rules population is not a fixed table that programs select from; composition happens at derivation, and that is the path all six witnesses now exercise. Controls, 6/6 green by execution: full byte equality against the exact #8129 oracle; every relation row derives, so the empty-row fallback is proven unreachable rather than trusted; dropping the negation changes the expression bytes and leaves the port region byte-identical; a two-port module emits through the same productions with the assignment region intact; and deriving against the REVERSED production population is byte-identical, so selection is structural rather than first-match. That last control replaced one asserting a production count, which proves nothing about order and was a literal measured from the tree it checked.

…lving it bare CI red at 1338af5: two TargetModel literals were missing produced_decl_support, a field main added to the type after this branch was cut. The local compile did not catch it because the branch had never been merged with main — the type it was checking against was the older one. The literals now supply ProducedDeclUnwired, matching every other target, and TargetModel is imported explicitly instead of resolving as a bare cross-module reference. The second half is the more useful repair: bare resolution succeeds by pool-membership coincidence rather than by the reference binding its target, so the type this module checked against depended on what else happened to be in the pool. That is the class DESIGN's import-strip thread records, and it is exactly how a field addition upstream stayed invisible here. Verified after merging main: 73 hard diagnostics, all annotation diagnostics in unrelated files, none from this module; the six emission witnesses green; the seven-witness serializer parity control green.

…arget renders This closes the §3 violation the lane exists to remove. product.compute_board carried a second Verilog authority beside v2.extdeps.languages.verilog: the keyword roster, the forbidden-character set, the punctuation, the layout and a full render_module/render_ports/render_assign/render_expr printer. All of it is gone. What remains is a fold from board vocabulary onto the target AST — no keyword, no punctuation, no layout — and the target renders it through the generic serializer. A grep for Verilog syntax in the product module now returns nothing outside its own prose. The module note claimed routing through the target AST was blocked on a general Symbol-to-text projection. That premise was wrong twice: no such projection is needed, because a target resolves a Symbol through its own binding spellings — which is why VerilogBinding now carries the symbol beside the spelling — and the emitter was never the obstacle, because rows derive from formal productions and emission is their backward reading. Identifier admissibility moved to the target too. What may be a Verilog identifier is a fact about Verilog, and a second target consuming this grammar now inherits it rather than re-deriving it from the same specification. What stays in the product is what the BOARD can get wrong: driving a non-output, referencing an undeclared signal, a signal with no binding or two, a spelling the target refuses. THE ORACLE IS UNCHANGED, which is the point. w_interlock_emits_exact_verilog_bytes still pins the exact #8129 source, so this is a replacement proven byte-identical rather than a rewrite that moved the goalposts. 9/9 product Verilog witnesses and 7/7 article witnesses green by execution.

…ed token class The header and expression parentheses were separate token classes lexing the SAME literal. That was fine for emission, where the production names the class, and a hazard for reparse, where the lexer sees "(" and cannot know which class it is looking at. Two classes over one literal is a lexical ambiguity waiting for the parser to arrive. The fork existed only because a transform is keyed by token class, so one class could not render " (\n" in the header and "(" inside an expression. A BOUND slot takes its spelling from its emitted atom instead of from a class transform, so the header parens carry their own layout and the expression parens stay bare. One class, no lexical ambiguity, byte-identical output. That is the same move direction and the operators already made — a spelling choice is a binding — applied to layout rather than to a name. 15/15 green by execution: the six emission witnesses and the nine product Verilog witnesses, including the exact #8129 byte oracle, unchanged.

The rows that render the module also recover it. Taking the derived row's token spine and running FORWARD selection rebuilds the emitted node, and it equals the node emission started from — one grammar read in both directions, discharged by execution. A separately authored parser could agree with an emitter by coincidence; a round trip through one row population cannot. WHAT THIS IS NOT, stated because the difference is easy to overclaim: this is a round trip over the TOKEN SPINE, not over emitted BYTES. Nothing in .dag lexes text today — v2.compiler.ingest begins at a ParseTree and takes no source string — so the step from "module ... \n" back to tokens is not executable here and is not claimed. What is proven is that the token sequence the row renders is the sequence the grammar reads back to the same structure. Byte-level reparse waits on a .dag lexer, which is a substrate capability rather than a Verilog gap. A TOOLING NOTE WORTH KEEPING. Importing v2.compiler.ingest first failed with 'dependency_resolution_facts not found in scope' — which is a host builtin the seed registers, not a missing function. The prebuilt claim_batch predated the main merge that added it, so the binary did not know its own builtin. Rebuilding the one bin fixed it, and every suite was then re-run against the fresh binary rather than trusting results a stale one had produced. 33/33 green by execution across all four suites: emission 7, product Verilog 9, article 7, SPICE 10.

… one coproduct

…lected causes

…wn spelling

…byte

…ck, ngspice solved the deck

…uted

…ecks the join

… are not

… refused once

gunbai-bot · 2026-08-12T21:18:16Z

Review 51444 was right and is fixed in 362119048, not argued with.

project_article_to_ngspice_run returned a bare String, and a String has nowhere to put a refusal — which is precisely how the second path got built without a gate. It now returns SpiceProjection and routes through the same first_refusal_or_net_spelling the receipt path uses, so there is one gate and both projections sit behind it. emit_ngspice_run surfaces the refusal instead of swallowing it.

The discriminating control the finding implies is now enrolled: floating_terminal_article is the production circuit with one net member removed, so pg_filt terminal 1 floats. Two tests, and both matter — w_the_floating_fixture_is_admitted_so_the_test_is_about_the_projection proves the fixture passes admit_board_article (terminal netting is deliberately a SPICE requirement, not an article-level fact), and w_both_spice_paths_refuse_the_same_article proves both paths then refuse it. Without the first, the second would pass on an article that never reached a projection at all.

Also from review 51442, both acted on rather than replied to: the projection's DrivenSignalIsNotAnOutput / ReferencedSignalUndeclared checks are deleted — article-level facts admission already refuses, and unreachable once the entry point took the sealed wrapper. And from review 51443, NodeReference.name / PassiveElementTopology.name now carry a CircuitNodeName brand rather than a bare String; the Symbol they replaced was grounding nothing structurally, but the reviewer is right that String alone read as a loosening.

Fixing this surfaced one more thing worth naming: a source annotation inside a declaration body is refused by gunbc run and not by the whole-corpus drift-gate compile, so the witness suites were green over a module run refuses. That is a real inconsistency in the annotation check's reach; the offending comment is moved, and I am flagging the gap rather than leaving it as a thing I happened to notice.

— sent from zesty-heron-736

…rose

gunbai-bot · 2026-08-12T21:43:54Z

Review 51447 is right, and the sharpest part of it is that this was my own argument turned back on me: the commit before it says a String has nowhere to put a refusal, and emission_entry was answering one with the literal "REFUSED: article not admitted". Fixed in f09fac997.

The entries return BoardEmission<R>, parameterized by the target's own refusal type rather than fusing SPICE and Verilog causes into one enum every caller would have to match. Admission refusal and target refusal are separate arms because their remedies are opposite — fix the board, or fix the target binding — and one fused refusal would tell a caller nothing about which.

Two things I changed beyond the literal finding, because fixing it exposed them:

The entries now take the article, with the production ones as thin wrappers. Hardwired to power_interlock_article, the refusal arms were unreachable by any call, so "it refuses" would have been a claim about code nothing executes — a typed arm nobody can reach is not obviously better than the string it replaced. The admission call stays inside the entry, so a caller still cannot skip it.

A new witness executes all three arms (compute_board_emission_entry_witness_test.dag), and the two refusal arms are separated by execution rather than by argument: an undriven-output article reaches BoardArticleNotAdmitted on all three entries with both causes intact across the boundary, while the floating-terminal article — which admission accepts, since netting is a SPICE requirement and not a fact about the board — reaches BoardTargetRefused on both SPICE entries and still emits as Verilog. That last one is what makes the target arm a statement about the target rather than about the board.

— sent from zesty-heron-736

* Model firmware targets, boot diagnostics, and memory part selection Modeling work from a live srv3/srv4 incident: both hosts failed to boot after a DIMM upgrade. Root cause of the first failure was host firmware three years stale; the residual failure is a DDR4 LRDIMM data-buffer training step. Nothing here is a blocklist -- each avoidance is derived from a mechanism, so a future ordering workflow can shop the whole market and explain every refusal by naming the failing step. extdeps.firmware.types (new) FirmwareTarget = BmcController | HostBios. The fleet could express which BMC image a host should run and had no way to express which BIOS, though BIOS owns DDR training. FirmwareImageKind distinguishes the OpenBMC tar (pushable to a dead host) from the Instant Flash ROM (needs a booting host). FirmwareReleaseRow carries a prerequisite, so an unappliable push is refused from the catalog rather than discovered from a vendor shell script after a 33MB upload. Consolidates BmcFirmwareSemanticVersion -> FirmwareSemanticVersion across 8 files: a version triple is one concept, and minting a second name for host firmware would be the CpuArchitecture/TargetArchitecture class. extdeps.ampere.scp_diagnostic (new) SCP console tokens as class+number with meaning held separately. Deliberately no token-to-meaning function: no codebook was obtained, so every implementation of one would be invention. The E prefix classifies a namespace, not a consequence -- E559/E571 appear on a same-family machine that boots normally. DiagnosticReadEffect records that several of these interfaces mutate what they report. extdeps.memory.training (new) Training steps, with the required set DERIVED from buffering. A registered module has no data buffer and cannot fail buffer calibration -- a difference in kind, which is what makes it sound as a purchase filter. capacity_reachable_as_dual_rank_registered derives from JEDEC die density why cheap high-capacity DDR4 is disproportionately load-reduced. gunbc.host_memory_qualification (new) Four independent standings: board class support, specific part qualification, DDR training outcome, host boot outcome. None derives another. Their collapse into one "does the RAM work" question cost three refuted hypotheses during the incident. Causal experiments land as receipts, including HypothesisWeakenedByIntervention for an intervention weaker than the one that would settle the question. gunbc.memory_part_selection (new) A candidate is refused iff it must execute a step this board has been observed to fail -- independent of vendor, part number, capacity, speed grade, or AVL membership. Implication is not a Pareto objective: implicated parts are refused before the frontier is computed. gunbc.host_boot_supervision, gunbc.host_diagnostic_channel (new) Two independent reset supervisors, kept separate because only one is configurable. Interval typed by how it is KNOWN: powermon's 306s is measured from eleven journal timestamps, not read from configuration. Five diagnostic authorities with their transports, and the standing that a missing projection does not establish a missing source. Witnesses cover the eight properties an external review required. Every digest was measured by acquiring the artifact; nothing is transcribed. NOT COMPILED. The local `gunbc compile --target dag` path rejects `//` at 1536 files corpus-wide, nearly all untouched, so it does not implement the section 4c annotation channel and cannot check this. CI is the first real compile. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Fix import placement, ground firmware/price units on std.measure The parse error CI named (expected name, found LBrace) was a misplaced import: the migration insert landed between the opening brace of a multi-line import block and its first name. Only this one file was affected; the other five insert sites were checked and are well-formed. Review 51271, both blockers, verified present and fixed: - FirmwareReleaseRow.image_bytes was a flat Nat beside a sibling capacity_bytes already carrying ByteSize in the same diff. Now ByteSize; the three ASRock call sites construct through byte_size. - PartCandidate carried unit_price_minor: Int and currency: NonEmptyStr, with a comment saying prices are deliberately not compared across currencies. That is exactly the invariant the type should enforce, so it is now MoneyAmountMicro + std.currency.CurrencyCode, and admission returns a typed CandidateAdmission whose CandidateCurrencyMismatch arm refuses a candidate priced in an undeclared currency rather than ranking it. The narration is now a wall. The selection rule had no executing consumer, which the unit fix made conspicuous. Adds memory_part_selection_witness_test with the currency refusal and its positive control, the implication rule and its RED control (a registered module of the same vendor/capacity/generation is NOT implicated, so the rule is discriminating on buffering rather than on part identity), and a no-observed-failure control proving the refusal comes from the observation rather than from a preference in the model. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Annotate observed_failures with its type data observed_failures was written without a type annotation, which the parser refuses (expected Colon, found Eq). Mine, in the witness added by the previous commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Ground the obmc push artifact byte count on ByteSize Review 51280, blocking item, verified present at extdeps.boards.asrock_rack asrock_altrad8ud_bios_3_10_obmc_push_artifact_bytes (the review cited line 369; the symbol is at 350 — naming it symbolically per DESIGN section 3). It was the last bare-Nat byte count in the diff and sits beside FirmwareReleaseRow.image_bytes, which the previous commit had already moved to ByteSize, so it was a fork of the carrier in one file. Now byte_size(count: 33566720). It has no consumers, so nothing downstream changes shape. Not taking the non-blocking import cleanup in extdeps.memory.training; see the PR reply for why. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Derive the BMC Redfish surface from firmware instead of storing it per host The srv3 flash exposed a dual representation. Which thermal resources bmcweb serves, how many sensors the chassis collection carries, and whether a fan-control resource exists are decided by the firmware BUILD for a board, but BmcRedfishSurfaceObservation stored those three fields per host, beside the firmware version they are a function of. So when srv3 went 2.07.00 -> 3.22.00 on 2026-08-11 its hand-authored row went on claiming ThermalSubsystemSensorCollection with 51 sensors, and two witnesses ASSERTED those constants as literals — the corpus stayed green while describing a surface the host did not have. There was no second authority that could disagree, so nothing could have caught it. MEASURED 2026-08-12, both hosts at once, which is what makes this a catalog row rather than a per-host note: srv3 (192.168.1.192) and srv4 (192.168.1.195), flashed independently on different days, both returned legacy Chassis Thermal 200, ThermalSubsystem 404, ThermalSubsystem/Fans 404, a 9-member Sensors collection, and a byte-identical Thermal key shape (12974 / 12975 bytes, differing in one reading value). Two independently-arrived-at hosts agreeing on every axis is the evidence that the shape follows the image; one host would only have established what that host does. An earlier probe returned 401 on BOTH hosts, which was a credential fact rather than a surface fact — checking the pair is what distinguished them. - extdeps.bmc.types gains BmcRedfishSurfaceShape, a cited BmcRedfishSurfaceRow catalog keyed by version, and bmc_redfish_surface_for / bmc_redfish_surface_of_host. An uncatalogued image derives SurfaceShapeUncatalogued carrying the version rather than a nearest-neighbour or default shape, so the next flash is loud at derivation instead of silently wrong at use. - BmcRedfishSurfaceObservation is DELETED rather than left beside the derivation; a dead carrier that can still be constructed re-opens the fork it was replaced for (DESIGN section 4b, dissolution on climb). - srv3's firmware observation is re-observed to 3.22.00 (VERSION_ID from /etc/os-release, authenticated BMC SSH). Its surface moves with it in one motion, because there is no longer a second place to update. Witnesses: the two that pinned the fork are replaced by the property that actually holds — hosts on the same image derive the same surface — plus a RED control proving the derivation discriminates on version (the 2.07.00 row still derives the old shape) and a fail-closed control that an uncatalogued image refuses. Per section 4b the evidence stays enrolled rather than retiring with the machinery it replaced. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Move source annotations to module-item grain DESIGN section 4c admits only standalone leading // blocks attached to module-scope declarations; body-position annotations refuse. Every new module in this change had them — comments sitting beside a field or a coproduct arm — so the heal job refused with a located diagnostic per line. Each block moves above its enclosing declaration and keeps its referent by naming it ("On prerequisite:", "On FirmwarePrerequisiteUnobserved:"), so no rationale is lost in the move. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Carry the firmware prerequisite's evidence as data, not prose Review 51290 (non-blocking) on the receipt Strings. Taking the one with a live consequence rather than the whole corpus-wide class: the BIOS-tar prerequisite declares BMC >= 3.22.00 as a LITERAL while the two executed pushes that established it sat only in an unstructured String, so the release row and its evidence could not be joined and a declared minimum the evidence contradicted read exactly like one it supported. FirmwarePrerequisiteObservation now carries each executed push (board, subject, packaging, gating target and version, outcome, timestamp), with the vendor diagnostic held on the refusal arm. The two ALTRAD8UD rows are the discriminating pair: identical bytes refused at BMC 2.07.00, accepted at 3.22.00. prerequisite_evidence_verdict checks a declared minimum against them, and its positive arm is deliberately PrerequisiteConsistentUpperBound rather than a bare "consistent": two pushes BOUND a threshold, they do not locate it — 3.06.00 is in the capability catalog and was never pushed, so the declared 3.22.00 may be stricter than the vendor requires. Claiming the threshold was measured would be the stronger-than-evidence reading the arm exists to prevent. Witness: the pair supports the declared minimum as an upper bound; a minimum inflated above the accepting version is contradicted BY the acceptance; a minimum relaxed to or below the refusing version is contradicted BY the refusal (the direction that would admit an unappliable push); and an empty observation list yields Absent, never consistent. The prose row keeps only what the carrier cannot hold: that the vendor page documents no such dependency, that the cause was legible only in the BMC journal because Redfish reported Exception with none, and why the prerequisite belongs to the packaging rather than the release. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Execute the prerequisite gate and the loop-cause fold Review 51292, both findings verified: firmware_release_applicability and host_boot_loop_cause had zero importing consumers and zero witnesses, so the PR's two central fail-closed claims were specification without execution — the exact bar this PR's own prose sets (DESIGN section 5). The applicability rows bind the PRODUCTION release rows rather than fixtures, so the gate runs against the prerequisite the catalog actually declares: - unreadable target version refuses (the srv3 BIOS-null case that justified the third arm); - the srv3 push at BMC 2.07.00 is Unmet and the verdict carries what it observed; - the srv4 push at 3.22.00 is Applicable (positive control); - 3.06.00 is Unmet — higher major, lower minor, so a major-only compare would wrongly admit it, and that version is a real catalogued image rather than an invented one; - the Instant Flash ROM row is Applicable on the SAME Absent observation that refuses on the tar row. Same input, opposite verdict, because the prerequisite belongs to the packaging. For the loop cause the discriminating pair is the intervention, not the signature: one E588 signature answers HostSelfResetOnError after the supervisor was stopped and the loop persisted, and CONFOUNDED with the identical signature when it was not. That is the state the incident sat in while the watchdog theory looked plausible, and it is why period alone cannot decide — a 306-second cycle looks the same whether or not a 306-second timeout causes it. A third row keeps a clean stop with no error code at Unobserved rather than inferring a supervisor verdict from silence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Keep observations immutable; split inventory from image; refuse duplicate keys Four findings, all verified against the code before acting. IMMUTABLE OBSERVATIONS (mine, introduced by this PR). Editing the single srv3 firmware row in place from 2.07.00 to 3.22.00 moved every receipt that referenced it, so srv3's JULY update-service snapshot began claiming it had been observed under firmware installed in AUGUST — the same temporal-authority defect this PR set out to fix, relocated one field sideways. The 2.07.00 and 3.22.00 observations are now separate immutable rows; srv3_bmc_firmware_observation is the CURRENT standing and advances by re-binding, not mutation; the update-service receipt binds the 2.07.00 row it was actually taken under. A 3.22.00 update-service receipt will land as a new row when one is measured, not by re-pointing this one. INVENTORY IS NOT AN IMAGE FACT. chassis_sensor_collection_member_count sat inside the image-derived shape. Two hosts returning nine members at one moment establishes agreement at those observations; it does not make cardinality invariant under fan, FRU, or sensor-service changes — and this same session measured installed fan sets DIFFERING under identical firmware, which is the same nearby-question mistake one axis over. The count is dropped from the shape rather than being derived from something that does not decide it. Route and resource availability stay, since those are compiled into bmcweb. DUPLICATE KEYS REFUSE. bmc_redfish_surface_for took the first match, so two rows for one version resolved by list position — a silent order-dependent answer where the catalog actually contradicts itself. It now answers SurfaceShapeAmbiguous with the collision count, with a RED control that plants the duplicate. SECOND, NOT NAT (review 51298, verified). SupervisorIntervalKnowledge carried seconds on bare Nat while std.measure Second is the authority used for the same concept elsewhere. The declared/measured epistemic split is unchanged; only the carrier moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Grade the memory refusal by evidence and scope it to the board The rule refused any module that merely EXECUTES a step some platform was observed to fail — on any board, at any evidence standing, including EvidenceUnobserved. Because capacities near a generation's die-density ceiling are disproportionately load-reduced, that removed most of the 64GB DDR4 market by construction: the blocklist this module's own prose claimed to avoid, reached by a different route, and the opposite of letting a buyer shop the whole market instead of an AVL. Severity is now a function of evidence, which is what the standing type was carrying all along and the verdict was discarding: - DecodedFromPlatformSyndrome refuses; - AssociatedByIdenticalSignature and InferredFromSequencePosition require a SAMPLE and stay on the Pareto frontier; - EvidenceUnobserved implicates nothing. gunbc holds MREP at association standing, so the honest verdict for another ALTRAD8UD LRDIMM is buy-one-and-test. Failures are also scoped to the board observed, so an ALTRAD8UD receipt cannot speak for a different platform. Witnesses discriminate on evidence with the board, step and module held fixed: association -> sample-required, decoded -> refused, unobserved -> nothing, registered module untouched at any standing. Two frontier rows show the market is not shrunk by an association (both candidates remain, the load-reduced one flagged) while a decoded refusal still drops one. KNOWN GAP, declared rather than hidden: BaseboardModel has exactly one variant today, so board scoping is real in the code but has no executing cross-board control. Minting a second board purely to test it would be a fabricated entity; the control lands when a second real board is modeled. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Carry the supervisor interval on Second, not bare Nat review 51303, same finding as review 51298 on the stacked PR. I fixed it there and not here, but host_boot_supervision.dag is introduced by THIS PR, so the fix belonged at its origin — the reviewer was correctly seeing bare Nat on the branch that declares the type. std.measure Second is the carrier siblings already use for this concept. The declared-vs-measured epistemic split is unchanged; only the unit moves. Duration is not a separate std.measure carrier in this corpus, so Second is the existing single authority rather than a new one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Stop fabricating evidence bounds; add the two missing witness imports review 51304 (non-blocking, but the finding is a section 5 violation by this repo's own standard, so taking it): prerequisite_evidence_verdict stored the DECLARED MINIMUM into whichever bound had no observation yet. A verdict backed only by an acceptance therefore reported a highest_refusal that never happened — a fabricated plausible value in the exact field a consumer reads to judge how well-bounded the threshold is. It was also order-dependent: once a bound was set, later observations were discarded, so the same evidence authored in the other order gave different bounds. The reviewer correctly noted my positive test greened only because the list happens to be authored refused-then-accepted. Both bounds are now Optional and computed as a real max-refusal / min-acceptance over all observations, which is associative and commutative and so cannot depend on authoring order. Absent means absent. Two controls added: the reversed list must produce an equal verdict, and an acceptance-only history must report NO refusal bound. review 51307 (blocking, verified): bmc_firmware_thermal_witness_test referenced firmware_semantic_version with no extdeps.firmware.types import at all, and asrock_altrad8ud_openbmc_3_22_00_capabilities while the asrock block imported only the 2.07.00 and 3.06.00 rows. Both were mine, from scripted edits that added references without their imports. Both added; the other changed witnesses were checked for the same class and are clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Declare ExternalModelScope on the new extdeps modules; fix optional imports Two real CI failures, both mine. RESOLUTION: Present and Absent were imported from std.types, where they do not live. The corpus idiom is v2.std.optional. Fixed in extdeps.firmware.types and both witnesses that matched on them. I had "verified imports" after the last review with a targeted check that only confirmed a symbol appeared in SOME import block — it never checked the symbol was exported by the module named, so it passed a wrong-module import cleanly. The check was weaker than the claim I made from it. EXTDEPS SCOPE PLACEMENT GATE: three new dag/extdeps modules were enrolled in neither scope_carrier_paths nor the machinery exemption, which the per-PR gate refuses by design — a new extdeps file's only landing states are scope carrier or genuine machinery, and the frozen legacy manifest is explicitly not an admission channel. Each now declares extdeps_model_scope naming its exact upstream subject and joins the carrier roster: - extdeps.firmware.types -> FirmwareReleaseRow: the vendor release and its applicability precondition, not the flashing mechanism and not fleet policy about which release to run. - extdeps.memory.training -> MemoryTrainingStep: the JEDEC DDR4 initialization calibration sequence, cited to JESD79-4A; platform failure receipts and purchasing policy are deliberately outside it. - extdeps.ampere.scp_diagnostic -> AmpereScpConsoleToken: the token stream and structured boot-progress interface as an upstream surface only, with the read-effect axis included because an acknowledged queue is not a sampled register, and with no token-to-meaning function since no codebook has been obtained. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Restore the deleted contradiction fn; rebind drift fixtures to 2.07.00 review 51313, all four findings verified and real. COMPILE BREAK, mine: rewriting the evidence-bounds block deleted prerequisite_observation_contradicts along with the accumulator it sat beside, while prerequisite_contradiction still called it. Nothing defined it anywhere in the tree, so the module could not compile and the contradiction arms were unreachable — the arms that do the actual gating. Restored with its own rationale: an acceptance strictly below the minimum falsifies it, a refusal at or above it falsifies it the other way, and consistent is not the same as supporting, which is what the bounds report separately. STALE FIXTURES, caused by this PR: three classification witnesses used srv3 as their drifted-host fixture and asserted 2.07.00. Advancing srv3's current standing to 3.22.00 did not merely break them — once srv3 satisfies the pinned track-3 intent, Drifted/Apply becomes Converged/Noop and the tests would have inverted what they claim to check. They now bind srv3_bmc_firmware_2_07_00_observation, the immutable historical row, which is what each test was always about: the classification logic on a host behind its intent, not srv3's present state. That also resolves the fourth finding without a separate change: the update-service receipt is bound to the 2.07.00 observation, so the plan test now pairs one firmware identity with itself and the update-surface identity check no longer refuses. This is the immutable-observation split paying for itself immediately — the historical row existing is what let three tests keep their meaning instead of being rewritten around a moved fact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Join the prerequisite oracle to the catalog instead of copying it review 51318, verified and correct. declared_minimum hand-wrote 3.22.00 while a comment two lines above claimed the witness "compares the SAME number the catalog declares" — it did not. Editing asrock_altrad8ud_bios_3_10_openbmc_release.prerequisite would have left executed_pair_supports_the_declared_minimum_as_an_upper_bound and the_bounds_do_not_depend_on_authoring_order green until someone remembered to edit the witness too. That is the tree-copied oracle DESIGN section 5 forbids, and the comment asserting otherwise is what made it look already checked. verdict_against_declared_minimum now matches the release row's own prerequisite and passes its minimum through, so the catalog and the tests move together. The sibling witness already used this join, so the pattern was in the tree and I did not follow it. The RED controls deliberately do NOT join: a falsifying probe is an authored input chosen to contradict the evidence, not an oracle, and joining it to the catalog would make it unauthorable. That split is stated in the module so the next reader does not "fix" it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Declare ExternalModelScope on the new extdeps modules; fix optional imports Cherry-picked to the branch that INTRODUCES these modules. I committed this fix on the stacked derivation branch instead, so #8171 — where extdeps.firmware.types, extdeps.memory.training and extdeps.ampere.scp_diagnostic are actually added — kept failing the placement gate it was failing before. The stack direction makes that invisible: merging the parent forward into the child hides that the child, not the parent, carries the fix. The extdeps scope placement gate refuses a new dag/extdeps file enrolled in neither scope_carrier_paths nor the machinery exemption, by design — the frozen legacy manifest is explicitly not an admission channel. Each module now declares extdeps_model_scope naming its exact upstream subject and joins the carrier roster: - extdeps.firmware.types -> FirmwareReleaseRow: the vendor release and its applicability precondition, not the flashing mechanism and not fleet policy about which release to run. - extdeps.memory.training -> MemoryTrainingStep: the JEDEC DDR4 initialization calibration sequence, cited to JESD79-4A. - extdeps.ampere.scp_diagnostic -> AmpereScpConsoleToken: the token stream and structured boot-progress interface as an upstream surface only, read-effect axis included because an acknowledged queue is not a sampled register, and still no token-to-meaning function. Also fixes Present/Absent, imported from std.types where they do not live; the corpus idiom is v2.std.optional. This branch's copy of extdeps.firmware.types needs them for firmware_release_applicability but not List/list_length, which belong to the evidence carrier that lives only on the stacked branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Drop two dead surface imports from the live-receipts witness review 51322, verified: srv3_bmc_redfish_surface and srv4_bmc_redfish_surface appear only on their own import lines in bmc_live_receipts_witness_test, left behind when the per-host surface assertions were replaced by the derivation. Removing these is NOT the case I declined on the earlier PR citing the #6985 Class B hazard, and the distinction is worth stating since I invoked that rule already. Class B is about a stripped file's bare cross-module references resolving only by pool-membership coincidence — the danger is dropping a MODULE from the assembled closure. Here gunbc.fleet_bmc_observation stays imported via ten other symbols, so the closure is unchanged and only two dead names go. The derivation itself keeps its real consumers in bmc_firmware_thermal_witness_test, which is where the surface is actually asserted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Make population admission true multiset equality review 51323. The finding as stated does not reproduce, and the defect underneath it is real but mirrored — both worth recording. NOT REPRODUCED: the cited candidate ["A1","A1","B1","E1"] is REFUSED today. population_slots_match folds `a` over `b`, and the call site passes a = documented row, b = candidate — so the subset test runs documented-into-candidate, not candidate-into-documented. A duplicated candidate slot shrinks its distinct set, so a same-length documented row with four distinct slots cannot be covered. Simulated over all four documented rows before changing anything. REAL, AND LATENT: the guard was equal-length-plus-subset, not multiset equality, and it relied on an unstated precondition that no DOCUMENTED row carries a duplicate. Violate that and it fails in the opposite direction from the report: documented ["A1","A1"] admits candidate ["A1","B1"], since both documented entries are found and lengths agree. No board row has a duplicate today, which is why it was latent — and why leaving correctness resting on that staying true is the wrong place to stop. Now compares occurrence counts, which is multiset equality given equal lengths and removes the precondition. Three controls: the duplicated candidate stays refused (the property callers rely on, previously true only incidentally); a synthetic duplicated documented row does NOT admit a distinct pair — the case that was actually broken; and that same row still admits its own multiset, so the refusal is discrimination rather than a blanket rejection of duplicated rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Flatten the multiset comparison onto one line Parse error I shipped in the previous commit: expected RParen, found EqEq at dag/extdeps/boards/types.dag. The comparison was written with a line break BEFORE the ==, inside fold's argument list, so the expression terminated at the newline and the parser then wanted the arg list to close. The corpus does carry `&& x == 5` unparenthesized, so the operator combination was never the problem — the continuation position was. Leading && and || continuations at statement level are used throughout and parse fine; a leading == inside a call's argument list is the shape that fails. Now one line, parenthesized, matching the style of slot_occurrence_count directly above it. Swept the rest of the change for the same shape: this was the only occurrence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Stop conflating admitted with undominated in the frontier witness The witness floor caught a real error, and it was in my test design rather than in the model: an_association_leaves_both_candidates_on_the _frontier returned false because both fixtures carried the SAME price and capacity, leaving data rate as the only difference. The registered module therefore strictly DOMINATED the load-reduced one on the Pareto axes and the frontier correctly dropped it — I read that dominance as an admission failure. Admitted and undominated are different properties, and a fixture pair differing on exactly one axis cannot distinguish them. The pair now differs on two: the load-reduced part is cheaper and slower, the registered part dearer and faster, so neither dominates and frontier membership is decided by admission alone — which is what the test claims to check. That also matches the market fact the module models, where the part near the density ceiling is the cheap one. Verified both frontier assertions by simulating the dominance relation over the new fixtures before pushing: association -> 2, decoded -> 1. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Take the money carrier at the helper's parameter, not inside it review 51333, verified: candidate_at_price took unit_price_micros as a bare Nat and wrapped it in money_amount_micro internally, so the unit lived inside the helper rather than at its boundary. Every caller was free to pass a raw number meaning anything. Now the parameter is MoneyAmountMicro and callers construct the carrier at the call site. Same class as the earlier ByteSize / MoneyAmountMicro / Second fixes in this stack; I introduced this one two commits ago while fixing the frontier fixtures and reached for a scalar out of habit, which is precisely why the rule is worth having as a wall rather than a preference. std.nat is dropped from this witness: Nat became unused with the parameter retyped, and I had added that import in the same commit that introduced the scalar, so this returns the file to its prior import set rather than stripping anything pre-existing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Import Present/Absent explicitly in host_boot_supervision review 51335 asked for this on the ground that the file "has unresolved constructors and won't compile". That reasoning is wrong, and the check is cheap: host_boot_loop_cause executed GREEN in CI run 31566167444 — all three of its witnesses passed, including the arms that match Present and Absent. Bare Absent resolves in this corpus without the import; extdeps.bmc.capability and bmc_fan_converge_witness_test both do the same and are green on main. Taking the change anyway, because it is right for the OTHER reason. That resolution works by pool-membership coincidence — the target module is in the assembled closure only because some unrelated import elsewhere dragged it there — which is exactly the #6985 Class B hazard DESIGN records, and the remedy that thread names is making the binding closure-independent with an explicit import. asrock_live_probe_witness carries the same repair for the same reason. So this is not a no-op: it removes a dependency on accidental closure membership that would break the next time an unrelated lane changes its imports. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Fix the parse error CI found, and make the order control discriminating CI's located cause: expected expression, found EqEq in firmware_prerequisite_evidence_witness_test.dag. A line break before == terminates the expression, so the operator began a new statement. Same class as the earlier fold-argument break; leading && is fine, leading == is not, so the comparison is now one line. This file had never been parsed by CI. It reached main's floor only because #8171 merged and GitHub retargeted this PR, which is what a stacked branch buys: approvals on a branch that no required check was ever configured to run. Reading the failing test to fix it showed it did not test what it claimed. It compared two orderings of a two-element list holding ONE refusal and ONE acceptance -- an ordering over which first-wins and max/min agree, so it could not distinguish them, though its comment said that was its whole purpose. Both lists now carry a second, lower refusal at 1.00.00: a first-wins fold reports 1.00.00 on the reversed ordering and reds. Simulated in both directions before pushing; the expected bounds are held in one helper so a disagreeing ordering cannot be absorbed by a second copy of the numbers. Also drops FirmwareSemanticVersion, unused here before this change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Reclassify srv3's install path as unestablished, not refused-forever CI's 13 reds were one derivation, and they were the tripwire in os_install_mechanism working exactly as written: "if srv3's BMC is upgraded and its evidence row follows, this witness reds instead of the fleet silently planning a delivery mechanism the firmware no longer implements." srv3 was measured live on BMC 3.22.00, BIOS 3.10, host Running; re-binding its firmware standing to that made the tripwire fire. WHAT THESE WITNESSES NOW SAY, and what they deliberately do not. The catalogued 3.22.00 row lists neither Redfish virtual media nor the bmcweb nbd-proxy, and no host has an established network-boot delivery, so the solver has nothing to select and refuses with InstallNoVirtualMediaAndNetworkBootUnestablished. That cause names UNESTABLISHED. It is NOT a claim that the host cannot be installed -- srv4 runs this same firmware and was installed over the configfs USB-gadget transport, which extdeps.bmc.virtual_media already models as ConfigfsGadgetTransport and which this solver cannot see because OsInstallMechanism predates that authority. WHAT I DID NOT DO, having started it and backed it out. The first attempt added CapabilityConfigfsVirtualMedia plus a matching OsInstallMechanism variant. That would have minted a third name for a transport VirtualMediaTransport already names -- the section 3 nicknaming violation -- and it surfaced that CapabilityNbdProxyVirtualMedia is already that same fork for NbdProxyWebsocatTransport. Widening a fork to turn CI green is the wrong trade. Reverted whole; the real repair is the install lane consuming VirtualMediaIntent/VirtualMediaTransport, which is INSTALL-0, not this PR. Each rewritten witness keeps its original load-bearing claim rather than being flipped to expect a refusal: no silent PXE fallback -- previously "is nbd-proxy, no fallback"; the fallback arm is now exactly where a defective solver would land, so refusing is the proof it does not plan is solver-derived -- a hardcoded plan would still be Ready after the firmware change; both halves refusing is strictly more discriminating than the old version, which could not tell a derived plan from a hardcoded one while the solve agreed with it boot target follows mechanism -- the mapping is pinned on the mechanisms directly, where the claim always lived prep is not install -- credential wiring and the seeded ISO path hold; the plan and seed halves refuse with the solve, so nothing here can read as a solved install srv4 has none -- srv3 has now joined it; both hosts run 3.22.00 and refuse with the same cause, so asserting a difference would assert a fact that stopped being true Also corrects srv3_install_mechanism_board_default_residue, which still said the legacy row "agrees TODAY" and cited a witness by its old name -- a stale citation in the note that predicted this very divergence. The target facts the plan witnesses used to assert are not lost: they are what INSTALL-0 must reproduce once srv3 has an established path, at which point those witnesses red and are replaced rather than silently passing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * INSTALL-0 C1: make "nobody probed this" representable The defect this lane opened on was not a wrong capability row. It was that BmcFirmwareCapabilityRow has no way to say nobody looked, so firmware_has_capability reads list non-membership as false and a hand-authored list that never mentioned configfs is indistinguishable from a probe that looked and found it missing. srv3 was refused an install path on that reading while its sibling srv4, on the same firmware, was installed over exactly the transport the list omits. This commit makes the distinction representable at the grain where it is decidable: not one flag per firmware, but one standing per requirement the transport rests on. observed absent -> Refused a probe looked; the thing is missing unobserved -> Unestablished nobody looked; the answer is owed all present -> Established Absence outranks ignorance, deliberately: one requirement observed missing refuses even with others unprobed, because no remaining probe can overturn it, and answering Unestablished there would send someone to run probes that decide nothing. srv3's four live probes from 2026-08-13 land as receipts carrying the command and its output, so a standing can be re-derived by someone who doubts it rather than resting on a Bool whose provenance is a memory. The other four requirements have NO row: an unobserved requirement is the absence of an observation, and giving TransportProbeOutcome a third arm would let an unrun probe be authored as though it had run. srv3 therefore stands Unestablished owing exactly those four. WHAT THIS DOES NOT DO, and why. It does not wire the standing into gunbc.os_install_mechanism. That solver reads its own OsInstallMechanism enum rather than extdeps.bmc.virtual_media VirtualMediaTransport, and teaching it to consume the transport authority drags the actuator step lists with it -- the next commit, not this one. Until then this row is an authority with a witness and no production consumer, which is stated rather than left to be discovered. It also does NOT fix catalog_has_vm_capable_firmware, which checks CapabilityVirtualMedia only and so cannot see that the 2.07.00 row is nbd-proxy capable. That looks like an isolated one-line defect and is not: fixing it flips srv3/srv4 from InstallNoVirtualMediaAndNetworkBootUnestablished to InstallFirmwareTransitionUnestablished, which is a different refusal cause and would red the witnesses reclassified in #8174. It belongs with the solver rewiring, where both halves move together. Stacked on the #8174 branch because it edits the same lane; it receives no CI until that merges and GitHub retargets it, same as #8174 did. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Keep the standing's expression on its = line CI's located cause: expected expression, found Newline in fleet_install_transport_observations.dag. The srv3 standing broke the line after `data ... =` and put the call beneath it; a .dag value expression must begin on its operator's line. Third instance of this class in this session -- the other two were a leading == on a continuation line and a line break before == inside a fold argument list. The boundary is narrower than "leading operators are bad": a leading && parses and is idiomatic in the corpus, and `type X =` followed by variants on the next line is a different production that has always parsed. It is specifically a VALUE expression that cannot start on the next line. Swept the whole branch for both shapes; this was the only site. The remaining `=`-terminated lines are all `type X =` coproducts in extdeps/bmc/types.dag, untouched here and long green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Move 18 body-grain source annotations to module-item grain DESIGN section 4c models source annotations only as standalone leading blocks on module-scope declarations. Eighteen comment blocks across five witness modules sat INSIDE declaration bodies -- annotating individual clauses of a conjunction, arms of a match, or lets in the middle of a function -- which the compile-clean gate refuses with: compile-clean: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes. This is pre-existing main debt, not a regression from any one branch. The count is exact: 18 in-body blocks under dag/ against 18 diagnostics, and the same refusal reproduces on two unrelated branches whose only common factor is that both force the whole-tree compile-clean baseline. Main's own recent runs are cancelled or in-flight, so no green verdict has observed it -- the debt has been accumulating unseen across at least five merged PRs (#8045, #8073, #8122, #8147, #8184-era files). The prose is preserved, not deleted. Each block is hoisted into its declaration's leading block, merged with any block already there, keeping the clause labels as sentences. Where a leading block already said the same thing -- fleet_converge_cli's join-1 header covers every clause note it carried -- the in-body copy is dropped as the duplicate it was. Comment-only: `git diff` contains no non-comment line, so no behavior, no witness assertion, and no emitted byte moves. WHAT THIS DOES NOT DO: the diagnostic is typed but UNLOCATED -- it names no file, line, or declaration, though AnnotationAttachmentRefusal carries `origin: SourceSpan` on every arm and BodyGrainNotModeled is constructed with it. The consumer discards the span it was handed. That is a section 5 located-ness gap which cost this diagnosis a full CI cycle and a bisection commit; it is left as a separate finding rather than repaired here, so this stays comment-only and reviewable as such. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Attach the two subject-less trailing annotations to the declarations they discuss CORRECTION TO THIS PR'S OWN DIAGNOSIS. The first commit claimed 18 in-body blocks were the whole annotation debt, on the strength of an exact count match. The match was real but the population was not the whole one: I grepped the failing log for the body-grain message and never checked whether a SECOND refusal class was also present. It was. The #8211 log carried 11 "source annotation names no subject: no module item follows it" refusals beside the 18 body-grain ones, and clearing the body-grain class left that second class as the visible failure. That is the nearby-question error: I confirmed the count of the class I was looking at and read it as the count of the failure. The unattached class is 7 at this PR's base, and it splits in two. FIXED HERE -- two genuine trailing notes, each explaining why something does NOT exist and therefore having no following declaration to attach to. Both move above the declaration they already discuss, which is where they belong on the merits and not only to satisfy the gate: dag/product/rack_mount.dag -- the note argues the mounting APERTURE is not the external envelope, which is exactly what the function directly below it computes; it now leads rack_mounting_aperture_height. resolved_graph_cache_hand_rust_witness_test.dag -- the note records a deleted tautological witness and points at the surviving positive control; it now leads that control. NOT FIXED HERE, deliberately -- the remaining 5 are comments sitting directly above `service` declarations (extdeps git.Inspect, git.PublicationTransport, sec.Edgar, tailscale.Serve, gcp.IamRoles). A `service` produces no depth-1 occurrence index entry, so it is not an eligible annotation subject and prose above it attaches to nothing. Relocating that prose would make the corpus worse. git/inspect.dag's block is 24 lines of measured rationale for the service's operations -- which porcelain version is pinned and why, why IgnoredFiles is a second operation rather than a flag, verified by execution against git 2.43.0. Moving it off the declaration it describes to satisfy a gate would be contorting the source to fit a model gap, which is the opposite of what section 4c is for. So the honest reading is that `service` SHOULD be an eligible annotation subject and is not. That is a change to the occurrence index / annotation subject model in the v1 seed, not a comment edit, and it is raised rather than improvised: this PR stays comment-only, and the gate stays red on those 5 until that decision is made. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Hoist 13 body-grain annotations out of four modules main landed while this branch was open The compile-clean gate failed on this branch's merge head with the body-grain refusal class -- the same class this PR was opened to clear. The refusals are NOT this branch's: they arrived on main in four files added after this PR's base (dag/std/affine_space.dag, dag/std/planar_projection.dag, dag/product/rack_power.dag, dag/product/spatial_projection.dag), and merging main brought them in. That is worth naming rather than just fixing. Main cleared this class in the witness corpus and simultaneously re-introduced it in new modules, so the population is not shrinking on its own -- clearing it is a moving target until the rule is enforced where the module is parsed, not swept afterwards. Two shapes, both moved to module-item grain with the subject named in the hoisted text so the prose does not become unmoored from what it discusses: - variant-attached blocks (OpProjectPoint3, ProjectionSourceFrameRequired, ViewUnitsAreNotMillimetres, OutletsExhausted, DepthOrderAmbiguous, and the two borrowed ProjectionRefusal causes) hoisted into the leading block of their type declaration; - in-body blocks inside fn bodies (the zero-page-right refusal, the dimetric direction, the outlet-before-capacity ordering, the load-count crossing, the nearer-candidate role naming) hoisted above their enclosing fn. One trailing block was also refusing under the second class, "names no subject": rack_power.dag's NO DERATING note sat at end of file with nothing following it. It now leads budget_capacity, the accessor returning the un-derated cited capacity the note is about. Its dissolve-on trigger is carried across verbatim and is pre-existing debt from main, not introduced here. Corpus scan after this change: zero indented // lines and zero trailing blocks across dag/ and src/v2. NOT verified locally: the shimmed gunbc on this host predates //-annotation support and reports a parse error on every module header block, so it is not an oracle for this class. CI is. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

…eclaration it describes (#8215) * Move 18 body-grain source annotations to module-item grain DESIGN section 4c models source annotations only as standalone leading blocks on module-scope declarations. Eighteen comment blocks across five witness modules sat INSIDE declaration bodies -- annotating individual clauses of a conjunction, arms of a match, or lets in the middle of a function -- which the compile-clean gate refuses with: compile-clean: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes. This is pre-existing main debt, not a regression from any one branch. The count is exact: 18 in-body blocks under dag/ against 18 diagnostics, and the same refusal reproduces on two unrelated branches whose only common factor is that both force the whole-tree compile-clean baseline. Main's own recent runs are cancelled or in-flight, so no green verdict has observed it -- the debt has been accumulating unseen across at least five merged PRs (#8045, #8073, #8122, #8147, #8184-era files). The prose is preserved, not deleted. Each block is hoisted into its declaration's leading block, merged with any block already there, keeping the clause labels as sentences. Where a leading block already said the same thing -- fleet_converge_cli's join-1 header covers every clause note it carried -- the in-body copy is dropped as the duplicate it was. Comment-only: `git diff` contains no non-comment line, so no behavior, no witness assertion, and no emitted byte moves. WHAT THIS DOES NOT DO: the diagnostic is typed but UNLOCATED -- it names no file, line, or declaration, though AnnotationAttachmentRefusal carries `origin: SourceSpan` on every arm and BodyGrainNotModeled is constructed with it. The consumer discards the span it was handed. That is a section 5 located-ness gap which cost this diagnosis a full CI cycle and a bisection commit; it is left as a separate finding rather than repaired here, so this stays comment-only and reviewable as such. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Attach the two subject-less trailing annotations to the declarations they discuss CORRECTION TO THIS PR'S OWN DIAGNOSIS. The first commit claimed 18 in-body blocks were the whole annotation debt, on the strength of an exact count match. The match was real but the population was not the whole one: I grepped the failing log for the body-grain message and never checked whether a SECOND refusal class was also present. It was. The #8211 log carried 11 "source annotation names no subject: no module item follows it" refusals beside the 18 body-grain ones, and clearing the body-grain class left that second class as the visible failure. That is the nearby-question error: I confirmed the count of the class I was looking at and read it as the count of the failure. The unattached class is 7 at this PR's base, and it splits in two. FIXED HERE -- two genuine trailing notes, each explaining why something does NOT exist and therefore having no following declaration to attach to. Both move above the declaration they already discuss, which is where they belong on the merits and not only to satisfy the gate: dag/product/rack_mount.dag -- the note argues the mounting APERTURE is not the external envelope, which is exactly what the function directly below it computes; it now leads rack_mounting_aperture_height. resolved_graph_cache_hand_rust_witness_test.dag -- the note records a deleted tautological witness and points at the surviving positive control; it now leads that control. NOT FIXED HERE, deliberately -- the remaining 5 are comments sitting directly above `service` declarations (extdeps git.Inspect, git.PublicationTransport, sec.Edgar, tailscale.Serve, gcp.IamRoles). A `service` produces no depth-1 occurrence index entry, so it is not an eligible annotation subject and prose above it attaches to nothing. Relocating that prose would make the corpus worse. git/inspect.dag's block is 24 lines of measured rationale for the service's operations -- which porcelain version is pinned and why, why IgnoredFiles is a second operation rather than a flag, verified by execution against git 2.43.0. Moving it off the declaration it describes to satisfy a gate would be contorting the source to fit a model gap, which is the opposite of what section 4c is for. So the honest reading is that `service` SHOULD be an eligible annotation subject and is not. That is a change to the occurrence index / annotation subject model in the v1 seed, not a comment edit, and it is raised rather than improvised: this PR stays comment-only, and the gate stays red on those 5 until that decision is made. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS * Hoist 13 body-grain annotations out of four modules main landed while this branch was open The compile-clean gate failed on this branch's merge head with the body-grain refusal class -- the same class this PR was opened to clear. The refusals are NOT this branch's: they arrived on main in four files added after this PR's base (dag/std/affine_space.dag, dag/std/planar_projection.dag, dag/product/rack_power.dag, dag/product/spatial_projection.dag), and merging main brought them in. That is worth naming rather than just fixing. Main cleared this class in the witness corpus and simultaneously re-introduced it in new modules, so the population is not shrinking on its own -- clearing it is a moving target until the rule is enforced where the module is parsed, not swept afterwards. Two shapes, both moved to module-item grain with the subject named in the hoisted text so the prose does not become unmoored from what it discusses: - variant-attached blocks (OpProjectPoint3, ProjectionSourceFrameRequired, ViewUnitsAreNotMillimetres, OutletsExhausted, DepthOrderAmbiguous, and the two borrowed ProjectionRefusal causes) hoisted into the leading block of their type declaration; - in-body blocks inside fn bodies (the zero-page-right refusal, the dimetric direction, the outlet-before-capacity ordering, the load-count crossing, the nearer-candidate role naming) hoisted above their enclosing fn. One trailing block was also refusing under the second class, "names no subject": rack_power.dag's NO DERATING note sat at end of file with nothing following it. It now leads budget_capacity, the accessor returning the un-derated cited capacity the note is about. Its dissolve-on trigger is carried across verbatim and is pre-existing debt from main, not introduced here. Corpus scan after this change: zero indented // lines and zero trailing blocks across dag/ and src/v2. NOT verified locally: the shimmed gunbc on this host predates //-annotation support and reports a parse error on every module header block, so it is not an oracle for this class. CI is. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

CI's first successful build gave the first CI-measured diagnostic count, and it matches the local binary exactly: 1000 error rows on both. The build step now passes; the floor step fails on the migration frontier, which is this branch's declared state, not a regression. Five files carried 123 sites the oracle could answer and had never been asked: they entered the branch by MERGE after the qualification passes ran, so the resolver stripped their imports and nothing re-qualified them. Top concentration was dag/product/compute_board/admission.dag (94 of the 1000), added by #8147. Also re-applied the pattern-head reversion (164 heads, 20 files): merges reintroduce qualified match-arm heads, which discard the scrutinee's generic instantiation. Measured: 1000 -> 910 rows, unresolved-type 186 -> 89.

gunbai-bot Bot changed the title ~~mobo design scoping~~ VERILOG-ROWS-0: prove compositional target emission with the board interlock Aug 11, 2026

Brian Searls and others added 20 commits August 12, 2026 00:28

Merge remote-tracking branch 'origin/main' into session/verilog-rows-0

a41cb09

A resistor rated in nanofarads has no constructor: kind and value are…

990443e

… one coproduct

No projection reads an unadmitted board: whole-article admission, col…

fd493da

…lected causes

The constructor decides the element letter: SPICE names carry their o…

a6d152f

…wn spelling

Delete the product-local SPICE printer: the format module owns every …

429f023

…byte

Real tools accepted the emitted bytes: iverilog simulated the interlo…

23733e9

…ck, ngspice solved the deck

The frontier rows say what ran: SPICE and Verilog have both been exec…

b240779

…uted

The firmware contract names the signals it rides on, and admission ch…

cf7db1d

…ecks the join

Five firmware roles, three cited upstreams, and two that say why they…

d547518

… are not

Merge main

0f5d7aa

std.bmc already spells OpenBmc: the cited project takes its own name

6dfc9e5

gunbai-bot Bot marked this pull request as ready for review August 12, 2026 19:53

Brian Searls added 2 commits August 12, 2026 20:20

Delete the projections second opinion: drivenness is an article fact,…

65d4b20

… refused once

One refusal gate, both SPICE paths: the run deck can no longer bypass it

3621190

The host boundary refuses in types: no entry answers a refusal with p…

f09fac9

…rose

briansrls merged commit a289b74 into main Aug 13, 2026
5 checks passed

briansrls deleted the session/verilog-rows-0 branch August 13, 2026 01:44

Navigation Menu

Repository navigation

VERILOG-ROWS-0: prove compositional target emission with the board interlock - #8147

VERILOG-ROWS-0: prove compositional target emission with the board interlock#8147
briansrls merged 25 commits into
mainfrom
session/verilog-rows-0

briansrls commented Aug 11, 2026 •

edited by gunbai-bot Bot

Loading

Uh oh!

gunbai-bot Bot commented Aug 11, 2026

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented Aug 11, 2026 • edited by gunbai-bot Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What this delivers

1. Verilog emits through the generic fold, with no compiler branch

2. Nothing projects an unadmitted board

3. A resistor rated in nanofarads has no constructor

4. The SPICE format module owns every byte

5. Real tools accepted the emitted bytes

6. The firmware contract names the signals it rides on

Rung, stated honestly

Not in scope

Uh oh!

gunbai-bot Bot commented Aug 11, 2026

Finding: alternation requires structural difference — the direction productions as committed are unselectable

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

gunbai-bot Bot commented Aug 12, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented Aug 11, 2026 •

edited by gunbai-bot Bot

Loading

Finding: alternation requires structural difference — the `direction` productions as committed are unselectable