docs(lessons): publish proof-engineering lessons from standards#134 session (Refs standards#134) by hyperpolymath · Pull Request #105 · hyperpolymath/ephapax

hyperpolymath · 2026-05-20T19:00:36Z

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

…ession (Refs standards#134) A single day's work under standards#124 (estate proof-debt epic) surfaced four recurring failure modes in proof-bearing code. This commit publishes them in both human-readable and machine-readable form so future humans and AI agents will know to look for the patterns rather than re-learn them the hard way. The four lessons: 1. **build-is-the-only-oracle** — in-file proof-status comments are NOT authoritative. ephapax/formal/Semantics.v carried "FULLY CLOSED" with Qed.; coqc rejected it. ephapax#87 propagated the lie into ROADMAP+PROOF-NEEDS without running the build. PR#92 + #103 reverted it. 2. **vacuous-wrapper-theorems** — a theorem can be vacuous. Check the BODY, not the header docstring. ephapax/src/formal/Ephapax/ Formal/RegionLinear.idr's `regionSafetyExtract` and `noGCExtract` have bodies `= ne` / `= (ne, lc)` (return inputs unchanged). ROADMAP cited them as 'regionSafetyTheorem' / 'noGCTheorem' complete — overstated. PR#95 flagged honestly in the seam. 3. **coq-show-existentials-recipe** — Show. + Show Existentials. before Admitted. is the precise diagnostic. Don't assume 'one more tactic'. ephapax/formal/Semantics.v::preservation had 910 open goals when the in-file comment claimed 'only ONE remains'. 4. **induction-doesnt-substitute-outer-slots** — for preservation- style proofs, `induction Hstep` leaves the outer expression slot abstract; `inversion Htype` then generates n×m cross-cases instead of n diagonals. Fix is the standard `remember (mu, R, e) as cfg eqn:Hcfg` + `inversion Hcfg; subst` pattern. ephapax#102 used this and reduced 910 → 29 open goals (97%). The anti-pattern `remember e_typed as e_orig eqn:He_orig` from the typing's expression was a misdiagnosis — wrong variable. Files: - `docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc` Human-readable session-report-format doc. Each lesson has: the pattern (with code), where it bit us (with file:line citations), the recipe (do this / don't do that), and cross-references to the PRs that fixed it. Follows the existing SESSION-*.adoc convention in docs/sessions/. - `.machine_readable/agent_instructions/lessons.a2ml` Machine-readable companion. 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 + related-memory list for chained lookups. 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` — existing agent-methodology file; lessons.a2ml is its failure-catalogue sibling. Refs standards#134 (NOT Closes — joint-close on agreement). 🤖 Generated with [Claude Code](https://claude.com/claude-code)

…essons

github-actions · 2026-05-21T18:46:50Z

🔍 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

hyperpolymath added 2 commits May 20, 2026 20:00

Merge branch 'main' into proof-debt/standards-134-proof-engineering-l…

5a8c7ef

…essons

hyperpolymath merged commit 3c02b06 into main May 20, 2026
8 checks passed

hyperpolymath deleted the proof-debt/standards-134-proof-engineering-lessons branch May 20, 2026 20:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

docs(lessons): publish proof-engineering lessons from standards#134 session (Refs standards#134)#105
hyperpolymath merged 2 commits into
mainfrom
proof-debt/standards-134-proof-engineering-lessons

hyperpolymath commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented May 20, 2026

Summary

The four lessons

What's added

Cross-references

Refs

Test plan

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant