Merge pull request #175 from link-foundation/issue-97-2fa46f510db9

Author: konard

docs/DIAGNOSTICS.md

@@ -103,8 +103,12 @@ The exit code is `1` whenever any diagnostic is emitted, `0` otherwise.
 | `E041` | Domain plugin error. Triggered by a malformed `(domain <name> ...)` block, an unknown domain plugin, or an unsupported request inside a registered domain plugin such as `automatic-sequences`. |
 | `E050` | Lean export error. Triggered when `rml export lean` sees forms outside the typed non-probabilistic subset, such as `has probability`, range/valence configuration, operator redefinitions, imports, namespaces, or templates. |
 | `E060` | Malformed `(root-construct …)` declaration. Triggered by a missing or non-symbolic name, an unrecognised child clause shape, or a non-symbolic value where a status / kind / dependency name is expected. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
-| `E061` | Malformed `(foundation …)` declaration. Triggered by a missing name, an unrecognised child clause shape, or a malformed `(defines <op> <aggregator>)` / `(extends …)` / `(numeric-domain …)` / `(truth-domain …)` clause. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
+| `E061` | Malformed `(foundation …)` declaration. Triggered by a missing name, an unrecognised child clause shape, or a malformed `(defines <op> <aggregator>)` / `(extends …)` / `(numeric-domain …)` / `(truth-domain …)` / `(carrier …)` / `(truth-table …)` clause. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
 | `E062` | `(with-foundation <name> …)` references a foundation that has not been registered. Evaluation skips the body but continues with the surrounding forms; the active foundation remains the previously-active one. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
+| `E063` | Carrier violation under `(strict-carrier)`. A probability assignment or query result fell outside the active foundation's declared carrier. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
+| `E064` | Proof-substrate error. Triggered by malformed proof rules, assumptions, proof objects, `(check-proof …)` forms, premise/rule/conclusion mismatches, unjustified raw premises, or cyclic proof dependencies. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
+| `E065` | Pure-links strict-mode error. Triggered by malformed `(strict-foundation …)` / `(allow-host-primitive …)` forms or by a query whose transitive dependency path reaches an unallowed `host-primitive` / `host-derived` construct. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
+| `E066` | MTC/anum encode/decode error. Triggered by non-`Node` encode inputs, characters outside the four-abit alphabet, unbalanced frames, malformed frame tags, or byte-unaligned leaf payloads. See [`FOUNDATIONS.md`](./FOUNDATIONS.md). |
 
 Codes are stable identifiers — they do not change between releases unless we
 explicitly note a breaking change in the changelog. The accompanying

docs/FOUNDATIONS.md

@@ -0,0 +1 @@
+{"baseRefName":"main","body":"## 🤖 AI-Powered Solution Draft\n\nThis pull request is being automatically generated to solve issue #97.\n\n### 📋 Issue Reference\nFixes #97\n\n### 🚧 Status\n**Work in Progress** - The AI assistant is currently analyzing and implementing the solution draft.\n\n### 📝 Implementation Details\n_Details will be added as the solution draft is developed..._\n\n---\n*This PR was created automatically by the AI issue solver*","headRefName":"issue-97-2fa46f510db9","number":175,"state":"OPEN","title":"[WIP] Use similar idea, but everything should be built from links and references","url":"https://github.com/link-foundation/relative-meta-logic/pull/175"}

docs/case-studies/issue-97/README.md

@@ -200,8 +200,40 @@ remain captured in `docs/case-studies/issue-171/data/recommendations.md`.
 
 The CI workflow already runs `npm test` and `cargo test` on every push
 and PR; this can be confirmed by viewing recent runs of the `tests`
-workflow on the `issue-97-bbe597194dee` branch. The eight new JS
-tests in `foundations.test.mjs` and the eight new Rust tests in
-`foundations_tests.rs`, plus the extended self-evaluator coverage,
-all execute under the existing `tests` workflow. No additional
-workflow changes are needed for issue #97.
+workflow on the `issue-97-2fa46f510db9` branch. The extended JS
+coverage in `foundations.test.mjs`, `proof-substrate.test.mjs`, and
+`pure-links-strict.test.mjs`, plus the mirrored Rust coverage and
+self-evaluator checks, all execute under the existing `tests`
+workflow. No additional workflow changes are needed for issue #97.
+
+### 8.1 Phase 2–9 follow-up coverage (PR #175)
+
+The subsequent phases that landed on PR #175 add the following test
+files to the same suite — no workflow changes required:
+
+| Phase | JS test file | Rust test file |
+|-------|--------------|----------------|
+| 2 — equality provenance | `js/tests/foundations.test.mjs` (extended) | `rust/tests/foundations_tests.rs` (extended) |
+| 3 — proof-object replay | `js/tests/proof-substrate.test.mjs` | `rust/tests/proof_substrate_tests.rs` |
+| 4 — links-defined truth tables | `js/tests/foundations.test.mjs` (extended) | `rust/tests/foundations_tests.rs` (extended) |
+| 5 — links-defined typed-kernel fragment | `js/tests/typed-kernel-links.test.mjs` | `rust/tests/typed_kernel_links_tests.rs` |
+| 6 — pure-links strict mode | `js/tests/pure-links-strict.test.mjs` | `rust/tests/pure_links_strict_tests.rs` |
+| 7 — dependency-graph traversal | `js/tests/dependency-graph.test.mjs` | `rust/tests/dependency_graph_tests.rs` |
+| 8 — carrier enforcement | `js/tests/foundations.test.mjs` (extended) | `rust/tests/foundations_tests.rs` (extended) |
+| 9 — `mtc-anum` experimental profile + MTC theory fragment + serialization invariants | `js/tests/mtc-anum.test.mjs` (extended) | `rust/tests/mtc_anum_tests.rs` (extended) |
+
+All of these are picked up automatically by `npm test` and
+`cargo test --all-targets`, which the existing `tests.yml` workflow
+already runs on every push and PR.
+
+### 8.2 Re-audit findings (2026-05-16)
+
+A second pass against the four templates (described in this file
+plus a fresh independent review documented in this PR) confirms no
+new gaps were introduced by the Phase 2–9 work. The reportable
+findings remain T-1, T-2, T-3, and the pre-existing CI-debt items
+tracked in `docs/case-studies/issue-171/data/recommendations.md`.
+The pattern of *path-filtered triggers + safer concurrency
+(`!= 'refs/heads/main'`)* this repo has on its `tests.yml` and
+`api-docs.yml` is still ahead of all four templates and is worth
+contributing upstream once the foundation PR has merged.

docs/case-studies/issue-97/data/pr-175.json

@@ -133,7 +133,7 @@ Snapshot-shape tests:
 - Rust — `rust/tests/foundations_tests.rs:172-211`
   (`builds_a_structured_foundation_report_snapshot`).
 
-## R7 — Structured diagnostics E060 / E061 / E062
+## R7 — Structured diagnostics E060 / E061 / E062 and follow-up foundation diagnostics
 
 The codes are emitted at:
 
@@ -155,55 +155,107 @@ Unknown-foundation tests:
 - Rust — `rust/tests/foundations_tests.rs:116-132`
   (`reports_unknown_foundation_as_e062_without_aborting`).
 
-The doc surface — `docs/DIAGNOSTICS.md` — lists E060, E061, E062 as
-new rows in its error code table.
+The doc surface — `docs/DIAGNOSTICS.md` — lists E060 through E066 in
+its error code table. E063 covers strict-carrier failures, E064 covers
+proof-substrate failures, E065 covers pure-links strict-mode failures,
+and E066 covers MTC/anum encode/decode failures.
 
 ## R8 — Self-bootstrap encoding
 
-`lib/self/foundations.lino` declares the registry as data
-(367 lines total, every section commented). `lib/self/evaluator.lino`
-encodes four matching evaluator rules at lines 253-263:
+`lib/self/foundations.lino` declares the registry as data and records
+the bundled foundations, including the finite truth-table
+`boolean-links` profile. `lib/self/evaluator.lino` encodes matching
+data-only evaluator rules for the foundation surface, strict mode,
+proof substrate, and MTC/anum helpers:
 
 ```lino
 (rule (eval (root-construct name details))
-  (register-root-construct name details))
+  (record-root-construct name details))
 
 (rule (eval (foundation name details))
-  (register-foundation name details))
+  (record-foundation name details))
+
+(rule (foundation-clause (carrier values))
+  (record-foundation-carrier values))
+
+(rule (foundation-clause strict-carrier)
+  (record-foundation-strict-carrier))
+
+(rule (foundation-clause (truth-table operator rows))
+  (record-foundation-truth-table operator rows))
+
+(rule (foundation-clause experimental)
+  (record-foundation-experimental))
+
+(rule (foundation-clause (root symbol))
+  (record-foundation-root symbol))
+
+(rule (foundation-clause (abit symbol bits))
+  (record-foundation-abit symbol bits))
 
 (rule (eval (with-foundation name body))
   (evaluate-body-under-foundation name body))
 
 (rule (eval (foundation-report))
-  (query (foundation-report-snapshot)))
+  (emit-foundation-report))
+
+(rule (eval (strict-foundation pure-links))
+  (enable-strict-foundation pure-links))
+
+(rule (eval (allow-host-primitive names))
+  (record-allowed-host-primitives names))
+
+(rule (eval (assumption name (judgement judgement)))
+  (record-proof-assumption name judgement))
+
+(rule (eval (axiom name (judgement judgement)))
+  (record-proof-axiom name judgement))
+
+(rule (eval (proof-object name clauses))
+  (record-proof-object name clauses))
+
+(rule (proof-object-clause (premise-by name))
+  (record-proof-dependency name))
+
+(rule (proof-object-clause (uses names))
+  (record-proof-dependencies names))
+
+(rule (eval (check-proof name))
+  (check-proof-object name))
+
+(rule (eval (encodeAnum node))
+  (encode-anum node))
+
+(rule (eval (decodeAnum payload))
+  (decode-anum payload))
 ```
 
-The Rust self-evaluator parity test requires all four rules to be
+The Rust self-evaluator parity test requires these rules to be
 present in the data file:
-`rust/tests/self_evaluator_tests.rs:11-63` enumerates
-`REQUIRED_EVAL_RULES`, including the four `(eval (root-construct …))`
-/ `(eval (foundation …))` / `(eval (with-foundation …))` /
-`(eval foundation-report)` entries; the assertion is at
-`rust/tests/self_evaluator_tests.rs:143-164`. The JS parity test
-covers the same forms with the `EncodedEvaluator` class which has
-explicit cases for `with-foundation`, `foundation`, and
-`root-construct` at
-`js/tests/self-evaluator.test.mjs:218-243`.
+`rust/tests/self_evaluator_tests.rs` enumerates `REQUIRED_EVAL_RULES`,
+including the foundation, strict-mode, proof, and MTC/anum entries, and
+`REQUIRED_SURFACE_RULES`, including foundation clauses, proof dependency
+clauses, and equality provenance. The JS parity test covers the same
+forms with the `EncodedEvaluator` class, including the bundled
+`boolean-links` truth-table foundation.
 
 ## R9 — Links-defined finite-logic example
 
-Two named alternative foundations ship as data in
+Three named alternative foundations ship as data in
 `lib/self/foundations.lino`:
 
-- `boolean-classical` at `lib/self/foundations.lino:343-351` —
-  two-valued logic, `and=min`, `or=max`, `both=min`,
-  `neither=product`, `(extends default-rml)`.
-- `kleene-three-valued` at `lib/self/foundations.lino:359-367` —
-  Strong Kleene over the real unit interval, same `and`/`or` shape.
-
-A complete end-to-end example uses both inside one file:
-`examples/foundation-boolean-kleene.lino` (46 lines, replayed through
-both engines). A minimal sanity-check example is at
+- `boolean-links` — strict `{0,1}` Boolean logic with finite
+  truth-table rows for `and`, `or`, and `not`. Activating this
+  foundation records those operators as `links-defined`.
+- `boolean-classical` — two-valued logic, `and=min`, `or=max`,
+  `both=min`, `neither=product`, `(extends default-rml)`. These are
+  host aggregator bindings.
+- `kleene-three-valued` — Strong Kleene over the real unit interval,
+  same `and`/`or` shape. These are also host aggregator bindings.
+
+A complete end-to-end example uses all three profiles inside one file:
+`examples/foundation-boolean-kleene.lino` (replayed through both
+engines). A minimal sanity-check example is at
 `examples/foundation-with-min.lino` (16 lines). Both are picked up
 automatically by the shared-example replay
 (`rust/tests/shared_examples.rs`, `js/tests/shared-examples.test.mjs`).