Skip to content

W1.1: lift GraphInvariant kernel from wiring_liveness + inhabit fix-generation via Correction.Suggested - #6680

Merged
briansrls merged 6 commits into
mainfrom
session/smart-crab-342
Jul 15, 2026
Merged

briansrls merged 6 commits into
mainfrom
session/smart-crab-342

Conversation

@briansrls

@briansrls briansrls commented Jul 15, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Wave 1 keystone (W1.1): lift the pure reach fixpoint from wiring_liveness into v2.lens.common.graph_invariant — a shared GraphInvariant<Projection> kernel with GraphReachProjection { edges, roots }.

  • Kernel (graph_invariant.dag): reach fixpoint engine + repair contract header (AddReachEdge | EnrollInExceptionRoster | Delete). Handlers emit fixes only via existing Correction.Suggested { node } — no new Repair type.
  • Repointed (pure reach only): wiring_liveness, wiring_liveness_preflight. Not touched (W3.1 fence): inert_lens, doc_reachability, host-fed lenses.
  • Fix generation: dead-wire handler produces Suggested { node: add_edge_repair }; apply path uses apply_edit / substitute_at.

Proof obligations (green-by-execution)

All in reach_repair_witness_test.dag + preflight tests:

  1. Dead wire → Suggested, not Unavailable (witness_dead_wire_produces_suggested_not_unavailable)
  2. The law: apply correction → re-run invariant → Satisfied (witness_apply_correction_reruns_satisfied)
  3. RED control: wrong correction stays Violated (witness_wrong_correction_stays_violated)
  4. Fixed-code: serialize_diff_as_source_patch + target_serialize_source_from_model on repaired tree (witness_apply_edit_emits_corrected_source)

Test plan

claim_batch over graph_invariant + wiring_liveness witnesses — all PASS.

@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review July 15, 2026 17:46
Brian Searls and others added 2 commits July 15, 2026 17:50
…ion.Suggested

Lift the pure reach fixpoint from wiring_liveness into v2.lens.common.graph_invariant
(parameterized GraphReachProjection), repoint wiring_liveness/preflight only, and emit
AddReachEdge repairs through the existing Correction.Suggested slot with apply_edit
proof witnesses (suggested-not-unavailable, apply→satisfied, wrong→violated, emit).

Co-authored-by: Cursor <cursoragent@cursor.com>
…ve-on

Document that graph_reach_root_replacement_edit is a proof-of-interface grain,
not the final surgical edit-at-locus repair shape (W1.1 parent review).

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

Re: cursor/composer-2.5 review @ 33146c (stale vs current HEAD)

That approval was written against the first commit, which placed the kernel in v2.std.graph_invariant and repointed inert_lens / doc_reachability. Current HEAD (8b9d435+) aligns with the W1.1 mandate:

  • Kernel lives in v2.lens.common.graph_invariant with GraphReachProjection { edges, roots }
  • Only wiring_liveness + wiring_liveness_preflight repointed; inert_lens / doc_reachability reverted (W3.1 host-fed fence)
  • Fix generation uses existing Correction.Suggested { node } + apply_edit; four discriminating witnesses in reach_repair_witness_test.dag

Latest commit adds the counted frontier marker: graph_reach_root_replacement_repair_frontier — root-replacement is first-inhabitant only; DISSOLVES-ON surgical edit-at-locus repair.

Re: claude/claude-opus-4-7 — trailing newline on reach_repair_witness_test.dag fixed in the same commit. graph_reach_saturate fold bound is intentional pure lift from old wiring_reach_saturate.

— sent from smart-crab-342

@cursor

cursor Bot commented Jul 15, 2026

Copy link
Copy Markdown

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

…zer smoke

witness_apply_edit_emits_corrected_source failed in floor because synthetic
Atom subjects do not serialize through dag_target_model. Split proof-4 into
apply_diff structural authority match and application_serializer pipeline smoke
on real emitted fixtures.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

Re: cursor/composer-2.5 @ 423459e (APPROVE, no findings) — Verified accurate on current HEAD. No code changes required for this review.

CI fix pushed (423459e+): witness_apply_edit_emits_corrected_source was failing in floor — synthetic Atom subjects do not serialize through dag_target_model. Replaced with:

  • witness_apply_diff_matches_repaired_authority — apply_diff result structurally equals repaired root (proof-2 apply law)
  • witness_emit_path_uses_application_serializer — emit pipeline smoke on real dag_fixture_emitted_loop_fn via serialize_diff_as_source_patch

