cut v0.20.0

.config/nextest.toml

@@ -30,10 +30,26 @@ filter = 'binary(differential) & test(/^gate::/)'
 test-group = 'corpus-compilers'
 slow-timeout = { period = "120s", terminate-after = 64 }
 
+# The tier-equivalence suite is the same shape at five effect-tier positions:
+# the sharded relation lowers and interprets a quarter of the corpus five
+# times, and the generated sweep adds a fuzz corpus on top. Same allowance as
+# the optimizer relation above.
+[[profile.default.overrides]]
+filter = 'binary(differential) & test(/^tier_gate::/)'
+test-group = 'corpus-compilers'
+slow-timeout = { period = "120s", terminate-after = 64 }
+
+# The typed-spine gates compile every corpus program twice, once with Core lint on
+# and once without, then diff the two Core dumps, and the group below pins them to
+# one thread. Measured at 1142s standalone in the debug profile on an M-series
+# laptop against the previous 1920s cap: headroom on a quiet machine, none left
+# once the rest of the suite competes for the cores, which is where it timed out.
+# Same rule as every other entry here: the timeout catches a hang, it does not
+# bound honest work.
 [[profile.default.overrides]]
 filter = 'binary(differential) & test(/^typed_spine::/)'
 test-group = 'corpus-compilers'
-slow-timeout = { period = "120s", terminate-after = 16 }
+slow-timeout = { period = "120s", terminate-after = 32 }
 
 [[profile.default.overrides]]
 filter = 'binary(compiler) & test(core_lint_clean_on_corpus)'
@@ -86,15 +102,31 @@ filter = 'binary(snapshots)'
 test-group = 'snapshot-goldens'
 slow-timeout = { period = "120s", terminate-after = 16 }
 
+# Several of this binary's modules drive the whole compiler over a corpus: the
+# receipt lane encodes every corpus file with the authority parser and re-encodes
+# it with the Prism-implemented one, and the bootstrap lanes compile the
+# compiler's own sources. That is minutes of honest work in the debug profile, and
+# the receipt lane crossed the shared default the first time the rest of the suite
+# competed for the machine while it ran. Same rule as every other entry here: the
+# timeout catches a hang, it does not bound honest work.
+[[profile.default.overrides]]
+filter = 'binary(tooling)'
+slow-timeout = { period = "120s", terminate-after = 16 }
+
 [[profile.ci.overrides]]
 filter = 'binary(differential) & test(/^gate::/)'
 test-group = 'corpus-compilers'
 slow-timeout = { period = "120s", terminate-after = 64 }
 
+[[profile.ci.overrides]]
+filter = 'binary(differential) & test(/^tier_gate::/)'
+test-group = 'corpus-compilers'
+slow-timeout = { period = "120s", terminate-after = 64 }
+
 [[profile.ci.overrides]]
 filter = 'binary(differential) & test(/^typed_spine::/)'
 test-group = 'corpus-compilers'
-slow-timeout = { period = "120s", terminate-after = 16 }
+slow-timeout = { period = "120s", terminate-after = 32 }
 
 [[profile.ci.overrides]]
 filter = 'binary(compiler) & test(core_lint_clean_on_corpus)'
@@ -124,3 +156,7 @@ slow-timeout = { period = "120s", terminate-after = 16 }
 filter = 'binary(snapshots)'
 test-group = 'snapshot-goldens'
 slow-timeout = { period = "120s", terminate-after = 16 }
+
+[[profile.ci.overrides]]
+filter = 'binary(tooling)'
+slow-timeout = { period = "120s", terminate-after = 16 }

.github/actions/setup-llvm/action.yml

@@ -8,8 +8,8 @@ inputs:
   packages:
     description: >
       Extra apt packages beyond the base set (llvm-22-dev, libpolly-22-dev,
-      clang-22), space-separated. e.g. "clang-tidy-22" or "libmlir-22-dev
-      mlir-22-tools".
+      clang-22, lld-22), space-separated. e.g. "clang-tidy-22" or
+      "libmlir-22-dev mlir-22-tools".
     required: false
     default: ""
 
@@ -35,13 +35,22 @@ runs:
     - name: Install LLVM 22 (cached)
       uses: awalsh128/cache-apt-pkgs-action@v1
       with:
-        packages: llvm-22-dev libpolly-22-dev clang-22 ${{ inputs.packages }}
-        version: llvm22
+        packages: llvm-22-dev libpolly-22-dev clang-22 lld-22 ${{ inputs.packages }}
+        # Bumped whenever the base package set changes, so a cache entry resolved
+        # from the old set can never be restored in place of the new one.
+        version: llvm22-lld
 
     # mold is a far faster linker than ld; the compiler links libLLVM on every
     # build, so linking is a real chunk of wall-clock. make-default routes rustc's
     # cc linking through mold with no RUSTFLAGS, so it adds no sccache-key churn.
     # (Pinned to a tag like the action above; pin to a SHA to harden further.)
+    #
+    # make-default replaces the host `ld`, so it would otherwise also link the
+    # binaries prism itself emits. That link runs under ThinLTO, where the
+    # linker is the code generator and decides final layout, and its bytes are
+    # pinned by oracles. lld-22 above is what keeps it on the same LLVM the rest
+    # of the pipeline uses: prism selects it explicitly rather than inheriting
+    # whichever linker happens to own `ld` on the host.
     - name: Install mold linker
       uses: rui314/setup-mold@v1
       with:

.github/workflows/ci.yml

@@ -89,7 +89,10 @@ jobs:
           "$bin" --version
 
   # docs/src cross-references anchors and {{#include}}s by hand; mdbook never
-  # validates either, so a rename or a moved example silently rots a link.
+  # validates either, so a rename or a moved example silently rots a link. Every
+  # other committed Markdown file is checked too, and those are the worse case:
+  # nothing builds them at all, so an index of the tree can point at files that
+  # were renamed away a release ago and still read as current.
   doc-links:
     name: Doc links resolve
     runs-on: ubuntu-latest
@@ -158,8 +161,11 @@ jobs:
           - name: default
             command: cargo check --all-targets
             wasm: false
+          # Lint the browser feature on its real target. A native
+          # `--all-features` run combines the wasm and MLIR/native backends into
+          # a configuration no shipped compiler uses.
           - name: wasm
-            command: cargo check --no-default-features --features wasm --target wasm32-unknown-unknown
+            command: cargo clippy --no-default-features --features wasm --target wasm32-unknown-unknown --lib -- -D warnings
             wasm: true
           - name: mlir
             command: cargo check --features mlir
@@ -384,6 +390,11 @@ jobs:
       # skipped, so a stale cache can never mask a regression.
       PRISM_GATE_CACHE: "1"
       PRISM_GATE_FINGERPRINT: source
+      # Names the solver installed below, so a workflow that stops installing it
+      # fails the solver-accept gate instead of silently skipping it. cvc5 is not
+      # listed: it is not packaged for this runner, so the two-solver agreement
+      # gate stays opt-in for a developer who has one.
+      PRISM_REQUIRE_SOLVERS: z3
     steps:
       - uses: actions/checkout@v7
 
@@ -395,6 +406,12 @@ jobs:
         with:
           prefix-key: "v1-libm"
 
+      # The certificate subsystem mints `prism-smt-certificate-v1` receipts by
+      # discharging obligations through an external solver, so without one
+      # installed its end-to-end path has no CI evidence behind it.
+      - name: Install z3
+        run: sudo apt-get update && sudo apt-get install -y z3
+
       # Per-shard gate-verdict cache: each partition owns a distinct key so the
       # parallel runs do not overwrite each other's snapshots.
       - name: Cache gate verdicts
@@ -436,7 +453,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        oracle: [fusion, tier, optimizer, typed-spine]
+        oracle: [fusion, tier, optimizer, tier-equiv, typed-spine]
         shard: [0, 1, 2, 3]
     env:
       LLVM_SYS_221_PREFIX: /usr/lib/llvm-22
@@ -488,6 +505,10 @@ jobs:
         if: ${{ matrix.oracle == 'optimizer' }}
         run: cargo nextest run --profile ci --test differential -E 'test(optimizer_configurations_have_identical_observation_traces)'
 
+      - name: Tier-equivalence relation (shard ${{ matrix.shard }} of 4)
+        if: ${{ matrix.oracle == 'tier-equiv' }}
+        run: cargo nextest run --profile ci --test differential -E 'test(tier_configurations_have_identical_observation_traces)'
+
       - name: Typed-spine relations (shard ${{ matrix.shard }} of 4)
         if: ${{ matrix.oracle == 'typed-spine' }}
         run: cargo nextest run --profile ci --test differential -E 'test(typed_erasure_preserves_corpus_core_identity) | test(full_front_crosses_typed_newtype_prefix_across_corpus)'
@@ -528,8 +549,8 @@ jobs:
         uses: mozilla-actions/sccache-action@v0.0.10
 
       # The viewer page reads a generated artifact (`prism index`), so the native
-      # binary is needed here, and with it LLVM — the same install the other
-      # compiling jobs share.
+      # binary is needed here, and with it LLVM. The other compiling jobs use the
+      # same installation.
       - name: Install LLVM 22
         uses: ./.github/actions/setup-llvm
 
@@ -628,7 +649,7 @@ jobs:
     steps:
       - uses: actions/checkout@v7
 
-      # Toolchain pinned via rust-toolchain.toml (single source of truth).
+      # Toolchain pinned by rust-toolchain.toml.
       - name: Setup Rust toolchain
         run: rustup show
 
@@ -655,7 +676,7 @@ jobs:
       # progress, effect-safety) and the differential `Certificates` whose `rfl`
       # proofs pin model output to live `prism run` output, and builds the `oracle`
       # executable the differential harness runs. The toolchain is read from
-      # models/lean-toolchain (single source of truth); no mathlib, so the build is
+      # models/lean-toolchain; no mathlib, so the build is
       # self-contained and fast. This is the one formal-methods gate that used to be
       # able to silently break (Lean was outside CI).
       - name: Build Lean model
@@ -713,7 +734,7 @@ jobs:
     steps:
       - uses: actions/checkout@v7
 
-      # Toolchain pinned via rust-toolchain.toml (single source of truth).
+      # Toolchain pinned by rust-toolchain.toml.
       - name: Setup Rust toolchain
         run: rustup show
 
@@ -754,6 +775,13 @@ jobs:
           MLIR_SYS_220_PREFIX: /usr/lib/llvm-22
           TABLEGEN_220_PREFIX: /usr/lib/llvm-22
 
+      - name: Test shared ABI plans with mlir
+        run: cargo test -p prism-native --features mlir codegen::abi::tests
+        env:
+          LLVM_SYS_221_PREFIX: /usr/lib/llvm-22
+          MLIR_SYS_220_PREFIX: /usr/lib/llvm-22
+          TABLEGEN_220_PREFIX: /usr/lib/llvm-22
+
       - name: Run mlir parity test
         run: PATH=/usr/lib/llvm-22/bin:$PATH cargo nextest run --profile ci --features mlir --test native mlir_matches_interpreter
         env:

CHANGELOG.md

@@ -1,5 +1,34 @@
 # Changelog
 
+## 0.20.0
+
+- Representations: one layout query decides storage, ABI, zero words, and ownership for every consumer.
+- Compiler contracts: phase doors, inference solves, and prompt facts now fail closed.
+- Typed Core: construction, verification, and reference-count insertion gained stages and named failures.
+- Reference counting: borrowed parameters lower as true loans, so read-only traversals retain nothing.
+- Memory: fixed two leaks, a shadowed match arm binder and a range expression in the syntax encoder.
+- Strings and bytes: slicing is now a constant-time window rather than a copy.
+- Strings: literals are static cells, allocated once and shared by every mention.
+- Performance: layout and parse throughput improved, the adversarially nested case tenfold.
+- Builds: native links select lld where the toolchain has it, so an artifact's bytes follow only from its inputs.
+- Lint: a new rule catches the recursive codepoint scan that turns traversals quadratic.
+- Effect tiers: shapes that used to fall to the free monad now hold the evidence tier.
+- Effect rows: callbacks stored in data keep exact witnesses, and pure ones stay direct.
+- Effect rows: an element row with no local witness compiles by subsumption with a warning.
+- Effect lowering: a refused rewrite names the declaration and the form it stopped at.
+- Handlers: one without a return arm now answers with its body's type, not an over-general scheme.
+- Arenas: promotion preserves shared structure instead of copying it exponentially.
+- Records: sum variants may reuse field names at different types.
+- Records: partial sum reads and constructor spreads now fail during checking.
+- Patterns: record arms can use `C { .. }` to ignore every field.
+- Checker bootstrap: the Prism shadow now covers effect rows, parameterized effects, and generalization.
+- Self-hosted parser: the whole corpus now parses to identical trees, with no known divergences.
+- Parser handover: froze the oracle terms and recorded a receipt for the shadow's corpus run.
+- Tier accountability: a gate diffs every lowering rung against the interpreter, corpus and fuzzed.
+- Code index: hover facts no longer perturb definition identity.
+- Store: every layer is sharded and bounds itself by entry count and bytes.
+- Store: collection reports what it reclaimed, and a runaway layer is retired wholesale.
+
 ## 0.19.0
 
 - Lint: added `prism lint`, twelve Prism-written house rules with coded suppressions, JSON output, and an advisory mode.
