docs(lessons): publish proof-engineering lessons from standards#134 session (Refs standards#134)

[hyperpolymath]

Summary

A single day's work under standards#124 (estate proof-debt epic) surfaced four recurring failure modes in proof-bearing code. This PR publishes them in both human-readable (asciidoc session report) and machine-readable (.a2ml) form so future humans and AI agents won't have to re-learn them.

The four lessons

ID	Title	Bit us where
build-is-the-only-oracle	In-file proof-status comments are NOT authoritative	formal/Semantics.v L3328 'FULLY CLOSED' lie → PR#87 propagated into ROADMAP+PROOF-NEEDS; .machine_readable/6a2/STATE.a2ml claimed '67 Qed, 0 Admitted' — also false
vacuous-wrapper-theorems	A theorem can be vacuous — check the body, not the header	src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract body is = ne; noGCExtract body is = (ne, lc). ROADMAP cited them as "complete" — overstated
coq-show-existentials-recipe	Show. Show Existentials. is the precise diagnostic	formal/Semantics.v::preservation had 910 open goals when in-file comment claimed "only ONE remains"
induction-doesnt-substitute-outer-slots	Standard remember (cfg) as cfg eqn:Hcfg fix for preservation proofs	910 → 29 (97%) via the right pattern after the anti-pattern remember e_typed failed

What's added

• docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc (human-readable, 318 lines). Follows the existing SESSION-*.adoc convention in docs/sessions/. Each lesson has: the pattern (with code), where it bit us (with file:line citations), the recipe (do / don't), and cross-references to the PRs that fixed it.

• .machine_readable/agent_instructions/lessons.a2ml (machine-readable, 196 lines). Read at session start by any AI agent touching formal-verification code. Each lesson is a [[lesson]] block with: id (kebab-case slug), title, severity, applies-to language list, pattern, bit-us-where, do, dont, fixed-by-pr, and cross-references to relevant memory files via related-memory.

Cross-references

• formal/PRESERVATION-HANDOFF.md (PR#102) — per-case checklist using the lesson-4 fix.
• RUST-SPARK-STANCE.adoc § Honest gaps (PR#95) — lesson-2 examples flagged at seam level.
• .machine_readable/agent_instructions/methodology.a2ml — the existing agent-methodology file; lessons.a2ml is its failure-catalogue sibling.

Refs

Refs standards#134 (NOT Closes — joint-close on agreement).

Test plan

• No source files touched — pure documentation
• Asciidoc syntax matches existing SESSION-*.adoc files
• .a2ml syntax matches existing agent_instructions/*.a2ml files
• CI green (governance + workflow security linter; no Rust/Coq jobs apply)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	7
🟠 High	6
🟡 Medium	17

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (1 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (2 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "from_raw constructs types from raw pointers without safety checks (1 occurrences, CWE-676)",
    "type": "from_raw",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence