proofs: commence AffineScript alignment (Phase 1 — proof foundation) by hyperpolymath · Pull Request #53 · hyperpolymath/betlang

hyperpolymath · 2026-06-02T12:05:49Z

Goal

Bring BetLang from where it is today to the same engineering position the AffineScript estate occupies — starting with proofs, as requested. This PR establishes the standing plan and commences Phase 1.

Where AffineScript is vs. where BetLang was

I examined hyperpolymath/affinescript (+ affinescript-vite, affinescriptiser). Finding: BetLang is ahead on proof content and behind on proof infrastructure.

AffineScript's solo-core Idris2 is statements-only (progress/preservation with ?todo holes, derivations scheduled weeks 3–12).
BetLang's proofs/BetLang.lean already proves Progress + Preservation + the distribution monad laws, with 0 sorry and exactly 1 classified necessary axiom (substTop_preserves_typing, already triaged in docs/proof-debt.adoc).

What BetLang lacked was the AffineScript-standard scaffold and enforcement around that content: a buildable/CI-checked proof project, the multi-prover verification/proofs layout, a PROOF-STATUS.md, a banned-pattern gate, and just proof-check-* recipes.

What this PR does (Phase 1 — proof foundation)

Without touching proofs/BetLang.lean:

lakefile.lean + lean-toolchain — the existing Lean 4 formalisation becomes a buildable Lake package (pure-core, no Mathlib).
.github/workflows/proofs.yml — CI machine-checks the proofs (lake build) and runs a banned-pattern gate on every push/PR. A green build is the machine-checked proof.
tools/proof-scan.sh — comment-aware scanner for banned soundness escape hatches (sorry/admit/Admitted/postulate/believe_me/assert_total/unsafeCoerce). Interim portable stand-in for panic-attack assail --proofs-only. The single classified axiom is permitted per standards#203.
Justfile — proof-check-lean4, proof-scan, proof-check-all.
PROOF-STATUS.md (new) + PROOF-NEEDS.md (restructured) — obligation register + live completion table, aligned to the AffineScript format. Current: 3/13 proven (23%).
verification/ — add the four RSR pillars BetLang lacked (simulations, coverage, traceability, safety_case) with AI manifests + READMEs, plus the pillar manifest and an updated index. (The proofs/tests/conformance/benchmarks/fuzzing symlinks already existed.)
docs/AFFINESCRIPT-ALIGNMENT.adoc (new) — gap analysis + the phased plan.

The plan (in place)

Phase	Focus
1 (this PR)	Make existing proofs machine-checked, standardised, governed
2	Discharge `substTop_preserves_typing` → axiom-free core; continuous measure semantics; mechanise max-entropy & SLLN statements
3	Multi-prover: Idris2 ABI/FFI proofs (Rust/Julia boundary), TLA+ concurrency spec
4	Fill remaining RSR pillars (coverage, simulations, traceability, safety_case)
5	Adopt `panic-attack --proofs-only`; cross-link into `.machine_readable/STATE.scm`; paper

Verification note

⚠️ No Lean toolchain was available in the build container, so lake build was not run locally — the new proofs.yml job is what will machine-check it. I pinned leanprover/lean4:v4.15.0; if the proof file needs a different version, CI will surface it and it's a one-line change. The banned-pattern scanner was run locally (11 proof files, clean — no false positives on the "no sorry" comments).

https://claude.ai/code/session_01NGKc4681nuptfQADqreAfc

Generated by Claude Code

github-actions · 2026-06-02T12:06:43Z

🔍 Hypatia Security Scan

Findings: 135 issues detected

Severity	Count
🔴 Critical	8
🟠 High	18
🟡 Medium	109

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Merge artifact in root",
    "type": "stale",
    "file": "SPEC.core.scm.orig",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in comprehensive-quality.yml",
    "type": "missing_timeout_minutes",
    "file": "comprehensive-quality.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-02T12:09:57Z

🔍 Hypatia Security Scan

Findings: 133 issues detected

