From aeb2f72ced823d90182a56bcf7f066bd7e7f1bed Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:36:59 +0100 Subject: [PATCH 1/2] docs: write up current state for humans and machines; make the golden path real MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The README documented `just build` / `just test` as the quickstart, but the Justfile was PARSE-DEAD — a `//` C-style comment on line 2 made `just` reject the whole file (`error: unknown start of token '.'`), so no recipe was reachable; and every recipe was an `@echo` stub anyway. `just verify` checked a `.machine_read/` path that has never existed and swallowed failures with `||`, so it always claimed success. Justfile: real cargo recipes (build/test/lint/fmt/check/proofs/pipeline), split `-all` variants for the LLVM-dependent crate, and a `verify` that exits non-zero when a path is missing. Parse- and run-verified: `just build` exits 0, `just test` reports 221 passing / 0 failing. STATE.a2ml (machines): version 0.1.0 -> 0.2.0 to match Cargo.toml; current session + maintenance status; a new [security-posture] section distinguishing EXPIRING baseline debt from PERMANENT scoped exemptions, with the three active exemptions and their rule-precision rationale, plus upstream rule-fix candidates; a [toolchain] section; the my-llvm/LLVM-21 local limitation recorded so a bare workspace build failure is not misread as a regression; and the dialect model corrected from four co-equal surfaces to solo ⊂ duet ⊂ ensemble with me as an outside projector. README (humans): quickstart now matches reality incl. the my-llvm caveat; dialect containment; measured test count (137+ -> 221); governance/security posture; `.machine_readable/` and `_exploratory/` documented, and the `contractiles/` path corrected (it is not at the repo root). CHANGELOG: Security / Fixed / Changed entries for #143, #146, #147. Co-Authored-By: Claude Fable 5 --- .machine_readable/6a2/STATE.a2ml | 80 +++++++++++++++++++++++----- CHANGELOG.md | 40 ++++++++++++++ Justfile | 89 +++++++++++++++++++++++--------- README.md | 36 +++++++++++-- 4 files changed, 202 insertions(+), 43 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a819a098..4584e354 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -4,20 +4,34 @@ # STATE.a2ml — My Lang project state [metadata] project = "my-lang" -version = "0.1.0" -last-updated = "2026-06-14" +version = "0.2.0" # matches Cargo.toml [workspace.package] +last-updated = "2026-07-27" status = "active" -session = "Coq solo-core: R2–R5b (SEMIRING functor / affine_pres / Tropical / usage-walk checker / aff_type_dec) + M1 me→solo elaboration + structure climb S1.0–S3c.3-msg (session-π: subject reduction, fidelity, progress, duet-by-projection, n-party projection totality, static n-party config, label-union merge, union-projection, n-ary located operational semantics, head-coupled message subject reduction = first earned n-party safety half) + E4 residue-measure SEAM (Coq mirror) — all axiom-free, CI-gated — 2026-06-14" +session = "CI/CD + supply-chain close-out (PRs #143/#146/#147): codeql-action repointed off a NONEXISTENT SHA; all 15 Hypatia findings triaged (8 fixed at source incl. a self-referential critical, 7 baselined to 2026-10-27 under issue #145); unsafe_block ruled unsatisfiable and scoped-exempted; GitHub Pages un-stuck (workflow was disabled_manually) and LIVE; ARCHITECTURE.md + Justfile de-boilerplated. main FULLY GREEN — 2026-07-27" +prior-session = "Coq solo-core: R2–R5b (SEMIRING functor / affine_pres / Tropical / usage-walk checker / aff_type_dec) + M1 me→solo elaboration + structure climb S1.0–S3c.3-msg (session-π: subject reduction, fidelity, progress, duet-by-projection, n-party projection totality, static n-party config, label-union merge, union-projection, n-ary located operational semantics, head-coupled message subject reduction = first earned n-party safety half) + E4 residue-measure SEAM (Coq mirror) — all axiom-free, CI-gated — 2026-06-14" [project-context] name = "My Lang" purpose = """ Multi-dialect programming language with QTT (Quantitative Type Theory) semantic -core. Four dialects: solo (affine, single-agent), duet (session-typed, two-party), -ensemble (multi-agent), me (block/visual/pedagogic). Formal verification — -mechanised Coq + Idris2 solo-core — is a first-class deliverable alongside the -Rust compiler implementation. +core. Formal verification — mechanised Coq + Idris2 solo-core — is a first-class +deliverable alongside the Rust compiler implementation. """ +# CORRECTION (2026-07-27): the dialects are NOT four co-equal surfaces. They are +# three NESTED SUBSETS plus a projector that sits outside the hierarchy: +# solo ⊂ duet ⊂ ensemble +# solo = innermost kernel (affine, single-agent) +# duet = solo + session-typed two-party (mechanised as ensemble|2-party by projection) +# ensemble= duet + multi-agent (session-typed π-calculus core) = the full language +# me = NOT a fourth dialect; an on-the-fly projector that cuts the hierarchy +# at a chosen point. Its Rust scaffolding is SIDELINED in +# _exploratory/me-scaffolding/ and is not in the Cargo workspace. +# Consequence for audits: grade the layered stack, not three standalone compilers. +# A broken solo breaks duet and ensemble by transitivity. +dialect-model = "nested-subsets" +dialects-ordered = ["solo", "duet", "ensemble"] +dialect-projector = "me" +architecture-doc = "ARCHITECTURE.md" completion-percentage = 50 [position] @@ -88,8 +102,10 @@ issues = [ { id = "product-elim", description = "RESOLVED (F1.4): additive & (projections) + multiplicative ⊗ (let-pair elim) both coherent; preservation proved sound over the open-term substitution lemma ht_subst.", severity = "resolved" }, { id = "typeck", description = "Solo dialect affine type-checker is TODO(#typeck) — mechanised solo-core (check / check_correct, R5) leads the implementation and is its spec; a hand-written Rust checker is tested against, not Coq-proved equal to, check", severity = "high" }, { id = "proof-ci", description = "RESOLVED (F5): .github/workflows/proofs.yml compiles the Coq solo-core + idris2 --build and asserts Print Assumptions closed per rung", severity = "resolved" }, - { id = "hypatia-reusable-timeout", description = "UPSTREAM/STANDARDS: Hypatia workflow_audit/missing_timeout_minutes fires on reusable-workflow CALLER jobs (governance/hypatia-scan/mirror/scorecard/secret-scanner/spark-theatre-gate all `uses:` hyperpolymath/standards). timeout-minutes is invalid on `uses:` jobs — real fix belongs in the standards reusable workflows + Hypatia should exempt caller jobs. Not fixable in my-lang.", severity = "medium" }, - { id = "expect-hot-path", description = "Hypatia code_safety/expect_in_hot_path: parser.rs (157), lib/common/string.rs (1), examples/measure_depth.rs (2). CWE-754 — replace expect() with recoverable errors in shipped hot paths.", severity = "medium" }, + { id = "hypatia-reusable-timeout", description = "UPSTREAM/STANDARDS (issue #95): Hypatia workflow_audit/missing_timeout_minutes fired on reusable-workflow CALLER jobs. MEASURED 2026-07-27: no longer reproduces — the current governance scan returns zero workflow_audit findings (PR #134 dropped the invalid timeout-minutes keys that were making those files parse-dead; wrappers are SHA-pinned). Kept open as the upstream tracker only.", severity = "low" }, + { id = "expect-hot-path", description = "SUPERSEDED by panic-surface (below). The parser.rs x157 count was a SCANNER FALSE POSITIVE — a name collision with the parser's own `self.expect(TokenKind) -> Result` method, not Option/Result::expect panics. Issue #94 closed as consolidated into #145.", severity = "resolved" }, + { id = "panic-surface", description = "Hypatia code_safety unwrap/expect debt, BASELINED not fixed (7 entries in .hypatia-baseline.json, expire 2026-10-27, tracked in issue #145): my-fmt x26 unwrap (infallible fmt::Write-to-String), my-llvm x3 unwrap (internal MIR invariants), my-mir x5 + string.rs x1 + measure_depth.rs x2 expect (deliberate invariant style), parser.rs x157 (scanner FP), modules.md SD022 (illustrative user-project layout). Revisit before the expiry or the gate re-reds.", severity = "medium", tracking = "hyperpolymath/my-lang#145" }, + { id = "justfile-parse-dead", description = "RESOLVED 2026-07-27: the Justfile carried a `// Owner:` C-style comment on line 2, so `just` refused the WHOLE file (`error: unknown start of token '.'`) and every recipe was unavailable — while README documented `just build` / `just test` as the golden path. Recipes were also `@echo` stubs. Now real cargo commands, parse-verified. ESTATE-WIDE: 143 of 751 Justfiles measured parse-dead (76x unindented shell `-`, 35x `//` comment, 32x Justfile/justfile case collision).", severity = "resolved" }, ] [critical-next-actions] @@ -100,11 +116,47 @@ actions = [ { priority = 4, description = "Echo parser syntax stage 2: Echo B> surface syntax in solo dialect", estimate = "4-6 hours" }, ] +[security-posture] +# Added 2026-07-27. How this repo's scanner findings are dispositioned, so an +# agent can tell "clean" from "suppressed" without re-deriving it. +hypatia-baseline = ".hypatia-baseline.json" +hypatia-baseline-entries = 7 +hypatia-baseline-expires = "2026-10-27" +hypatia-baseline-tracking = "hyperpolymath/my-lang#145" +hypatia-baseline-schema = "array of {severity, rule_module, type, file|file_pattern, note?, expires_at?, tracking_issue?}; validated by hyperpolymath/standards scripts/apply-baseline.sh" +hypatia-ignore = ".hypatia-ignore" +# Scoped exemptions live in .hypatia-ignore (PERMANENT facts) rather than the +# baseline (EXPIRING debt). Three are active, each a rule-precision problem: +exemptions = [ + { rule = "code_safety/coq_axiom", file = "proofs/verification/coq/solo-core/ResourceAlgebra.v", reason = "keyword-matches `Axiom` without distinguishing a Module Type field from a top-level Axiom; the development is axiom-free in the kernel sense (Print Assumptions closed)" }, + { rule = "code_safety/transmute", file = "crates/my-llvm/src/lib.rs", reason = "keyword-matches the WORD transmute, which appears only inside a SAFETY comment; no mem::transmute call exists" }, + { rule = "code_safety/unsafe_block", file = "crates/my-llvm/src/lib.rs", reason = "UNSATISFIABLE RULE: a bare `unsafe\\s*\\{` regex (hypatia lib/rules/code_safety.ex) — the 'requires SAFETY comment' in its description is never checked, so no documentation can clear it. The single unsafe block is mandated by inkwell's unsafe build_gep and carries a 17-line invariant argument." }, +] +# Upstream rule-fix candidates surfaced by the 2026-07-27 triage: +upstream-rule-fixes = [ + "code_safety/expect_in_hot_path: disambiguate a user-defined `self.expect(..) -> Result` method from the panicking Option/Result::expect (157 false hits here)", + "code_safety/unsafe_block: actually check for an adjacent SAFETY comment, per the rule's own description", + "security_errors/secret_detected: an exemption file's own explanatory comment should not re-trigger the assignment-shape matcher (this produced the only critical)", +] +secret-scanning = "gitleaks (Secret Scanner workflow) + trufflehog (just secret-scan-trufflehog); no live credentials known in tree or history" + +[toolchain] +rust = "1.97.0" # mise.toml + .tool-versions +llvm = "21" # my-llvm only, via LLVM_SYS_211_PREFIX; excluded from default build/test and from coverage CI +coq = "distro (apt) — see proofs.yml" +idris2 = "built from source in CI — see proofs.yml" +task-runner = "just (Justfile); parse-verified 2026-07-27" + [maintenance-status] -last-run-utc = "2026-06-05T14:01:00Z" +last-run-utc = "2026-07-27T18:15:00Z" last-result = "pass" -ci-governance = "pass" -ci-security-scan = "pass" -ci-rust-tests = "pass" -ci-pr = "PR #92 — all 18 checks green (governance, scans, SPARK, Hypatia success, CodeQL neutral)" +main-commit = "8636e15" +main-board = "FULLY GREEN — every workflow on main succeeds or is deliberately skipped" +ci-governance = "pass" # incl. Validate Hypatia Baseline, green for the first time since >=2026-07-22 +ci-security-scan = "pass" # Hypatia Security Scan + Secret Scanner + CodeQL + Scorecard +ci-rust-tests = "pass" # Coverage (llvm-cov, floor 40%) +ci-pages = "pass" # https://hyperpolymath.github.io/my-lang/ returns HTTP 200 +ci-pr = "PRs #143/#146/#147 merged 2026-07-27; no open PRs" proof-build = "pass — coqc 10/10 solo-core modules (Quantity, EchoMode, ResourceAlgebra, SoloCore, Tropical, Context, ContextProps, EchoResidue, EchoMeasure, SessionPi; local full clean rebuild 2026-06-14); idris2 --build OK; all per-rung Print Assumptions closed (R-ladder, M1, S1.0–S3c.3-msg, E4)" +known-local-limitation = "my-llvm cannot be built in the maintainer's WSL environment (no system LLVM 21). `cargo build --workspace` FAILS there; `--exclude my-llvm` succeeds. Do not read a bare workspace build failure as a regression without checking for the llvm-sys compile_error." +superseded-branch = "origin/feat/stdlib-fs-env-format — SUPERSEDED, safe to delete: main carries every builtin it adds PLUS fs_list_dir, its stdlib.rs is 355 lines behind, it conflicts on stdlib.rs + CONTRIBUTING.md, and it is 188 commits behind main" diff --git a/CHANGELOG.md b/CHANGELOG.md index 0b396d46..f47c912d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,46 @@ this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Security + +- fix(hypatia): triage all 15 findings — 8 fixed at source, 7 baselined (#146). + The **critical** was self-referential: `.hypatia-ignore`'s own comment + explaining the API-key false positive itself matched the secret detector's + `KEY="..."` assignment shape. Also fixed two genuine empty-name panics in + `my-lint`, a guarded `unwrap` in `my-hir`, and five stale directory + references in docs/config. Remaining debt is baselined to 2026-10-27 under + #145, validated against standards' own `apply-baseline.sh` before merge. +- fix(hypatia): scoped exemption for the unsatisfiable `unsafe_block` rule + (#147). The rule is a bare `unsafe\s*\{` regex — its "requires SAFETY + comment" is never checked — so it belongs in `.hypatia-ignore` as a + permanent fact, not in the baseline as expiring debt. +- fix(ci): repoint `github/codeql-action` off a **nonexistent SHA** (#143). + The pin `29b1f65c` does not exist upstream; an unresolvable `uses:` pin + produces a startup failure with *no check run at all*, so it is invisible + to `gh pr checks`. Now pinned to `4187e74d` (v3.37.3), API-verified. + +### Fixed + +- fix(just): the `Justfile` was **parse-dead**. A `//` C-style comment on line + 2 made `just` reject the entire file (`error: unknown start of token '.'`), + so every recipe was unavailable — while `README.md` documented `just build` + / `just test` as the golden path. Recipes were also `@echo` stubs. They are + now real `cargo` commands, and `just verify` checks paths that actually + exist instead of swallowing every failure with `||`. + +### Changed + +- docs: `ARCHITECTURE.md` replaced mint-time boilerplate (which described + `src/`, `config/` and `scripts/` directories that do not exist) with the + real 15-crate workspace layout, the `solo ⊂ duet ⊂ ensemble` containment + hierarchy (with `me` as a projector outside it), and the CI gate map. +- docs: `README.md` and `.machine_readable/6a2/STATE.a2ml` now record the + dialects as nested subsets rather than four co-equal surfaces, and carry a + security-posture section distinguishing expiring baseline debt from + permanent scoped exemptions. +- chore: `mise.toml` replaced ~30 tools pinned to `latest` (Node, Go, Zig, + Java… none used here) with a single pinned `rust = "1.97.0"`. + ### Added - test(conformance): run conformance/valid|invalid + examples/*.my fixtures under `cargo test`, with a fail-closed KNOWN_PARSE_GAPS allowlist (#84) diff --git a/Justfile b/Justfile index 91e927b6..3021d908 100644 --- a/Justfile +++ b/Justfile @@ -1,36 +1,75 @@ # SPDX-License-Identifier: MPL-2.0 -// Owner: Jonathan D.A. Jewell -# Justfile - hyperpolymath standard task runner +# Owner: Jonathan D.A. Jewell +# Justfile — hyperpolymath standard task runner +# +# NOTE: every comment here must start with `#`. A `//` C-style comment makes +# the whole file parse-dead (`error: unknown start of token '.'`) and every +# recipe unavailable — which is exactly what happened to this file until +# 2026-07-27, silently breaking the README's documented golden path. +# +# my-llvm needs a system LLVM 21 (LLVM_SYS_211_PREFIX). The default build/test +# recipes exclude it so the golden path works on a clean checkout; use the +# `-all` variants when you have the toolchain. CI does the same (coverage.yml). default: @just --list -# Build the project +# Build the workspace (excludes my-llvm — needs system LLVM 21) build: - @echo "Building..." + cargo build --workspace --exclude my-llvm -# Run tests +# Build everything including the LLVM back end (requires LLVM 21) +build-all: + cargo build --workspace + +# Run unit + conformance tests (excludes my-llvm) test: - @echo "Testing..." + cargo test --workspace --exclude my-llvm + +# Run the full test suite including the LLVM back end (requires LLVM 21) +test-all: + cargo test --workspace # Run lints lint: - @echo "Linting..." - -# Clean build artifacts -clean: - @echo "Cleaning..." + cargo clippy --workspace --exclude my-llvm --all-targets # Format code fmt: - @echo "Formatting..." + cargo fmt --all + +# Check formatting without writing (CI-style) +fmt-check: + cargo fmt --all -- --check + +# Clean build artifacts +clean: + cargo clean # Run all checks -check: lint test +check: fmt-check lint test + +# Machine-check the Coq solo-core (the authoritative proof track) +proofs-coq: + cd proofs/verification/coq/solo-core && \ + coq_makefile -f _CoqProject -o CoqMakefile && \ + make -f CoqMakefile + +# Machine-check the Idris2 solo-core +proofs-idris: + cd proofs/verification/idris/solo-core && idris2 --build solo-core.ipkg + +# Both proof tracks +proofs: proofs-coq proofs-idris + +# End-to-end pipeline smoke test (build -> parse -> interpret an example) +pipeline: + ./test_pipeline.sh # Prepare a release release VERSION: @echo "Releasing {{VERSION}}..." + @echo "Set version = \"{{VERSION}}\" in Cargo.toml [workspace.package] and .machine_readable/6a2/STATE.a2ml, then tag." # Run dialect demos (per golden-path contract) # Usage: just demo [dialect] @@ -67,10 +106,6 @@ demo dialect="all": echo "" echo "Note: Hives are coming soon. Add submodules to ./hives/" echo "" - # When hives are available, iterate: - # for d in me solo duet ensemble; do - # run_demo "$d" || true - # done echo "Run 'just demo ' once hives are installed." echo "Dialects: me, solo, duet, ensemble" else @@ -81,14 +116,20 @@ demo dialect="all": init: git submodule update --init --recursive -# Verify playground health +# (The previous version checked a `.machine_read/` path that has never existed +# and swallowed every failure with `||`, so it always reported success.) +# Verify repository structure — exits non-zero when something is missing verify: - @echo "Verifying playground structure..." - @test -d .machine_read && echo "[OK] .machine_read/ exists" || echo "[FAIL] .machine_read/ missing" - @test -f .machine_read/ANCHOR.scm && echo "[OK] ANCHOR.scm exists" || echo "[FAIL] ANCHOR.scm missing" - @test -f .machine_read/SPEC.playground.scm && echo "[OK] SPEC.playground.scm exists" || echo "[FAIL] SPEC.playground.scm missing" - @test -d hives && echo "[OK] hives/ exists" || echo "[FAIL] hives/ missing" - @echo "Verification complete." + #!/usr/bin/env bash + set -uo pipefail + fail=0 + for p in .machine_readable .machine_readable/6a2/STATE.a2ml \ + .hypatia-baseline.json .hypatia-ignore \ + proofs/STATUS.md Cargo.toml; do + if [[ -e "$p" ]]; then echo "[OK] $p" + else echo "[FAIL] $p missing"; fail=1; fi + done + exit "$fail" # Run panic-attacker pre-commit scan assail: diff --git a/README.md b/README.md index bd8df838..7a1a81a5 100644 --- a/README.md +++ b/README.md @@ -18,13 +18,14 @@ For a gentler entry point see [EXPLAINME.adoc](EXPLAINME.adoc). | Path | Contents | |------|----------| | `crates/` | Rust compiler crates. `crates/my-lang/src/types.rs` is the type checker, including `EchoMode`, `Ty::Echo`, and full affine-weakening semantics. | -| `dialects/` | Per-dialect surface-syntax definitions: *solo* (affine, single-agent), *duet* (session-typed), *ensemble* (multi-agent), *me* (visual/pedagogic). | +| `dialects/` | Per-dialect surface-syntax definitions. The dialects are **nested subsets, not four co-equal languages**: `solo` (affine, single-agent) ⊂ `duet` (session-typed, two-party) ⊂ `ensemble` (multi-agent) — the full language. `me` (visual/pedagogic) is **not** a fourth dialect but an on-the-fly *projector* that cuts the hierarchy at a chosen point; its Rust scaffolding is sidelined in `_exploratory/me-scaffolding/`. Audit the layered stack, not three standalone compilers — a broken `solo` breaks the other two by transitivity. See [ARCHITECTURE.md](ARCHITECTURE.md). | | `proofs/` | Formal verification assets — paper proofs, mechanised Coq + Idris2 solo-core. See [`proofs/STATUS.md`](proofs/STATUS.md) for the authoritative proof-status registry. | | `conformance/` | Conformance tests — programs any compliant implementation must accept or reject identically. | | `examples/` | Worked examples for each dialect. | | `docs/` | Design notes, ADRs. Includes the [echo-types integration design note](docs/design/echo-types-integration.md). | | `frontier-practices/` | Forward-looking research experiments (not shipped). | -| `contractiles/` | Project-level Mustfile / Dustfile invariant and recovery contracts. | +| `.machine_readable/` | Machine-facing state. `6a2/STATE.a2ml` is the authoritative project-state file for agents; `contractiles/` holds the Mustfile / Dustfile invariant and recovery contracts. | +| `_exploratory/` | Sidelined scaffolding, **not** in the Cargo workspace (currently `me-scaffolding/`). | ## Quickstart @@ -32,10 +33,18 @@ For a gentler entry point see [EXPLAINME.adoc](EXPLAINME.adoc). git clone git@github.com:hyperpolymath/my-lang.git cd my-lang -just build # builds the workspace (Rust) +just # list every recipe +just build # builds the workspace (Rust), excluding my-llvm just test # runs unit + conformance tests +just check # fmt-check + lint + test ``` +`build` and `test` exclude the `my-llvm` crate, which needs a system LLVM 21 +(`LLVM_SYS_211_PREFIX`); without it `cargo build --workspace` fails with an +`llvm-sys` `compile_error!` that is **not** a regression. Use `just build-all` +/ `just test-all` when you have the toolchain — CI makes the same split +(`coverage.yml` excludes `my-llvm` to stay hermetic). + To check the Coq solo-core: ```bash @@ -108,9 +117,26 @@ Consult these before opening a feature request. ## Status - **Licence**: MPL-2.0 -- **Maturity**: design-iteration / early alpha. Working Rust compiler core exists (137+ passing tests); surface syntax and semantics still settling. +- **Maturity**: design-iteration / early alpha. Working Rust compiler core + exists — **221 tests pass, 0 failures** (`just test`, measured 2026-07-27, + excluding `my-llvm`); surface syntax and semantics still settling. - **Proof phase**: F1.4 done on the Coq track — QTT semiring + `progress` + `preservation` machine-checked (axiom-free, CI-guarded); Idris twin pending (Phase F5 parity). **R2 done**: the Coq solo core is now one functor `SoloCoreF (M : SEMIRING)` parametric over a resource-algebra interface — `Include SoloCoreF Linear3` recovers the axiom-free result, and tropical/affine instances fall out (**R4 done**: `SoloCoreF Tropical` is verified axiom-free at an *infinite* min-plus carrier). **R3 done**: `affine_pres` is now a *distinct* theorem — affine budget-preservation over `ule` (pointwise `qle`), not an alias of `preservation` — with the functor parameter widened to `ORDERED_SEMIRING`. **R5 done (F1.4 tail)**: the declarative static context-splitting judgement is proved equivalent to an *executable* one-pass usage-walk checker `check` — `check_correct : has_type G D t a ↔ check G t = Some (a, D)` is axiom-free `Qed.`, the spec for the Rust `dialects/solo` checker; it inherits to the infinite tropical carrier for free and **overtakes AffineScript** (which leaves this equivalence as prose "future work"). **M1.0/M1.1/M1.1b done (2026-06-14)**: the visual `me` surface now elaborates into the solo core (`elab`, a core-landing analogue of the paper `translate`) with a machine-checked, axiom-free Visual-Soundness theorem (`elab_data_check`) for the **no-linear-use data fragment** — and **M1.1b** a me typing judgement (`me_wt`/`me_wt_sound`) making the linear-use constructs (token-consume, `MeLet`, pair-split, the faithful `MeIf → Case`) universal over the whole `me_tm` (incl. `MeSeq`) — M1 complete. For that fragment it is the first mechanised surface→core elaboration correctness in either sibling, as surveyed against AS@main 2026-06-02 (axis-4 SURFACE rung M1). **S1 + S2 done (2026-06-14)**: the *structure climb* (axis-2) is mechanised in the standalone Coq development `SessionPi.v` — a synchronous binary session-typed π-calculus core (session types + computed duality, polarised endpoints, a linear channel-typing judgement, small-step reduction) with **subject reduction** (`sr_comm`, `config_subject_reduction`), **session fidelity** (`session_fidelity`) and **progress / deadlock-freedom** (`config_progress`) for the binary fragment (**S1.0–S1.2**), and the **duet-by-projection** layer (**S2.0/S2.1**) — multiparty-shaped global types, the three-case projection, `projection_duality`, and corollaries that transport the whole S1 guarantee across projection so a projected choreography is deadlock-free by construction — all axiom-free and CI-guarded. **S1.3 done (2026-06-14)**: n-ary labelled **choice** (S1.3a, the three fused theorems extended), structural **congruence** preserves typing (S1.3c, `wt_congr`), and the equi-recursive **μ type-layer** (S1.3b-core: `unfold_mu`/`dual_unfold`/`guarded`). **S2.2 done (2026-06-14)**: global-type labelled **choice** (`GBra`) + equi-recursive (`GMu`/`GVar`) projection — projection is now **partial** (`option sty`) with a plain **`merge`** (keystone `merge_idem`) for uninvolved roles and `projection_duality` reproved in option-map form over choice + μ; fenced as plain (not union) merge, unpruned μ, no global-level metatheory. **S3a done (2026-06-14)**: the first n≥3 theorem — `projection_total` (every role of a `projectable_wf` global type projects), breaking the "no theorem quantifies over a genuine n-party system" fence. **S3b done (2026-06-14)**: the first n-party *configuration* form — `role_assignment` + the In-based `wf_assignment`, the binary `Conf` recovered as the **n=2 slice** (`conf_is_role_assignment2`, reusing `projected_config_wf`), an n=3 non-`Conf` witness over `g_ring`, and honesty witnesses (duplicate keys; projectable-but-uncoverable); static only — `wf_assignment` = typed-at-projection NOT n-party safety. **S3c.0 done (2026-06-14)**: the full label-union merge `umerge` (keystone `umerge_idem`) added alongside the plain merge — type-algebra only, unlocks different-label `&` choices (not the different-payload class). **S3c.1 done (2026-06-14)**: a SEPARATE union-projection `proj_u` (the only token changed from `proj` is `merge`→`umerge` in the uninvolved fold) + `projectable_u_wf` + the keystone existence theorem `projection_total_u` + the one-directional monotonicity bridge `projectable_wf_implies_u` (on the keystone `merge_forces_eq`: plain merge is the identity-meet); canonical `proj` byte-identical, projection-EXISTENCE only, non-vacuity `g_union3` genuinely in *union-projectable minus plain-projectable*. **S3c.2 done (2026-06-14)**: the first operational metatheory over an n-party config — a located reduction `nstep` (located mirror of the fused `cstep`) + `ra_set` + a global `gstep` + `nstar`/`gstar` + the functional `wf_assignment_f` (`wf_assignment_to_f` keeps S3b green); the 3-party ring run witnessed both sides (`ring_runs_to_end`, `g_ring_gsteps`); adequacy ONLY — `nstep_breaks_wf_at_fixed_G` proves no fixed-`G` subject reduction. **S3c.3-msg done (2026-06-14)**: the first EARNED n-party safety half — `nstep_sr_msg_head` (head-coupled message subject reduction, 3-way located role split), coupled corollary `nstep_gstep_sr_msg_head`, the earned-safety headline `sr_earns_safety_across_step` (the same `ra_ring1` S3c.2 refuted at the fixed g is wf at the stepped g), and the self-witnessed run-ahead fence `runahead_breaks_head_coupling`; adversary-verified sound-and-honest. Remaining: μ typing/SR up-to-unfolding (**S1.3b-meta**, deferred), select SR (**S3c.3-choice**), run-ahead SR (**S3c.3-perm**), n-party progress (**S3c.4**). A greenfield overtake — AS has no concurrency/session/π/multiparty metatheory in any form (surveyed AS@main 2026-06-02). -- **Governance**: CI green on all shipped checks; proof CI **live** (`proofs.yml` machine-checks the solo-cores). +- **Governance** *(measured 2026-07-27, commit `8636e15`)*: **main is fully + green** — every workflow succeeds or is deliberately skipped. Proof CI is + **live** (`proofs.yml` machine-checks both solo-cores and asserts the + theorems axiom-free via `Print Assumptions`). Docs deploy to + [GitHub Pages](https://hyperpolymath.github.io/my-lang/). +- **Security posture**: scanner findings are dispositioned in two places, and + the distinction matters — `.hypatia-baseline.json` holds **expiring debt** + (7 entries, expire 2026-10-27, tracked in + [#145](https://github.com/hyperpolymath/my-lang/issues/145)), while + `.hypatia-ignore` holds **permanent scoped exemptions** for rules that + cannot be satisfied (a keyword-matching `coq_axiom`, a keyword-matching + `transmute`, and `unsafe_block` — a bare `unsafe\s*\{` regex whose + "requires SAFETY comment" is never actually checked). See + `[security-posture]` in + [`.machine_readable/6a2/STATE.a2ml`](.machine_readable/6a2/STATE.a2ml) for + the machine-readable version. ## Contributing From 8edb9ba96b2202422ae2e33b784dbb02aa19a5b4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 12 Aug 2026 18:14:58 +0100 Subject: [PATCH 2/2] fix(ci): remove timeout-minutes from job using reusable workflow Files fixed: - .github/workflows/governance.yml Related: hyperpolymath/standards#426 Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- frontier-practices/.github/workflows/governance.yml | 1 - playground/.github/workflows/governance.yml | 1 - 2 files changed, 2 deletions(-) diff --git a/frontier-practices/.github/workflows/governance.yml b/frontier-practices/.github/workflows/governance.yml index 60e8e904..6f0afb7e 100644 --- a/frontier-practices/.github/workflows/governance.yml +++ b/frontier-practices/.github/workflows/governance.yml @@ -21,4 +21,3 @@ permissions: jobs: governance: uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613 - timeout-minutes: 10 diff --git a/playground/.github/workflows/governance.yml b/playground/.github/workflows/governance.yml index 60e8e904..6f0afb7e 100644 --- a/playground/.github/workflows/governance.yml +++ b/playground/.github/workflows/governance.yml @@ -21,4 +21,3 @@ permissions: jobs: governance: uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613 - timeout-minutes: 10