Repair Lean proof suite + make Echo Types a structural typesystem gate by hyperpolymath · Pull Request #26 · hyperpolymath/jtv-lang

hyperpolymath · 2026-06-03T17:47:39Z

Summary

Two related pieces of work on JtV's proofs and the Echo-Types feature of the type system.

1. Lean 4 proof suite — repair + close the orphan gap (`8a82e97`)

Under the pinned leanprover/lean4:v4.12.0 toolchain, lake build did not succeed, and the apex module JtvExtended.lean was orphaned — absent from lakefile.lean, so lake build never checked it, despite verification/PROOF-CAPABILITY-MATRIX.adoc listing it as verified.

JtvEcho.neg_injective — after intro a b h, h keeps its un-beta-reduced form (fun n => -n) a = (fun n => -n) b, so rw [h] couldn't match the goal - -a = - -b. Coerced h to its beta-reduced form (defeq) and closed with omega.
JtvExtended.lean (never compiled against v4.12.0): replaced the Mathlib-only ring with omega; added missing omega discharges (sub_eq_add_neg, simplify_add_neg_self); dropped a redundant omega after a closing simp; converted four dangling /-- … -/ doc comments (attached to no declaration — hard parse errors that cascaded) to /- … -/; fixed the invalid (eval e σ; σ) sandbox field to (eval e σ, σ).2 = σ; data_is_sandboxed theorem → def (it's a Type); spelled dead_code_elim's congruence with explicit semanticEquiv (the ≃ infix mis-parses there); rebuilt groundEquivDecidable on the real evalDataExpr _ State.empty value.
lakefile.lean — added lean_lib JtvExtended and wired it into the JtvAll default target, so the apex module is now verified by lake build / the proof-regression workflow.

lake build is green from a clean tree (all 10 targets, cold); the sorry/admit/axiom-free invariant holds across all eight libraries.

2. Echo Types as a structural, uniform typesystem gate (`ebc37b9`)

The Echo lattice (crates/jtv-core/src/echo.rs) gated only reverse { … }, with one pre-existing bug and one gap:

The gate ran after per-statement type inference, so an unbound/ill-typed variable masked the Echo violation behind a type error. This is why test_reverse_block_rejects_breaking_echo was failing on the baseline (reverse { x += x } errored as UndefinedVariable, not the asserted EchoViolation). Echo classification is purely structural, so the gate now runs first and fires regardless of type bindings.
ControlStmt::ReversibleBlock (the v2 reversible { … } -> tok form, whose recorded log is later inverted by reverse tok) skipped the Echo gate entirely. It now enforces the same Safe-only rule.

Also corrected the stale doc comment (policy is Safe-only — both EchoNeutral and EchoBreaking are rejected) and added test_reversible_block_{rejects_breaking,accepts_safe}_echo.

cargo test -p jtv-core is now fully green (97 lib + all integration suites); the previously-failing reverse-block Echo test passes. The Lean model (JtvEcho.lean, blockEcho_admissible) is unchanged and remains the source of truth for this gate.

Verification

cd jtv_proofs && lake build → green (cold, 10 targets), 0 sorry/admit/axiom.
cargo test -p jtv-core → all suites pass (lib 97/0; harvard_boundary 35; reversibility 7+5; mutation_killers 156; …).

Notes / not done

The Idris2 ABI half of proof-regression.yml (src/abi/Types.idr) was not re-verified locally (it needs the heavy idris2-pack/Chez bootstrap); Types.idr is %default total type definitions and untouched here.
Widening Echo into a first-class effect on every function signature was deliberately not attempted — it would ripple through the parser/grammar/serialization. The gate is integrated where reversibility/loss actually matters in the type system (both reverse forms).

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

Generated by Claude Code

… build The Lean 4 proof suite (jtv_proofs/) did not compile under the pinned v4.12.0 toolchain, and the apex module JtvExtended.lean was orphaned — absent from lakefile.lean, so `lake build` never checked it, despite verification/PROOF-CAPABILITY-MATRIX.adoc listing it as `verified`. Fixes: * JtvEcho.neg_injective: after `intro a b h`, `h` keeps its un-beta-reduced form `(fun n => -n) a = (fun n => -n) b`, so `rw [h]` could not match the goal `- -a = - -b`. Coerce `h` to its beta-reduced form (defeq) and close with `omega`. * JtvExtended.lean (never compiled against v4.12.0): - replace the Mathlib-only `ring` with `omega` (Lean core has no Mathlib here); - add the missing `omega` discharges to `sub_eq_add_neg` and `simplify_add_neg_self`; - drop the redundant `omega` after a closing `simp` in `neg_subexpr_size_lt` (use `simp only … ; omega`); - convert four dangling `/-- … -/` doc comments (attached to no declaration) to plain `/- … -/` block comments — these were hard parse errors that cascaded spurious failures downstream; - `DataSandbox.noStateMod`: replace the invalid term `(eval e σ; σ)` with `(eval e σ, σ).2 = σ` (Data eval is a read-only function); - `data_is_sandboxed`: `theorem` → `def` (DataSandbox is a Type, a record of proofs, not a Prop); - `dead_code_elim`: spell the congruence hypothesis with explicit `semanticEquiv` (the `≃` infix mis-parses in that higher-order position); - `groundEquivDecidable`: rebuild on the real value `evalDataExpr _ State.empty` (the previous `have v := …` lost the definitional link, leaving the iff unprovable). * lakefile.lean: add `lean_lib JtvExtended` and include it in the `JtvAll` default target so the apex module is verified by `lake build` and the proof-regression workflow. `lake build` is green from a clean tree (all 10 targets, cold); the sorry/admit/axiom-free invariant holds across all eight libraries. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

…rsibility Echo Types were modelled in `crates/jtv-core/src/echo.rs` and gated only the `reverse { … }` form, with one pre-existing bug and one gap: * The Echo admissibility check ran AFTER per-statement type inference, so an unbound/ill-typed variable masked the Echo violation behind a type error. This is why `test_reverse_block_rejects_breaking_echo` was *failing* on the baseline: `reverse { x += x }` (x unbound) errored as `UndefinedVariable` rather than the asserted `EchoViolation`. Echo classification is purely structural (does the target appear in the expression?), so the gate now runs FIRST and the violation is reported regardless of type bindings. * `ControlStmt::ReversibleBlock` (the v2 `reversible { … } -> tok` form, which records a reversal log later inverted by `reverse tok`) skipped the Echo gate entirely. It now enforces the same Safe-only admissibility rule — an irreversible body (e.g. `y += y`) can't produce a soundly-invertible log. Changes: * typechecker.rs: gate both `ReverseBlock` and `ReversibleBlock` on `check_echo_admissible`, checked structurally and before type inference; correct the stale doc comment (the policy is Safe-only — `EchoNeutral` and `EchoBreaking` are both rejected, not just `EchoBreaking`). * Add `test_reversible_block_{rejects_breaking,accepts_safe}_echo` mirroring the reverse-block tests. * PROOF-CAPABILITY-MATRIX.adoc: record that the gate covers both reversibility forms and is structural/first. `cargo test -p jtv-core` is now fully green (97 lib + all integration suites); the previously-failing reverse-block Echo test passes. The Lean model (`jtv_proofs/JtvEcho.lean`, `blockEcho_admissible`) is unchanged and remains the source of truth for this gate. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-03T17:48:35Z

🔍 Hypatia Security Scan

Findings: 106 issues detected

Severity	Count
🔴 Critical	13
🟠 High	19
🟡 Medium	74

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action tions/upload-artifact@v4\n  needs attention",
    "type": "unpinned_action",
    "file": "coverage.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "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": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "proof-regression.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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 coverage.yml",
    "type": "missing_timeout_minutes",
    "file": "coverage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in deno.yml",
    "type": "missing_timeout_minutes",
    "file": "deno.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Clears the failing `governance / Workflow security linter` check and the Hypatia `missing_timeout_minutes` / `unpinned_action` (medium) findings — all on workflow files this branch had not otherwise touched. * coverage.yml: pin `actions/upload-artifact@v4` to its commit SHA (`ea165f8d65b6e75b540449e92b4886f43607fa02`), matching the repo's existing pin-everything convention. This is the one finding that actually failed the security linter. * Add `timeout-minutes` to every normal (`runs-on`) job that lacked one: cflite_batch (60, ≥ its 1800s fuzz budget), cflite_pr (20), codeql (30), coverage (45), deno (15), dogfood-gate (20 ×5), the SLSA generator's build job (20), jekyll-gh-pages (20 ×2), language-policy (15 ×2), rust-ci (30 ×2). Deliberately NOT changed (would be unsound or out of this scope): * Jobs that *call* reusable workflows (governance, mirror, hypatia-scan, scorecard, and the SLSA provenance job) — `timeout-minutes` is not valid on a reusable-workflow-call job, so adding it would break them. * proof-regression.yml already sets per-job timeouts. * The `download_then_run` (toolchain `curl | sh`) and the `governance-reusable.yml@main` ref are higher-effort / possibly intentional; left for a dedicated governance pass. Verified: the linter's own checks pass locally (no unpinned actions; SPDX + permissions present on all workflows) and every workflow still parses as valid YAML. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-03T17:57:29Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	13
🟠 High	19
🟡 Medium	56

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "proof-regression.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in generator-generic-ossf-slsa3-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "generator-generic-ossf-slsa3-publish.yml",
    "action": "flag",
    "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 scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

… failure) `rust-ci.yml` and `coverage.yml` gated their jobs with `if: hashFiles('Cargo.toml') != ''` at the JOB level. `hashFiles()` is not a valid function in a job-level `if:`, so GitHub rejected the whole workflow at validation time: Unrecognized function: 'hashFiles'. Located at position 1 within expression: hashFiles('Cargo.toml') != '' The result was a *startup failure with zero jobs scheduled* — so Rust CI (build / fmt / clippy / test, 3-OS matrix) and Coverage have not actually run on any push since at least 2026-05-27. Every `Rust CI` run on `main` is a 0-job `failure`. (This is the exact gotcha already documented in proof-regression.yml, which guards in a post-checkout step instead.) Fixes, at root: * Remove the invalid job-level guards from both workflows (this repo is unconditionally a Cargo workspace, so no guard is needed) and add a comment so the broken pattern is not reintroduced. * `echo.rs`: clear the one `clippy::cloned_ref_to_slice_refs` lint (`&[safe.clone()]` → `std::slice::from_ref(&safe)`) that `clippy -D warnings` flags — previously invisible because the `check` job never ran. * `.gitattributes`: pin `*.jtv` / `*.pata` to `eol=lf`. The conformance corpus (57 `.jtv` files) is parsed byte-exactly; pinning LF keeps the Windows leg of the now-live matrix reading identical bytes (CRLF would otherwise fail conformance tests only on Windows). Verified locally (Linux): `cargo fmt --all --check`, `cargo check --all-targets`, `cargo clippy --all-targets -- -D warnings`, and `cargo test --all-targets` all pass; the workflows parse as valid YAML and still satisfy the governance linter (SHA-pinned actions, SPDX, permissions). https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-03T21:40:20Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	13
🟠 High	19
🟡 Medium	56

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "proof-regression.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in generator-generic-ossf-slsa3-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "generator-generic-ossf-slsa3-publish.yml",
    "action": "flag",
    "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 scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

