Lean Formal Feedback Loop

Lean Formal Feedback Loop

Treat proof friction as evidence. Hard proof failures are high-signal indicators of Rust defects, model drift, or theorem-scope mismatch. This skill is an execution program, not a theorem-writing tutorial.

Quick Start (90 Seconds)

cd /data/projects/asupersync

# 1) Load frog candidates from coverage
cat formal/lean/coverage/gap_risk_sequencing_plan.json | jq '.gaps[] | {id, priority_score, summary}'
cat formal/lean/coverage/invariant_theorem_test_link_map.json | \
  jq '.invariant_links[] | select(.theorem_witnesses | length == 0) | .invariant_id'

# 2) Verify cass index health (history mining is mandatory)
cass status --robot

# 3) Build Lean baseline
(cd formal/lean && lake build)

Pick one frog and close a full loop before touching another frog.

Critical Rules (Non-Negotiable)

• Work one frog at a time; no parallel frogs.
• No theorem is "done" before 7-check conformance parity passes.
• No alignment claim without witness + regression + artifact hash.
• Treat proof friction as evidence, not tactic debt.
• Change one lever per iteration, then re-run proof + conformance.
• When uncertain, bias code-first (expected-loss asymmetry).

Loop Checklist (Required Every Time)

• Intake: target subsystem, risk, current tier, target tier, fallback mode.
• Mine historical signals from cass (Step 0.5 below) and update BugPrior.
• Rank frogs with EV + posterior; pick top valid candidate (EV_frog >= 2.0).
• Fill reverse-round card (Surface, Failure Class, Math, Artifact).
• Attempt proof to first hard blocker; classify route.
• Extract executable witness (trace or lab seed) + regression candidate.
• Apply one route-specific change and rerun proof.
• Run 7-check conformance pass and quality gates.
• Emit proof-carrying artifact record.
• Recompute queue and stop or pick next frog.

Step 0.5: Mine Project History (sc Requirement, Mandatory)

Mine session history before ranking frogs.

cd /data/projects/asupersync

# Health check + index readiness
cass status --robot

# If missing/stale:
# cass index --full

# Pull bug-family and proof-surface signals
cass search "notify lost wakeup" --robot --limit 12
cass search "semaphore cascading wakeup" --robot --limit 12
cass search "pool.rs TOCTOU can_create" --robot --limit 12
cass search "refinement_conformance" --robot --limit 12
cass search "race losers drained cancellation" --robot --limit 12

Required extraction from hits (minimum 3 records):

• source_path and line_number
• concrete bug/fix clue (commit id, test name, theorem id, or failure shape)
• whether the signal raises or lowers BugPrior

No frog starts until this extraction is recorded in notes/artifacts.

Historical anchors (seed priors):

• aee9d1b: notify lost-wakeup fix
• e9eb3d5: semaphore cascading-wakeup fix
• a2e4c64: pool TOCTOU fix

Frog Ranking (Alien + Graveyard Math)

EV_frog = (Impact * BugPrior * RuntimeReach) / (ProofCost * ModelCost) (all 1-5)

• Impact: correctness consequence if wrong | BugPrior: chance proof exposes real code defect
• RuntimeReach: how hot the code path is | ProofCost: Lean difficulty | ModelCost: modeling overhead

Work frogs with EV_frog >= 2.0 first.

Update bug probability from proof signals:

odds_post = odds_prior * BayesFactor(signals)

Starting Bayes-factor signals:

• constructive interleaving counterexample found: BF ~= 8.0
• contradiction with existing passing regression test: BF ~= 0.35
• stuck only on tactic normalization/declaration order: BF ~= 0.2
• stuck at linearization point existence: BF ~= 4.0
• historical match to previously fixed bug family from cass: BF ~= 2.0 to 3.5

Priority:

priority = EV_frog * P_bug_post * AssuranceGapMultiplier

AssuranceGapMultiplier:

• 1.0 for tier A/B already
• 1.4 for tier C target
• 1.8 for tier D/E target

Full scoring details and queue operations: references/FROG-PRIORITY.md

