You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs: state write-up for humans and machines; make the golden path real (#148)
Closes out the my-lang session by recording current state in-repo (not
only in dev-notes) and fixing the documentation defects found while
doing it.
## The Justfile was parse-dead
`README.md` documented `just build` / `just test` as the quickstart.
Neither worked: a `//` C-style comment on line 2 made `just` reject the
**entire file** (`error: unknown start of token '.'`), so no recipe was
reachable — and every recipe was an `@echo` stub regardless. `just
verify` checked `.machine_read/` (a path that has never existed) and
swallowed every failure with `||`, so it always reported success.
Now: real cargo recipes, `-all` variants for the LLVM-dependent crate,
and a `verify` that exits non-zero. **Verified by running them** — `just
build` exits 0; `just test` reports **221 passing, 0 failing**.
*(Estate note: 143 of 751 Justfiles across the estate are parse-dead by
the same class of defect — 76× unindented shell blocks, 35× `//`
comments, 32× `Justfile`/`justfile` case collisions. Out of scope here;
recorded in dev-notes.)*
## For machines — `.machine_readable/6a2/STATE.a2ml`
- version `0.1.0` → `0.2.0` (was drifting from `Cargo.toml`)
- new `[security-posture]`: distinguishes **expiring baseline debt** (7
entries → 2026-10-27, #145) from **permanent scoped exemptions** (3,
each a rule-precision problem), plus upstream rule-fix candidates
- new `[toolchain]`; `known-local-limitation` records that `my-llvm`
needs system LLVM 21, so a bare workspace build failure is not misread
as a regression
- dialect model corrected: **solo ⊂ duet ⊂ ensemble**, with `me` an
outside projector — not four co-equal surfaces
- `superseded-branch` records the evidence that
`feat/stdlib-fs-env-format` is safe to delete
## For humans — README + CHANGELOG
Quickstart matches reality (incl. the my-llvm caveat); dialect
containment; measured test count (137+ → 221); governance/security
posture; `contractiles/` path corrected (it is under
`.machine_readable/`, not the repo root). CHANGELOG gains
Security/Fixed/Changed entries for #143, #146, #147.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
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"
Multi-dialect programming language with QTT (Quantitative Type Theory) semantic
16
-
core. Four dialects: solo (affine, single-agent), duet (session-typed, two-party),
17
-
ensemble (multi-agent), me (block/visual/pedagogic). Formal verification —
18
-
mechanised Coq + Idris2 solo-core — is a first-class deliverable alongside the
19
-
Rust compiler implementation.
17
+
core. Formal verification — mechanised Coq + Idris2 solo-core — is a first-class
18
+
deliverable alongside the Rust compiler implementation.
20
19
"""
20
+
# CORRECTION (2026-07-27): the dialects are NOT four co-equal surfaces. They are
21
+
# three NESTED SUBSETS plus a projector that sits outside the hierarchy:
22
+
# solo ⊂ duet ⊂ ensemble
23
+
# solo = innermost kernel (affine, single-agent)
24
+
# duet = solo + session-typed two-party (mechanised as ensemble|2-party by projection)
25
+
# ensemble= duet + multi-agent (session-typed π-calculus core) = the full language
26
+
# me = NOT a fourth dialect; an on-the-fly projector that cuts the hierarchy
27
+
# at a chosen point. Its Rust scaffolding is SIDELINED in
28
+
# _exploratory/me-scaffolding/ and is not in the Cargo workspace.
29
+
# Consequence for audits: grade the layered stack, not three standalone compilers.
30
+
# A broken solo breaks duet and ensemble by transitivity.
31
+
dialect-model = "nested-subsets"
32
+
dialects-ordered = ["solo", "duet", "ensemble"]
33
+
dialect-projector = "me"
34
+
architecture-doc = "ARCHITECTURE.md"
21
35
completion-percentage = 50
22
36
23
37
[position]
@@ -88,8 +102,10 @@ issues = [
88
102
{ 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" },
89
103
{ 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" },
90
104
{ 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" },
91
-
{ 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" },
92
-
{ 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" },
105
+
{ 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" },
106
+
{ 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" },
107
+
{ 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" },
108
+
{ 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" },
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"
127
+
hypatia-ignore = ".hypatia-ignore"
128
+
# Scoped exemptions live in .hypatia-ignore (PERMANENT facts) rather than the
129
+
# baseline (EXPIRING debt). Three are active, each a rule-precision problem:
130
+
exemptions = [
131
+
{ 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)" },
132
+
{ 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" },
133
+
{ 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." },
134
+
]
135
+
# Upstream rule-fix candidates surfaced by the 2026-07-27 triage:
136
+
upstream-rule-fixes = [
137
+
"code_safety/expect_in_hot_path: disambiguate a user-defined `self.expect(..) -> Result` method from the panicking Option/Result::expect (157 false hits here)",
138
+
"code_safety/unsafe_block: actually check for an adjacent SAFETY comment, per the rule's own description",
139
+
"security_errors/secret_detected: an exemption file's own explanatory comment should not re-trigger the assignment-shape matcher (this produced the only critical)",
140
+
]
141
+
secret-scanning = "gitleaks (Secret Scanner workflow) + trufflehog (just secret-scan-trufflehog); no live credentials known in tree or history"
142
+
143
+
[toolchain]
144
+
rust = "1.97.0" # mise.toml + .tool-versions
145
+
llvm = "21" # my-llvm only, via LLVM_SYS_211_PREFIX; excluded from default build/test and from coverage CI
146
+
coq = "distro (apt) — see proofs.yml"
147
+
idris2 = "built from source in CI — see proofs.yml"
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."
162
+
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"
0 commit comments