## Why An honest inventory of the Lean suite (`jtv_proofs/`) found that, although it is `sorry`/`admit`/`axiom`-free and `lake build`-green, **eight theorems were laundering unproven claims through a `True` statement** — they compiled while asserting nothing. Two of them (`string_not_executable`, `confluence`) were even labelled `verified` in `PROOF-CAPABILITY-MATRIX.adoc`. The `no-sorry` invariant is honest about the *kernel* but said nothing about *vacuity*. This PR closes that gap: every believeme becomes a real statement with a real, compiled proof, and the matrix gains a **NO-VACUITY invariant** plus an honest **Int-only semantic-scope** note. ## The eight, before → after | Theorem | Now proves (real) | |---|---| | `string_not_executable` | Data is inert: `∃ n : Int, evalDataExpr e σ = n` (value, never a `ControlStmt`) | | `no_vulnerable_constructs` | structural induction `e.isInert = true` over the actual `DataExpr` constructors (adds `DataExpr.isInert`) | | `no_reverse_joinpoints` | `∀ fl ∈ s.flows, fl = dataToControl` — every flow is Data→Control (stronger than "no controlToData") | | `data_evaluation_secure` | `∃ n : Int, evalDataExpr e σ = n` (terminates in a value) | | `dataExpr_no_control` | `∃ n : Int, evalDataExpr e σ = n` (eval lands in `Int`, disjoint from `ControlStmt`) | | `confluence` | determinism ⇒ confluence | | `control_data_noninterference` | `free_vars_sufficient` corollary — Control affects Data only via assigned state variables | | `rev_composition` | the Safe reversal round-trip `execBackward (addAssign x e) (execForward … σ) x = σ x` for `x ∉ e.freeVars` (subtraction = the *generated* inverse, never a primitive) | These rest on theorems that were already genuinely proved (`dataExpr_totality`, `free_vars_sufficient`, `rev_forward_backward`, `ControlStmt.flows`), so the new content is sound, not aspirational. ## Honesty recorded in the matrix - **NO-VACUITY invariant** (`grep ':\s*True\s*:='` ⇒ 0) alongside the existing no-`sorry` one. - **Semantic scope**: `evalDataExpr` is `Int`-only; the seven number systems are *typed* (`JtvType` + typing rules) but their evaluation is `stated-unproven`, and `type_preservation` is mechanised only for `τ = int`. (Orthogonal to v2 — Echo is representation-agnostic.) ## Verification `cd jtv_proofs && lake build` green from a clean tree (all 10 targets, cold); `grep -rEc 'sorry|admit|axiom'` ⇒ 0; `grep -rE ':\s*True\s*:='` ⇒ 0. ## Context Follow-up to #26 (merged). The injection-impossibility story is unchanged and now better-supported: it rests on the genuinely-real `no_control_to_data_flow` + the disjoint `DataExpr`/`ControlStmt` types + data-inertness — not on the vacuous theorems, which never carried it. Next planned step remains **(c)**, the token/residue neutral-reversal bridge. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- _Generated by [Claude Code](https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742)_ Co-authored-by: Claude <noreply@anthropic.com>