Severity	Count
🔴 Critical	8
🟠 High	18
🟡 Medium	107

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Merge artifact in root",
    "type": "stale",
    "file": "SPEC.core.scm.orig",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in comprehensive-quality.yml",
    "type": "missing_timeout_minutes",
    "file": "comprehensive-quality.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Bring BetLang's verification posture toward the AffineScript estate's RSR standard, starting with proofs. BetLang already has strong proof *content* (Lean 4 Progress + Preservation + monad laws, 0 sorry, 1 classified axiom) but lacked the *infrastructure* to machine-check and govern it. This change adds, without touching proofs/BetLang.lean: - lakefile.lean + lean-toolchain: the existing Lean 4 formalisation is now a buildable Lake package (pure-core, no Mathlib). - .github/workflows/proofs.yml: CI machine-checks the proofs (lake build) and runs a banned-pattern gate on every push/PR. - tools/proof-scan.sh: comment-aware scanner for banned soundness escape hatches (sorry/admit/Admitted/postulate/believe_me/assert_total/ unsafeCoerce); shared by CI and `just`. - Justfile: proof-check-lean4, proof-scan, proof-check-all recipes. - PROOF-STATUS.md (new) + PROOF-NEEDS.md (restructured): proof obligation register and live completion table, aligned to the AffineScript format. - verification/: add the four RSR pillars BetLang lacked (simulations, coverage, traceability, safety_case) with AI manifests + READMEs, plus the pillar manifest and an updated index. - docs/AFFINESCRIPT-ALIGNMENT.adoc (new): gap analysis and the phased plan (Phase 1 here; Phases 2-5 cover axiom discharge, continuous semantics, multi-prover ABI/FFI proofs, and the remaining pillars). https://claude.ai/code/session_01NGKc4681nuptfQADqreAfc

https://claude.ai/code/session_01NGKc4681nuptfQADqreAfc

github-actions · 2026-06-02T17:59:49Z

🔍 Hypatia Security Scan

Findings: 63 issues detected

Severity	Count
🔴 Critical	8
🟠 High	15
🟡 Medium	40

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in spark-theatre-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "spark-theatre-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…rack, SPDX, license badge Reconcile docs to the axiom-free reality. substTop_preserves_typing is a proved theorem (proofs/BetLang.lean:918), verified by `lake build`; zero `axiom` declarations remain. Six artefacts still called it a live axiom: - docs/proof-debt.adoc: move substTop from §(c) NECESSARY AXIOM to §(a) DISCHARGED; marker count 1 -> 0. - PROOF-STATUS.md: TP-4 -> Done; axiom-free note; banned-patterns wording. - PROOF-NEEDS.md: TP-4 status -> done. - .machine_readable/6a2/STATE.a2ml: M4 done; axioms=[]; remaining 10->9; drop already-merged-PR (#53/#54/#55) next-actions. - README.md / README.adoc / EXPLAINME.adoc: "one permitted axiom" -> axiom-free. Untrack build rot + tidy: - remove 8 stale *.bak.20250719-182140 backups. - untrack 321 Gleam build artefacts under lsp/bet-lsp/build/ (already gitignored). - remove broken root symlink SPEC.core.scm (target migrated .scm -> .a2ml). - gitignore lake-manifest.json (zero-dep project; regenerated on every build). Conformance: - add SPDX headers to core/betlang.rkt, lib/ternary.rkt, repl/shell.rkt, tests/basics.rkt (Mustfile requires SPDX on .rkt). - drop redundant/incorrect PMPL-1.0 license badge (LICENSE + SPDX = MPL-2.0). Verified: `lake build` green (Lean v4.15.0), tools/proof-scan.sh clean, working tree clean. No Lean sources changed. https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku

hyperpolymath mentioned this pull request Jun 2, 2026

chore(governance): clear pre-existing CI/governance debt #54

Merged

hyperpolymath marked this pull request as ready for review June 2, 2026 13:00

hyperpolymath enabled auto-merge (squash) June 2, 2026 13:00

hyperpolymath mentioned this pull request Jun 2, 2026

feat(types,docs): Echo types in type checker + comprehensive documentation pass #55

Merged

claude added 2 commits June 2, 2026 17:49

ci(proofs): add timeout-minutes to proof jobs (workflow_audit hygiene)

67f8725

https://claude.ai/code/session_01NGKc4681nuptfQADqreAfc

hyperpolymath force-pushed the claude/affinescript-betlang-alignment-Lwvm3 branch from 762b72e to 67f8725 Compare June 2, 2026 17:50

hyperpolymath merged commit bd4a599 into main Jun 2, 2026
31 of 34 checks passed

hyperpolymath deleted the claude/affinescript-betlang-alignment-Lwvm3 branch June 2, 2026 18:25

hyperpolymath mentioned this pull request Jun 5, 2026

chore(betlang): housekeeping — axiom-free docs, rot untrack, SPDX, license badge #57

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

proofs: commence AffineScript alignment (Phase 1 — proof foundation)#53

proofs: commence AffineScript alignment (Phase 1 — proof foundation)#53
hyperpolymath merged 2 commits into
mainfrom
claude/affinescript-betlang-alignment-Lwvm3

hyperpolymath commented Jun 2, 2026

Uh oh!

github-actions Bot commented Jun 2, 2026

Uh oh!

github-actions Bot commented Jun 2, 2026

Uh oh!

github-actions Bot commented Jun 2, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 2, 2026

Goal

Where AffineScript is vs. where BetLang was

What this PR does (Phase 1 — proof foundation)

The plan (in place)

Verification note

Uh oh!

github-actions Bot commented Jun 2, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 2, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 2, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants