From 69d7fb9eda305c33224b55209e58f526df87eae5 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:26:26 +0000 Subject: [PATCH 1/4] fix(proofs): a pinned Agda receipt for DOM-1/2, PWG labels, and no silent proof skips MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 2026-11-09 proof audit found proof-burrower's proof claims inconsistent with each other and with PROOF-POLICY §2.1/§8: - CLAUDE.md said "0 of 7 obligations proven; nothing at Grade 3" while PROOF-STATUS said "2 of 14 proven; DOM-1/2 Grade 3". DOM-1/2 do check, but no receipt (commit, digests, import cone) and no CI job existed, so the grade could not be derived. Both now say: 2 of 14 proven, ungraded until a receipt exists. - New `agda` job in proof-safety.yml: Agda 2.7.0.1 and agda-stdlib 2.1, both digest-pinned (the same pins as echidna's agda-meta-checker), the canonical --safe --without-K --cubical-compatible flags, and a printed receipt (version, commit, SHA-256 of each first-party source). Its first green run on main makes DOM-1/2 PWG-3. It uses only the actions/checkout pin already listed for this workflow, so actions.lock is unchanged. - verification/proofs/agda/burrow.agda-lib added; before it, checking the modules needed an ad hoc `-l standard-library`. - The ladder in CLAUDE.md said "2ii = two, the second non-DTT"; §8 makes non-DTT a +foundation-diverse tag, not a grade. Replaced with the §8 PWG definitions. The Rust row names Creusot with Pearlite, and Verus (§1.2). - proof-debt.adoc §(c) said "No first-party proof exists"; DOM-1/2 do, and --safe rejects postulates. - `just proof-check-{idris2,lean4,agda,coq}` printed SKIP and exited 0 when the prover was missing — a silent green, which §2.1 and this repo's own rule forbid. They now exit 1 with NOT RUN. No workflow calls them. Checked locally: both modules type-check under the canonical flags on Agda 2.6.3 + stdlib 1.7.3 using the new .agda-lib; the workflow parses. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .github/workflows/proof-safety.yml | 43 ++++++++++++++++++++++++ CLAUDE.md | 21 ++++++++---- Justfile | 16 ++++----- docs/proof-debt.adoc | 4 ++- docs/status/PROOF-STATUS.adoc | 17 +++++++--- verification/proofs/agda/burrow.agda-lib | 5 +++ 6 files changed, 85 insertions(+), 21 deletions(-) create mode 100644 verification/proofs/agda/burrow.agda-lib diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index c276766..0ad4344 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -64,3 +64,46 @@ jobs: ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna run: | bash tests/e2e.sh + agda: + name: Agda proofs (PROOF-POLICY §2.1 canonical invocation) + runs-on: ubuntu-24.04 + timeout-minutes: 20 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - name: Install pinned, digest-checked Agda and standard library + run: | + set -euo pipefail + tc="$RUNNER_TEMP/agda" + mkdir -p "$tc" + curl --fail --location --retry 3 -o "$tc/agda.tar.xz" \ + https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz + echo "975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a $tc/agda.tar.xz" | sha256sum --check + curl --fail --location --retry 3 -o "$tc/stdlib.tar.gz" \ + https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz + echo "72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431 $tc/stdlib.tar.gz" | sha256sum --check + tar --no-same-owner -xJf "$tc/agda.tar.xz" -C "$tc" + tar --no-same-owner -xzf "$tc/stdlib.tar.gz" -C "$tc" + printf '%s\n' "$tc/agda-stdlib-2.1/standard-library.agda-lib" \ + "$GITHUB_WORKSPACE/verification/proofs/agda/burrow.agda-lib" > "$tc/libraries" + { + echo "Agda_datadir=$tc/Agda-v2.7.0.1/data" + echo "AGDA_LIBRARIES_FILE=$tc/libraries" + echo "LC_ALL=C.UTF-8" + } >> "$GITHUB_ENV" + echo "$tc/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH" + - name: Type-check DOM-1 and DOM-2 and print the receipt + working-directory: verification/proofs/agda + run: | + set -euo pipefail + agda --version + echo "commit: $GITHUB_SHA" + echo "flags: --safe --without-K --cubical-compatible" + echo "import cone (first-party):" + sha256sum Burrow/Trust.agda Burrow/Ledger.agda burrow.agda-lib + find . -name '*.agdai' -delete + for m in Burrow/Trust.agda Burrow/Ledger.agda; do + agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \ + --safe --without-K --cubical-compatible "$m" + done diff --git a/CLAUDE.md b/CLAUDE.md index dab6e6d..29c6bc5 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -45,7 +45,7 @@ file, not this summary. | Obligation | Verifier | |------------|----------| -| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot | +| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot with Pearlite contracts, and Verus (PROOF-POLICY §1.2) | | APIs, ABIs, wire formats, engineering properties | Idris2 | | Theory (anything true of any implementation) | Agda, rechecked in Rocq and Lean | @@ -53,10 +53,15 @@ file, not this summary. `agda --safe --without-K --cubical-compatible `. `--cubical-compatible` is not full `--cubical`. Pin and record the Agda version and standard library with each source commit and proof result. -- Grade ladder (Mathesis §5): Grade 3 = type-checks locally in Agda, - untranslated; 2i = one independent system; 2ii = two, the second - non-DTT (e.g. Isabelle/HOL); 1 = machine-checked via a verified checker - API in headless CI. Never flatten this into a confidence percentage. +- Proof Witness Grades (PROOF-POLICY §8, normative; always write the `PWG-` + prefix): `PWG-3` = the Agda source is checked under the §2.1 invocation + with a receipt (Agda version, stdlib pin, flags, import cone); + `PWG-2i` = plus one counted Rocq or Lean recheck (kernel-accepted and + §2.2 `RECONCILED`); `PWG-2ii` = plus both; `PWG-1` = every counted + witness has a current per-commit receipt from a headless, pinned run. + Engineering proofs (Creusot, Verus, SPARK, Idris2) carry no PWG (§8.1). + Grades are derived from receipts, never asserted, and never flattened + into a percentage. - Missing tools, incompatible dependencies or failed theorems are open obligations. Do not skip proofs or weaken flags to make a check green. - Escape hatches follow `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` and are @@ -64,7 +69,9 @@ file, not this summary. - An ECHIDNA result is *evidence about someone else's proof*. Burrower records the grade it was told and never asserts one it derived. -Status for this repo: 0 of 7 obligations proven; no first-party Agda -theorem yet, so nothing here is at Grade 3. See +Status for this repo: 2 of 14 tracked obligations proven (DOM-1, DOM-2, +first-party Agda). Both are `ungraded` until the `agda` job in +`.github/workflows/proof-safety.yml` has produced a receipt on `main`; +`PWG-3` follows from that receipt, not from this sentence. See `docs/status/PROOF-STATUS.adoc` and `docs/reports/audit/2026-11-01-echidna-topology-audit.adoc`. diff --git a/Justfile b/Justfile index b40ae3e..d562f6e 100644 --- a/Justfile +++ b/Justfile @@ -1351,8 +1351,8 @@ proof-check-idris2: set -euo pipefail echo "=== Checking Idris2 proofs ===" if ! command -v idris2 &>/dev/null; then - echo "SKIP: idris2 not installed" - exit 0 + echo "NOT RUN: idris2 not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2 + exit 1 fi ERRORS=0 for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do @@ -1376,8 +1376,8 @@ proof-check-lean4: set -euo pipefail echo "=== Checking Lean4 proofs ===" if ! command -v lean &>/dev/null; then - echo "SKIP: lean not installed" - exit 0 + echo "NOT RUN: lean not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2 + exit 1 fi ERRORS=0 for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do @@ -1401,8 +1401,8 @@ proof-check-agda: set -euo pipefail echo "=== Checking Agda proofs ===" if ! command -v agda &>/dev/null; then - echo "SKIP: agda not installed" - exit 0 + echo "NOT RUN: agda not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2 + exit 1 fi # Estate canonical invocation (standards 3-practice/PROOF-POLICY.adoc # §2.1). `--cubical-compatible` implies `--without-K`; both are named @@ -1441,8 +1441,8 @@ proof-check-coq: set -euo pipefail echo "=== Checking Coq proofs ===" if ! command -v coqc &>/dev/null; then - echo "SKIP: coqc not installed" - exit 0 + echo "NOT RUN: coqc not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2 + exit 1 fi ERRORS=0 for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 1420dc8..37bd89f 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -44,7 +44,9 @@ would be exactly the unfalsifiable "covered by tests" the policy rejects. - (none) -No first-party proof exists, so no first-party axiom exists. +The first-party proofs (DOM-1 `Burrow/Trust.agda`, DOM-2 +`Burrow/Ledger.agda`) check under `--safe`, which rejects `postulate`, so +no first-party axiom exists. == 1. Debt diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 0e51571..5e97f82 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -17,10 +17,17 @@ *Overall*: 2 of 14 tracked obligations proven. -Estate grade (`hyperpolymath/mathesis` §5): the two Domain proofs are -*Grade 3* — constructed in Agda and type-checked locally, not yet -translated to an independent foundational system. Nothing else in this -repository has a grade. +Proof Witness Grade (`PROOF-POLICY` §8, normative): the two Domain proofs +are `ungraded` until a receipt exists. A grade is derived from a receipt +that records the Agda version, the standard-library pin, the flags in +force and the import cone; the 2026-11-01 local run recorded the first +three but no source commit or digests. The `agda` job in +`.github/workflows/proof-safety.yml` (Agda 2.7.0.1 and agda-stdlib 2.1, +both digest-pinned; canonical §2.1 flags; prints the commit and the +SHA-256 of each first-party source) produces that receipt. The first green +run on `main` makes them `PWG-3`. No Rocq or Lean recheck exists, so +nothing can be higher. Nothing else in this repository is a theory +theorem, so nothing else carries a PWG. === Proofs Done @@ -122,7 +129,7 @@ panic-attack assail --proofs-only |=== |Date |Change |By |2026-04-04 |Initial proof status tracking |Template -|2026-11-01 |DOM-1 and DOM-2 proved in Agda (Grade 3); DOM-3..7 added; +|2026-11-01 |DOM-1 and DOM-2 proved in Agda (receipt pending; see above); DOM-3..7 added; `just proof-check-agda` moved to the estate canonical flags with an include path |Audit 2026-11-01 |=== diff --git a/verification/proofs/agda/burrow.agda-lib b/verification/proofs/agda/burrow.agda-lib new file mode 100644 index 0000000..f425fc0 --- /dev/null +++ b/verification/proofs/agda/burrow.agda-lib @@ -0,0 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Agda library for proof-burrower's first-party proofs (DOM-1, DOM-2). +name: burrow +depend: standard-library +include: . From 4e581423dbff7308e85811279c0200ee6ef446f9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:53:25 +0000 Subject: [PATCH 2/4] fix(proofs): full import cone in the Agda receipt; collect all proof checks Review follow-ups on the proof-honesty change: - proof-safety.yml: the receipt now records the stdlib archive digest and the transitive import cone (every interface the check wrote, stdlib and first-party). --safe is coinfective, so the whole cone was checked under it. curl is restricted to HTTPS, redirects included. - Justfile: proof-check-all runs every checker even after a failure, then fails naming each one that failed or did not run. - PROOF-STATUS, CLAUDE.md: the 2026-11-01 run is labelled historical; a PWG-3 grade needs a receipt for the current main commit and lapses if a later run fails. - proof-debt: the Grade 3 wording names the Mathesis grade; the "empty proof set" sentence now acknowledges DOM-1 and DOM-2. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .github/workflows/proof-safety.yml | 17 +- CLAUDE.md | 5 +- Justfile | 15 +- docs/proof-debt.adoc | 15 +- docs/status/PROOF-STATUS.adoc | 8 +- verification/proofs/coq/.TypeSafety.aux | 7 + verification/proofs/coq/TypeSafety.glob | 205 ++++++++++++++++++++++++ verification/proofs/coq/TypeSafety.vo | Bin 0 -> 32902 bytes verification/proofs/coq/TypeSafety.vok | 0 verification/proofs/coq/TypeSafety.vos | 0 10 files changed, 256 insertions(+), 16 deletions(-) create mode 100644 verification/proofs/coq/.TypeSafety.aux create mode 100644 verification/proofs/coq/TypeSafety.glob create mode 100644 verification/proofs/coq/TypeSafety.vo create mode 100644 verification/proofs/coq/TypeSafety.vok create mode 100644 verification/proofs/coq/TypeSafety.vos diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index 0ad4344..7e3b141 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -77,10 +77,10 @@ jobs: set -euo pipefail tc="$RUNNER_TEMP/agda" mkdir -p "$tc" - curl --fail --location --retry 3 -o "$tc/agda.tar.xz" \ + curl --proto '=https' --proto-redir '=https' --fail --location --retry 3 -o "$tc/agda.tar.xz" \ https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz echo "975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a $tc/agda.tar.xz" | sha256sum --check - curl --fail --location --retry 3 -o "$tc/stdlib.tar.gz" \ + curl --proto '=https' --proto-redir '=https' --fail --location --retry 3 -o "$tc/stdlib.tar.gz" \ https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz echo "72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431 $tc/stdlib.tar.gz" | sha256sum --check tar --no-same-owner -xJf "$tc/agda.tar.xz" -C "$tc" @@ -100,10 +100,19 @@ jobs: agda --version echo "commit: $GITHUB_SHA" echo "flags: --safe --without-K --cubical-compatible" - echo "import cone (first-party):" + echo "stdlib: agda-stdlib v2.1, archive sha256 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431" + echo "first-party sources:" sha256sum Burrow/Trust.agda Burrow/Ledger.agda burrow.agda-lib - find . -name '*.agdai' -delete + stdlib="$RUNNER_TEMP/agda/agda-stdlib-2.1" + find . "$stdlib" -name '*.agdai' -delete for m in Burrow/Trust.agda Burrow/Ledger.agda; do agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \ --safe --without-K --cubical-compatible "$m" done + # The transitive import cone is exactly the set of interfaces this + # check wrote. --safe is coinfective, so every module in it was + # itself checked under --safe: no postulate, no unsafe pragma. + echo "import cone (standard-library modules, sources pinned by the archive digest):" + find "$stdlib" -name '*.agdai' | sed "s|.*/agda/||; s|^src/||; s|\.agdai$||; s|/|.|g" | LC_ALL=C sort + echo "import cone (first-party modules):" + find . -name '*.agdai' | sed "s|.*/agda/||; s|^src/||; s|\.agdai$||; s|/|.|g" | LC_ALL=C sort diff --git a/CLAUDE.md b/CLAUDE.md index 29c6bc5..68ceab6 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -71,7 +71,8 @@ file, not this summary. Status for this repo: 2 of 14 tracked obligations proven (DOM-1, DOM-2, first-party Agda). Both are `ungraded` until the `agda` job in -`.github/workflows/proof-safety.yml` has produced a receipt on `main`; -`PWG-3` follows from that receipt, not from this sentence. See +`.github/workflows/proof-safety.yml` has produced a receipt for the current +`main` commit; `PWG-3` follows from that receipt, not from this sentence, and +lapses if a later run on `main` fails or cannot be reproduced. See `docs/status/PROOF-STATUS.adoc` and `docs/reports/audit/2026-11-01-echidna-topology-audit.adoc`. diff --git a/Justfile b/Justfile index d562f6e..e9bf0a0 100644 --- a/Justfile +++ b/Justfile @@ -1342,8 +1342,19 @@ help-me: # ═══════════════════════════════════════════════════════════════════════════════ # Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous - @echo "=== All proof checks complete ===" +# Runs every checker even when an earlier one fails, then fails if any did. +proof-check-all: + #!/usr/bin/env bash + set -uo pipefail + failed=() + for r in proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous; do + just "$r" || failed+=("$r") + done + if [ ${#failed[@]} -gt 0 ]; then + echo "=== Proof checks FAILED or NOT RUN: ${failed[*]} ===" >&2 + exit 1 + fi + echo "=== All proof checks complete ===" # Check Idris2 proofs (ABI, types, dependent type proofs) proof-check-idris2: diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 37bd89f..daeb4cb 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -22,9 +22,11 @@ reading of the situation. == (a) Discharged in this repo - `verification/proofs/agda/Burrow/Trust.agda` — the receipt/warrant - semantics (DOM-1). Grade 3: type-checks under + semantics (DOM-1). Mathesis Grade 3 on a historical local run: type-checks under `agda --safe --without-K --cubical-compatible`, 0 warnings, also clean - under full `--cubical`. Agda 2.7.0.1, agda-stdlib 2.4, 2026-11-01. + under full `--cubical`. Agda 2.7.0.1, agda-stdlib 2.4, 2026-11-01. Under + PROOF-POLICY §8 it is `ungraded` until the CI `agda` job (stdlib 2.1) + records a receipt for the current commit. - `verification/proofs/agda/Burrow/Ledger.agda` — the ledger read path and `no-launder` (DOM-2). Same toolchain, same flags, same date. @@ -144,12 +146,15 @@ already retired for `TODO` markers — "grepping prose … measures the prose, not the proofs" — and it should be reported upstream rather than triaged here. -The absence of markers is not a clean bill of health. It reflects an empty -proof set: there is nothing to have escaped from. +The absence of markers is not a clean bill of health. The only proofs are +DOM-1 and DOM-2 in §(a), both under `--safe`, which rejects every marker the +scan looks for; the markers say nothing about the twelve obligations that +have no proof at all. == 3. What a Grade 3 result would look like here -Mathesis §5: "A proof is Grade 3 if it type-checks locally in Agda but has +This section uses the Mathesis grade, not the Proof Witness Grade of +PROOF-POLICY §8 (`PWG-3`), which needs a CI receipt as well. Mathesis §5: "A proof is Grade 3 if it type-checks locally in Agda but has not been translated to an independent foundational system." For this repository the shortest honest path is one theorem about Burrower's own contract handling, checked with: diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 5e97f82..c134211 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -25,7 +25,8 @@ three but no source commit or digests. The `agda` job in `.github/workflows/proof-safety.yml` (Agda 2.7.0.1 and agda-stdlib 2.1, both digest-pinned; canonical §2.1 flags; prints the commit and the SHA-256 of each first-party source) produces that receipt. The first green -run on `main` makes them `PWG-3`. No Rocq or Lean recheck exists, so +run on `main` makes them `PWG-3`, for as long as the receipt is current: +a later failing or unreproducible run on `main` withdraws the grade. No Rocq or Lean recheck exists, so nothing can be higher. Nothing else in this repository is a theory theorem, so nothing else carries a PWG. @@ -41,8 +42,9 @@ theorem, so nothing else carries a PWG. |Agda 2.7.0.1 |`verification/proofs/agda/Burrow/Trust.agda` |2026-11-01 -|`just proof-check-agda`, `agda --safe --without-K --cubical-compatible`, - 0 warnings; also clean under full `--cubical` +|Historical local run only (no commit or digests recorded): + `agda --safe --without-K --cubical-compatible`, 0 warnings; also clean + under full `--cubical`. Current verification is the CI receipt. |DOM-2 |Ledger read path: no function from a stored record to the fact exists diff --git a/verification/proofs/coq/.TypeSafety.aux b/verification/proofs/coq/.TypeSafety.aux new file mode 100644 index 0000000..d7e9ecb --- /dev/null +++ b/verification/proofs/coq/.TypeSafety.aux @@ -0,0 +1,7 @@ +COQAUX1 5a330d09e1171d55938427353b10d782 /home/user/proof-burrower/verification/proofs/coq/TypeSafety.v +0 0 VernacProof "tac:no using:no" +2143 2147 proof_build_time "0.018" +0 0 type_soundness "0.018" +2089 2142 context_used "" +2143 2147 proof_check_time "0.005" +0 0 vo_compile_time "0.211" diff --git a/verification/proofs/coq/TypeSafety.glob b/verification/proofs/coq/TypeSafety.glob new file mode 100644 index 0000000..768ed4f --- /dev/null +++ b/verification/proofs/coq/TypeSafety.glob @@ -0,0 +1,205 @@ +DIGEST 5a330d09e1171d55938427353b10d782 +FTypeSafety +R275:288 Coq.Lists.List <> <> lib +R306:320 Coq.Arith.Arith <> <> lib +R338:350 Coq.Bool.Bool <> <> lib +R360:372 Coq.Lists.List ListNotations <> mod +ind 530:531 <> ty +constr 547:551 <> TyNat +constr 563:568 <> TyBool +R556:557 TypeSafety <> ty:1 ind +R572:573 TypeSafety <> ty:1 ind +scheme 530:531 <> ty_rect +scheme 530:531 <> ty_ind +scheme 530:531 <> ty_rec +scheme 530:531 <> ty_sind +ind 606:609 <> expr +constr 625:630 <> EConst +constr 650:654 <> ETrue +constr 668:673 <> EFalse +constr 686:690 <> EPlus +constr 720:722 <> EEq +R637:640 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R634:636 Coq.Init.Datatypes <> nat ind +R641:644 TypeSafety <> expr:3 ind +R659:662 TypeSafety <> expr:3 ind +R677:680 TypeSafety <> expr:3 ind +R699:702 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R695:698 TypeSafety <> expr:3 ind +R707:710 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R703:706 TypeSafety <> expr:3 ind +R711:714 TypeSafety <> expr:3 ind +R733:736 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R729:732 TypeSafety <> expr:3 ind +R741:744 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R737:740 TypeSafety <> expr:3 ind +R745:748 TypeSafety <> expr:3 ind +scheme 606:609 <> expr_rect +scheme 606:609 <> expr_ind +scheme 606:609 <> expr_rec +scheme 606:609 <> expr_sind +ind 776:780 <> value +constr 796:799 <> VNat +constr 821:825 <> VBool +R807:810 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R804:806 Coq.Init.Datatypes <> nat ind +R811:815 TypeSafety <> value:5 ind +R833:836 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R829:832 Coq.Init.Datatypes <> bool ind +R837:841 TypeSafety <> value:5 ind +scheme 776:780 <> value_rect +scheme 776:780 <> value_ind +scheme 776:780 <> value_rec +scheme 776:780 <> value_sind +ind 878:885 <> has_type +constr 915:921 <> T_Const +constr 965:970 <> T_True +constr 1001:1007 <> T_False +constr 1038:1043 <> T_Plus +constr 1149:1152 <> T_Eq +R893:896 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R889:892 TypeSafety <> expr ind +R899:902 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R897:898 TypeSafety <> ty ind +binder 932:932 <> n:9 +R935:942 TypeSafety <> has_type:7 ind +R955:959 TypeSafety <> TyNat constr +R945:950 TypeSafety <> EConst constr +R952:952 TypeSafety <> n:9 var +R975:982 TypeSafety <> has_type:7 ind +R990:995 TypeSafety <> TyBool constr +R984:988 TypeSafety <> ETrue constr +R1011:1018 TypeSafety <> has_type:7 ind +R1027:1032 TypeSafety <> TyBool constr +R1020:1025 TypeSafety <> EFalse constr +binder 1055:1056 <> e1:10 +binder 1058:1059 <> e2:11 +R1085:1088 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1068:1075 TypeSafety <> has_type:7 ind +R1080:1084 TypeSafety <> TyNat constr +R1077:1078 TypeSafety <> e1:10 var +R1106:1115 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1089:1096 TypeSafety <> has_type:7 ind +R1101:1105 TypeSafety <> TyNat constr +R1098:1099 TypeSafety <> e2:11 var +R1116:1123 TypeSafety <> has_type:7 ind +R1139:1143 TypeSafety <> TyNat constr +R1126:1130 TypeSafety <> EPlus constr +R1132:1133 TypeSafety <> e1:10 var +R1135:1136 TypeSafety <> e2:11 var +binder 1166:1167 <> e1:12 +binder 1169:1170 <> e2:13 +R1196:1199 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1179:1186 TypeSafety <> has_type:7 ind +R1191:1195 TypeSafety <> TyNat constr +R1188:1189 TypeSafety <> e1:12 var +R1217:1226 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1200:1207 TypeSafety <> has_type:7 ind +R1212:1216 TypeSafety <> TyNat constr +R1209:1210 TypeSafety <> e2:13 var +R1227:1234 TypeSafety <> has_type:7 ind +R1248:1253 TypeSafety <> TyBool constr +R1237:1239 TypeSafety <> EEq constr +R1241:1242 TypeSafety <> e1:12 var +R1244:1245 TypeSafety <> e2:13 var +scheme 878:885 <> has_type_ind +scheme 878:885 <> has_type_sind +ind 1285:1288 <> eval +constr 1321:1327 <> E_Const +constr 1370:1375 <> E_True +constr 1408:1414 <> E_False +constr 1448:1453 <> E_Plus +constr 1572:1575 <> E_Eq +R1296:1299 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1292:1295 TypeSafety <> expr ind +R1305:1308 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1300:1304 TypeSafety <> value ind +binder 1338:1338 <> n:16 +R1341:1344 TypeSafety <> eval:14 ind +R1358:1361 TypeSafety <> VNat constr +R1363:1363 TypeSafety <> n:16 var +R1347:1352 TypeSafety <> EConst constr +R1354:1354 TypeSafety <> n:16 var +R1380:1383 TypeSafety <> eval:14 ind +R1392:1396 TypeSafety <> VBool constr +R1398:1401 Coq.Init.Datatypes <> true constr +R1385:1389 TypeSafety <> ETrue constr +R1418:1421 TypeSafety <> eval:14 ind +R1431:1435 TypeSafety <> VBool constr +R1437:1441 Coq.Init.Datatypes <> false constr +R1423:1428 TypeSafety <> EFalse constr +binder 1465:1466 <> e1:17 +binder 1468:1469 <> e2:18 +binder 1471:1472 <> n1:19 +binder 1474:1475 <> n2:20 +R1501:1504 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1484:1487 TypeSafety <> eval:14 ind +R1493:1496 TypeSafety <> VNat constr +R1498:1499 TypeSafety <> n1:19 var +R1489:1490 TypeSafety <> e1:17 var +R1522:1531 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1505:1508 TypeSafety <> eval:14 ind +R1514:1517 TypeSafety <> VNat constr +R1519:1520 TypeSafety <> n2:20 var +R1510:1511 TypeSafety <> e2:18 var +R1532:1535 TypeSafety <> eval:14 ind +R1552:1555 TypeSafety <> VNat constr +R1560:1562 Coq.Init.Peano <> ::nat_scope:x_'+'_x not +R1558:1559 TypeSafety <> n1:19 var +R1563:1564 TypeSafety <> n2:20 var +R1538:1542 TypeSafety <> EPlus constr +R1544:1545 TypeSafety <> e1:17 var +R1547:1548 TypeSafety <> e2:18 var +binder 1589:1590 <> e1:21 +binder 1592:1593 <> e2:22 +binder 1595:1596 <> n1:23 +binder 1598:1599 <> n2:24 +R1625:1628 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1608:1611 TypeSafety <> eval:14 ind +R1617:1620 TypeSafety <> VNat constr +R1622:1623 TypeSafety <> n1:23 var +R1613:1614 TypeSafety <> e1:21 var +R1646:1655 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R1629:1632 TypeSafety <> eval:14 ind +R1638:1641 TypeSafety <> VNat constr +R1643:1644 TypeSafety <> n2:24 var +R1634:1635 TypeSafety <> e2:22 var +R1656:1659 TypeSafety <> eval:14 ind +R1674:1678 TypeSafety <> VBool constr +R1681:1687 Coq.Arith.PeanoNat Nat eqb def +R1689:1690 TypeSafety <> n1:23 var +R1692:1693 TypeSafety <> n2:24 var +R1662:1664 TypeSafety <> EEq constr +R1666:1667 TypeSafety <> e1:21 var +R1669:1670 TypeSafety <> e2:22 var +scheme 1285:1288 <> eval_ind +scheme 1285:1288 <> eval_sind +def 1730:1743 <> value_has_type +R1750:1754 TypeSafety <> value ind +binder 1746:1746 <> v:25 +R1762:1763 TypeSafety <> ty ind +binder 1758:1758 <> t:26 +R1787:1787 TypeSafety <> t:26 var +R1784:1784 TypeSafety <> v:25 var +R1798:1801 TypeSafety <> VNat constr +R1806:1810 TypeSafety <> TyNat constr +R1817:1820 Coq.Init.Logic <> True ind +R1826:1830 TypeSafety <> VBool constr +R1835:1840 TypeSafety <> TyBool constr +R1845:1848 Coq.Init.Logic <> True ind +R1873:1877 Coq.Init.Logic <> False ind +prf 1971:1984 <> type_soundness +binder 1995:1995 <> e:29 +binder 1997:1997 <> t:30 +binder 1999:1999 <> v:31 +R2016:2019 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R2004:2011 TypeSafety <> has_type ind +R2013:2013 TypeSafety <> e:29 var +R2015:2015 TypeSafety <> t:30 var +R2028:2031 Coq.Init.Logic <> ::type_scope:x_'->'_x not +R2020:2023 TypeSafety <> eval ind +R2025:2025 TypeSafety <> e:29 var +R2027:2027 TypeSafety <> v:31 var +R2032:2045 TypeSafety <> value_has_type def +R2047:2047 TypeSafety <> v:31 var +R2049:2049 TypeSafety <> t:30 var diff --git a/verification/proofs/coq/TypeSafety.vo b/verification/proofs/coq/TypeSafety.vo new file mode 100644 index 0000000000000000000000000000000000000000..0a2917bb502a930684f2cf624333993d7a483e4e GIT binary patch literal 32902 zcmeHwd0!WsV^YTH1wB+B55uV5 zIUyx7B{m^G+3;%@ADd!S4M|AUtwBK@CvKayy_R2z(bw)**r53thF`~&$f%r^j3#wb zCro+w)!~uDS`MgCd%a;)>zFVsHdn2*opZnJ(yQn6DXWh8-fZz>bs!Cm1X9qF3+YSC z0{-r{vXy@LY=KWb>olKg82&v*$3(>r&53sA>i2)0H2%Vt5iRGQp3%P05yJ=wMXgbh zaXIU)7_fZTD`j@9-qIm6g-4fQ!>HLdW^811UUiQvpN02)u(HjUJqG=Lvh>*Jfx2_* zs39>)IYFj<_;xXM&eop28?Mm98+E>F7*#t*rsS++>(zJOJJ0Ss+%Tj><<|9^c!PDp z<5FUBR_b}J*n|b&1x&3`DC6SpA?p`_bzNg3;}de$+B&%5>8N)v&#JLw!RIIXSA54X zs`Spq48JWqre5k$>z@j{ls=h#Gv|CFc&#XMv>c+W>9~(x4?lE!Z%!mk$ z85)bJVNR0j&fM&d-Km(~?wPm zNzKimx!YbYu+pR5+Vs;U?+>j0=`)}|IXNjx1WP0e&rVU8yEgE6?M>$kU0eFv3r&l5 zDq$FbC{2xz#>{oCSD}4`U-X9Kew7NQm+E_D9!9A;>Lr_0+Rl6aHBlc5}+fBJ=IV&}%2gWS5!eKUOQ~xoycO4T{w) zHZb7aW%RjA5;&M=FSyg12I)tRR<6AIdVx=TuleEvPGFc|Af?Z?q?Yr zn}GS}4~5^O z-`u31g31M!=;$Xl7go>Yv1~qt!%P&gah}*)Dec)oR#v7KlzuV?+BsX%% zVJs%clO#9J7S|;@y63=B@!y?)HYqJ!hCWN!11&?6Q<5;XkQE7K1rsW_+|O<@_24JJ zcGxv&`ho8oczzE9qgLmBvMOY0ohM;U@K}H8?VnDxJKnuAef4Rvo6<3Jy10S!%+A|0 zk4%`k{-bRpx>)=J?qGrMEEC6#rolIvfv0SY7bC-G0Z^i5Dk&{8TY0u6}Q;XB8N*)jMa4z8m=898y~?I(J65 zd9#;Pxjp5ZqtfplsYBf9_nAUI?~d5i-s48gc^glDy8#AFKxb$_=s9O$L1GaMcw+5Y= z(5~queWpl>IV0U@+x)BZ-iL1_pQV%nFa5gWpQPPVyPAbQ!Spa zz9UU#mb%gOgOi_MzjUel?x7!FwEEtj&`Kyq(;#=+wknwBK4Yb<6y{Fr5`lwu3*_YlPw`0{gv$Ij7+-dsD^wbNsS+!m z&a%Mb58~b`yy0tXzdGiw^PFCD&8XqOHoSc4?!lLrAA&ek>6n|i4=Q}Vu>-~LK3zJ) zuRgxy>=BV=hN=D$l6^2sZDN3jV>Sj(SQ4&S8K05edg52&cI2Xp&x={QeKRSiO*GW#^kjf9{l1{@E&D zulZ`qoNe|aKiwFUJQ%%q$X6c1bv9}FovyXUqz3-7GCJkeHLzX+f@9-hK4S}*%ZUE? z#LQD)ygR(js&~G>v;O$;Ip{sAc1=je&eZVlnxp%#cKW>Kg4Nc$zxkecIOXEzk3g!U zZtjXfS5MAreC2cBXI|-@_}k=gbX|a=?f_qv1U#{x#*q z_Rp*LyOSX!^|*cWq}GdGd3b63vCZ4Gq?b~|{tj6$t$PfMhxO}D-|zM}KB`f5<+#7r zdM)k0>c$mm{kV1XB;4s8OMG|B-`4-bjCCzez0h!@3|B7e=t)h-+&+EnwTHVS+t>Cu zG&t$Lst9NaR~`Y?zAslDLmS`WWs_) z^HV;3v%|t#LV7NHM}>h+sX(3+7S8!znYc)Q))htd>AhdWq9i_{K^9_k-wyjrm0 zf?%Jy=CsOXb36&{$Qyeqhka(e`|Ye#Ju1Dm2^80K-K@AFsISE&yz^;;7apAaJ@apU3>M&+r>DkdK5Snkk+=e#B!7#R3$b(|yD6g}oVGs|h&G+TXa z#?emi7TH;RxX+%Lx;T}o)-PrZmgiiAoZmA4a+xlJ!%vP^&dfZK(iRp~zbMD@n7iu8 zI_GDv)Z4VXUH|%|?K{rEy!P*xAjd+vD<0qYp|{V4j^!TIUR+R_b$T17M-QBx%jvG; zjMw>_Lfo1~zijZ{wPJ9umPt`v1F$4;;%1 zj->KhBwCJ{TyJygiVaH-lpOVfXTlChgjwHQ)bnbP_VbcqSLapUUToRafa2ZSV-fOu zA~79$m#ffz)EH{r;rz;`pYB`+;HHQ@vBAE6T|Q5n{`<#$>dmT=bmY4lV2nd1ADyIM z-|))hs1XgPcj$gJEZTpmkAH*Ob@2&U|H2RHiG2Qk@_;$-zp}Bs<42;lwLLtFkN5Cs zG~L6a-n@*xIesO&XeF{(VTq=UOE2i*(cHs|yY4}(TaAUm!T1ef94rR^@Nwo@K8Uww zSPd$tQz_MZuCYf?BTroqF$|pw;qo$c9iP>@b(Ix0sVY@=R5MoTY53^DI;!f1Mb~u; zzGnRaWi1bj#j;mFuB%m&?|C2B1q!ca)yy+4KdQFl%48P9XmMT zW2f>|)=qUP#%2vAZ!p*>w6Lb*2R#oB=}cUKxT@ol?{YQ6rFwWMUPy~%<#k3{7}q}! zA3j9lLAV04Qv4v8{fu_m&v^6@Tv9IeOJ=2lQ~sXC<%dh!7*;T&uSNHj5u)Bu3t(hy zeDoteQX4yk(%6L-dcjWZNuy__H&n`OInvn@hYZpZL*UY~ubq0)Y?^0#Lj+_tMXOcE z9V?qg_3bp6JgK(H7C$Fjgd8V{4e>00kI0-42sVm0A^1Kk#7=gMdU8%`6YUgFs~2Ky zDcV9qkPNU;zf4M@jTpv_I;|wb;xddc$QFfX_CG1p;M%$?<4Wq6yVW^YY z*>%p&u7M7S89O@Zu~|e%f{*)$h2RI+lxksE*kk;|T1Unu$5acGEn?NMu*Bnb2vFA4 z%KMkos<55aqQ5>;V5c(RpC_r9kH;a|fGLt#7}K%{ zuA*64B^@PYbSmSlEt?yK@q=Qk;Sv$d0eV#5O0gc{fogt8@bbpy|QD zYOw&T%tC065KJb^qd880L-7fNa!pCPCi5{yCyUE`EOg7)n!!pXx*UobNk2%Hc%Ay$ z=$zFi^Rk;IjlRgF%Qm`X&dT1Hl`>E3>Nfh?%o!Zw$f>8>sX7g_(-^vLr~CM)GRll0VT{ z@|UHlCaY-G~Sfy}P!6jO&4z545w3bs-N!kKeAzT%42~9G^1y^%iq5`B&U0juM zd1qbD@1hB%9pS2)m3ks|w{3-7?aJW0^ign@c6pY52p=V1aES($XQz5{)u66*g%6^- zq;3;j@|RZ|Sz2k1rFD9`LCf?i*5A`~NCy;JpgC)DXf#%!(q_>otkj@M82n^Xsl2Iz zF{uG&rGTN*P9QjXZ~)1nidmUvr{(lDEAN@gn3bKhL9KV=Id4eeAV8f1ZBkF5vQpEq zLfNu%k}}L1rnY5evvW@8RJg1xv(pax1>|M2Qk`tL2hvLD-8U?>1jz!6o!+Crq4yxw zT2qmukV>e9 zr|=Oy4f)+1nMzkbv4qv4_xc4u!xuI!EK^If(qAY125vx+P%+WrP`MUMwysuNQw;|= zSX|H>jm&!!Xmvws21CEQ=ww!_!9+L7&ZU)EEh9R2j81i3)Ux-jl@J28J*y>KLoc&h z0yIAlIkK_J4$auo0@mI`Q88&hM5k8JRu3Iz?Sj)-^~|K_s3R0)N1d8bQz%I3OSWG0 z2W*{HY#l&75P4zH$^v{TR-du68bY;kZ$MRXuSpf{6hwnShG{fBQOk)YkxMib{xo?O zd#V^N(MqEE^0K9zT1hmFXe61*&OFg<&OAImrWr&-QGD|2mf=< zZ?%`5ER+B?Qe$+r59W6nbAFdJt&Z?)0Fd4+06FKjiWRRrf!}XB=C-M2L6+(VxLsR)D)Nl{kMu^MGL9uOX3T44U+5n_Vjt7(Jbs~BN^ z;Spkmv9bqpZ_ApPKTsvLWVcQ4=xGKkds$s;BTqcN&+2j;Hao1m!|DnMd6k&D=vi6w zsUDsx0B;Q&l{Q%2%<2w&d!95Kl{GLCwj&e0U&-n&I~8Zu&rU@!2~np3dEwrWykQqe z%?(tL)t$k?7Sogi(|!Qx7CKA>ovPsSMSsCyD(^^eU<-~`l{)5AO*~norlYvJBf((_ zY6+1Y&8HXe)K#bIV(^8AI_}x3L<^uc4O1AGp`I`7eoP@Mj{6E56`^7_YX<>Pl8UnCBMVY6EI>?CD{4fbs-3kk z*2anQ8xC9a4TH71tTjWEYIv-|T74@pj$m~o`qq`TX_@3r1u<_{>C~SF=ozMs_-Gw7 zzsk*g5Ze(7cp_`)`C*&26EQ( z2r7e={u!*bWNi>@y;vKJjDg5#gGazct9NN9*1X!t?@R^Jp_k|c?jwcC+7KFuo{ojF z$?9n8FTKVlxQS>Is8n^pe}||E=_Q&!pm(%JLYp)e9SF2O% zihh?mPODRNzrdB$smsNBbXuK~3M|1db=u+*{V&$0FD}vha!J0V&U~?;otMCq_Em8? z>3Le1PAk<3&uOI!jZQ07o?R_Z>5EvYl0Ord@WaVFu|{PL6sxrwE~)F^_tz&X6UD{#@>>XBbBDu@jA=dmc4Xe>a-2G@g z%+!1I67H}@zh(7TJ7M+s4N|X~7U4Z?3t1z25i7+5>?czkH7~RJkDV?7FiH#21;ExQ z0ngs_GM*V*wo%!d0tjM70|0daAl=H^rA(}PL!kj4>X>=&S=`b9=UCgzS^y0~hcnFS z{{;<@S)U=d9mZZ(3bRs>CgWd!`Bsz_FPe&fJwezpYJz)z!s4X$qqjk1J<7nnE;Yiv zCXA}N<|-U+a{M!s<60eXoC;%G(IY3nv9I@&W4Jt*WzAf8pm@w>Sqo>aHE{NXUB}uc zEX!e8%W{}wSq{rumcty&a+qUT)|j;cS<5nZ@Re{Faps^b%bF)E=gnnVQ?X{Al8rws zYD=08#~oNekay0JS2@@;uUU)1*mY)Ys4UmTy;V3(1J`KRr7xKi)Hay}tMS0A`<58X3h}qD(wd0;`JYWO2!ZA#y@u0o!G#)Op zwln*aWkMitSN10lL!z}2g6)Q@Awl?!El`9mmk~ir2^H;DYX2N`{jTW;q1L)oWo_lD7@be5b<#ADXAZk;CY4F+9X3J;xM|qXC`i zyyzY6AuvGaXy@g2(YVNJQ?X;OKp|2wd~DRFps0A(PBDGXbb#qorf<-x&tP<%rcMl1 zOV{xISO(Kc>c#Y zSDaS zo@Km5JB$~uEeC3%*K!#y{2T;*3R4P_sjM|&+6uMy7R|(c3r)uipGL3XJ{3A(D3ff8 zqD*zAlrhzzQj%#l+RkOA7^cZ|nuag05f(*lCNv`~AMF*iNdR;taV+J^b4;QnD=;lU z?M19Si|X^_pp0HOb!<8%QQ{*-G?PX`*FZhce83CD?jn;$(r`JU3)Sfm9nRCXd7`oz zDVr36jrFt6jH5lM*deUkgq|VU)crLhRb0DTgvQKu-qA>PfTjGxs<1`DJEo#5vk996#<@ zvtEs3y5c8?6>9OX#?6Phll9Y&S2gqKLM;*V@CI@LI1aFq9IzHK!!F?QfJH@c$%xI6 z^_F{OX+>r1leD5}75S6x68^G}$$aodG*@d}&SNq$_hkl4D%&V;T+$BT&7Ueo6N$+# z?fh^_JAp5G&Y9l;&rUd!FW+6u{}Wu<8VFqHR?QWzE1cYToc)(}uG=H2Ct6nE2(ACN zp7d!ZuH5j9i#R;h-mrus;eD16%zycn`*Dv-mr*zCP!ZQ5m)55(db-t8LvK>Lc!Sc# z0|NtP=fkHVlX5^7k(>bksQ8%VWT#Bd-;44Bg+%_pWv+BMkA>XG6wb1p~KZdoGw1tf6GWy7ub2kv=eXOWo6Y#XX(>;nVmL zK8^R%|926~(?QhtF&D9?aKn2#r^ToBwtOmA(f>7%$*1?Kdpe)Xf9;`~Z+G~A=YRfx z$G2ai0p!mM8{HS5(F3&7;Q19Cn* zRNZq2cGH#8-H1*9B23Z0kBRheBi*{(4Xoy-BbU1|$Fl4F=lEOhg(q_(9-6zZ+E3ws`?RjG`SOGN-}6w0ck{n?!!#XN zpThCEz}UxbWBhFY<+-+hCQ%s;9H!|O3x21Bn`V~SKwuy#@3=HI<@MEU(R7j5g?dPqyt-sA z(?f%WH4Z@gOmGKsgWIHsxm3a{62N)Vtdu4Bt1?(oUHE|a_Uef2d)|oD|?~Oqqs7db9Urc+$0M#(0tP zF&@kT*11^}K!GXNCs8ofl?RoDf@2N}vS!C1b9SH;-u>iqp#?KSXXUzMN`&I^nknxL zhrFBSQ=wp1Zo7~sqTgM|-y>>Gk?t#^kJpM!K`p#5cX6~HjG0kG{Mm9$jhD@eSz1+rVXZsYpp5nr<8a*bI#Ye;UHy|?P@?c*XBZQw!i zOipBY0oELq@6koI?75Q1;A!THRy38vYvfs^0md#lFpdJo=$shSvoO|W z@3HXn+BcHb^v5yA0NYSp!*ci0bs=EoS703Dz?dazi6*a8AS3{h^KzjBQui#YA3CJ2 zqR#3br_`zYol>WMY(5nUVfBdlR3emB=x$RRv-*V#(IS(L;M?fblSQneoQlS~R54{V z%ps#tS|~2EId^f_ytH!fytMKl_(=)2M;PBTL4IH=ML3W{HNKY{e5xLntI-Lw(J8a~ zG4p=HY?L(}Qt_TpA>GW$k{7K}*65vP?=-c{?6!SaYvh6ly0e|Znino_lRDPq4ftZ& zl$wGgWM_*|Q4+*OFUh^IV!|?~jf-V58bLrsr_`kyF49~V)af~?8|9#`SP}Mat`>@X z53duAdYn3_3C$cUq+z&P|5wyC6S|6(GpTFxh&oq$z)9Y42YFe7_>3utY!eT%- z3g)7l&HMZ2eUIF|qs{xU+$eAAVNO7m0m$bOpij)kN6h=z=KZ`0VybzcZUS-$tk>^& zb(>wdix(X0Wr@TW?DbHsajeuhWVzsW2rP_!CQm_$6vIUh;RPgzm`Xvmz!vim#6>lk<|}qgD|6EGNUs&G zEI5k4V3ud`yi3OX91yejRI;uVAIM$<)Rx`n;0@XjazYI=dnY}VUSW<+G-3Cbd(qZ% zFJk5tZVK?V4|iV_c4doC*DF4|p1U>k8%IPT^Yuu);pq6&4}KqB;`M&F5?9i?ly@HX z)$>uQqTR!T@4|)cZCs13Rs$;3H^vzZ#r40lFoUaP#XONpDUM211d)rfLJ>*!n5^uw z4sZM{*LsvxYb&ot>JB#|s*>$Z?DX-qhFF8mYV!KEvs#ep+2r&$Le!q3=4+AEB!?HP zsgKj}a(kdhCWR0JmNcdYb~tWODTB&e!yIkGa=kB{^;#u@j8qlEJVe4ys)I+) zH&dxWm6$}e`0*me^|TC{M?-B?+e)3_zYH&{3^>?~w6?QRSHmj*p#vPp(sXKwod|Wc zp<7krgLLYiNzLI`l|kz%%ti>1lqe-_#YH7BgI+f~vJ@SmS=P3;OzLc-dKt9KM!l_+ zZlk_d8hwaLXE8otXhe*};8$B@yjwZ#A|0UQOuSlt5M4iLc0D*)7!VA%T)Z+43CiZvGbjPCNYBRw-Av!mH`X>tB_@PMjchdDN{m=B)K7X1FEfzV)JB6c zXaN~i7aXtBwyqA>B8twSrL=;2IY^8Nj7c;%=SiyX?s`>0qam?|*3v43O0rQx27L>k z7)rOIpW6*<7sMkHQF$?guGpxHm4;h89Rj>%Hkz10H*M6@YV81Co8gis`#WH(K5N<& zApdEj2&=VYCf%nyHu}tfN5FWvDc`0CR1h!Ds}e=yhK;TnHri#SinP;4r}3O%rRp>z z6Mks)3%>3{35-hvTdA5gGm3r@3v&#z=6%oDwX?5Z-xtW*n56L&m8bIT>dg(VHtXVOI*9YEdo zRF>8rqScU;i>!2_^5{r6IPKl1Su%dCgfFz{bW;ZK~-`voJN4CwOiaMKGT@Y|a_sUYgnHc@X*|UehiH z952&zW`PGb&NR%p2&qIo0=Z+gHC-I#4);dI7awpL;MQdlz^~6FFZ2}dV2E`B$}E8R z67Z$aeSAYiC(J8kRR@x7j^TSdG!5m$Ss9J|9`w37i|gt5(h!x_A}x}`K~jl(mm3~LX0o6a>_>4P=qaLRS<&^HD~U_@yo%r z^E68bnI_lz(@by-4rnx6col&Uy&_MM_`t#CLqMKlwL*TwkymWD`97@3~Pp8--a%}+krT~zsydbzlZ_H(+6BF(P zM(hLR)WSX+0)uZ4fb4C=??F-=ksOfoow@k2a?p~7t!gJ$7TJjLgs>DEVEfrv^+oN< z=odPB10B1Djsa+2Rv}WSfaXhpIqAp=V#OahXOVLnIbp2UXT=5>h!UY3kr}Uc4^GqJ z6)p@>pOIc*6I%wXeTX*SqfIQU1rclqIs1@v1vxz>n254K>J~uOkH{L$$}Wf;D3WzmBSkW%5#K~A!M3c^F@&R49hJ*fix`KOcx{Cby zhP5|M0F&tweJ4E#GnHy9R+_U45$Gp4+pzjA5(xeUBsg}NhXnq&aA8v+jZKlfz{(5A zguJVRf$9nY)DC3SMMe}dzMyYl90;2s?dmY({3Ox2-UI#9LFYBlf15so=dXf}!ATi@ z$%wC_yejm!K#K&l_?GsNFM)IOutwh#Scuf{7m^=Xg_Dx{BI@B}1c4h==-Wfc0SnZz z$hnI6Kde^6w|5Qb16pmsn;54@$XIUJ=zZ*K8D32``T)hZS^Wq=;eo7vg?dW?98|8k z&#GZ639W>QcrM_-iaK*}+JT&FtQfRQM@%1634AQ%q1izs+fZu(YL#OZ^Bex>Y9eJw z`8z0Bf`aG7CsTO~)yE*G+(p)W;cG=$JuvG*{`;aoSF!RNtGi8kejn9VqG2^0v?0zA zKux5j0&y=fproO=DxhHILq8x;g(o;|iq&cG^pME#E3hEHFe&sfAwuJ*TL7^hG!#An zHJhdj#G}NxOGme(*jI|x2;exu>Pc~%SL*{2#Qp#bGWd1hX3d|KkKx`~1K}s&KvoJz zJ;lMs8xBumwrJ`5A>$LX@$MQYGdeSR{xMWjw)E4hX_3%n=ATWQ%n*5R76vU2W(AfKKxE_$ z13d|*rz&Edbr5~76@n(GNvyoc$`~}%Qdmnwf?z!oZAUtB3t&>gA*eZm#ilZAt-$RP z2oiu_P7tpLYK~HY`UeEHK!PX-6JV?Pn>%1c$V6vQs}HL`A~&#I+pK(yW`C6RLD^u| zFe^1V^xiHZ1DuV;*wf-sVK`!*xHLwPP1Z)BY#7QSS-p&v12m69&IriBO+@NIha12b zwytB2t!8ZwWC5+7L!FA~5OSdKmEQmWk(m%CK|?eI%@-wB)}Zp=W;H`+4e_w>eSk1V zID#Y$)u8INZLC3ypF@r(a%v%G8Eb@KC{nj0vVxEW4n6<}J<&19qA!RN6};mj{C^>? zth8nIbz~GqIm8W7DSERy92xyEsWe0((3%4XRB#K-OnjS&&LMb2Eg?o-EPTa^strO3 zv^v7esEg1RN0I6;=mScy)@u0qLC9Eu*(sC_Lskc5VZyC|LI6e8(FQg!;w7l7WU*8; zs2;e^5)=z7B?v)iCankB?1!3Q^?Oz^!pTrgCiY|$_D11(Ob&vPqBTTDKV%#>?G%w` z4T@76ge+)Qv?~szvh-d6QmE1~tVTmeQW$HKv4WsrnjppgKpToSUqTDB`ln1B4a@r; z%o!D23TL&OtfLTcEzaEf#{^-#M0Tpg)W?%(^8T#Jr0vTZ)TA~aO^|eleT7803uUf7 zV6_Wyb}_6yuxU);w$K|8Tx|56=8p&A8Sz3`645%8X-I# zm0&6gscUDNR#X}ppu|++8Yc5ZSXJ6&xlMsRMR0Vlz;fuzR7pM%2(>jx8EII1!OlS_ z6#!ofw3VfoYF!)fy^E}9;H!!c@C7jW0bhgzUkzjc-#$}jzd?vIK_#Y~CZ-(KH9sVe z_2r}0h3aB;GK8uxJ%io>_Ew;4z}lPmsZ=_C3|Uar)C7UVV9$X7D{Ci_xf7YqAc@w# z_|hE&wX|YqK_NKB#Mpg^Oc>Spil}agU7`Yywig*N-ZVrM!7^uvLeZL8CCC>HK-rm5 zHIRg_>+#hGES`)hjK{);bqH&_LCqGb2pLDq+f)XC;()e~6>}0M6ZHd@b;vveEMTIx zO|Yy+UAXlRu?_~WT<3;|4H3}g@AOi1FO>}h*&WKG! zBY;R$)d7K-378XE!^Fb|ivU;xvrs#Of>7f#EPH@^l3)ZXRcW*U{?$O2`%+~nYhS>CBBU{h zvW^D-NQ0Xo2~+iBWDgZ6h^L7*^fnW$OQkYeOh?gFgZyzy#W>Z%t)SGo3sJg4?=e+D z(4E(V5%aM#Ba-Sw>p+T@j`U(o1G#@7cj_%4^#CS6CbbqI3qMQ(*e}!^AM9q2GwqeI zs{{)I)(H;spr*kj^ko3V8wsKwRYc}@pa3e6ARhba2r^(NP#7}afyQ9yPGns}Ry$;U z4ikz#ImC#0%-RtQEesbZ-?t$Aw2N`@fv8Ln4+GAy23OT#K^$E2x5?f;|cXI%zETb#C8h>?*S_m-Wr{0nP?QU zOaH*3ok&)q!c;^CD8#f8>o0PER;+tki;|frDT*NmAF)sE1N2yS$m=3A;(|bxtz_+I zloiHF5Tc5(wg+D_z;GIc6C%_+0hU1DK#*XPAtcWZS!rlHN)`h$#vI(&p25)^a#LC9 zVG@SY6dDgh_d%CD@Q#k8P6rVm*=j@J7H9n79?RGn!*Yj;c(`_W`Q zfMA7vpI~&+G*-F@^iNQ*83lErG%%2WJ_|Xu03F)$Bi1lCic@2zW2{{O^b-R8HO6rw zLZ_Ty#P5WFuVxJ$Uk;TZ(m7pvc?t z8OaQ7j1xN^0Mhm{7e=y&SyslsShFKRMkbO8z<3@Qp>GG04>Gsn02=v|k$(yK!&z%f zl@GC4>9hqs0BDFfCom)W2yHOeJ5EA|4jB~bWIx6^Q5w?)xm`32=5g|&M0p%QU|t3g*g!Nx;*CszNB}Edg*^|-zA&ez(iCPnT5fkNc??^L(gey|=Ghf* zV%~t}3((dIjR%uhX$aB5LaswZkzn^2gu+QEq`A`YT~;vrL=aXWf0;DG_NgY7!kXOy zpn!ofBA61GHqzh#j Date: Mon, 9 Nov 2026 14:56:46 +0000 Subject: [PATCH 3/4] chore(proofs): drop committed Coq build artefacts and ignore them 4e58142 picked up TypeSafety.{vo,vok,vos,glob} and .TypeSafety.aux from a local proof-check-all run. They are build output, not sources. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .gitignore | 7 + verification/proofs/coq/.TypeSafety.aux | 7 - verification/proofs/coq/TypeSafety.glob | 205 ------------------------ verification/proofs/coq/TypeSafety.vo | Bin 32902 -> 0 bytes verification/proofs/coq/TypeSafety.vok | 0 verification/proofs/coq/TypeSafety.vos | 0 6 files changed, 7 insertions(+), 212 deletions(-) delete mode 100644 verification/proofs/coq/.TypeSafety.aux delete mode 100644 verification/proofs/coq/TypeSafety.glob delete mode 100644 verification/proofs/coq/TypeSafety.vo delete mode 100644 verification/proofs/coq/TypeSafety.vok delete mode 100644 verification/proofs/coq/TypeSafety.vos diff --git a/.gitignore b/.gitignore index 4ce862d..2161e8e 100644 --- a/.gitignore +++ b/.gitignore @@ -118,3 +118,10 @@ dist/ /exports/*.lgt composer/*.beam composer/build/ + +# Coq/Rocq build artefacts (written by `just proof-check-coq`) +*.vo +*.vok +*.vos +*.glob +.*.aux diff --git a/verification/proofs/coq/.TypeSafety.aux b/verification/proofs/coq/.TypeSafety.aux deleted file mode 100644 index d7e9ecb..0000000 --- a/verification/proofs/coq/.TypeSafety.aux +++ /dev/null @@ -1,7 +0,0 @@ -COQAUX1 5a330d09e1171d55938427353b10d782 /home/user/proof-burrower/verification/proofs/coq/TypeSafety.v -0 0 VernacProof "tac:no using:no" -2143 2147 proof_build_time "0.018" -0 0 type_soundness "0.018" -2089 2142 context_used "" -2143 2147 proof_check_time "0.005" -0 0 vo_compile_time "0.211" diff --git a/verification/proofs/coq/TypeSafety.glob b/verification/proofs/coq/TypeSafety.glob deleted file mode 100644 index 768ed4f..0000000 --- a/verification/proofs/coq/TypeSafety.glob +++ /dev/null @@ -1,205 +0,0 @@ -DIGEST 5a330d09e1171d55938427353b10d782 -FTypeSafety -R275:288 Coq.Lists.List <> <> lib -R306:320 Coq.Arith.Arith <> <> lib -R338:350 Coq.Bool.Bool <> <> lib -R360:372 Coq.Lists.List ListNotations <> mod -ind 530:531 <> ty -constr 547:551 <> TyNat -constr 563:568 <> TyBool -R556:557 TypeSafety <> ty:1 ind -R572:573 TypeSafety <> ty:1 ind -scheme 530:531 <> ty_rect -scheme 530:531 <> ty_ind -scheme 530:531 <> ty_rec -scheme 530:531 <> ty_sind -ind 606:609 <> expr -constr 625:630 <> EConst -constr 650:654 <> ETrue -constr 668:673 <> EFalse -constr 686:690 <> EPlus -constr 720:722 <> EEq -R637:640 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R634:636 Coq.Init.Datatypes <> nat ind -R641:644 TypeSafety <> expr:3 ind -R659:662 TypeSafety <> expr:3 ind -R677:680 TypeSafety <> expr:3 ind -R699:702 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R695:698 TypeSafety <> expr:3 ind -R707:710 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R703:706 TypeSafety <> expr:3 ind -R711:714 TypeSafety <> expr:3 ind -R733:736 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R729:732 TypeSafety <> expr:3 ind -R741:744 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R737:740 TypeSafety <> expr:3 ind -R745:748 TypeSafety <> expr:3 ind -scheme 606:609 <> expr_rect -scheme 606:609 <> expr_ind -scheme 606:609 <> expr_rec -scheme 606:609 <> expr_sind -ind 776:780 <> value -constr 796:799 <> VNat -constr 821:825 <> VBool -R807:810 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R804:806 Coq.Init.Datatypes <> nat ind -R811:815 TypeSafety <> value:5 ind -R833:836 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R829:832 Coq.Init.Datatypes <> bool ind -R837:841 TypeSafety <> value:5 ind -scheme 776:780 <> value_rect -scheme 776:780 <> value_ind -scheme 776:780 <> value_rec -scheme 776:780 <> value_sind -ind 878:885 <> has_type -constr 915:921 <> T_Const -constr 965:970 <> T_True -constr 1001:1007 <> T_False -constr 1038:1043 <> T_Plus -constr 1149:1152 <> T_Eq -R893:896 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R889:892 TypeSafety <> expr ind -R899:902 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R897:898 TypeSafety <> ty ind -binder 932:932 <> n:9 -R935:942 TypeSafety <> has_type:7 ind -R955:959 TypeSafety <> TyNat constr -R945:950 TypeSafety <> EConst constr -R952:952 TypeSafety <> n:9 var -R975:982 TypeSafety <> has_type:7 ind -R990:995 TypeSafety <> TyBool constr -R984:988 TypeSafety <> ETrue constr -R1011:1018 TypeSafety <> has_type:7 ind -R1027:1032 TypeSafety <> TyBool constr -R1020:1025 TypeSafety <> EFalse constr -binder 1055:1056 <> e1:10 -binder 1058:1059 <> e2:11 -R1085:1088 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1068:1075 TypeSafety <> has_type:7 ind -R1080:1084 TypeSafety <> TyNat constr -R1077:1078 TypeSafety <> e1:10 var -R1106:1115 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1089:1096 TypeSafety <> has_type:7 ind -R1101:1105 TypeSafety <> TyNat constr -R1098:1099 TypeSafety <> e2:11 var -R1116:1123 TypeSafety <> has_type:7 ind -R1139:1143 TypeSafety <> TyNat constr -R1126:1130 TypeSafety <> EPlus constr -R1132:1133 TypeSafety <> e1:10 var -R1135:1136 TypeSafety <> e2:11 var -binder 1166:1167 <> e1:12 -binder 1169:1170 <> e2:13 -R1196:1199 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1179:1186 TypeSafety <> has_type:7 ind -R1191:1195 TypeSafety <> TyNat constr -R1188:1189 TypeSafety <> e1:12 var -R1217:1226 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1200:1207 TypeSafety <> has_type:7 ind -R1212:1216 TypeSafety <> TyNat constr -R1209:1210 TypeSafety <> e2:13 var -R1227:1234 TypeSafety <> has_type:7 ind -R1248:1253 TypeSafety <> TyBool constr -R1237:1239 TypeSafety <> EEq constr -R1241:1242 TypeSafety <> e1:12 var -R1244:1245 TypeSafety <> e2:13 var -scheme 878:885 <> has_type_ind -scheme 878:885 <> has_type_sind -ind 1285:1288 <> eval -constr 1321:1327 <> E_Const -constr 1370:1375 <> E_True -constr 1408:1414 <> E_False -constr 1448:1453 <> E_Plus -constr 1572:1575 <> E_Eq -R1296:1299 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1292:1295 TypeSafety <> expr ind -R1305:1308 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1300:1304 TypeSafety <> value ind -binder 1338:1338 <> n:16 -R1341:1344 TypeSafety <> eval:14 ind -R1358:1361 TypeSafety <> VNat constr -R1363:1363 TypeSafety <> n:16 var -R1347:1352 TypeSafety <> EConst constr -R1354:1354 TypeSafety <> n:16 var -R1380:1383 TypeSafety <> eval:14 ind -R1392:1396 TypeSafety <> VBool constr -R1398:1401 Coq.Init.Datatypes <> true constr -R1385:1389 TypeSafety <> ETrue constr -R1418:1421 TypeSafety <> eval:14 ind -R1431:1435 TypeSafety <> VBool constr -R1437:1441 Coq.Init.Datatypes <> false constr -R1423:1428 TypeSafety <> EFalse constr -binder 1465:1466 <> e1:17 -binder 1468:1469 <> e2:18 -binder 1471:1472 <> n1:19 -binder 1474:1475 <> n2:20 -R1501:1504 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1484:1487 TypeSafety <> eval:14 ind -R1493:1496 TypeSafety <> VNat constr -R1498:1499 TypeSafety <> n1:19 var -R1489:1490 TypeSafety <> e1:17 var -R1522:1531 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1505:1508 TypeSafety <> eval:14 ind -R1514:1517 TypeSafety <> VNat constr -R1519:1520 TypeSafety <> n2:20 var -R1510:1511 TypeSafety <> e2:18 var -R1532:1535 TypeSafety <> eval:14 ind -R1552:1555 TypeSafety <> VNat constr -R1560:1562 Coq.Init.Peano <> ::nat_scope:x_'+'_x not -R1558:1559 TypeSafety <> n1:19 var -R1563:1564 TypeSafety <> n2:20 var -R1538:1542 TypeSafety <> EPlus constr -R1544:1545 TypeSafety <> e1:17 var -R1547:1548 TypeSafety <> e2:18 var -binder 1589:1590 <> e1:21 -binder 1592:1593 <> e2:22 -binder 1595:1596 <> n1:23 -binder 1598:1599 <> n2:24 -R1625:1628 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1608:1611 TypeSafety <> eval:14 ind -R1617:1620 TypeSafety <> VNat constr -R1622:1623 TypeSafety <> n1:23 var -R1613:1614 TypeSafety <> e1:21 var -R1646:1655 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R1629:1632 TypeSafety <> eval:14 ind -R1638:1641 TypeSafety <> VNat constr -R1643:1644 TypeSafety <> n2:24 var -R1634:1635 TypeSafety <> e2:22 var -R1656:1659 TypeSafety <> eval:14 ind -R1674:1678 TypeSafety <> VBool constr -R1681:1687 Coq.Arith.PeanoNat Nat eqb def -R1689:1690 TypeSafety <> n1:23 var -R1692:1693 TypeSafety <> n2:24 var -R1662:1664 TypeSafety <> EEq constr -R1666:1667 TypeSafety <> e1:21 var -R1669:1670 TypeSafety <> e2:22 var -scheme 1285:1288 <> eval_ind -scheme 1285:1288 <> eval_sind -def 1730:1743 <> value_has_type -R1750:1754 TypeSafety <> value ind -binder 1746:1746 <> v:25 -R1762:1763 TypeSafety <> ty ind -binder 1758:1758 <> t:26 -R1787:1787 TypeSafety <> t:26 var -R1784:1784 TypeSafety <> v:25 var -R1798:1801 TypeSafety <> VNat constr -R1806:1810 TypeSafety <> TyNat constr -R1817:1820 Coq.Init.Logic <> True ind -R1826:1830 TypeSafety <> VBool constr -R1835:1840 TypeSafety <> TyBool constr -R1845:1848 Coq.Init.Logic <> True ind -R1873:1877 Coq.Init.Logic <> False ind -prf 1971:1984 <> type_soundness -binder 1995:1995 <> e:29 -binder 1997:1997 <> t:30 -binder 1999:1999 <> v:31 -R2016:2019 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R2004:2011 TypeSafety <> has_type ind -R2013:2013 TypeSafety <> e:29 var -R2015:2015 TypeSafety <> t:30 var -R2028:2031 Coq.Init.Logic <> ::type_scope:x_'->'_x not -R2020:2023 TypeSafety <> eval ind -R2025:2025 TypeSafety <> e:29 var -R2027:2027 TypeSafety <> v:31 var -R2032:2045 TypeSafety <> value_has_type def -R2047:2047 TypeSafety <> v:31 var -R2049:2049 TypeSafety <> t:30 var diff --git a/verification/proofs/coq/TypeSafety.vo b/verification/proofs/coq/TypeSafety.vo deleted file mode 100644 index 0a2917bb502a930684f2cf624333993d7a483e4e..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 32902 zcmeHwd0!WsV^YTH1wB+B55uV5 zIUyx7B{m^G+3;%@ADd!S4M|AUtwBK@CvKayy_R2z(bw)**r53thF`~&$f%r^j3#wb zCro+w)!~uDS`MgCd%a;)>zFVsHdn2*opZnJ(yQn6DXWh8-fZz>bs!Cm1X9qF3+YSC z0{-r{vXy@LY=KWb>olKg82&v*$3(>r&53sA>i2)0H2%Vt5iRGQp3%P05yJ=wMXgbh zaXIU)7_fZTD`j@9-qIm6g-4fQ!>HLdW^811UUiQvpN02)u(HjUJqG=Lvh>*Jfx2_* zs39>)IYFj<_;xXM&eop28?Mm98+E>F7*#t*rsS++>(zJOJJ0Ss+%Tj><<|9^c!PDp z<5FUBR_b}J*n|b&1x&3`DC6SpA?p`_bzNg3;}de$+B&%5>8N)v&#JLw!RIIXSA54X zs`Spq48JWqre5k$>z@j{ls=h#Gv|CFc&#XMv>c+W>9~(x4?lE!Z%!mk$ z85)bJVNR0j&fM&d-Km(~?wPm zNzKimx!YbYu+pR5+Vs;U?+>j0=`)}|IXNjx1WP0e&rVU8yEgE6?M>$kU0eFv3r&l5 zDq$FbC{2xz#>{oCSD}4`U-X9Kew7NQm+E_D9!9A;>Lr_0+Rl6aHBlc5}+fBJ=IV&}%2gWS5!eKUOQ~xoycO4T{w) zHZb7aW%RjA5;&M=FSyg12I)tRR<6AIdVx=TuleEvPGFc|Af?Z?q?Yr zn}GS}4~5^O z-`u31g31M!=;$Xl7go>Yv1~qt!%P&gah}*)Dec)oR#v7KlzuV?+BsX%% zVJs%clO#9J7S|;@y63=B@!y?)HYqJ!hCWN!11&?6Q<5;XkQE7K1rsW_+|O<@_24JJ zcGxv&`ho8oczzE9qgLmBvMOY0ohM;U@K}H8?VnDxJKnuAef4Rvo6<3Jy10S!%+A|0 zk4%`k{-bRpx>)=J?qGrMEEC6#rolIvfv0SY7bC-G0Z^i5Dk&{8TY0u6}Q;XB8N*)jMa4z8m=898y~?I(J65 zd9#;Pxjp5ZqtfplsYBf9_nAUI?~d5i-s48gc^glDy8#AFKxb$_=s9O$L1GaMcw+5Y= z(5~queWpl>IV0U@+x)BZ-iL1_pQV%nFa5gWpQPPVyPAbQ!Spa zz9UU#mb%gOgOi_MzjUel?x7!FwEEtj&`Kyq(;#=+wknwBK4Yb<6y{Fr5`lwu3*_YlPw`0{gv$Ij7+-dsD^wbNsS+!m z&a%Mb58~b`yy0tXzdGiw^PFCD&8XqOHoSc4?!lLrAA&ek>6n|i4=Q}Vu>-~LK3zJ) zuRgxy>=BV=hN=D$l6^2sZDN3jV>Sj(SQ4&S8K05edg52&cI2Xp&x={QeKRSiO*GW#^kjf9{l1{@E&D zulZ`qoNe|aKiwFUJQ%%q$X6c1bv9}FovyXUqz3-7GCJkeHLzX+f@9-hK4S}*%ZUE? z#LQD)ygR(js&~G>v;O$;Ip{sAc1=je&eZVlnxp%#cKW>Kg4Nc$zxkecIOXEzk3g!U zZtjXfS5MAreC2cBXI|-@_}k=gbX|a=?f_qv1U#{x#*q z_Rp*LyOSX!^|*cWq}GdGd3b63vCZ4Gq?b~|{tj6$t$PfMhxO}D-|zM}KB`f5<+#7r zdM)k0>c$mm{kV1XB;4s8OMG|B-`4-bjCCzez0h!@3|B7e=t)h-+&+EnwTHVS+t>Cu zG&t$Lst9NaR~`Y?zAslDLmS`WWs_) z^HV;3v%|t#LV7NHM}>h+sX(3+7S8!znYc)Q))htd>AhdWq9i_{K^9_k-wyjrm0 zf?%Jy=CsOXb36&{$Qyeqhka(e`|Ye#Ju1Dm2^80K-K@AFsISE&yz^;;7apAaJ@apU3>M&+r>DkdK5Snkk+=e#B!7#R3$b(|yD6g}oVGs|h&G+TXa z#?emi7TH;RxX+%Lx;T}o)-PrZmgiiAoZmA4a+xlJ!%vP^&dfZK(iRp~zbMD@n7iu8 zI_GDv)Z4VXUH|%|?K{rEy!P*xAjd+vD<0qYp|{V4j^!TIUR+R_b$T17M-QBx%jvG; zjMw>_Lfo1~zijZ{wPJ9umPt`v1F$4;;%1 zj->KhBwCJ{TyJygiVaH-lpOVfXTlChgjwHQ)bnbP_VbcqSLapUUToRafa2ZSV-fOu zA~79$m#ffz)EH{r;rz;`pYB`+;HHQ@vBAE6T|Q5n{`<#$>dmT=bmY4lV2nd1ADyIM z-|))hs1XgPcj$gJEZTpmkAH*Ob@2&U|H2RHiG2Qk@_;$-zp}Bs<42;lwLLtFkN5Cs zG~L6a-n@*xIesO&XeF{(VTq=UOE2i*(cHs|yY4}(TaAUm!T1ef94rR^@Nwo@K8Uww zSPd$tQz_MZuCYf?BTroqF$|pw;qo$c9iP>@b(Ix0sVY@=R5MoTY53^DI;!f1Mb~u; zzGnRaWi1bj#j;mFuB%m&?|C2B1q!ca)yy+4KdQFl%48P9XmMT zW2f>|)=qUP#%2vAZ!p*>w6Lb*2R#oB=}cUKxT@ol?{YQ6rFwWMUPy~%<#k3{7}q}! zA3j9lLAV04Qv4v8{fu_m&v^6@Tv9IeOJ=2lQ~sXC<%dh!7*;T&uSNHj5u)Bu3t(hy zeDoteQX4yk(%6L-dcjWZNuy__H&n`OInvn@hYZpZL*UY~ubq0)Y?^0#Lj+_tMXOcE z9V?qg_3bp6JgK(H7C$Fjgd8V{4e>00kI0-42sVm0A^1Kk#7=gMdU8%`6YUgFs~2Ky zDcV9qkPNU;zf4M@jTpv_I;|wb;xddc$QFfX_CG1p;M%$?<4Wq6yVW^YY z*>%p&u7M7S89O@Zu~|e%f{*)$h2RI+lxksE*kk;|T1Unu$5acGEn?NMu*Bnb2vFA4 z%KMkos<55aqQ5>;V5c(RpC_r9kH;a|fGLt#7}K%{ zuA*64B^@PYbSmSlEt?yK@q=Qk;Sv$d0eV#5O0gc{fogt8@bbpy|QD zYOw&T%tC065KJb^qd880L-7fNa!pCPCi5{yCyUE`EOg7)n!!pXx*UobNk2%Hc%Ay$ z=$zFi^Rk;IjlRgF%Qm`X&dT1Hl`>E3>Nfh?%o!Zw$f>8>sX7g_(-^vLr~CM)GRll0VT{ z@|UHlCaY-G~Sfy}P!6jO&4z545w3bs-N!kKeAzT%42~9G^1y^%iq5`B&U0juM zd1qbD@1hB%9pS2)m3ks|w{3-7?aJW0^ign@c6pY52p=V1aES($XQz5{)u66*g%6^- zq;3;j@|RZ|Sz2k1rFD9`LCf?i*5A`~NCy;JpgC)DXf#%!(q_>otkj@M82n^Xsl2Iz zF{uG&rGTN*P9QjXZ~)1nidmUvr{(lDEAN@gn3bKhL9KV=Id4eeAV8f1ZBkF5vQpEq zLfNu%k}}L1rnY5evvW@8RJg1xv(pax1>|M2Qk`tL2hvLD-8U?>1jz!6o!+Crq4yxw zT2qmukV>e9 zr|=Oy4f)+1nMzkbv4qv4_xc4u!xuI!EK^If(qAY125vx+P%+WrP`MUMwysuNQw;|= zSX|H>jm&!!Xmvws21CEQ=ww!_!9+L7&ZU)EEh9R2j81i3)Ux-jl@J28J*y>KLoc&h z0yIAlIkK_J4$auo0@mI`Q88&hM5k8JRu3Iz?Sj)-^~|K_s3R0)N1d8bQz%I3OSWG0 z2W*{HY#l&75P4zH$^v{TR-du68bY;kZ$MRXuSpf{6hwnShG{fBQOk)YkxMib{xo?O zd#V^N(MqEE^0K9zT1hmFXe61*&OFg<&OAImrWr&-QGD|2mf=< zZ?%`5ER+B?Qe$+r59W6nbAFdJt&Z?)0Fd4+06FKjiWRRrf!}XB=C-M2L6+(VxLsR)D)Nl{kMu^MGL9uOX3T44U+5n_Vjt7(Jbs~BN^ z;Spkmv9bqpZ_ApPKTsvLWVcQ4=xGKkds$s;BTqcN&+2j;Hao1m!|DnMd6k&D=vi6w zsUDsx0B;Q&l{Q%2%<2w&d!95Kl{GLCwj&e0U&-n&I~8Zu&rU@!2~np3dEwrWykQqe z%?(tL)t$k?7Sogi(|!Qx7CKA>ovPsSMSsCyD(^^eU<-~`l{)5AO*~norlYvJBf((_ zY6+1Y&8HXe)K#bIV(^8AI_}x3L<^uc4O1AGp`I`7eoP@Mj{6E56`^7_YX<>Pl8UnCBMVY6EI>?CD{4fbs-3kk z*2anQ8xC9a4TH71tTjWEYIv-|T74@pj$m~o`qq`TX_@3r1u<_{>C~SF=ozMs_-Gw7 zzsk*g5Ze(7cp_`)`C*&26EQ( z2r7e={u!*bWNi>@y;vKJjDg5#gGazct9NN9*1X!t?@R^Jp_k|c?jwcC+7KFuo{ojF z$?9n8FTKVlxQS>Is8n^pe}||E=_Q&!pm(%JLYp)e9SF2O% zihh?mPODRNzrdB$smsNBbXuK~3M|1db=u+*{V&$0FD}vha!J0V&U~?;otMCq_Em8? z>3Le1PAk<3&uOI!jZQ07o?R_Z>5EvYl0Ord@WaVFu|{PL6sxrwE~)F^_tz&X6UD{#@>>XBbBDu@jA=dmc4Xe>a-2G@g z%+!1I67H}@zh(7TJ7M+s4N|X~7U4Z?3t1z25i7+5>?czkH7~RJkDV?7FiH#21;ExQ z0ngs_GM*V*wo%!d0tjM70|0daAl=H^rA(}PL!kj4>X>=&S=`b9=UCgzS^y0~hcnFS z{{;<@S)U=d9mZZ(3bRs>CgWd!`Bsz_FPe&fJwezpYJz)z!s4X$qqjk1J<7nnE;Yiv zCXA}N<|-U+a{M!s<60eXoC;%G(IY3nv9I@&W4Jt*WzAf8pm@w>Sqo>aHE{NXUB}uc zEX!e8%W{}wSq{rumcty&a+qUT)|j;cS<5nZ@Re{Faps^b%bF)E=gnnVQ?X{Al8rws zYD=08#~oNekay0JS2@@;uUU)1*mY)Ys4UmTy;V3(1J`KRr7xKi)Hay}tMS0A`<58X3h}qD(wd0;`JYWO2!ZA#y@u0o!G#)Op zwln*aWkMitSN10lL!z}2g6)Q@Awl?!El`9mmk~ir2^H;DYX2N`{jTW;q1L)oWo_lD7@be5b<#ADXAZk;CY4F+9X3J;xM|qXC`i zyyzY6AuvGaXy@g2(YVNJQ?X;OKp|2wd~DRFps0A(PBDGXbb#qorf<-x&tP<%rcMl1 zOV{xISO(Kc>c#Y zSDaS zo@Km5JB$~uEeC3%*K!#y{2T;*3R4P_sjM|&+6uMy7R|(c3r)uipGL3XJ{3A(D3ff8 zqD*zAlrhzzQj%#l+RkOA7^cZ|nuag05f(*lCNv`~AMF*iNdR;taV+J^b4;QnD=;lU z?M19Si|X^_pp0HOb!<8%QQ{*-G?PX`*FZhce83CD?jn;$(r`JU3)Sfm9nRCXd7`oz zDVr36jrFt6jH5lM*deUkgq|VU)crLhRb0DTgvQKu-qA>PfTjGxs<1`DJEo#5vk996#<@ zvtEs3y5c8?6>9OX#?6Phll9Y&S2gqKLM;*V@CI@LI1aFq9IzHK!!F?QfJH@c$%xI6 z^_F{OX+>r1leD5}75S6x68^G}$$aodG*@d}&SNq$_hkl4D%&V;T+$BT&7Ueo6N$+# z?fh^_JAp5G&Y9l;&rUd!FW+6u{}Wu<8VFqHR?QWzE1cYToc)(}uG=H2Ct6nE2(ACN zp7d!ZuH5j9i#R;h-mrus;eD16%zycn`*Dv-mr*zCP!ZQ5m)55(db-t8LvK>Lc!Sc# z0|NtP=fkHVlX5^7k(>bksQ8%VWT#Bd-;44Bg+%_pWv+BMkA>XG6wb1p~KZdoGw1tf6GWy7ub2kv=eXOWo6Y#XX(>;nVmL zK8^R%|926~(?QhtF&D9?aKn2#r^ToBwtOmA(f>7%$*1?Kdpe)Xf9;`~Z+G~A=YRfx z$G2ai0p!mM8{HS5(F3&7;Q19Cn* zRNZq2cGH#8-H1*9B23Z0kBRheBi*{(4Xoy-BbU1|$Fl4F=lEOhg(q_(9-6zZ+E3ws`?RjG`SOGN-}6w0ck{n?!!#XN zpThCEz}UxbWBhFY<+-+hCQ%s;9H!|O3x21Bn`V~SKwuy#@3=HI<@MEU(R7j5g?dPqyt-sA z(?f%WH4Z@gOmGKsgWIHsxm3a{62N)Vtdu4Bt1?(oUHE|a_Uef2d)|oD|?~Oqqs7db9Urc+$0M#(0tP zF&@kT*11^}K!GXNCs8ofl?RoDf@2N}vS!C1b9SH;-u>iqp#?KSXXUzMN`&I^nknxL zhrFBSQ=wp1Zo7~sqTgM|-y>>Gk?t#^kJpM!K`p#5cX6~HjG0kG{Mm9$jhD@eSz1+rVXZsYpp5nr<8a*bI#Ye;UHy|?P@?c*XBZQw!i zOipBY0oELq@6koI?75Q1;A!THRy38vYvfs^0md#lFpdJo=$shSvoO|W z@3HXn+BcHb^v5yA0NYSp!*ci0bs=EoS703Dz?dazi6*a8AS3{h^KzjBQui#YA3CJ2 zqR#3br_`zYol>WMY(5nUVfBdlR3emB=x$RRv-*V#(IS(L;M?fblSQneoQlS~R54{V z%ps#tS|~2EId^f_ytH!fytMKl_(=)2M;PBTL4IH=ML3W{HNKY{e5xLntI-Lw(J8a~ zG4p=HY?L(}Qt_TpA>GW$k{7K}*65vP?=-c{?6!SaYvh6ly0e|Znino_lRDPq4ftZ& zl$wGgWM_*|Q4+*OFUh^IV!|?~jf-V58bLrsr_`kyF49~V)af~?8|9#`SP}Mat`>@X z53duAdYn3_3C$cUq+z&P|5wyC6S|6(GpTFxh&oq$z)9Y42YFe7_>3utY!eT%- z3g)7l&HMZ2eUIF|qs{xU+$eAAVNO7m0m$bOpij)kN6h=z=KZ`0VybzcZUS-$tk>^& zb(>wdix(X0Wr@TW?DbHsajeuhWVzsW2rP_!CQm_$6vIUh;RPgzm`Xvmz!vim#6>lk<|}qgD|6EGNUs&G zEI5k4V3ud`yi3OX91yejRI;uVAIM$<)Rx`n;0@XjazYI=dnY}VUSW<+G-3Cbd(qZ% zFJk5tZVK?V4|iV_c4doC*DF4|p1U>k8%IPT^Yuu);pq6&4}KqB;`M&F5?9i?ly@HX z)$>uQqTR!T@4|)cZCs13Rs$;3H^vzZ#r40lFoUaP#XONpDUM211d)rfLJ>*!n5^uw z4sZM{*LsvxYb&ot>JB#|s*>$Z?DX-qhFF8mYV!KEvs#ep+2r&$Le!q3=4+AEB!?HP zsgKj}a(kdhCWR0JmNcdYb~tWODTB&e!yIkGa=kB{^;#u@j8qlEJVe4ys)I+) zH&dxWm6$}e`0*me^|TC{M?-B?+e)3_zYH&{3^>?~w6?QRSHmj*p#vPp(sXKwod|Wc zp<7krgLLYiNzLI`l|kz%%ti>1lqe-_#YH7BgI+f~vJ@SmS=P3;OzLc-dKt9KM!l_+ zZlk_d8hwaLXE8otXhe*};8$B@yjwZ#A|0UQOuSlt5M4iLc0D*)7!VA%T)Z+43CiZvGbjPCNYBRw-Av!mH`X>tB_@PMjchdDN{m=B)K7X1FEfzV)JB6c zXaN~i7aXtBwyqA>B8twSrL=;2IY^8Nj7c;%=SiyX?s`>0qam?|*3v43O0rQx27L>k z7)rOIpW6*<7sMkHQF$?guGpxHm4;h89Rj>%Hkz10H*M6@YV81Co8gis`#WH(K5N<& zApdEj2&=VYCf%nyHu}tfN5FWvDc`0CR1h!Ds}e=yhK;TnHri#SinP;4r}3O%rRp>z z6Mks)3%>3{35-hvTdA5gGm3r@3v&#z=6%oDwX?5Z-xtW*n56L&m8bIT>dg(VHtXVOI*9YEdo zRF>8rqScU;i>!2_^5{r6IPKl1Su%dCgfFz{bW;ZK~-`voJN4CwOiaMKGT@Y|a_sUYgnHc@X*|UehiH z952&zW`PGb&NR%p2&qIo0=Z+gHC-I#4);dI7awpL;MQdlz^~6FFZ2}dV2E`B$}E8R z67Z$aeSAYiC(J8kRR@x7j^TSdG!5m$Ss9J|9`w37i|gt5(h!x_A}x}`K~jl(mm3~LX0o6a>_>4P=qaLRS<&^HD~U_@yo%r z^E68bnI_lz(@by-4rnx6col&Uy&_MM_`t#CLqMKlwL*TwkymWD`97@3~Pp8--a%}+krT~zsydbzlZ_H(+6BF(P zM(hLR)WSX+0)uZ4fb4C=??F-=ksOfoow@k2a?p~7t!gJ$7TJjLgs>DEVEfrv^+oN< z=odPB10B1Djsa+2Rv}WSfaXhpIqAp=V#OahXOVLnIbp2UXT=5>h!UY3kr}Uc4^GqJ z6)p@>pOIc*6I%wXeTX*SqfIQU1rclqIs1@v1vxz>n254K>J~uOkH{L$$}Wf;D3WzmBSkW%5#K~A!M3c^F@&R49hJ*fix`KOcx{Cby zhP5|M0F&tweJ4E#GnHy9R+_U45$Gp4+pzjA5(xeUBsg}NhXnq&aA8v+jZKlfz{(5A zguJVRf$9nY)DC3SMMe}dzMyYl90;2s?dmY({3Ox2-UI#9LFYBlf15so=dXf}!ATi@ z$%wC_yejm!K#K&l_?GsNFM)IOutwh#Scuf{7m^=Xg_Dx{BI@B}1c4h==-Wfc0SnZz z$hnI6Kde^6w|5Qb16pmsn;54@$XIUJ=zZ*K8D32``T)hZS^Wq=;eo7vg?dW?98|8k z&#GZ639W>QcrM_-iaK*}+JT&FtQfRQM@%1634AQ%q1izs+fZu(YL#OZ^Bex>Y9eJw z`8z0Bf`aG7CsTO~)yE*G+(p)W;cG=$JuvG*{`;aoSF!RNtGi8kejn9VqG2^0v?0zA zKux5j0&y=fproO=DxhHILq8x;g(o;|iq&cG^pME#E3hEHFe&sfAwuJ*TL7^hG!#An zHJhdj#G}NxOGme(*jI|x2;exu>Pc~%SL*{2#Qp#bGWd1hX3d|KkKx`~1K}s&KvoJz zJ;lMs8xBumwrJ`5A>$LX@$MQYGdeSR{xMWjw)E4hX_3%n=ATWQ%n*5R76vU2W(AfKKxE_$ z13d|*rz&Edbr5~76@n(GNvyoc$`~}%Qdmnwf?z!oZAUtB3t&>gA*eZm#ilZAt-$RP z2oiu_P7tpLYK~HY`UeEHK!PX-6JV?Pn>%1c$V6vQs}HL`A~&#I+pK(yW`C6RLD^u| zFe^1V^xiHZ1DuV;*wf-sVK`!*xHLwPP1Z)BY#7QSS-p&v12m69&IriBO+@NIha12b zwytB2t!8ZwWC5+7L!FA~5OSdKmEQmWk(m%CK|?eI%@-wB)}Zp=W;H`+4e_w>eSk1V zID#Y$)u8INZLC3ypF@r(a%v%G8Eb@KC{nj0vVxEW4n6<}J<&19qA!RN6};mj{C^>? zth8nIbz~GqIm8W7DSERy92xyEsWe0((3%4XRB#K-OnjS&&LMb2Eg?o-EPTa^strO3 zv^v7esEg1RN0I6;=mScy)@u0qLC9Eu*(sC_Lskc5VZyC|LI6e8(FQg!;w7l7WU*8; zs2;e^5)=z7B?v)iCankB?1!3Q^?Oz^!pTrgCiY|$_D11(Ob&vPqBTTDKV%#>?G%w` z4T@76ge+)Qv?~szvh-d6QmE1~tVTmeQW$HKv4WsrnjppgKpToSUqTDB`ln1B4a@r; z%o!D23TL&OtfLTcEzaEf#{^-#M0Tpg)W?%(^8T#Jr0vTZ)TA~aO^|eleT7803uUf7 zV6_Wyb}_6yuxU);w$K|8Tx|56=8p&A8Sz3`645%8X-I# zm0&6gscUDNR#X}ppu|++8Yc5ZSXJ6&xlMsRMR0Vlz;fuzR7pM%2(>jx8EII1!OlS_ z6#!ofw3VfoYF!)fy^E}9;H!!c@C7jW0bhgzUkzjc-#$}jzd?vIK_#Y~CZ-(KH9sVe z_2r}0h3aB;GK8uxJ%io>_Ew;4z}lPmsZ=_C3|Uar)C7UVV9$X7D{Ci_xf7YqAc@w# z_|hE&wX|YqK_NKB#Mpg^Oc>Spil}agU7`Yywig*N-ZVrM!7^uvLeZL8CCC>HK-rm5 zHIRg_>+#hGES`)hjK{);bqH&_LCqGb2pLDq+f)XC;()e~6>}0M6ZHd@b;vveEMTIx zO|Yy+UAXlRu?_~WT<3;|4H3}g@AOi1FO>}h*&WKG! zBY;R$)d7K-378XE!^Fb|ivU;xvrs#Of>7f#EPH@^l3)ZXRcW*U{?$O2`%+~nYhS>CBBU{h zvW^D-NQ0Xo2~+iBWDgZ6h^L7*^fnW$OQkYeOh?gFgZyzy#W>Z%t)SGo3sJg4?=e+D z(4E(V5%aM#Ba-Sw>p+T@j`U(o1G#@7cj_%4^#CS6CbbqI3qMQ(*e}!^AM9q2GwqeI zs{{)I)(H;spr*kj^ko3V8wsKwRYc}@pa3e6ARhba2r^(NP#7}afyQ9yPGns}Ry$;U z4ikz#ImC#0%-RtQEesbZ-?t$Aw2N`@fv8Ln4+GAy23OT#K^$E2x5?f;|cXI%zETb#C8h>?*S_m-Wr{0nP?QU zOaH*3ok&)q!c;^CD8#f8>o0PER;+tki;|frDT*NmAF)sE1N2yS$m=3A;(|bxtz_+I zloiHF5Tc5(wg+D_z;GIc6C%_+0hU1DK#*XPAtcWZS!rlHN)`h$#vI(&p25)^a#LC9 zVG@SY6dDgh_d%CD@Q#k8P6rVm*=j@J7H9n79?RGn!*Yj;c(`_W`Q zfMA7vpI~&+G*-F@^iNQ*83lErG%%2WJ_|Xu03F)$Bi1lCic@2zW2{{O^b-R8HO6rw zLZ_Ty#P5WFuVxJ$Uk;TZ(m7pvc?t z8OaQ7j1xN^0Mhm{7e=y&SyslsShFKRMkbO8z<3@Qp>GG04>Gsn02=v|k$(yK!&z%f zl@GC4>9hqs0BDFfCom)W2yHOeJ5EA|4jB~bWIx6^Q5w?)xm`32=5g|&M0p%QU|t3g*g!Nx;*CszNB}Edg*^|-zA&ez(iCPnT5fkNc??^L(gey|=Ghf* zV%~t}3((dIjR%uhX$aB5LaswZkzn^2gu+QEq`A`YT~;vrL=aXWf0;DG_NgY7!kXOy zpn!ofBA61GHqzh#j Date: Mon, 9 Nov 2026 16:18:12 +0000 Subject: [PATCH 4/4] docs(proofs): say exactly what --safe rejects Review on #126 (CodeRabbit): the passage said --safe rejects every marker the scan looks for. It rejects postulate and the unsafe pragmas and options in Agda; the textual scan covers other languages' markers too. The two are now described as different checks. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- docs/proof-debt.adoc | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index daeb4cb..68b3a50 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -147,9 +147,13 @@ not the proofs" — and it should be reported upstream rather than triaged here. The absence of markers is not a clean bill of health. The only proofs are -DOM-1 and DOM-2 in §(a), both under `--safe`, which rejects every marker the -scan looks for; the markers say nothing about the twelve obligations that -have no proof at all. +DOM-1 and DOM-2 in §(a). Their CI check runs under `--safe`, which rejects +`postulate` and the unsafe pragmas and options (`TERMINATING`, +`NON_TERMINATING`, `--type-in-type` and the like) in the whole import cone. +That check and the marker scan are different things: the scan is textual and +covers other languages' markers (`sorry`, `Admitted`, `believe_me`), which +`--safe` neither knows nor replaces. Neither says anything about the twelve +obligations that have no proof at all. == 3. What a Grade 3 result would look like here