@@ -320,7 +349,7 @@
 - Instance coherence: each `(class, type-head)` has one canonical instance that implicit resolution always selects, so ambiguity-at-use is gone. A lone instance is canonical by default; when several share a head one is named with a top-level `canonical Class(Head) = name`, and two undesignated instances are a coherence error at definition (caret plus designation hint). `f(args, using name)` stays the visible override, and a `newtype` is the way to a different default. No Core, runtime, or backend change, so the parity oracle is byte-identical. `canonical` is reserved.
 - A right-associative power operator `^` (tighter than `*`), the method of a new `Pow` class: `2 ^ 10` is bignum-correct `Int`, `2.0 ^ 10.0` is `Float`, mixed `Int ^ Float` a type error. The prior integer `pow` is now `int_pow`.
 - Imperative loops (`while`/`loop`) lower to a tail-recursive prelude driver (constant stack, no per-iteration allocation), an unconditional `loop` to the bottom-typed `forever`. `break`/`continue`/`return` compile to non-resumable performs of internal, fully-handled effects, so none surfaces in a function's row, and a loop installs a handler only for the keyword it uses. The prelude's old `while` is now `repeat_while`.
-- Principal effect-row inference: a lambda delimits its effects onto its own arrow row, the arrow is covariant in that row (a pure function fits any effectful context via row subsumption), and the call-graph set pass is dropped as a row seed so the inferred row is the single source of truth. Builtins carry their effect row on the type, so inference attributes `IO`/`Exn`/`Fail` directly; rows display in canonical name-sorted order; and definitions are inferred in dependency-SCC order so a forward reference sees a generalized type.
+- Principal effect-row inference: a lambda delimits its effects onto its own arrow row, the arrow is covariant in that row (a pure function fits any effectful context via row subsumption), and the call-graph set pass is dropped as a row seed so the inferred row alone determines the effect set. Builtins carry their effect row on the type, so inference attributes `IO`/`Exn`/`Fail` directly; rows display in canonical name-sorted order; and definitions are inferred in dependency-SCC order so a forward reference sees a generalized type.
 - `mask` over the sole handler of an effect now leaves the operation genuinely unhandled (the label stays in the row) instead of inferring it pure and hitting an effect-reconciliation ICE at lowering.
 - Two source warnings (the prelude is exempt): an unused local binding and a name shadowing one in scope (a leading `_` and a consuming rebind `let s = f(s)` are exempt). Annotations are name-checked uniformly across parameters, returns, constraints, and rows: an undeclared effect or constructor is a hard error, and an annotation broader than the inferred row warns.
 - Standard library split into on-demand modules under `lib/std` (`Data.Char`/`List`/`Map`/`Maybe`/`Result`/`Set`/`String`), shrinking the always-loaded prelude; `Set` gains `set_union`/`set_intersection`/`set_difference`, and a project may replace the built-in prelude via `[package] prelude` in `prism.toml`.

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prism"
-version = "0.19.0"
+version = "0.20.0"
 authors = ["Stephen Diehl <stephen.m.diehl@gmail.com>"]
 categories = ["compilers"]
 default-run = "prism"
@@ -190,7 +190,7 @@ exclude = ["tools/prismup"]
 resolver = "2"
 
 [workspace.package]
-version = "0.19.0"
+version = "0.20.0"
 authors = ["Stephen Diehl <stephen.m.diehl@gmail.com>"]
 edition = "2021"
 license = "MIT"

Dockerfile

@@ -1,4 +1,4 @@
-# Bundles LLVM 22 + clang so prism runs with no host toolchain.
+# Bundles LLVM 22 + clang + lld so prism runs with no host toolchain.
 FROM rust:1-bookworm AS builder
 RUN set -eux; \
     apt-get update; \
@@ -25,7 +25,7 @@ RUN set -eux; \
     echo "deb http://apt.llvm.org/bookworm/ llvm-toolchain-bookworm-22 main" \
       > /etc/apt/sources.list.d/llvm.list; \
     apt-get update; \
-    apt-get install -y --no-install-recommends llvm-22 clang-22; \
+    apt-get install -y --no-install-recommends llvm-22 clang-22 lld-22; \
     apt-get purge -y wget gnupg; apt-get autoremove -y; \
     rm -rf /var/lib/apt/lists/*
 COPY --from=builder /src/target/release/prism /usr/bin/prism