… STATE refresh Durable capture of the 2026-06 design basis so it survives context loss. * docs/design-decisions/0007-…: records the core mandates re-affirmed in the 2026-06 sessions — - D1 addition-only is absolute (no ×, no primitive −; ×/÷ generated, not Data primitives); - D2 subtraction = REVERSE addition (not twos-complement, not a primitive) — flags the open `DataExpr.neg`-as-primitive tension; - D3 Turing-completeness via a Harvard block embedded in a von-Neumann host, both graftable as AOLD aspects (universal extender); - D4 computation = shortest-path-to-equality with Echo recording lineage (incl. cross-number-system routing); - D5 reversal is a fallback ladder: algorithmic (Safe) → residue/token (Neutral, Bennett) → Breaking; - D6 the additive algebra of a number system fixes its Echo tier: group→Safe, cancellative monoid→Neutral, idempotent monoid→Breaking (Echo's own join is idempotent — why Breaking is one-way; answers "a number system with no subtraction at all" = idempotent semirings). * .machine_readable/6a2/STATE.a2ml: reflect PR #26 (Lean repair + Echo structural type-system gate + root-cause Rust-CI revival), PR #27 (de-vacuation of 8 True-typed believeme theorems), ADR-0007, the reordered next-actions (governance hardening → number-system semantics → v2 (c) bridge → (b)), and the Int-only semantic-scope gap. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

claude added 2 commits June 3, 2026 17:38

hyperpolymath marked this pull request as ready for review June 3, 2026 19:58

hyperpolymath enabled auto-merge (squash) June 3, 2026 20:03

hyperpolymath disabled auto-merge June 3, 2026 23:32

hyperpolymath enabled auto-merge (squash) June 3, 2026 23:38

hyperpolymath disabled auto-merge June 4, 2026 01:06

hyperpolymath merged commit f53071f into main Jun 4, 2026
31 checks passed

hyperpolymath deleted the claude/dazzling-albattani-ubS9r branch June 4, 2026 01:06

hyperpolymath mentioned this pull request Jun 4, 2026

Proof honesty: de-vacuate 8 True-typed believeme theorems #27

Merged

hyperpolymath mentioned this pull request Jun 13, 2026

Checkpoint: ADR-0007 addition-only mandate + Echo reversibility tiering, STATE refresh #29

Merged

hyperpolymath mentioned this pull request Jun 15, 2026

Bookkeeping & tidying: lint-clean proofs, license hygiene, branch consolidation, ADR note #33

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Repair Lean proof suite + make Echo Types a structural typesystem gate#26

Repair Lean proof suite + make Echo Types a structural typesystem gate#26
hyperpolymath merged 4 commits into
mainfrom
claude/dazzling-albattani-ubS9r

hyperpolymath commented Jun 3, 2026

Uh oh!

github-actions Bot commented Jun 3, 2026

Uh oh!

github-actions Bot commented Jun 3, 2026

Uh oh!

github-actions Bot commented Jun 3, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 3, 2026

Summary

1. Lean 4 proof suite — repair + close the orphan gap (8a82e97)

2. Echo Types as a structural, uniform typesystem gate (ebc37b9)

Verification

Notes / not done

Uh oh!

github-actions Bot commented Jun 3, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 3, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 3, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

1. Lean 4 proof suite — repair + close the orphan gap (`8a82e97`)

2. Echo Types as a structural, uniform typesystem gate (`ebc37b9`)