diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml index 141953ff..9191997e 100644 --- a/.github/workflows/dogfood-proofs-ci.yml +++ b/.github/workflows/dogfood-proofs-ci.yml @@ -78,6 +78,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Lean is not in the Guix manifest and the + # container has no Lean stage. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install elan + pinned Lean toolchain run: | set -euo pipefail @@ -130,6 +133,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Lean is not in the Guix manifest and the + # container has no Lean stage. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install elan + pinned Lean toolchain run: | set -euo pipefail @@ -180,6 +186,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Idris 2 is not in the Guix manifest and no + # container stage installs it. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install Idris2 run: | set -euo pipefail diff --git a/.github/workflows/idris2-abi-ci.yml b/.github/workflows/idris2-abi-ci.yml index 5bb4ed37..a2ef75e5 100644 --- a/.github/workflows/idris2-abi-ci.yml +++ b/.github/workflows/idris2-abi-ci.yml @@ -62,6 +62,9 @@ jobs: echo "Non-PR event — running full type-check." fi + # PROOF-POLICY §6 deviation (open): Idris 2 is not in the Guix manifest and no + # container stage installs it. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install Idris2 if: steps.detect.outputs.relevant == 'true' run: | diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index c318766a..9d05a59c 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -3,12 +3,14 @@ = Proof status — policy-vocabulary view -*Status*: reviewed 2026-11-04. Each row is scoped to its recorded source -identity and check; this file does not claim a single revision was checked -for every obligation. +*Status*: reviewed 2026-11-09 against main `+2ab7574ae1e574b0e881422fde6252bf79dea178+`. +Each row is scoped to its recorded source identity and check; this file does +not claim a single revision was checked for every obligation. *Normative policy*: `+3-practice/PROOF-POLICY.adoc+` in -https://github.com/metadatastician/standards[metadatastician/standards] (owner -ruling 2026-10-26). +https://github.com/metadatastician/standards[metadatastician/standards], read +at commit `+b8f60511e76c9015d86990317162dce653c92fe1+` (owner rulings +2026-10-26, 2026-11-04 for §8 Proof Witness Grades, and 2026-11-07 for §1.2 +Creusot, Pearlite and Verus). This is ECHIDNA's *proof-status file* in the sense `+PROOF-POLICY+` uses the term: the place each obligation's ledger row lives, in the closed vocabulary of @@ -78,6 +80,19 @@ headless, isolated, pinned run). Always write the `+PWG-+` prefix. * A recheck leg counts only when its kernel accepted it *and* its §2.2 correspondence is `+RECONCILED+`. Until then it is not a witness. +[width="100%",cols="22%,10%,12%,56%",options="header"] +|=== +|Theory theorem |`+pwg+` |`+foundation_diverse+` |Legs (route, §5 token, §2.2 state, receipt) + +|Receipt/warrant separation, `+meta-checker/src/Echidna/Receipt.agda+` (R11) +|`+3+` +|`+false+` +|*Agda*: source, `+proven+`, `+AGDA-VERIFIED+`, hosted run +https://github.com/hyperpolymath/echidna/actions/runs/42551607796[42551607796] +on `+2ab7574+`. *Rocq*: `+open+`, `+BRIDGE-PENDING+`, no receipt. *Lean*: +`+open+`, `+BRIDGE-PENDING+`, no receipt. Owes both recheck legs (§8.4.1). +|=== + Grades are derived from receipts, never asserted, and are never flattened into a percentage. See R5 and R6. @@ -168,7 +183,7 @@ decides their fate (open question A5). |=== -=== Lean 4 — cross-checks and algebraic properties (§4 exceptions) +=== Lean 4 — engineering properties held outside Idris 2 (§3 re-homing pending) [width="100%",cols="24%,13%,38%,25%",options="header"] |=== @@ -225,7 +240,21 @@ here. axiom-tracker completeness, integrity, clamp bounds, receipt/warrant (9 modules) |`+proven+` |First-party Agda in `+meta-checker/src/+`, type-checked with the §2.1 -canonical invocation. The reproducible local receipt is +canonical invocation. +*Current receipt (exact commit):* the scheduled Agda Meta-Checker run +https://github.com/hyperpolymath/echidna/actions/runs/42551607796[42551607796] +on main `+2ab7574ae1e574b0e881422fde6252bf79dea178+` passed, using the pinned +`+scripts/ci/setup-agda.sh+` and `+scripts/ci/check-agda.sh+`. A local recheck of +the same commit on 2026-11-09 also passed: 9 of 9 modules produced fresh +interfaces, the receipt controls accepted the two witnesses and rejected the +three planted claims, and there were 55 `+UnsupportedIndexedMatch+` warnings at +the same six sites. The Agda executable SHA-256 matched +`+6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6+`. The standard +library came from the `+v2.1+` git tag, commit `+97bc55e+`, because that +session's network refused the archive host; see Toolchain deviations. Every +source digest at `+2ab7574+` equals the corresponding digest in the earlier +receipt below. +*Earlier local receipt:* link:reports/2026-11-04-agda-meta-checker-receipt.json[`+2026-11-04-agda-meta-checker-receipt.json+`]. It records base commit `+9dd7847dfb095f0ddf3d41bac3327fcc4486fb6b+` plus the exact SHA-256 of every checked source and library descriptor, and names @@ -268,6 +297,47 @@ on `+main+`. The earlier 2026-11-01 timing/count report is historical, not the evidence for the current `+proven+` row; the source-bound 2026-11-04 receipt replaces it. +**Classification (§1), decided 2026-11-09:** only `+Receipt+` states theory. +`+TrustLevel+`, `+AxiomSafety+`, `+Portfolio+`, `+Dispatch+`, +`+AxiomTrackerCompleteness+`, `+Integrity+` and `+ClampTrust+` name this +repository's types, and §1 places them as engineering. The owner chose to +*split* the meta-checker. Generic theory stays in Agda: `+Receipt+`, and any +statement that holds for an arbitrary logic or order, such as E9 composition +(#471). The echidna-specific statements are verified *on the Rust* with +Creusot/Pearlite and Verus (R1). They are not restated in Idris 2: the strict +§1 ruling that #477 applies retires Idris restatements of Rust behaviour +(it removes `+TrustKernelMonotonicity.idr+`). Each Agda module retires once its +Rust contracts carry a receipt. Until then these rows keep their `+proven+` +token as statements about a model. They carry no PWG. + +**Design review of the statements (2026-11-09, at `+2ab7574+`, before #477 +replaced the trust kernel and retired `+TrustKernelMonotonicity.idr+`):** the kernel accepting a proof +says nothing about whether the statement models the code or says what its name +claims. A statement-by-statement comparison with the Rust, the Idris 2 corpus +and the Lean corpus found the following. Each is to be fixed in the split, not +by changing a token. + +* *Model diverges from the Rust.* `+Dispatch.compute-trust+` gives Level 2 for a + cross-checked result without a certificate. The Rust + (`+src/rust/verification/confidence.rs+`, the "Cross-checked without + certificate" branch) and Idris 2 `+TrustKernelMonotonicity.computeTrustLevel+` + give Level 3. `+Integrity.check+` maps an uninitialised manifest to `+Missing+`, + where the Rust and Lean `+verify_placeholder+` give `+Uninitialized+`; the model + also has no "file not found" input. +* *No Rust counterpart.* `+Portfolio.portfolio-trust+` (the Rust + `+compute_trust_level+` never reads `+portfolio_confidence+`) and + `+ClampTrust.clamp-trust+` (R10). +* *Statements weaker than their names.* `+AxiomSafety.comment-skip-sound+` + ignores its hypothesis and proves only `+danger-to-policy DC-Safe ≡ Clean+`. + `+AxiomSafety.real-pattern-classified+` proves only that a function has a + value. `+Dispatch.pipeline-deterministic+` and + `+AxiomTrackerCompleteness.scan-deterministic+` are instances of `+cong+`. The + `+classify-*+` stubs always return `+DC-Safe+` and no theorem uses them. +* *Gaps.* Idris 2 proves the sufficiency of the Level 5 conditions + (`+trustMono_level5_exact+`) but not their necessity, which Agda + `+max-trust-requires-all+` states. Idris 2 `+ClampTrustBounds+` lacks + `+clamp-idempotent+`. + |R9. E11 solver-integrity soundness |`+proven+` |`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the @@ -306,6 +376,22 @@ validate the Idris2 file or its correspondence to runtime code. Existing Idris2 interface and engineering checks remain active under §1; their receipt status is R2. Monotonicity here is by step lemma plus transitivity, rather than the Idris2 file's decision table. +**Model and code differ:** the Rust has +`+echidna_core_creusot::clamp_trust(level, min_level, max_level)+` +(`+crates/echidna-core-creusot/src/lib.rs:274+`). It clamps a `+TrustLevel+` into +a level range. Its bounds contract (`+requires min_level <= max_level+`, +`+ensures min_level <= result <= max_level+`) is written but not discharged, and +unit test PO-7 checks it exhaustively. The Agda model instead clamps a natural +number into the five levels. Only its bounds statement carries over, as a +special case of the Rust contract (range `+[Level1, Level5]+`). Its fixed-point +and monotone-in-ℕ statements have no counterpart. `+src/rust/verification/ +confidence.rs+` does not call `+clamp_trust+`; it derives a level from +`+TrustFactors+`. The module header's reason for restating the obligation in +Agda ("`there is no idris2 binary in CI that runs it`") is out of date: R2 +records the Idris 2 corpus, `+ClampTrustBounds+` included, building in CI. Under +the R4 split, the target is Creusot/Verus on the Rust `+clamp_trust+`: discharge +the written bounds contract, and add idempotence and monotonicity in `+level+` +as level-to-level statements. The ℕ-specific statements retire with the module. |R11. Epistemic separation: receipt vs warrant |`+proven+` @@ -336,6 +422,10 @@ through Dedukti or re-proved, with the route recorded per theorem. |Never attempted. This is what holds the theory set at `+PWG-3+`: locally checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the transport route exists; using it is unstarted work, not a missing capability. +Owner decision 2026-11-09: try the §2 *transport* route first (Agda → +Dedukti/Lambdapi → Rocq), record how it performs, then re-prove in Lean (core +library, no Mathlib) and Rocq where transport fails. Each leg records its +route, §5 token, §2.2 state and receipt in the PWG table. |R6. E9 "proof composition soundness" |`+argued+` until the `+agda-meta-checker+` job prints a source-bound receipt @@ -369,10 +459,11 @@ show. Rocq/Lean rechecks (§2): not started. |R7. `+verification/confidence.rs+` 0–1 score; `+DispatchResult.trust_level+` 1–5 |`+tested-only+` (internal ranking) — *not an assurance claim* -|Mathesis §6: "`Do not flatten proof confidence into a percentage.`" +|`+PROOF-POLICY+` §8.4.7: a census, never a percentage or a single confidence +score. §8 also says an ECHIDNA `+TrustLevel+` does not convert into a PWG. |The score ranks backends against each other and is unweighted by any receipt. It is a routing heuristic. Do not publish it as assurance and do not compare it -with a Mathesis grade. +with a PWG. |R8. `+echidna.prove.result/1+` `+trust.confidence+` |`+open+`, correctly @@ -384,6 +475,53 @@ guess. |=== +== Toolchain deviations (`+PROOF-POLICY+` §6) + +§6 requires proof toolchains to install through the repository's Guix manifest +or its container. Where a lane installs another way, it must carry a +`+deviation+` record here and in the installing workflow. These records were +missing until 2026-11-09. All three are `+open+`. + +[width="100%",cols="16%,18%,30%,24%,12%",options="header"] +|=== +|Leg |Tool and digest |How CI installs it |Why not Guix or the container |State + +|R4, R11 (Agda) +|Agda 2.7.0.1, archive SHA-256 +`+975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a+`; agda-stdlib 2.1, archive SHA-256 `+72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431+` +|`+scripts/ci/setup-agda.sh+` downloads both GitHub release archives, checks +them against the pinned digests (including on a cache hit), and +`+check-agda.sh+` asserts the version and fails on a mismatch. +|`+manifests/live-provers.scm+` names `+agda+`, but the lane pins a binary +distribution to avoid a cold GHC bootstrap (comment in `+setup-agda.sh+`). The +Guix `+agda+` package's version and stdlib pin have not been checked against +2.7.0.1 and 2.1. +|`+open+` + +|R2 (Idris 2) +|Ubuntu `+idris2+` package, otherwise the v0.8.0 source tarball; no digest +recorded +|`+dogfood-proofs-ci.yml+` *Idris2 (verification)* job and +`+idris2-abi-ci.yml+` install from apt, falling back to a source build. +|`+manifests/live-provers.scm+` records Idris 2 as absent from its baseline. No +container stage installs it. +|`+open+`; the lane does not yet assert a version or a digest. + +|R3 (Lean 4) +|Lean 4.13.0 through elan; local recheck archive SHA-256 `+44ceeac7ee4c98d177bfb4a3e5c210555c87e75b08807b68d523237fe4f09997+` +|`+dogfood-proofs-ci.yml+` *Lean 4 (verification)* job runs `+elan-init.sh+` and +installs the toolchain pinned by `+verification/proofs/lean4/lean-toolchain+`. +|Not in Guix (`+manifests/live-provers.scm+`). The manifest points to the +Wave-3 container, but `+Containerfile.wave3+` has no Lean stage. +|`+open+`; the lane asserts the version through `+lean-toolchain+`, not a digest. +|=== + +The local rechecks on 2026-11-09 add one more deviation. The agent session's +network refused `+codeload.github.com+`, so it fetched agda-stdlib by the +`+v2.1+` git tag (peeled commit `+97bc55e47367c562b3032bf104f2a00b19716f88+`) +rather than by the archive digest. That affects only the local corroboration +of R4, not the hosted receipt. + == Not obligations `+PROOF-POLICY+` §3: "`Corpora that exist to exercise provers are not diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 8b7ce9ac..f578b70c 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -7,93 +7,141 @@ Jonathan D.A. Jewell == Overview -The ECHIDNA meta-checker is an **Agda formalisation** that proves correctness properties -about ECHIDNA's trust-hardening pipeline. When Agda successfully type-checks these modules, -it provides a **machine-verified guarantee** that the system's safety invariants hold. - -== Verified Properties (30+) - -=== Trust Level System (`TrustLevel.agda`) - -* Trust levels form a **total order** (reflexive, antisymmetric, transitive, total) -* `min-trust` correctly computes lower bounds -* **Dangerous axioms always cap trust at Level1** -* Safe axioms preserve trust level -* Capping is monotonic - -=== Axiom Safety (`AxiomSafety.agda`) - -* Axiom policies form a total preorder -* `worst-policy` is commutative, associative, with identity (Clean) -* **Rejected is absorbing** — once rejected, always rejected -* Comment-aware scanning is sound -* Every danger class maps to exactly one policy - -=== Portfolio Verification (`Portfolio.agda`) +The meta-checker is an *Agda model* of ECHIDNA's trust-hardening pipeline. It +states properties of that model and proves them. A successful check means the +model has those properties. It does not establish that the Rust implementation +has them: no refinement between these definitions and the Rust source is proved +here. Verifying the Rust is the job of Creusot with Pearlite contracts and Verus +(`+PROOF-POLICY+` §1.2), recorded as obligation R1 in +link:../docs/PROOF-STATUS.adoc[`+docs/PROOF-STATUS.adoc+`]. + +That file is the authoritative record of what is proved, by which receipt, and +with which limits. This README describes the modules and how to check them. + +The model does not match the Rust everywhere, and some theorem names promise more +than their statements give. The design review under R4 in `+PROOF-STATUS+` +lists each case: for example, the dispatch model gives Level 2 where the Rust +gives Level 3, and `+comment-skip-sound+` ignores its hypothesis. Until the +Rust contracts replace these modules, read each statement, not its name. + +== Modules + +[cols="1,3",options="header"] +|=== +|Module |What it states + +|`+Echidna.TrustLevel+` +|The five trust levels form a total order; `+min-trust+` is a lower bound; +dangerous axioms cap trust at Level 1; capping is monotone. + +|`+Echidna.AxiomSafety+` +|Axiom policies form a total preorder; `+worst-policy+` is commutative and +associative with `+Clean+` as identity; `+Rejected+` is absorbing; every danger +class maps to exactly one policy. + +|`+Echidna.Portfolio+` +|Cross-checking does not lower trust below a single solver; inconclusive and +timed-out results give Level 1; agreement is reflexive and symmetric; unknown +verdicts never count as agreement. + +|`+Echidna.Dispatch+` +|Failed integrity and dangerous axioms each give Level 1; Level 5 needs every +positive factor; the modelled pipeline only degrades trust and is deterministic. + +|`+Echidna.AxiomTrackerCompleteness+` +|Every registered pattern yields exactly one policy; the policy fold +distributes over registry concatenation and is monotone; an empty registry +yields `+Clean+`; a `+Reject+` pattern anywhere forces `+Rejected+`; scanning is +deterministic. + +|`+Echidna.Integrity+` +|Obligation E11 over digests: verification needs an initialised manifest, means +the recorded digest matched, and never accepts a different digest. Digest +comparison soundness is a record field, not a postulate. + +|`+Echidna.ClampTrust+` +|Bounds, monotonicity, fixed points and idempotence of a modelled +`+clamp-trust : ℕ → TrustLevel+`. The Rust `+clamp_trust+` in +`+crates/echidna-core-creusot+` has a different signature (it clamps a level +into a level range), so only the bounds statement carries over (R10). + +|`+Echidna.Receipt+` +|A two-world Kripke countermodel separating receipts (factive) from warrants +(not factive). This is the module's one *theory* statement under §1. + +|`+Echidna.MetaChecker+` +|The entry point that imports the eight modules above. +|=== -* **Cross-checking improves trust** over single-solver -* Inconclusive and timeout always produce Level1 -* Small-kernel provers always have higher trust -* Agreement relation is reflexive and symmetric -* Unknown verdicts never count as agreement +Under `+PROOF-POLICY+` §1 only `+Receipt+` is theory. The other modules state +properties of this repository's own types, which §1 places with Idris 2. The +owner's decision of 2026-11-09 splits them. What holds for any implementation +stays as Agda theory. The echidna-specific statements are verified on the Rust +with Creusot/Pearlite and Verus, not restated in Idris 2, and each module here +retires once its contracts carry a receipt. See R4 in +`+docs/PROOF-STATUS.adoc+`. -=== Dispatch Pipeline (`Dispatch.agda`) +== Escape hatches -* **Failed integrity always produces Level1** -* **Dangerous axioms always produce Level1** -* Maximum trust (Level5) requires all positive factors -* Pipeline is monotonically degrading -* Pipeline is deterministic +The check runs with `+--safe+`, so the compiler refuses `+postulate+`, +`+primTrustMe+` and unsafe options anywhere in the import cone. There are no +postulates in these modules. The kernel enforces that; a text search is not the +evidence. -== Zero Unsafe Constructs +The check reports `+UnsupportedIndexedMatch+` warnings at a few sites. They mean +the flagged functions do not compute under Cubical transports, which is the +difference between `+--cubical-compatible+` and full `+--cubical+` that +`+PROOF-POLICY+` §2.1 draws. They are recorded in `+PROOF-STATUS+`, not +suppressed. -[cols="1,1"] -|=== -| Construct | Count +== Running -| `postulate` | 1 (funext — standard, provable in HoTT) -| `sorry` | 0 -| `believe_me` | 0 -| `Admitted` | 0 -| `TRUSTME` | 0 -|=== +Use the pinned toolchain and the canonical invocation (`+PROOF-POLICY+` §2.1). +The scripts install Agda 2.7.0.1 and agda-stdlib 2.1 from release archives +checked against pinned SHA-256 digests, then check every module and require a +fresh interface for each one: -== Running +Outside GitHub Actions, `+setup-agda.sh+` cannot change the calling shell's +environment. Give it the two files Actions would provide, then load them: [source,bash] ---- -# Install Agda (requires GHC) -cabal install Agda +export GITHUB_ENV=$(mktemp) GITHUB_PATH=$(mktemp) +bash scripts/ci/setup-agda.sh # writes Agda_datadir, AGDA_LIBRARIES_FILE, LC_ALL +set -a; . "$GITHUB_ENV"; set +a # the values are mktemp paths, without spaces +export PATH="$(cat "$GITHUB_PATH"):$PATH" +bash scripts/ci/check-agda.sh # runs from meta-checker/ +---- -# Install standard library -agda-stdlib-utils install +`+check-agda.sh+` runs: -# Type-check all proofs -cd meta-checker -agda src/Echidna/MetaChecker.agda +[source,bash] +---- +agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \ + --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda ---- -If the command exits with code 0, all 30+ properties are machine-verified. - -== CI Integration +It then fails if any module under `+src/Echidna/+` produced no interface, and runs +`+scripts/ci/check-receipt-controls.sh+`, whose planted claims must be rejected. -The `.github/workflows/agda-meta-checker.yml` workflow automatically type-checks -the meta-checker on every push. A green badge means all proofs are valid. +== CI -== Architecture +`+.github/workflows/agda-meta-checker.yml+` runs the same two scripts on relevant +pushes and pull requests and on a schedule. A passing run on a commit is that +commit's receipt for the Agda leg; `+PROOF-STATUS+` cites it by run and commit. -The meta-checker mirrors the Rust source structure: +== Rust counterparts -[cols="1,1"] +[cols="1,1",options="header"] |=== -| Agda Module | Rust Source +|Agda module |Rust source it models -| `Echidna.TrustLevel` | `verification/confidence.rs` -| `Echidna.AxiomSafety` | `verification/axiom_tracker.rs` -| `Echidna.Portfolio` | `verification/portfolio.rs` -| `Echidna.Dispatch` | `dispatch.rs` +|`+Echidna.TrustLevel+` |`+src/rust/verification/confidence.rs+` +|`+Echidna.AxiomSafety+` |`+src/rust/verification/axiom_tracker.rs+` +|`+Echidna.Portfolio+` |`+src/rust/verification/portfolio.rs+` +|`+Echidna.Dispatch+` |`+src/rust/dispatch.rs+` +|`+Echidna.Integrity+` |`+src/rust/integrity/solver_integrity.rs+` |=== -Each Agda definition is annotated with which Rust function or type it models. -The proofs verify that the *design* is correct — they do not replace unit tests -which verify that the *implementation* matches the design. +The correspondence is by reading, not by proof. These proofs check the design; +the unit tests and, once R1 lands, the Rust verifiers check the implementation. diff --git a/scripts/ci/setup-agda.sh b/scripts/ci/setup-agda.sh index ba0e4601..3dd1b39b 100644 --- a/scripts/ci/setup-agda.sh +++ b/scripts/ci/setup-agda.sh @@ -2,6 +2,9 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell # Pinned upstream binaries: no cold GHC bootstrap and no cached proof results. +# PROOF-POLICY §6 deviation (open): installs from GitHub release archives, not +# the Guix manifest or the container. Recorded in docs/PROOF-STATUS.adoc, +# "Toolchain deviations". set -Eeuo pipefail trap 'echo "::error::Agda setup did not complete; proof check NOT RUN"; exit 2' ERR