Repository navigation
v4 PROOF-1: external trust-discharge for A3 (no new file) - #3158
Merged
Merged
Conversation
Operator-ratified 2026-05-15 (option b, AGENT-1-style placement — no new file). gunbc's structural evidence (A2 termination descent, the algebra- homomorphism epistemic chain, cost, effects) is emitted as a machine- checkable proof term in an external prover (Lean/Coq); their small independently-audited kernel checks it. This is the honest completion of A3: it converts A3's named seed-trust axiom into an INTERSUBJECTIVE check against an anchor gunbc does not own. It does NOT make gunbc un-gameable — the external kernel + the evidence→ proof-term faithfulness are the NEW named axioms; trust is MOVED to a stronger anchor, not eliminated (same Trusting-Trust honesty A3 states). Constraints: the lens EXPORTS witnesses gunbc already has, the prover only KERNEL-CHECKS (never searches — no-engine + A2 checker-not- discoverer); discharges only structurally GROUNDED claims (ungroundable ⇒ fail-closed Diagnostic). Placed in A3's homes: STRUCTURE.md §7 + workflow/bootstrap.dag A3 block + DECISIONS.md PROOF-1 row + TASKS.md T-15 note. Realized later as a composition (evidence read ⊕ B2-OMNI emit to a lean/coq model) — no new file, closed-tree invariant preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
commented
May 15, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
Author
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
576d205c· Trigger:schedule - Thinking:
128s wall
BLOCKING (1)
Root Cause
src/v4/STRUCTURE.mdPROOF-1 adds a proof-assistant target without reconciling the closed file tree → either ratify the Lean/Coq model file(s) in the tree or rewrite PROOF-1 to consume an already-enumerated target.
| discoverer"); (ii) it discharges only what is structurally GROUNDED — | ||
| ungroundable concepts remain fail-closed Diagnostics; PROOF-1 inherits | ||
| gunbc's honesty boundary, it does not paper over it. Realized as a | ||
| lens = (evidence read) ⊕ (B2-OMNI emit to a `lean`/`coq` language |
Contributor
Author
There was a problem hiding this comment.
BLOCKING: PROOF-1 requires B2-OMNI emission to a lean/coq language model while also requiring no new file, but the closed v4 tree enumerates no Lean/Coq model, so the design has no substrate home and violates INVARIANTS P1/P5.
Contributor
Author
|
Review metadata
1. Story of the diffThis PR adds PROOF-1 to the v4 planning spine as an external trust-discharge mechanism for A3, without adding a new file or implementation surface. The new decision says gunbc will export structural evidence it already has—A2 descent, algebra-homomorphism chain, cost, and effects—as machine-checkable Lean/Coq proof terms, with the external prover kernel checking rather than searching ( The load-bearing design choice is that PROOF-1 is not a new proof engine inside gunbc. It is described as “lens = evidence read ⊕ B2-OMNI emit,” with ordinary Lean/Coq target emission and no new subsystem ( chatgpt-review-d803db69-e8bc-4a… 2. Invariant categories
chatgpt-review-335a2851-89fa-4d…
2.5. Top-down PM intent reviewCompliant. The highest-level intent is preserved: gunbc’s correctness surface remains structural, lens-readable, and v4-applicable; PROOF-1 adds an external check for already-derived evidence rather than turning structural guarantees into optional testing or hand-maintained proof infrastructure ( I do not see a PM-level mismatch. The plan does not postpone a must-have target without reconciliation, does not create permanent scaffolding, and does not add hand-written compiler implementation where the active v4/zero-floor direction requires generated/data-authored structure. The “ordinary emit targets, no new subsystem” language is the key PM-preserving clause ( chatgpt-review-d803db69-e8bc-4a… chatgpt-review-b4ef00af-9559-44… 3. VerdictAPPROVE. The PR is documentation-only, but it threads the new PROOF-1 concept through the right authorities and keeps the boundaries explicit: existing structural witnesses, kernel-check only, fail-closed on ungrounded facts, ordinary Lean/Coq target emission, and no new subsystem/file. I found no diff-cited invariant or PM-intent violation. |
briansrls
added a commit
that referenced
this pull request
May 15, 2026
B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 16, 2026
…ursor #3162 APPROVE_WITH_COMMENTS) Valid NON-BLOCKING finding: B-2 added lean.dag + the L-4 row but the PROOF-1 row still ended "**NO new file** (closed-tree invariant)", contradicting L-4 (which lands extdeps/languages/lean.dag). Reconciled: PROOF-1's framing (#3158) added no file (framing-only, deferred the model "lands later"); that deferred model subsequently lands as lean.dag per B-2/L-4. One coherent story; PROOF-1 row now cross-refs L-4 and states "No contradiction" explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 16, 2026
…#3162) * WIP: v4 design * v4 D1: Diff/Path structural-delta vocabulary over Node Side-session-ratified B-1. EdgeSelector/Path/Edit/Diff data types in std/node.dag (DATA ONLY; A1-clean — Node stays the sole recursive type; B1/Hash precedent for substrate-tier placement). Operations (subterm_at/apply_diff -> Result<Node,Diagnostic>, paths_independent/ diff_well_formed) contracted into lens/application.dag header — forced off node.dag by the diagnostic.dag->node.dag cycle (Correction= Suggested(Node)); the node.dag "consumers fail-close" discipline. affected_set.dag consumes the type. DECISIONS.md Part-1 row D1 carries the data/op-split PROPOSED sub-point for operator confirmation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 D1: dissolve two P2 illegal-state surfaces (codex #3162 REQUEST_CHANGES) Both findings valid; fixed structurally rather than patched. Finding 1 (node.dag:~478 ByPosition{index:Int} admits negatives): drop EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step descends the Named edge keyed by that opaque Symbol. No ordinal exists, so the negative/out-of-range illegal state is structurally impossible (dissolved, not deferred to path resolution). Positional-connective children are reached by replacing the enclosing Named subtree (the safe over-fire #3157 blesses); surgical positional addressing is a future operator-ratified extension (consumes-nothing root has no Nat; recursive Peano = A1 STOP). Finding 2 (node.dag:~514 Diff=List<Edit> validity via external predicate): drop the set / pairwise-independence / parallel-positions framing and paths_independent/diff_well_formed. Diff = ORDERED List<Edit> applied SEQUENTIALLY; any List<Edit> is a valid rewrite program (no representable illegal state). A non-resolving Edit => fail-closed Diagnostic at apply time (operational, not a type-level illegal state); apply_diff is a fold, all-or-nothing. Both refine the operator-ratified shape — flagged in DECISIONS.md D1 PROPOSED-for-operator-eye for confirm/redirect. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: add Practice-4 dissolution receipt; fix RATIFIED/PROPOSED contradiction (#3162 BLOCKING) BLOCKING (codex via briansrls relay, vs pre-fix sha a06a066 — verified against current HEAD): - "D1 sum vocabulary without coproduct receipt": the EdgeSelector sum was already deleted in 7c91f73, but the DECISION not to have a positional selector is itself a Practice-4 dissolution requiring the formal 4-pattern ledger (algebra.dag precedent). Added the receipt to std/node.dag D1 (🟢 GREEN terminal: positional addressing subsumed by enclosing-Named-subtree replacement; not a deferred gap). - "root-status driving the index carrier": resolved by the same dissolution — there is no index carrier; the receipt documents why none is needed (vs the reviewer's Nat/Fin suggestion) and why a future surgical form is an explicit operator-ratified extension. Non-blocking: DECISIONS.md D1 row no longer carries a "confirm or redirect" clause inside a RATIFIED row — refinements are stated as encoded-via-PR-review (the normal channel), not an open fork. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: fix stale EdgeLabel cross-reference in node.dag header (cursor #3162 editorial) The D1 header block cited "lines ~221-230" for the no-stored-index discipline, but adding the D1 header block shifted line numbers — that range is now `Connective`. Re-anchored by construct name + corrected approx lines: `type EdgeLabel` ~284 and its "deliberately NO stored index" rationale ~278. Editorial only; cursor APPROVE on this PR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-4: affected_set R2 node-precise-resolution contract Encodes the B-4 cross-cutting decision (operator-greenlit): affected_set minimality requires 04_infer resolution to bind each use-site name-ref to the EXACT declaration Node (not module/scope). The use->def graph is derived by traversal over already-resolved name-references, NOT a 5th InferredFacts field (IR-1-safe; same derive-don't-store discipline as content_hash/D1). Coarse resolution = correct but maximally over-fires. Reciprocal header contracts: 04_infer.dag B-4 block + affected_set.dag Consumes note. DECISIONS.md Part-1 row B-4. Scaffold headers only; no bodies. Continues the v4 design-survey on the session branch alongside D1 (operator sequences/carves at manual merge). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-5 + subsume #3153 + B-2 (lean.dag PROOF-1 model) B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 B-4: correct the use→def carrier (Symbol/K-1, not resolved_type) — #3162 BLOCKING Valid P2/Practice-3 finding (briansrls inline @ 04_infer.dag:54): resolved_type is the node's TYPE; many declarations share a type, so it is lossy for binding identity — the use→def fact had no named forward carrier. Corrected: the carrier is the post-resolution opaque Symbol (K-1) on the name-ref Atom, AUTHORED by 03_resolve.dag (binding = Symbol equality, node.dag name_occurrences pattern). 04_infer is preserve-only (no 5th InferredFacts field, IR-1-safe); affected_set derives by Symbol-equality traversal. Fixed consistently across 04_infer.dag B-4 block, new 03_resolve.dag B-4 authority note, affected_set.dag Consumes note, DECISIONS.md B-4 row. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * WIP: v4 design * v4 C5-2 emit-locality + T-9 infer keystone contracts (operator-ratified) C5-2 (emit-locality): emit is structurally local — a D1 apply_diff at Path p re-emits ONLY p's subtree. Per operator code-as-data steer: locality is Node-relative, NOT file-relative; a file is a convenience projection, the substrate anchors no semantic on the file concept; non-local emit = declared normalization at the enclosing NODE scope, never "file scope". The C5↔D1 hinge (AGENT-1 faithful re-emit). 05_emit.dag header + Owns + DECISIONS C5-2 row. T-9 A+B: A — Find decidable by construction (closed declared-inhabitance candidate set, not a synthesized search; structural descent ⇒ the inferencer terminates; empty = decidable fail-closed Diagnostic). B — single-file discipline is the 03_resolve scope boundary (env/scope/ lookup/binding belongs to 03_resolve per B-4; infer owns only Find + cardinality + diagnostic precision). 04_infer.dag header + DECISIONS T-9 row. Receipts: in-header (operator decision; status quo, no change). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: complete the Practice-4 receipt — add Pattern 5 (#3162 codex REQUEST_CHANGES) Valid finding. docs/modeling-discipline.md:112 requires FIVE dissolution patterns; the node.dag #3160 operator-ratified receipts already use 5. The D1 receipt did only 4 (I wrongly followed algebra.dag's older 4-pattern style). Added Pattern 5 (Parameterized family) — FAILS: ByName/ByPosition are not one mechanical F<X> over a declared set (different payload types + addressing semantics; mirror EdgeLabel's genuine 2-variant discriminant, not an enumerated copy à la Homomorphism-per-algebra); no source set to project over (Practice-7 N/A); post-dissolution one constructor = not a family. "four" → "five". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 C5-1 + C5-3 (operator-ratified) — node-level round-trip law + spec-provable F C5-1: the bidirectional_roundtrip TestClaim asserts ingest∘emit=id_Node via B1 content_hash (meaning round-trips), NOT text-byte identity. Text-level fidelity recorded as a DEFERRED orthogonal future layer (a trivia sidecar outside Node/content_hash, partial; the C5-fidelity Declared-normalized dispositions are its forward hook — node-level adoption preserves it zero-rework). Non-orthogonal route (lexical in the Node) explicitly rejected. C5-3: F = the spec-provable meaning core; spec silence ⇒ out of F (Declared-normalized or Fail-closed). Conservative/fail-safe — the spec decides, modeler has no discretion; per-language non-F shrinkage declared up front, not discovered at test time. Encoded: lens/testgen.dag C5-1/C5-3 header block + DECISIONS C5-1/C5-3 rows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4: reconcile PROOF-1 row with L-4 — DECISIONS.md self-consistency (cursor #3162 APPROVE_WITH_COMMENTS) Valid NON-BLOCKING finding: B-2 added lean.dag + the L-4 row but the PROOF-1 row still ended "**NO new file** (closed-tree invariant)", contradicting L-4 (which lands extdeps/languages/lean.dag). Reconciled: PROOF-1's framing (#3158) added no file (framing-only, deferred the model "lands later"); that deferred model subsequently lands as lean.dag per B-2/L-4. One coherent story; PROOF-1 row now cross-refs L-4 and states "No contradiction" explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Operator-ratified 2026-05-15 (option b; AGENT-1-style placement — no new file). The "proof export to Coq/Lean" capability, framed correctly: not transpilation, but the external trust-discharge for A3.
gunbc's structural evidence — A2 termination descent, the algebra-homomorphism epistemic chain, cost, effects — is emitted as a machine-checkable proof term in an external prover (Lean/Coq); their small, independently-audited kernel checks it. This converts A3's named seed-trust axiom into an intersubjective check against a trust anchor gunbc does not own.
Honest framing (consistent with A3)
Placement (operator-chosen — no new file)
Encoded in A3's existing homes:
STRUCTURE.md§7 +workflow/bootstrap.dagA3 block +DECISIONS.mdPROOF-1 row +TASKS.mdT-15 note. Cross-ref A2 (primary evidence source) / AGENT-1 (an agent may request it) / B2-OMNI (lean/coq = ordinary emit targets). Realized later as a composition(evidence read) ⊕ (B2-OMNI emit to a lean/coq model)— no new subsystem, closed-tree invariant preserved.Test plan
cargo fmt --all --checkcleanv2-compiler compile --source-root src/v4 --target dag→ 0 diagnostics🤖 Generated with Claude Code