Repository navigation
Conversation
…5/B7/B8 Interfaces and evidence, not implementations. No production domain, no translator, no runtime integration — the point is that the boundaries get reviewed before anything rests on them. Three layers, one-way dependencies: domain/capabilities/delta (B1 B3); invariants/context (B4 B8); laws/policy/version DAG (B2 B7 B5). B6 is out of scope and remains the RFC's own open question. **The output that matters is five proof obligations** — places where the RFC states a requirement whose terms it never defines, and where an implementer's reasonable guess silently becomes a normative decision nobody made. The first is the seam. §6.2 rule 2 requires a policy to state "the minimum status each boundary requires", and §6.2 defines NO ORDER on LawStatus. Part 03 repeats the phrase three times without repairing it. The text relates falsified and asserted to the rest and never relates `proved` to `tested` — and LawClaim.scope, LawClaim.precondition and tested.domain make that gap load-bearing: a proof over a narrow precondition and a test over a strictly wider generation domain are incomparable, and ranking proved first would let a boundary accept a proof about a region it does not operate in over evidence about the region it does. That is the same shape Suitability.lean already proved as `no_meet` (finding C3) — "the lower of two levels" over an order with no meet. Which is why this package does NOT invent a total order: an invented order is a normative decision wearing an implementation's clothes. `statedBelow` returns null for "the text does not order these", which is a different answer from false and is the one a policy has to act on. BoundaryPolicy states an accept SET, which needs no order. No Lean is included. The theorem candidate is stated exactly, and so is the condition for wanting it: it decides between the two available repairs, and if the steward takes the accept-set repair there is nothing left to prove. Adding theorems for the other repair before that choice is made would be weight rather than evidence. The other four obligations: InvariantDefinition has no field for the context surfaces §6.1.2 rule 1 requires it to declare; DeltaDescriptor is required with its own content address and never given a shape; the version-label projection is required and never specified; and scope widening is neither permitted nor forbidden. Properties are labelled structural / requires-a-LawClaim / has-a-countermodel, because the general form of Codex's warning is deriving a property from a shape. The countermodel category is non-empty on purpose — an empty one would mean nobody looked, not that the design is sound. Four are executable: a proof narrower than a test; clamped translations as a well-typed non-associative delta space, with the arithmetic witness; scope widening producing two different reports from two legal world snapshots; and the one version conflict §6.2.1 names. Fail-closed everywhere, with a code per refusal and nothing falling through to an accept. Two conditions are deliberately not-assessed rather than refused — over budget and stale snapshot — because §6.1.2 rule 5 requires an outcome distinct from held, and collapsing it to a boolean is how a boundary comes to believe an invariant held when nobody checked it. Reuses rather than reinvents: the full-digest convention and reference kinds come from the fast-path debt-scope probe, which already types RFC-0003 references. 20 controls. ./t check READY, 602 tests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DRHMVB9rUYNggn4wLmc1An
PR Summary by QodoAdd Tranche B typed-domain interface and evidence package
AI Description
Diagram
High-Level Assessment
Files changed (13)
|
|
Joint gate round 1/2 on exact Positive: the three-layer scope is correct, all seven B items are mapped, the 20 shipped controls run, and keeping Lean out before a normative choice is correct. P1 — the central no-meet claim is false for the implemented relationExecuted against {"lower_bounds":["asserted","falsified"],"greatest_lower_bounds":["asserted"]}The package defines Required: withdraw the no-meet/theorem claim. Accept-sets may remain the proposed repair, justified because scope/precondition/generation-domain are not captured by a status threshold. If a contextual no-meet is claimed, first define the contextual relation and then prove/test that relation. P1 — supplied context is not an observed read
Rule 1 prohibits undeclared reads, not available inputs. Required: separate provided surfaces from observed/authorized reads (for example an execution trace or The current “scope-widening” fixture also changes worldSnapshot, so differing reports are expected for differing declared inputs; it is not a countermodel to widening. Reframe any remaining gap as snapshot/logical-step binding, or supply an actual same-input widening counterexample. P1 — law policy and composition say stronger things than they enforceExecuted:
P1 — these are typed decision helpers, not yet fail-closed schema validators
The package promises executable schemas/validators and “nothing falls through”. Required: entrypoints that consume fixture/untrusted data must accept P2 — evidence claims currently outrun the controls
Required: execute all claimed countermodels, use a real rooted graph with a disconnected cycle to hit P2 — two additional normative choices are currently silent
Add both to the obligation map, or model boundary acceptance explicitly without claiming the RFC supplied those orders/relations. Next response is final round 2/2. Keep the same closed package and delta-only report; no Lean and no production implementation. |
Code Review by Qodo
1. Claimed meet actually exists
|
![qodo-code-review[bot]](https://avatars.githubusercontent.com/in/484649?s=60&v=4){kind=small}
| (i) the stated relation is a strict partial order; | ||
| (ii) `proved` and `tested` are incomparable in it; | ||
| (iii) therefore { proved, tested } has no greatest lower bound, | ||
| and "the minimum status" is undefined for any policy that must |
There was a problem hiding this comment.
1. Claimed meet actually exists 🐞 Bug ≡ Correctness
The theorem candidate says {proved, tested} has no greatest lower bound, but statedBelow places
asserted below both and falsified below asserted, making asserted their greatest lower
bound. This invalidates the package's central no-meet proof obligation and its claimed analogy to
Suitability.lean.
Agent Prompt
## Issue description
The documented no-GLB theorem contradicts the relation implemented by `statedBelow`: `asserted` is a greatest lower bound of `proved` and `tested`.
## Issue Context
Re-evaluate whether the actual ambiguity is lack of comparability/minimum rather than lack of a meet, and update the README, proof-obligation text, countermodel claims, and tests consistently.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/README.md[155-183]
- probes/typed-domain-kernel-v0/README.md[226-243]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[55-100]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[359-379]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| }; | ||
| } | ||
|
|
||
| return { ok: true }; |
There was a problem hiding this comment.
2. Evaluation predicate is unbound 🐞 Bug ≡ Correctness
admitEvaluation never verifies that e.predicate equals d.predicate, so a held report produced by predicate B can be admitted as evidence for invariant A. The function runs its other checks and returns success despite the RFC requiring reproducibility for the same predicate and snapshots.
Agent Prompt
## Issue description
Reject an evaluation whose predicate address differs from the invariant definition's predicate address.
## Issue Context
Both values are independently supplied to `admitEvaluation`; success currently does not establish that the report belongs to the invariant being admitted.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer2_invariant.ts[182-191]
- probes/typed-domain-kernel-v0/ts/layer2_invariant.ts[258-275]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[99-120]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| if ( | ||
| boundary.freshness && | ||
| boundary.snapshotLogicalStepsBehind !== undefined && | ||
| boundary.snapshotLogicalStepsBehind > boundary.freshness.maxLogicalStepsBehind |
There was a problem hiding this comment.
3. Missing freshness passes admission 🐞 Bug ≡ Correctness
When a boundary supplies freshness but omits snapshotLogicalStepsBehind, the conjunction skips
the stale check and admitEvaluation returns {ok: true}. A snapshot whose freshness cannot be
measured has not been shown current and must not pass a fail-closed boundary.
Agent Prompt
## Issue description
Return `notAssessed: "snapshot-missing"` when a freshness requirement exists but no snapshot age is supplied.
## Issue Context
The reason is already present in `NOT_ASSESSED_REASONS`; the current condition only handles a known age that exceeds the limit.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer1_domain.ts[106-113]
- probes/typed-domain-kernel-v0/ts/layer2_invariant.ts[258-275]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[167-181]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| // Both admitted and scopes agree. The composite's status is NOT computed: | ||
| // that would require the order §6.2 does not state. A caller that needs one | ||
| // must consult both, which is what returning the pair-checked decision means. | ||
| return { admitted: true, status: l.status }; |
There was a problem hiding this comment.
4. Composition status depends on side 🐞 Bug ≡ Correctness
decideComposition says it does not compute a composite status but returns the left claim's status in the normal LawDecision field. Composing an admitted proved claim with an admitted tested claim therefore reports proved, while reversing the operands reports tested, exposing an order-dependent and unsupported result.
Agent Prompt
## Issue description
Make composition success avoid presenting the left operand's status as a composite status.
## Issue Context
Use a distinct composition decision type that either carries both checked statuses/claims or omits status entirely; add mixed-status operand-order tests.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[128-130]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[237-260]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[266-282]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| if (kind === "tested") { | ||
| // §6.2 rule 3, enforced at the consumer. The producing side declaring a | ||
| // generator is not enough: a boundary must be able to say which generation | ||
| // domains it will take, or "tested" is a word. | ||
| if (!claim.status.generator || !claim.status.domain) { |
There was a problem hiding this comment.
5. Short law references admitted 🐞 Bug ≡ Correctness
For tested claims, decideLaw checks only that generator and domain are nonempty, so values such as "x" pass despite both fields being content-addressed references. Proved evidence/checkers, tested evidence, falsified counterexamples, preconditions, and policy generation domains likewise receive no full-digest validation.
Agent Prompt
## Issue description
Apply `isContentAddress` to every reference-bearing law claim and policy field before making an admission decision.
## Issue Context
The package states that every reference is a full digest, but nonempty short handles currently pass layer 3.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[16-49]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[119-126]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[145-226]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[220-264]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| /** Laws of delta composition, if the domain composes deltas at all. | ||
| * DELIBERATELY OPTIONAL and deliberately not defaulted to associative: | ||
| * typedness does not confer associativity, and assuming it is exactly the | ||
| * move §6.2 exists to prevent. Absent means "no claim", not "no law". */ | ||
| composition?: ContentAddress; |
There was a problem hiding this comment.
6. Delta composition reference unchecked 🐞 Bug ≡ Correctness
DeltaDescriptor.composition is declared as a ContentAddress, but validateDomain omits it from the reference list, so a geometric domain with composition: "deadbeef" is admitted. This directly contradicts the package's claim that every reference is checked as a full digest.
Agent Prompt
## Issue description
Include `deltaDescriptor.composition` in `validateDomain`'s content-address checks when present.
## Issue Context
The optional field remains a reference even when no composition law is required.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer1_domain.ts[67-83]
- probes/typed-domain-kernel-v0/ts/layer1_domain.ts[233-261]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[69-93]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| /** Required when `tested` is accepted: the generation domain a boundary will | ||
| * take. Without it, §6.2 rule 3's "a test whose generation domain is unstated | ||
| * is `asserted` with extra steps" is unenforceable on the CONSUMING side. */ | ||
| requiresGenerationDomain?: PredicateRef; |
There was a problem hiding this comment.
7. Test-domain constraint is optional 🐞 Bug ≡ Correctness
requiresGenerationDomain is documented as required whenever a policy accepts tested, but the optional field and guarded comparison let such a policy admit every nonempty generation domain. The default test policy exercises exactly this unconstrained configuration, so the consuming-side requirement is not enforced.
Agent Prompt
## Issue description
Reject or make unrepresentable a policy that accepts `tested` without `requiresGenerationDomain`.
## Issue Context
Use a discriminated policy type and retain a runtime check for JSON-derived values.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[115-126]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[155-161]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[202-224]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[193-197]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| const byAddress = new Map(releases.map((r) => [r.address, r])); | ||
| const roots = releases.filter((r) => r.predecessor === null); |
There was a problem hiding this comment.
8. Duplicate releases collapse silently 🐞 Bug ≡ Correctness
validateVersionDag constructs a map without checking duplicate addresses, so two distinct non-root
release records with the same content address collapse to one node and can still produce `{ok:
true}`. The accepted input is not an unambiguous content-addressed version DAG.
Agent Prompt
## Issue description
Detect duplicate release addresses before constructing the DAG map and return a dedicated refusal.
## Issue Context
Do not allow later records to overwrite earlier records silently; cover duplicates with identical and conflicting metadata.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[272-279]
- probes/typed-domain-kernel-v0/ts/layer3_law.ts[290-311]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[284-309]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| for (const c of d.capabilities) { | ||
| if (!(CAPABILITIES as readonly string[]).includes(c)) { | ||
| return no("unknown-capability", `${c} is not a capability of this kernel`); |
There was a problem hiding this comment.
9. Malformed declarations throw 🐞 Bug ☼ Reliability
validateDomain directly iterates and indexes fields such as capabilities, implements, and laws, so JSON-derived inputs with missing/null fields throw instead of returning a coded refusal. That breaks the package's fail-closed validator contract at the exact runtime boundary where tests already use JSON.parse plus a TypeScript cast.
Agent Prompt
## Issue description
Validate the runtime shape of domain declarations before iterating or indexing their members.
## Issue Context
TypeScript types do not validate parsed JSON. Return structured refusal codes for missing, null, wrongly typed, or malformed fields rather than throwing.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/layer1_domain.ts[137-160]
- probes/typed-domain-kernel-v0/ts/layer1_domain.ts[162-240]
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[35-46]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
| const r = admitEvaluation( | ||
| inv({ scope: "trace", reads: ["state", "trace"] }), | ||
| evaluation(), | ||
| ); | ||
| if ("code" in r) assertEquals(r.code, "missing-trace-for-trace-scope"); |
There was a problem hiding this comment.
10. Trace control can pass falsely 🐞 Bug ⚙ Maintainability
The trace-scope control checks the refusal code only when a code field exists, so it also passes
if admitEvaluation regresses to {ok: true}. This makes one of the package's claimed executable
controls non-discriminating.
Agent Prompt
## Issue description
Add the same explicit `ok === false` assertion used by the transition branch before checking the trace refusal code.
## Issue Context
The test must fail if the validator unexpectedly admits the trace evaluation.
## Fix Focus Areas
- probes/typed-domain-kernel-v0/ts/kernel_test.ts[134-147]
ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools
1 participant
Campaign 2, one frozen package for B1–B5/B7/B8. Interfaces and evidence only — no production domain, no translator, no runtime integration.
Frozen SHA:
0ed65d7494cac34a11742e5512eb7d26a1cdbddfThree layers, one-way dependencies
B6 out of scope — it is the RFC's own open question (§20.19).
The seam
§6.2 rule 2 requires a policy to state "the minimum status each boundary requires". §6.2 defines no order on
LawStatus. Part 03 repeats the phrase three times (§7.1 :397, :540, :678) without repairing it.The text gives two relations —
falsifiedbelow everything,assertedbelow the evidenced kinds at translation/irreversible boundaries — and never relatesprovedtotested.LawClaim.scope,LawClaim.preconditionandtested.domainmake that load-bearing rather than cosmetic:Executable at
fixtures/countermodels/proved-narrower-than-tested.json.This is the same shape
Suitability.leanalready proved asno_meet(finding C3) — a document saying "the lower of two" over an order with no meet. Which is exactly why this package does not invent a total order.statedBelowreturnsnullfor "the text does not order these" — a different answer fromfalse, and the one a policy must act on.BoundaryPolicystates an accept set, which needs no order.Lean: not included, and the condition for wanting it is stated
The theorem candidate is written out exactly. It decides between the two available repairs — state a partial order and prove every comparable pair has a GLB, or replace "minimum status" with an accept set. If the steward takes the second, there is nothing left to prove, and adding theorems for the first before that choice would be weight rather than evidence.
Five proof obligations
LawStatushas no order, yet a minimum over it is required (the seam)InvariantDefinitionhas no field for the context surfaces §6.1.2 rule 1 requires it to declare — obligation exists, carrier does notDeltaDescriptoris required with its own content address and never given a shapeProperties, labelled
Your warning generalised: the failure is deriving a property from a shape. Every property carries one of three labels — structural, requires a
LawClaim, has a countermodel.Four countermodels, executable:
provedbeatstested"The countermodel category is non-empty on purpose. An empty one would mean nobody looked, not that the design is sound.
Fail-closed
Every refusal has a code; nothing falls through to an accept. Two conditions are deliberately not-assessed rather than refused — cost over budget, stale snapshot — because §6.1.2 rule 5 requires an outcome distinct from
held, and collapsing it to a boolean is how a boundary comes to believe an invariant held when nobody checked it.ValidationReportis three-valued for that reason; the RFC never types it.Full table in the README, plus closed member sets (asserted by a control) marking which are quoted from the RFC and which are proposed.
Checks
Reuses the full-digest convention and reference kinds from the fast-path debt-scope probe rather than reinventing them.