docs: restate compression claims to held-out truth; retire ≥3× Abrash gate #141

Workflow file for this run

	name: CI

	on:
	push:
	branches: [main, bootstrap]
	pull_request:

	# RELIABILITY (issue #58): supersede stale in-flight runs so a re-push does not
	# sit behind an obsolete run for a queue slot — a direct queue-pressure win
	# against the documented runner-dispatch starvation (RELEASE-NOTES-0.4.0.md,
	# "The CI that never ran"). The group key is the PR head branch on pull_request
	# and the unique run id on push, so:
	# * a new push to a PR CANCELS the PR's older in-flight run (saves the slot);
	# * pushes to a protected branch (main/bootstrap) each get a unique group and
	# are therefore NEVER cancelled — default-branch runs always complete.
	concurrency:
	group: ${{ github.workflow }}-${{ github.head_ref \|\| github.run_id }}
	cancel-in-progress: true

	permissions:
	contents: read

	jobs:
	# Cheap path gate: docs-only diffs skip the heavy verus/coverage/fuzz legs so
	# they never consume a hosted-runner slot for a README typo. The fast `cargo`
	# gate below always runs (no `needs: changes`) so a required status check
	# always reports on every push/PR, docs-only or not.
	changes:
	name: detect code changes
	runs-on: ubuntu-latest
	timeout-minutes: 5
	outputs:
	code: ${{ steps.filter.outputs.code }}
	steps:
	- uses: actions/checkout@v4
	- uses: dorny/paths-filter@v3
	id: filter
	with:
	# `code` is true iff at least one changed file is NOT docs/markdown/
	# metadata. `predicate-quantifier: every` means a file matches `code`
	# only when it matches ALL of the negations (i.e. it is a real code
	# file); the filter output is then true if ANY changed file does.
	predicate-quantifier: 'every'
	filters: \|
	code:
	- '!docs/**'
	- '!*/.md'
	- '!LICENSE'
	- '!.gitignore'

	cargo:
	name: cargo check + test (stable)
	runs-on: ubuntu-latest
	# Fast gate: always runs (no path gate) so it can serve as the always-green
	# required check. Bounded so a hung runner turns RED instead of hanging the
	# queue indefinitely.
	timeout-minutes: 20
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	# Cache registry + git + target dir to cut cold-build time (reliability:
	# a shorter job holds a runner slot for less time).
	- uses: Swatinem/rust-cache@v2
	- name: cargo check
	run: cargo check --workspace --all-targets
	- name: cargo test
	run: cargo test --workspace

	verus:
	name: verus verify (0.2026.07.05.49b8806)
	runs-on: ubuntu-latest
	# Skip on docs-only diffs (queue-pressure win); always runs when code changed.
	needs: changes
	if: needs.changes.outputs.code == 'true'
	# The heaviest leg: bounded generously so a genuinely stuck runner fails RED
	# rather than hanging the queue, but long enough for a cold Verus install +
	# the full proof set (P1/P3 + P5 + Layer C + arena refinement).
	timeout-minutes: 45
	# Toolchain health is a HARD gate. Install + a `verus --version` smoke check run
	# fail-fast (NO continue-on-error): if Verus cannot even be invoked, this job
	# goes RED. It must never again read as "skipped, job green" — which is exactly
	# what happened when `verus --version` died on a missing Rust toolchain while the
	# verify step got SKIPPED under a job-level continue-on-error. Only the actual
	# proof verification outcome stays advisory (continue-on-error on that step):
	# proofs are visible-but-non-blocking per the #5 design; toolchain breakage is not.
	env:
	# DEVIATION FROM SPEC (spec pins bare "0.2026.07.05"):
	# verus-lang publishes every release tag WITH a trailing build/commit hash.
	# The real, downloadable release is tag `release/0.2026.07.05.49b8806` with
	# asset `verus-0.2026.07.05.49b8806-x86-linux.zip`. The bare "0.2026.07.05"
	# tag/asset does NOT exist on GitHub — the previous workflow 404'd on exactly
	# that URL, which is why this job had been failing at the install step (verus
	# never even ran). The underlying Verus version is still 0.2026.07.05; only
	# the published id carries the .49b8806 suffix. ACTION FOR SPEC-REVISION
	# SESSION: update the spec pin to include the .49b8806 suffix (or record the
	# commit hash alongside the version).
	VERUS_VERSION: "0.2026.07.05.49b8806"
	# ROOT CAUSE of the historical silent failure (run 29171900326 @ d92a463):
	# the Verus binary release is a thin wrapper that shells out — via rustup — to
	# a PINNED Rust toolchain, and `verus --version` itself fails if that toolchain
	# is absent. The install step succeeded (binary found at verus-x86-linux/verus,
	# PATH exported fine), but `verus --version` then died with:
	# "verus: required rust toolchain 1.96.0-x86_64-unknown-linux-gnu not found".
	# GitHub's ubuntu-24.04 image ships rustup but NOT this toolchain, so we install
	# exactly it before invoking verus.
	VERUS_RUST_TOOLCHAIN: "1.96.0"
	steps:
	- uses: actions/checkout@v4

	# Cache the pinned Verus release zip across runs. The release asset is
	# immutable per tag, so a hit skips the network entirely — removing the
	# single most stall-prone step (the historical 404 + rate-limited fetch).
	- name: Cache Verus release zip
	uses: actions/cache@v4
	with:
	path: verus.zip
	key: verus-zip-${{ env.VERUS_VERSION }}-x86-linux

	- name: Install Verus ${{ env.VERUS_VERSION }} (+ pinned Rust toolchain) — fail-fast
	run: \|
	set -euxo pipefail
	# 1) Fetch + unpack the pinned Verus release.
	# Tag is `release/<VERUS_VERSION>`; the '/' is URL-encoded as %2F.
	url="https://github.com/verus-lang/verus/releases/download/release%2F${VERUS_VERSION}/verus-${VERUS_VERSION}-x86-linux.zip"
	# RELIABILITY (issue #58): only fetch on a cache miss, and retry the
	# download with exponential backoff so a transient network/rate-limit
	# blip does not fail the job (bounded: 4 tries, 2s/4s/8s/16s).
	if [ ! -s verus.zip ]; then
	n=0
	until curl -fL "$url" -o verus.zip; do
	n=$((n + 1))
	if [ "$n" -ge 4 ]; then
	echo "Verus download failed after $n attempts" >&2
	exit 1
	fi
	sleep $((2 ** n))
	done
	else
	echo "Using cached verus.zip"
	fi
	unzip -q verus.zip -d verus-dist
	# Resolve the dir holding the `verus` binary; make it (+ its driver) invocable.
	verus_dir="$(dirname "$(find verus-dist -name verus -type f \| head -1)")"
	test -n "$verus_dir"
	chmod +x "$verus_dir/verus" "$verus_dir/verus-driver" 2>/dev/null \|\| true
	echo "$PWD/$verus_dir" >> "$GITHUB_PATH"
	# 2) Install the Rust toolchain Verus wraps — `verus --version` needs it.
	rustup toolchain install "${VERUS_RUST_TOOLCHAIN}-x86_64-unknown-linux-gnu" --profile minimal

	- name: verus --version (toolchain smoke check) — fail-fast
	run: \|
	set -euxo pipefail
	# Proves the binary AND its pinned toolchain are actually invocable. NO
	# continue-on-error: a broken/uninvocable toolchain turns the job RED here,
	# so it can never again masquerade as "skipped, job green".
	verus --version \| tee /tmp/verus-version.txt
	grep -Eq '[0-9]+\.[0-9]+' /tmp/verus-version.txt

	- name: verus verify — core P1/P3 proofs (machine-checked; regression signal)
	id: core
	# Advisory-but-visible (per #5): the proof VERIFICATION OUTCOME does not gate
	# the merge queue, but a regression is clearly surfaced (red step + job
	# step-summary). This is the ONLY continue-on-error step — toolchain health
	# above is a hard gate.
	continue-on-error: true
	# Full verification of the Verus artifact `mtl_core.rs`. The stubbed P2
	# refinement is a trusted boundary (#[verifier::external_body] bodies +
	# p2_refinement's admit()), so this run PASSES on the real, machine-checked
	# core proofs — p3_progress (P3 progress/totality), div_semantics_witnesses
	# + trunc_divmod_correct (pinned truncating div/mod), smoke_dup_apply (P1
	# step determinism witness) — and FAILS iff one of THOSE regresses. That is
	# the meaningful, honest signal. Admitted/stubbed P2 can never fail here.
	run: \|
	set -o pipefail
	mkdir -p artifacts
	if verus crates/mtl-core/src/mtl_core.rs 2>&1 \| tee artifacts/proof-log.txt ; then
	echo "core_status=pass" >> "$GITHUB_OUTPUT"
	echo "### Verus core proofs (P1/P3): VERIFIED" >> "$GITHUB_STEP_SUMMARY"
	echo "Machine-checked: p3_progress, div_semantics_witnesses, trunc_divmod_correct, smoke_dup_apply." >> "$GITHUB_STEP_SUMMARY"
	else
	echo "core_status=fail" >> "$GITHUB_OUTPUT"
	echo "### Verus core proofs (P1/P3): REGRESSED — see proof log artifact" >> "$GITHUB_STEP_SUMMARY"
	exit 1
	fi

	- name: verus verify — P5 Turing-completeness proof (HARD GATE; admit-free)
	id: p5
	# HARD GATE (NO continue-on-error): unlike the P2-stubbed core step above,
	# P5 (`p5_universality.rs`) is a fully machine-checked, admit-free proof — the
	# two-counter Minsky simulation over `spec_step` (§6, §6.5 of docs/mtl-spec.md).
	# If it regresses, Turing completeness is no longer proven, so the job goes RED.
	# NOTE: p5_universality.rs does `mod mtl_core;`, so this invocation ALSO
	# re-verifies the frozen core (the explicit core step above is kept for its
	# dedicated regression signal + honesty audit).
	run: \|
	set -o pipefail
	mkdir -p artifacts
	if verus crates/mtl-core/src/p5_universality.rs 2>&1 \| tee artifacts/p5-proof-log.txt ; then
	echo "p5_status=pass" >> "$GITHUB_OUTPUT"
	echo "### Verus P5 (Turing completeness): VERIFIED" >> "$GITHUB_STEP_SUMMARY"
	echo "Machine-checked (admit-free): p5_lockstep, p5_simulation, p5_halt_forward, p5_halt_forward_monotone, p5_diverge, p5_halt_reverse (re-verifies mtl_core.rs alongside)." >> "$GITHUB_STEP_SUMMARY"
	else
	echo "p5_status=fail" >> "$GITHUB_OUTPUT"
	echo "### Verus P5 (Turing completeness): FAILED — see p5 proof log artifact" >> "$GITHUB_STEP_SUMMARY"
	exit 1
	fi

	- name: verus verify — Layer C checker soundness M1+M2+M3+M4 (crates/mtl-core/src/checker_verus.rs)
	id: checkerc
	# HARD GATE on VERIFICATION (like P5): `checker_verus.rs` mechanizes the v0.6
	# static stack-effect checker's soundness (T-Static / T-Progress / T-Branch)
	# over `spec_step`. It does `#[path] mod mtl_core;`, so this invocation ALSO
	# re-verifies the frozen core.
	# STATUS: 116 verified, 0 errors. Every lemma is machine-checked.
	# * M1/M2: straight-line + If T-Static (If-inlining CLOSED, no assume),
	# Times + PrimRec fully proven, reusable frame/compose/invariant machinery.
	# * M3: deterministic literal-Uncons soundness (lemma_uncons_case) and the
	# homogeneous-all-PushInt literal-seq Fold (lemma_fold_case/lemma_fold_splice)
	# are FULLY PROVEN Static; LinRec is conservatively REJECTED by check_m1
	# (sound) with the desugaring + branch shape-compatibility lemmas
	# (lemma_linrec_desugar / lemma_linrec_if_shape) machine-checked and the
	# full-recursion fixpoint marked as a loud UNPROVEN GAP.
	# * M4: row-polymorphic T-Static — thm_static_rowpoly lifts the pre=[]
	# self-contained slice to arbitrary non-empty `pre` (input-borrowing
	# programs), via lemma_models_stack_append re-using the already
	# base-polymorphic lemma_check_invariant. Borrowed-Int inputs FULLY
	# COVERED across the whole M1–M3 fragment; borrowed-Quote inputs remain a
	# loudly marked GAP (the AInt\|ALit lattice cannot name an opaque quote).
	# The only residual --no-cheating gaps are the 2 mtl_core P2 Clone external_body
	# stubs (pulled in via `mod mtl_core`, not from checker_verus itself).
	run: \|
	set -o pipefail
	mkdir -p artifacts
	if verus crates/mtl-core/src/checker_verus.rs 2>&1 \| tee artifacts/checkerc-proof-log.txt ; then
	echo "checkerc_status=pass" >> "$GITHUB_OUTPUT"
	echo "### Verus Layer C checker soundness (M1+M2+M3+M4): VERIFIED (116/0)" >> "$GITHUB_STEP_SUMMARY"
	echo "Machine-checked: lemma_prim_step_sound (per-primitive T-Progress), thm_static_straightline (If-free T-Static), thm_progress, thm_branch_progress, lemma_join_sound (T-Branch), thm_static_with_if (full straight-line + If T-Static, no assume), the M3 combinators — lemma_uncons_case (deterministic literal-Uncons), lemma_fold_case/lemma_fold_splice (homogeneous-Int literal-seq Fold), lemma_linrec_desugar/lemma_linrec_if_shape (LinRec desugaring + branch shape-compatibility; full recursion conservatively Rejected) — and the M4 row-polymorphic lift: lemma_models_stack_append, thm_static_rowpoly, thm_static_rowpoly_allint (non-empty `pre`, ∀ρ. ρ++pre -> ρ++post)." >> "$GITHUB_STEP_SUMMARY"
	else
	echo "checkerc_status=fail" >> "$GITHUB_OUTPUT"
	echo "### Verus Layer C checker soundness (M1+M2+M3+M4): FAILED — see checkerc proof log artifact" >> "$GITHUB_STEP_SUMMARY"
	exit 1
	fi

	- name: verus verify — arena refinement (arena_step ⇒ spec_step) (crates/mtl-arena/proofs/arena_verus.rs)
	id: arena
	# HARD GATE on VERIFICATION (like checkerc/P5, NO continue-on-error):
	# `arena_verus.rs` mechanizes the production arena backend's refinement of
	# the frozen `spec_step` — the unconditional one-step theorem
	# `α(arena_step(s)) = spec_step(α(s))` for all 23 primitives + the non-prim
	# (PushInt/PushQuote) cases, with fault parity and the u32-capacity→Overflow
	# characterization, plus the multi-step driver corollary. This DISCHARGES the
	# §5/§7 P2-style refinement obligation for the arena, mirroring the P2
	# exec_step refinement. If it regresses, the arena is no longer proven to
	# refine the spec, so the job goes RED.
	# STATUS: 145 verified, 0 errors. Admit-free arena refinement.
	run: \|
	set -o pipefail
	mkdir -p artifacts
	if verus crates/mtl-arena/proofs/arena_verus.rs 2>&1 \| tee artifacts/arena-proof-log.txt ; then
	echo "arena_status=pass" >> "$GITHUB_OUTPUT"
	echo "### Verus arena refinement (arena_step ⇒ spec_step): VERIFIED (145/0)" >> "$GITHUB_STEP_SUMMARY"
	echo "Machine-checked: α(arena_step(s)) = spec_step(α(s)) for all 23 prims + non-prim cases, fault parity, u32-capacity→Overflow, multi-step driver corollary." >> "$GITHUB_STEP_SUMMARY"
	else
	echo "arena_status=fail" >> "$GITHUB_OUTPUT"
	echo "### Verus arena refinement (arena_step ⇒ spec_step): FAILED — see arena proof log artifact" >> "$GITHUB_STEP_SUMMARY"
	exit 1
	fi

	- name: verus honesty audit — Layer C --no-cheating (reports the 2 mtl_core stubs; non-fatal)
	if: always()
	# `--no-cheating` rejects assume/admit/external_body. EXPECTED to flag exactly
	# the two mtl_core P2 Clone external_body stubs (pulled in via `mod mtl_core`).
	# checker_verus.rs itself contains NO assume/admit/external_body. Any OTHER cheat
	# appearing here is a regression. Report-only.
	run: \|
	mkdir -p artifacts
	verus --no-cheating crates/mtl-core/src/checker_verus.rs 2>&1 \| tee artifacts/checkerc-no-cheating-audit.txt \|\| true
	{
	echo "### Honesty audit (verus --no-cheating) — Layer C"
	echo "EXPECTED gaps: 2 mtl_core P2 Clone external_body stubs (from \`mod mtl_core\`). checker_verus.rs itself is assume/admit/external_body-free. No other cheat is permitted."
	} >> "$GITHUB_STEP_SUMMARY"

	- name: verus honesty audit — --no-cheating (reports stubbed P2; non-fatal)
	if: always()
	# `--no-cheating` rejects assume/admit/external_body. It is EXPECTED to fail
	# here because P2 is deliberately stubbed. We run it report-only so the job
	# (a) makes the trust boundary explicit and (b) would flag any NEW cheat
	# that sneaks into code meant to be fully proven. It never fails CI.
	run: \|
	mkdir -p artifacts
	verus --no-cheating crates/mtl-core/src/mtl_core.rs 2>&1 \| tee artifacts/no-cheating-audit.txt \|\| true
	{
	echo "### Honesty audit (verus --no-cheating)"
	echo "The failures in this step are the KNOWN, intended P2 stubs (trust boundary):"
	echo "- \`p2_refinement\` uses \`admit()\`"
	echo "- \`exec_step\` / \`exec_prim\` / \`exec_arith\` / \`exec_divmod\` / \`exec_cmp\` / \`run\` / \`value_to_exec_word\` use \`#[verifier::external_body]\`"
	echo ""
	echo "Core P1/P3 proofs (previous step) are machine-checked and are NOT admitted."
	} >> "$GITHUB_STEP_SUMMARY"

	- name: verus verify — P4 round-trip + exec printer/parser refinement (crates/mtl-syntax/proofs/p4_verus.rs)
	id: p4
	# Advisory-but-visible, mirroring the `core` step above: the P4 proof
	# VERIFICATION OUTCOME does not gate the merge queue, but a regression is
	# clearly surfaced (red step + job step-summary). Toolchain health (the
	# smoke check above) remains the only hard gate. NOTE: P4 verification is
	# intentionally kept advisory (continue-on-error) to match the `core`
	# step and avoid flaky-runner failures — it is NOT a hard gate like P5.
	continue-on-error: true
	# Full verification of the Verus artifact `p4_verus.rs`. This is now BOTH
	# levels of option (b):
	# * the level-(b) Seq<char> model parser/printer proving the P4
	# round-trip + idempotence theorems (p4_roundtrip, p4_idempotent)
	# over all 23 glyphs; AND
	# * the EXECUTABLE refinement (§15-22): exec_print / exec_digits /
	# exec_needs_sep / scan_digits / scan_name / exec_lex / exec_group /
	# exec_parse, each machine-checked to refine its spec, culminating in
	# exec_roundtrip (exec_parse(exec_print(p)) == Ok(p)).
	# All with 0 admit()/assume()/external_body. The proven exec surface is
	# pinned to the production Rust parser/printer by the differential
	# proptest + adversarial suite in crates/mtl-syntax/tests/p4_model_twin.rs
	# (run in the cargo job).
	run: \|
	set -o pipefail
	mkdir -p artifacts
	if verus crates/mtl-syntax/proofs/p4_verus.rs 2>&1 \| tee artifacts/p4-proof-log.txt ; then
	echo "p4_status=pass" >> "$GITHUB_OUTPUT"
	echo "### Verus P4 proofs (round-trip + idempotence + exec refinement): VERIFIED" >> "$GITHUB_STEP_SUMMARY"
	echo "Machine-checked Seq<char> model + proven exec printer/parser (§15-22): p4_roundtrip, p4_idempotent, exec_roundtrip, all 23 glyphs; 0 admit()." >> "$GITHUB_STEP_SUMMARY"
	else
	echo "p4_status=fail" >> "$GITHUB_OUTPUT"
	echo "### Verus P4 proofs: REGRESSED — see p4 proof log artifact" >> "$GITHUB_STEP_SUMMARY"
	exit 1
	fi

	- name: verus honesty audit — P4 --no-cheating (report-only)
	if: always()
	# Unlike the core P2 boundary, P4 uses NO admit/assume/external_body, so
	# this audit is EXPECTED TO PASS clean. Run report-only so it never gates
	# CI but would flag any NEW cheat that sneaks into the P4 proof.
	run: \|
	mkdir -p artifacts
	verus --no-cheating crates/mtl-syntax/proofs/p4_verus.rs 2>&1 \| tee artifacts/p4-no-cheating-audit.txt \|\| true
	{
	echo "### Honesty audit (verus --no-cheating) — P4"
	echo "P4 (model round-trip + exec printer/parser refinement §15-22) uses NO"
	echo "admit/assume/external_body; this audit is expected to PASS clean."
	} >> "$GITHUB_STEP_SUMMARY"

	- name: upload verus proof log
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: verus-proof-log
	path: artifacts/
	if-no-files-found: warn

	# ---------------------------------------------------------------------------
	# Coverage (issue #58). ADVISORY: reports line/region % over the core surface
	# (mtl-core interp + host, and the mtl-check checker) as a step summary and an
	# HTML+lcov artifact. It NEVER gates the merge (no threshold failure) so it
	# cannot join the historical stall in blocking merges; the number is baselined
	# here and ratcheted (not lowered) per the issue's success metric (>=70% on
	# the core surface).
	# ---------------------------------------------------------------------------
	coverage:
	name: coverage (cargo-llvm-cov, advisory)
	runs-on: ubuntu-latest
	needs: changes
	if: needs.changes.outputs.code == 'true'
	timeout-minutes: 30
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@stable
	with:
	components: llvm-tools-preview
	- uses: Swatinem/rust-cache@v2
	- name: Install cargo-llvm-cov
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-llvm-cov
	- name: Coverage (workspace) — text summary + lcov + HTML
	run: \|
	set -o pipefail
	mkdir -p coverage
	# One instrumented test run, three reports (summary/lcov/html) from the
	# same profraw so the numbers are consistent.
	cargo llvm-cov --workspace --no-report
	cargo llvm-cov report --summary-only \| tee coverage/summary.txt
	cargo llvm-cov report --lcov --output-path coverage/lcov.info
	cargo llvm-cov report --html --output-dir coverage/html
	- name: Publish coverage to step summary (core surface highlighted)
	if: always()
	run: \|
	{
	echo "### Coverage (advisory — cargo-llvm-cov)"
	echo ""
	echo "Success-metric surfaces (issue #58 target: >= 70%):"
	echo '```'
	grep -E 'interp.rs\|mtl-core/src/host.rs\|mtl-check/src/lib.rs\|^TOTAL' coverage/summary.txt \|\| true
	echo '```'
	echo ""
	echo "Full per-file table is in the \`coverage-report\` artifact (open \`html/index.html\`)."
	} >> "$GITHUB_STEP_SUMMARY"
	- name: Upload coverage report
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: coverage-report
	path: coverage/
	if-no-files-found: warn

	# ---------------------------------------------------------------------------
	# Fuzz (issue #58). GATING on findings: a SHORT libFuzzer smoke per PR over the
	# parser round-trip/totality and the interp-vs-arena differential (the Engine
	# seam). libFuzzer exits non-zero on the FIRST panic or engine divergence, so
	# this job goes RED on any new finding and uploads the crash artifact. The
	# budget is a smoke, not a soak; fuzz/README.md documents the longer local run.
	# Wired to the existing properties: p4_roundtrip.rs, the arena oracle, and the
	# mtl-core run_refines_reference differential.
	# ---------------------------------------------------------------------------
	fuzz:
	name: fuzz smoke (cargo-fuzz, gates on findings)
	runs-on: ubuntu-latest
	needs: changes
	if: needs.changes.outputs.code == 'true'
	timeout-minutes: 25
	steps:
	- uses: actions/checkout@v4
	- uses: dtolnay/rust-toolchain@nightly
	- uses: Swatinem/rust-cache@v2
	with:
	workspaces: fuzz
	- name: Install cargo-fuzz
	uses: taiki-e/install-action@v2
	with:
	tool: cargo-fuzz
	# Each target runs a bounded smoke under libFuzzer resource guards
	# (`-rss_limit_mb` + `-timeout`). We then GATE precisely per issue #58 AC:
	# a genuine panic or engine divergence is saved by libFuzzer as a
	# `crash-` artifact and FAILS the job; a `timeout-`/`oom-*` artifact is an
	# adversarial RESOURCE-EXHAUSTION input (step-fuel bounds steps, not the
	# memory of an exponential quote-doubling loop — see docs/ci-reliability.md
	# §3 and fuzz/README.md), reported as advisory rather than flaking the gate.
	- name: Fuzz smoke — parser totality + round-trip (gates on crash)
	run: bash .github/scripts/fuzz-smoke.sh parse_roundtrip 60
	- name: Fuzz smoke — interp-vs-arena differential / Engine seam (gates on crash)
	run: bash .github/scripts/fuzz-smoke.sh differential 90
	- name: Fuzz smoke — parse -> execute pipeline (gates on crash)
	run: bash .github/scripts/fuzz-smoke.sh parse_exec 60
	- name: Upload fuzz artifacts (crashes / timeouts / oom, if any)
	if: always()
	uses: actions/upload-artifact@v4
	with:
	name: fuzz-artifacts
	path: fuzz/artifacts/
	if-no-files-found: ignore

Navigation Menu

docs: restate compression claims to held-out truth; retire ≥3× Abrash gate #141

Workflow file

docs: restate compression claims to held-out truth; retire ≥3× Abrash gate #141

Uh oh!

Workflow file for this run