Full emit-on-reach-repair for real fn bodies remains on the dissolve-on frontier (graph_reach_root_replacement_repair_frontier).

— sent from smart-crab-342

@gunbai-bot

gunbai-bot Bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

Review feedback response (@60cdf3c1ec)

Verified all four dashboard APPROVE artifacts (cursor @38388/@38395, claude @38389/@38393) against current HEAD — no code changes required; the findings hold.

Claim verification:

  • §2 consolidation: wiring_liveness delegates reach to v2.lens.common.graph_invariant via thin adapters (wiring_reaches / graph_reach_contains) — confirmed in source.
  • §3 single authority: repairs emit through Correction.Suggested only; graph_invariant_repair_contract on-carrier at graph_invariant.dag:32; no parallel Repair type.
  • §5 fail-closed: graph_reach_unreachable_diagnostic returns Unavailable when target already reaches (lines 134–139), Suggested only when genuinely unreachable; preflight + wrong-correction RED witnesses green.
  • §6 scaffold: graph_reach_root_replacement_repair_frontier at line 34 documents root-replacement as first-inhabitant with named dissolve-on for surgical edit-at-locus.
  • W3.1 scope fence: inert_lens / doc_reachability untouched — intentional incremental W1.1.

Proof-4 (parent hold): witness_apply_edit_emits_corrected_source restored on emittable loop fixture with surgical Edit.at Path { steps: [^arrow_body_edge] } (not root replacement). CI run 29440545768 — all 5 reach_repair witnesses PASS including proof-4 (34ms).

Merge readiness @60cdf3c1ec: mergeable=CLEAN, CI green (build + ci), ≥2 distinct APPROVE reviews, no REQUEST_CHANGES. Ready for operator merge.

— sent from smart-crab-342

@briansrls
briansrls merged commit 1fe168b into main Jul 15, 2026
2 checks passed
@briansrls
briansrls deleted the session/smart-crab-342 branch July 15, 2026 19:00
gunbai-bot Bot pushed a commit that referenced this pull request Jul 15, 2026
…t first