Reverse-Round Card (Mandatory)

For each frog, fill all four fields:

1. Surface: which Rust subsystem/function boundary
2. Failure class: concrete failure mode family
3. Math: theorem family and proof strategy (use router below)
4. Artifact: executable witness (test seed, trace, mapping, proof hash)

No frog proceeds without all 4.

Routing (Expected Loss, Not Vibes)

Classify first hard blocker:

• code-first: likely Rust defect
• model-first: Lean abstraction mismatch
• harness-first: stale tests/mappings/fixtures
• theorem-first: property too strong or mis-scoped

Use the asymmetric loss matrix:

              | code-first | model-first | harness-first |
--------------+------------+-------------+---------------+
code_bug      |     0      |    100      |      80       |
model_issue   |    30      |      0      |      20       |
stale_harness |    20      |     15      |       0       |

Bias toward code-first under uncertainty.

Escalation rule:

• unresolved after two iterations -> split theorem and route separately.

Failure-class strategy router:

• references/LEAN-PATTERNS.md (Failure Class -> Technique Router)
• references/FEEDBACK-EXAMPLES.md (route heuristics and examples)

Stuck-Proof Elicitation (Alien Artifact Mode)

When blocked:

• run the deep-math elicitation prompt from references/FEEDBACK-EXAMPLES.md
• emit a galaxy-brain diagnostic card from the same reference
• continue only after choosing a concrete discriminator action

Conformance and Artifact Closure

Core closure rule:

• theorem not done until statement parity + transition parity + runtime evidence parity pass.

Run the mandatory 7-check pass:

• references/CONFORMANCE-PROCEDURE.md

Assurance ladder target:

• A: invariants + golden checksums
• B: property/fuzz tests with minimized counterexamples
• C: bounded model checking (loom/kani) where feasible
• D: protocol model checks (TLA+/PlusCal or equivalent)
• E: deductive proof (Lean theorem family)

For this skill, target C + E minimum on high-risk frogs.

Artifact contract, hashing, witness, and emission workflow:

• references/PROOF-ARTIFACTS.md
• No artifact record, no formal closure claim.

Budgeted Mode + Fallback Trigger (Graveyard Pattern)

Each loop must declare budgets and an exhaustion action:

• proof iteration budget (default: 2 hard blockers before route split)
• witness search budget (default: 30 minutes targeted extraction)
• conformance rerun budget (default: full 7-check after each route change)

On budget exhaustion:

• split theorem scope (theorem-first) or
• switch route with explicit rationale and updated posterior

Quality Gates

cd /data/projects/asupersync/formal/lean
lake build

cd /data/projects/asupersync
cargo test --test refinement_conformance -- --nocapture
cargo test --test lean_baseline_report
cargo test --test lean_invariant_theorem_test_link_map
cargo check --all-targets
cargo clippy --all-targets -- -D warnings
cargo fmt --check

If Rust changed, run module-targeted tests for touched areas as well.

Full conformance command set:

• references/CONFORMANCE-PROCEDURE.md

Troubleshooting Quick Map

Use:

• references/FEEDBACK-EXAMPLES.md for symptom -> route mapping and stuck-proof cards
• references/LEAN-PATTERNS.md for theorem and modeling strategy patterns

Anti-Patterns

• proving easy lemmas first to inflate theorem count
• declaring "verified" without tier + artifacts
• treating every proof failure as a tactic problem
• skipping witness extraction from stuck proofs
• updating Lean without rerunning conformance tests
• closing beads/issues without proof-carrying record
• changing multiple levers in one loop iteration
• claiming alignment without posterior/routing rationale

Reference Router

Reference Index

• Frog ranking and live queue: references/FROG-PRIORITY.md
• Conformance protocol and routing matrix: references/CONFORMANCE-PROCEDURE.md
• Concrete proof-failure -> bug examples: references/FEEDBACK-EXAMPLES.md
• Lean modeling/proof patterns for this codebase: references/LEAN-PATTERNS.md
• Proof-carrying artifact spec and workflow: references/PROOF-ARTIFACTS.md