main (#6680 lane) independently made the identical nfr roster fix while this PR
was in review: same two nbd_proxy_serve stale rows deleted, same
emit_host::run_test_claim_emit_vs_eval_verdict stale row deleted, and the same
apply_role backfill added (its own wording, different position in the roster).

Resolution takes MAIN's side wholesale. Keeping mine would have produced two
apply_role rows -- harmless at use (the roster collapses to a BTreeSet) but a
pointless redundancy, and re-litigating identical work for authorship is not a
reason to diverge. cli_run.rs is now byte-identical to origin/main.

This PR therefore reduces to the work main does NOT have, verified against
origin/main:
  - the cargo fmt CI gate (de-fused from the nextest bundle) + its authority
    note amendment + regenerated ci.yml
  - the latent main fmt red fix (main still carries the unformatted import)

Independent convergence on the roster is a receipt for the falsifier itself:
two lanes hit the same cold-sweep reds and reached the same verdicts on which
rows were genuinely migrated vs still live.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 16, 2026
…; re-enroll cargo fmt in CI (de-fused from nextest) (#6691)

* WIP: falsifier is failing

* non_fold_residue roster: burn down 3 stale rows, backfill apply_role (#6637)

The affected-set-falsifier has been red on every cold sweep since 2026-07-15
04:32 UTC (last green 07-14 23:10, run 29374839251). It was doing its job:
three discovery witnesses returned Bool(false) against the whole corpus that
per-PR selection had predict-skipped. This clears the two non_fold_residue
ones; the inert_carrier one is a separate lens-precision question, left red
deliberately rather than papered over.

Stale rows deleted (roster 120 unique -> live 118; each verified as genuinely
migrated, NOT merely gone lens-invisible -- the converge_cli_applied_knob_count
trap):
  - nbd_proxy_serve.dag::shell_command_leading_lit_text
  - nbd_proxy_serve.dag::shell_rawline_starts_with_tool
    both fns DELETED by #6629 (P6 Part 2: RawLine body -> typed session-lease
    effect), firing the dissolve-on their rows carried.
  - emit_host.dag::run_test_claim_emit_vs_eval_verdict
    fn still exists (emit_host.dag:335) but #6650 enumerated its wildcard into
    three explicit constructor arms -- residue genuinely folded, no bare `_ =>`
    remains. Ratchet tightens.

Unrostered row backfilled: bash_composition_recognizer.dag::apply_role, landed
by #6637. Two-special-variant dispatch over TokenRole's 5 variants; the other
three all reduce to the closed run, so enumerating would clone the general arm
3x. Same class as the orch_emit_let_step row above it (receipt #10).

Green-by-execution (claim_batch, local):
  PASS non_fold_residue_no_unrostered_or_stale (src/v2/lens)
  PASS non_fold_residue_clean_holds            (dag/test/claim)
  FAIL inert_carrier_no_unrostered_or_stale    <- unchanged, see PR body
Discriminating RED control: both nfr witnesses were red on this same tree
before the roster edit and green after; no witness or assertion was weakened.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: falsifier is failing

* WIP: falsifier is failing

* Re-enroll cargo fmt in CI as a standalone step, de-fused from the nextest bundle

Operator ruling 2026-07-15. Restores fmt enforcement without re-enrolling
RustMonolithGate (still rejected).

WHY IT WAS GONE: tools.rust_gates_ci.run_gates welds two separable facts into
one ProcessExit -- fmt (4.3s measured, parse-only, no build, green) and nextest
(~37 GiB, compile+run, red on main). The 2026-07-11 ruling removed the bundle
for reasons that are ALL facts about nextest; fmt was collateral damage of that
fusion (DESIGN 3).

WHY THE HOOK ISN'T COVERAGE: the ruling's declared replacement was the pre-push
hook. That is an escape hatch (DESIGN 5) -- opt-in per clone via a manual
core.hooksPath, bypassable with --no-verify, absent in container worktrees --
and PROVEN ineffective, not just theoretically weak: in this very worktree
core.hooksPath points at a directory with no pre-push hook at all, and #6658
landed an unformatted .rs on main 2026-07-15 with nothing catching it. The hook
stays as fast local feedback, never as the wall.

SHAPE: standalone RunStep, FIRST in the build job -- a 4-second violation now
fails in 4 seconds instead of after the ~33min release build. build is not
protection-required itself, but ci needs:[build], so a red fmt blocks the
required job by construction. Toolchain already installs the rustfmt component
in ci_prelude_steps, so marginal cost is ~4s and no build.

Step-budget discipline (gunbc_ci_job_timeout_policy_disposition: "the backstop
is the exact step-sum + prelude"): the new step carries the aux cap and
gunbc_ci_build_job_backstop_timeout_minutes() gains exactly one aux term
(65 -> 70), so no step is uncapped and the sum stays exact.

Authority updated, not left lying: commit_gate_rust_suite_removed_disposition
declared "cargo fmt stays enforced by the pre-push hook". That claim is now
retracted in-row and the fmt half marked reversed; the nextest half and the
RustMonolithGate rejection are preserved verbatim.

ci.yml regenerated through the emit authority (expected_ci_yml), never hand-
edited; trailing-newline gotcha handled.

GREEN-BY-EXECUTION:
  PASS generated_artifact_drift_witnesses   <- the real drift gate, ci.yml byte-exact
  0 FAILs across ci_yaml_serializer, ci_compile_jobs, placement_grain,
    rust_gates_ci, ci_budget_tree witnesses
DISCRIMINATING RED: planted a fmt violation, ran the EXACT emitted step command
  -> exit 1 (caught); restored tree -> exit 0. The gate discriminates.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* Resolve merge conflict: drop duplicate nfr roster work, main landed it first

main (#6680 lane) independently made the identical nfr roster fix while this PR
was in review: same two nbd_proxy_serve stale rows deleted, same
emit_host::run_test_claim_emit_vs_eval_verdict stale row deleted, and the same
apply_role backfill added (its own wording, different position in the roster).

Resolution takes MAIN's side wholesale. Keeping mine would have produced two
apply_role rows -- harmless at use (the roster collapses to a BTreeSet) but a
pointless redundancy, and re-litigating identical work for authorship is not a
reason to diverge. cli_run.rs is now byte-identical to origin/main.

This PR therefore reduces to the work main does NOT have, verified against
origin/main:
  - the cargo fmt CI gate (de-fused from the nextest bundle) + its authority
    note amendment + regenerated ci.yml
  - the latent main fmt red fix (main still carries the unformatted import)

Independent convergence on the roster is a receipt for the falsifier itself:
two lanes hit the same cold-sweep reds and reached the same verdicts on which
rows were genuinely migrated vs still live.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: falsifier is failing

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant