diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index ca24705..405c83f 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -15,6 +15,8 @@ workflows: - 'actions/checkout@v7.0.1' - 'actions/deploy-pages@v5.0.1' - 'actions/upload-pages-artifact@v5.0.0' + '.github/workflows/secret-scanner.yml': + - 'actions/checkout@v7.0.1' dependencies: 'actions/cache@caa296126883cff596d87d8935842f9db880ef25': ref: 'v5.1.0' diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index fa6eb1f..815ab1b 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,19 +1,12 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 -# Prevention workflow - scans for hardcoded secrets before they reach main. -# -# Calls the estate's shared secret scanner (gitleaks + rust-secrets + -# shell-secrets). The job key MUST stay `scan`: the estate-wide -# Secret-Scan-Floor ruleset requires the check context `scan / gitleaks`. -# -# No `secrets:` line, deliberately: the reusable references no secrets -# (gitleaks runs as a checksum-verified binary, not gitleaks-action), so -# `secrets: inherit` would only hand it every repo and org secret (CWE-250). name: Secret Scanner on: pull_request: push: branches: [main] + workflow_dispatch: concurrency: group: ${{ github.workflow }}-${{ github.ref }} @@ -22,6 +15,312 @@ concurrency: permissions: contents: read +# The estate secret-scanning contract, run inline. Ported unchanged (job +# bodies) from hyperpolymath/rsr-template-repo `2be7b88`, its #295 "run all +# three secret scanners inline". The baseline is pinned to +# metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6. +# +# Why inline. The previous caller here was one job-level call to a remote +# reusable (`hyperpolymath/standards/.github/workflows/secret-scanner- +# reusable.yml@74d2f66`). It failed at startup, with zero jobs, on every run +# since it was added in #33. The template measured the same class: a remote +# reusable is not lockable by `gh actions-lock`, and check names that a +# remote repository can rename are not a contract. Here each scanner is an +# ordinary job whose `name:` is its check context: +# +# scan / gitleaks estate baseline (+ .gitleaks.toml if present): +# working tree, full history, AsciiDoc mirror +# scan / rust-secrets hardcoded literals in .rs files; self-skips +# without a Cargo.toml (marches has none) +# scan / shell-secrets hardcoded literals in shell scripts +# +# All three declare `permissions: contents: read` and no `secrets:`; none +# needs any secret (CWE-250 if one were forwarded). +# +# actions.lock: the only action is actions/checkout, pinned by the tag +# marches' lock already resolves (v7.0.1 → commit 3d3c42e…), the same commit +# the template pins by SHA. No marches ruleset requires these checks today. + jobs: - scan: - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@74d2f66f575246cf6e313ae7775f44df6e097ff2 + gitleaks: + name: "scan / gitleaks" + runs-on: ubuntu-24.04 + timeout-minutes: 15 + permissions: + contents: read + env: + GITLEAKS_VERSION: '8.18.4' + GITLEAKS_SHA256: 'ba6dbb656933921c775ee5a2d1c13a91046e7952e9d919f9bac4cec61d628e7d' + STANDARDS_SHA: 'e064539116c2dcfdf282a4749dbd58c69961c7e6' + steps: + - name: Checkout repository with full history + uses: actions/checkout@v7.0.1 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Checkout estate gitleaks baseline + uses: actions/checkout@v7.0.1 + with: + repository: metadatastician/standards + ref: e064539116c2dcfdf282a4749dbd58c69961c7e6 + path: .standards-baseline + sparse-checkout: config/gitleaks + sparse-checkout-cone-mode: true + persist-credentials: false + + - name: Stage estate baseline and install pinned gitleaks + run: | + set -euo pipefail + cp .standards-baseline/config/gitleaks/estate-baseline.toml .gitleaks-estate.toml + rm -rf .standards-baseline + test -s .gitleaks-estate.toml + + TARBALL="gitleaks_${GITLEAKS_VERSION}_linux_x64.tar.gz" + URL="https://github.com/gitleaks/gitleaks/releases/download/v${GITLEAKS_VERSION}/${TARBALL}" + curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 \ + --retry 3 --retry-delay 2 \ + -o "$RUNNER_TEMP/$TARBALL" "$URL" + echo "${GITLEAKS_SHA256} ${RUNNER_TEMP}/${TARBALL}" | sha256sum -c - + tar -xzf "$RUNNER_TEMP/$TARBALL" -C "$RUNNER_TEMP" gitleaks + chmod +x "$RUNNER_TEMP/gitleaks" + rm -f "$RUNNER_TEMP/$TARBALL" + + - name: Gitleaks working-tree pass + run: | + set -euo pipefail + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=(".gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=(".gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source . \ + --no-git \ + --redact \ + --no-banner \ + --verbose \ + --config "$CONFIG" \ + --exit-code 1 + done + + - name: Gitleaks full-history pass + run: | + set -euo pipefail + if [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then + echo "::error::checkout is shallow; refusing vacuous history scan" + exit 1 + fi + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=(".gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=(".gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source . \ + --redact \ + --no-banner \ + --verbose \ + --config "$CONFIG" \ + --exit-code 1 + done + + - name: Gitleaks AsciiDoc mirror pass + run: | + set -euo pipefail + MIRROR="$RUNNER_TEMP/adoc-mirror" + rm -rf "$MIRROR" + mkdir -p "$MIRROR" + found=0 + while IFS= read -r -d '' f; do + dest="$MIRROR/$(dirname "$f")" + mkdir -p "$dest" + cp "$f" "$dest/$(basename "$f").txt" + found=$((found + 1)) + done < <(find . -path ./.git -prune -o \( -name '*.adoc' -o -name '*.asciidoc' \) -type f -print0) + + if [ "$found" -eq 0 ]; then + echo "No AsciiDoc files present." + exit 0 + fi + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=("$PWD/.gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=("$PWD/.gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source "$MIRROR" \ + --no-git \ + --redact \ + --no-banner \ + --config "$CONFIG" \ + --exit-code 1 + done + + rust-secrets: + name: "scan / rust-secrets" + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + env: + # Findings outside ./src (newly visible — see the scan-scope note in the + # step below) warn until this date, then block. Same warn-then-enforce + # idiom and same cutoff as the estate canonical reusable + # (metadatastician/standards .github/workflows/secret-scanner-reusable.yml + # at the pin named in this file's header), so this job and the reusable + # cannot disagree about when the widened scan starts blocking. + ENFORCE_RUST_WIDE_SCAN_FROM: '2026-08-21' + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + + - name: Check for hardcoded secrets in Rust + run: | + set -euo pipefail + TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}" + + # An unparseable cutoff would pick the warn branch forever, silently + # disarming the widened scan. Refuse to run instead. + require_date() { + case "$2" in + [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;; + *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD." + echo "Refusing to run: an unparseable cutoff would disarm this gate." + exit 1 ;; + esac + } + require_date ENFORCE_RUST_WIDE_SCAN_FROM "$ENFORCE_RUST_WIDE_SCAN_FROM" + require_date RUST_TODAY "$TODAY" + + # Self-skips when the tree has no Cargo.toml, so the job is safe on a + # repository that is not (yet) Rust. The check run still appears, which + # is what keeps the context stable across every generated repository. + if ! find . -name Cargo.toml -not -path './target/*' -print -quit | grep -q .; then + echo 'No Cargo.toml found — skipping Rust secrets check' + exit 0 + fi + + # Scan every .rs file, not just ./src. A Cargo workspace keeps its + # code in crates/*/src, and a `grep … src/` matches nothing there: + # grep exits 2 on a missing directory, which an `if` reads as "clean". + mapfile -t FILES < <(find . -name '*.rs' \ + -not -path './target/*' -not -path '*/target/*' \ + -not -path './vendor/*' -not -path '*/vendor/*' \ + -not -path './.git/*' -print) + if [ ${#FILES[@]} -eq 0 ]; then + echo 'Cargo.toml present but no .rs files — nothing to scan' + exit 0 + fi + echo "Scanning ${#FILES[@]} Rust file(s)." + + # Each pattern requires an assignment DIRECTLY to a string literal of + # meaningful length, so lookups, paths and demos do not match. A + # credential shorter than 8 characters is not a credential either. + # `static` is accepted alongside `const`: a `static AUTH_KEY: &str = + # "…"` is a genuine hardcoded secret. + PATTERNS=( + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*SECRET[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*KEY[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[a-zA-Z0-9]{16,}"' + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*TOKEN[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + '(let|static)[[:space:]]+(mut[[:space:]]+)?[a-z0-9_]*api_key[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + 'HMAC.*"[a-fA-F0-9]{32,}"' + '[a-z0-9_]*password[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + ) + + # Exemptions match on the VALUE or on an explicit pragma, never on a + # file path: a path-based exemption would blind the job to a genuine + # secret in the same file. + # 1. env-lookup RHS — `env::var("NAME")` IS the practice this job + # exists to enforce, so flagging it fails the correct code. + # 2. URL values — an OAuth endpoint is public, not a credential. + # 3. comment lines — documentation of a pattern is not a secret. + # 4. inline pragma `// scanner-allow: rust-secrets`. + COMMENT='^[^:]*:[0-9][0-9]*:[[:space:]]*(//|/\*|\*)' + ENV_RHS='=[^;]*(env::var|env::var_os|std::env|env!\(|option_env!\(|from_env|dotenv)' + URL_RHS='=[[:space:]]*b?"(https?|wss?|ftp)://' + PRAGMA='scanner-allow:[[:space:]]*rust-secrets' + + blocking=0 + advisory=0 + for pattern in "${PATTERNS[@]}"; do + hits="$(grep -nHE "$pattern" "${FILES[@]}" 2>/dev/null \ + | grep -vE "$COMMENT" \ + | grep -vE "$ENV_RHS" \ + | grep -vE "$URL_RHS" \ + | grep -vE "$PRAGMA" || [ $? -eq 1 ])" + [ -n "$hits" ] || continue + + # ./src hits keep blocking. Hits outside it are newly visible, so + # they warn until the cutoff rather than reddening repositories + # whose wider tree was never actually being scanned. + old_scope="$(printf '%s\n' "$hits" | grep -E '^\./src/' || [ $? -eq 1 ])" + new_scope="$(printf '%s\n' "$hits" | grep -vE '^\./src/' || [ $? -eq 1 ])" + + if [ -n "$old_scope" ]; then + printf '%s\n' "$old_scope" + echo "WARNING: Potential hardcoded secret found matching: $pattern" + blocking=1 + fi + if [ -n "$new_scope" ]; then + printf '%s\n' "$new_scope" + if [[ "$TODAY" < "$ENFORCE_RUST_WIDE_SCAN_FROM" ]]; then + echo "::warning::Potential hardcoded secret outside ./src matching:" \ + "$pattern — becomes BLOCKING on $ENFORCE_RUST_WIDE_SCAN_FROM (today is $TODAY)." + advisory=1 + else + echo "WARNING: Potential hardcoded secret found matching: $pattern" + blocking=1 + fi + fi + done + + if [ "$blocking" -eq 1 ]; then + echo "::error::Potential hardcoded secrets detected. Use environment variables instead." + exit 1 + fi + if [ "$advisory" -eq 1 ]; then + # Never claim a clean pass while findings are outstanding. + echo "NOT YET ENFORCED: findings outside ./src are advisory until $ENFORCE_RUST_WIDE_SCAN_FROM." + exit 0 + fi + echo 'No hardcoded secrets detected in Rust sources.' + + shell-secrets: + name: "scan / shell-secrets" + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + + - name: Run repository secret pattern hook + run: | + set -euo pipefail + rc=0 + git grep -IlE '(ghp_[A-Za-z0-9]{36}|github_pat_[A-Za-z0-9_]{82}|glpat-[A-Za-z0-9_-]{20,}|AKIA[0-9A-Z]{16}|-----BEGIN (RSA |EC |OPENSSH )?PRIVATE KEY-----)' > "$RUNNER_TEMP/hits.txt" || rc=$? + # git grep exits 1 when nothing matches; above 1 is an error. + if [ "$rc" -gt 1 ]; then + echo "::error::Secret pattern scan failed with exit ${rc}" + exit 2 + fi + # Exclude intentional scanner rules and adversarial negative test fixtures. + filtered="$(grep -vE '^(\.github/hooks/scan-secrets\.sh|\.github/workflows/secret-scanner\.yml|\.machine_readable/testing/adversarial-content\.k9\.ncl|tests/)' "$RUNNER_TEMP/hits.txt" || :)" + if [ -n "$filtered" ]; then + echo "::error::Hardcoded credential material detected:" + printf '%s\n' "$filtered" + exit 1 + fi + echo "No hardcoded shell/source credentials detected." diff --git a/CLAUDE.md b/CLAUDE.md index 91af05f..cdc483a 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -3,8 +3,16 @@ - UK English. AsciiDoc for docs (`.adoc`), not Markdown (this file and the bootstrap prompt are the only exceptions). - GitHub is the single source of truth; mirrors are spokes. -- No Python. Lean 4 for proofs; shell for glue; Podman if containers - are ever needed. +- No Python. Shell for glue; Podman if containers are ever needed. +- Proofs follow the estate policy (`hyperpolymath/standards` + `3-practice/PROOF-POLICY.adoc`): marches is *theory*, so Agda is the + source of truth, rechecked in Rocq and Lean, with no Mathlib. The + Lean 4 development here predates that ruling and is target-only + evidence (the Lean leg) until an Agda proof of the same statement is + checked and the two are reconciled. Every theorem is `ungraded` + (no PWG) until then; `PROOF-STATUS.adoc` holds the record. Never call + a theorem graded or "verified" under the estate policy on the + strength of the Lean build alone. - Claim taxonomy: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Anti-Goodhart clause: a status upgrade must name the transcribable artifact that discharges it (build log, eval output, test run). @@ -17,4 +25,5 @@ - Before ending a session: update STATE.adoc, commit with a message naming the rung, and tag only if all gates pass. - Gates for this repo: `lake build` green; `grep -rn "sorry" Marches/` - empty; the BadGadget `#eval` prints the period-2 orbit. + empty; the BadGadget `#eval` prints the period-2 orbit. A change that + adds or alters a theorem also updates `PROOF-STATUS.adoc`. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..62dbe1b --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,219 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += marches — Proof Status +:toc: +:sectnums: + +[abstract] +The proof-status file the estate proof policy asks of every home repository +(`hyperpolymath/standards` `3-practice/PROOF-POLICY.adoc` §2 and §8.5). It +records, per theorem group, each witness leg with its route, status token +(§5), correspondence state (§2.2) and receipt, and the Proof Witness Grade +derived from them. It claims nothing the receipts below do not show. + +== Classification + +marches is *theory* under policy §1: its statements (disciplines, region +DAGs, cuts, path grades) would be true of any implementation and name no +type, function or wire format of one system. Theory has *Agda* as its source +of truth, rechecked in *Rocq* and *Lean* (§2), with no Mathlib. + +marches was written in Lean 4 from 2026-07, before the 2026-10-26 ruling. +By §3 its Lean files keep their value but are *target-only evidence*: they +count as the Lean leg only once an Agda proof of the same statement is +`PROVEN` and the two statements have been compared and the comparison +recorded (`RECONCILED`). Until then every Agda row is `OPEN`. + +== Grades + +Every theorem below is *`ungraded`*: no Agda witness exists, so not even +`PWG-3` applies (§8.2). `foundation_diverse` is false throughout. + +Grade census (§8.4), denominator 211 theorems in the `Marches` namespace: +`PWG-1` 0, `PWG-2ii` 0, `PWG-2i` 0, `PWG-3` 0, `ungraded` 211. The 235 +definitions in the same namespace are not proof obligations and are not +counted; the axiom census below covers both kinds. + +[cols="1,1,1,1",options="header"] +|=== +|Leg |Route |Status token |§2.2 state + +|Agda (source) +|— +|`OPEN` (no Agda development yet) +|— + +|Lean +|`re-proved` (written directly in Lean; no Agda to transport from) +|`PROVEN` or `PROVEN-WITH-AXIOMS`, per group below; target-only evidence (§3) +|not `RECONCILED`: no Agda statement to compare against + +|Rocq +|— +|`OPEN` +|— +|=== + +== Lean leg receipt + +Taken 2026-11-09 on `main` at `abe636aaba3f36eebee7f40b0707ef6bb090715e`, +Lean `v4.35.0` (`lean-toolchain`), no Mathlib (the only dependency is +tropical-types, core Lean, at the `lake-manifest.json` pin). Input digest: +the git tree of `Marches/` at that commit is +`7ef83e438a687872157fcb4187bd99f242641f8a`. The run was repeated on +2026-11-09 at `6db6c0a`, whose Lean inputs (`Marches/`, `Marches.lean`, +`lakefile.toml`, `lake-manifest.json`, `lean-toolchain`) are unchanged from +`abe636a`, with the same result. + +---- +$ lake build +Build completed successfully (19 jobs). +$ grep -rnw sorry Marches/ Marches.lean # empty +$ grep -rnwE 'admit|axiom|native_decide|implemented_by|extern' Marches/ Marches.lean # empty +$ lake env lean Marches/BadGadget.lean +[(false, false), (true, true), (false, false), (true, true)] +---- + +Axiom census, `Lean.collectAxioms` over every theorem and definition in the +`Marches` namespace: + +---- +declarations audited: 446 (211 theorems, 235 definitions) + 171 theorems, 231 definitions × axioms: none + 37 theorems, 4 definitions × axioms: propext + 3 theorems, 0 definitions × axioms: Quot.sound, propext +---- + +No declaration depends on `sorryAx` or `Classical.choice`. + +*Scope of this receipt.* It is historical evidence for the Lean inputs +named above, from a local run. It is not the current, pinned, isolated +receipt that §8.4 ("claims need receipts") and §8.2 (`PWG-1`) require, so +nothing in this repository may be described as verified *through* Lean +on the strength of it. CI's `lake build` runs on every commit with the +toolchain and actions pinned, but it records no axioms and no input digest. +A CI job that emits a full §8.2 receipt per commit is `OPEN` (see the +plan below). When the Lean inputs change, this receipt is superseded and +must be retaken. + +== Theorem groups + +`PROVEN` here means the Lean kernel accepted the term with no axioms. +`PROVEN-WITH-AXIOMS` means it rests on Lean's built-in `propext` and/or +`Quot.sound`, named in the row. The policy does not yet rule on whether +those two built-ins count as "necessary axioms" (§5, +`TRUSTED-BASE-REDUCTION-POLICY.adoc`); this file takes the cautious reading +and names them. The constructor lemmas Lean generates for structures and +inductives (`*.injEq`) use `propext` in every module that has them. They +are not headline theorems and no row below depends on them. + +[cols="2,3,2,1",options="header"] +|=== +|Group (module) |Headline theorems |Lean leg |Agda + +|Kernel: single-region loop-freedom (`Kernel`, `Basic`) +|`run_worsens`, `no_return`, `strict_implies_inflationary` +|`PROVEN` +|`OPEN` + +|Two-region composition (`Compose`) +|`trace_worsens`, `wt_cycles_are_empty`, `no_back_cross`, `no_a_label_in_B` +|`PROVEN` +|`OPEN` + +|Gao–Rexford table (`GaoRexford`, namespace `GR`) +|`gr_inflationary`, `gr_not_strict`, `valley_dies`, `peer_route_not_upward` +|`PROVEN-WITH-AXIOMS` (`propext`, from the `gext` match) +|`OPEN` + +|Gao–Rexford as a typing judgment (`GRTrace`, namespace `GR`) +|`gtrace_iff_valley_free` (`PROVEN`); `valley_free_iff_gwalk` +(`PROVEN-WITH-AXIOMS`, `propext`); `no_valley_step`, `no_peer_reexport_up`, +`no_second_peer`, `no_step_from_bot` (`PROVEN`) +|mixed, as listed +|`OPEN` + +|Hierarchy loop-freedom (`GRHierarchy`, `Digraph`) +|`gr_loop_free` (conditional on `Acyclic`, which stays `ASSUMED`) +|`PROVEN` +|`OPEN` + +|DISAGREE exhibit (`BadGadget`, namespace `Disagree`) +|`disagree_not_inflationary`, `disagree_two_cycle`; `#eval orbit` is `TESTED` +|`PROVEN` +|`OPEN` + +|Falsifier F2 (`Freewheel`) +|`f2_discharged`, `freewheel_not_strict` +|`PROVEN` +|`OPEN` + +|Tropical instance and grade laws (`Tropical`) +|`tropical_strict`, `seq_unitl`, `alt_idem`, `better_reverses_altLe`, +`altLe_one`, `s3_witness` +|`PROVEN` +|`OPEN` + +|Reassembly (`Reassembly`) +|`Discipline.no_loop`, `PathAlgebra.toDiscipline`, `DiscSys.compose`, +`compose_no_loop` (conditional on `Acyclic`), `no_foreign_local`, +`no_self_cross` +|`PROVEN` +|`OPEN` + +|Cuts (`Cut`) +|`edge_crosses_past`, `path_back_crosses_no_cut`, `trace_cross_crosses_cut`, +`no_reentry`, `composeCut`, `composeCut_trace_embed`, +`composeCut_trace_reflect` +|`PROVEN` +|`OPEN` + +|Provenance (`Provenance`) +|`accum_append`, `run_eq_seq_carried`, `carried_cons_ne_one`, +`no_return_of_carried`, `trace_cross_shape`, `carried_in_cut`, +`carried_to_cross_in_past` +|`PROVEN` +|`OPEN` + +|Tropical adapter (`TropicalAdapter`, imports tropical-types) +|`pathCost_eq_accum`, `pathCost_append_via_accum`, `carried_floor` +(`propext`, `Quot.sound`); `bottleneck`, `bottleneck_carries_unit` +(`propext`); every axiom inherited from the upstream lemma used +|`PROVEN-WITH-AXIOMS` +|`OPEN` +|=== + +Stated hypotheses stay `ASSUMED` whatever the legs: `Marches.Acyclic` for +real topologies and real region DAGs, and every row of +`docs/kcut-correspondence.adoc` except KC-13. KC-13 is a Lean-to-Lean +import, checked by `lake build`, but it inherits the same `OPEN` Agda status. + +== Plan: closing the Agda gap + +Owner decision 2026-11-09: record the gap here now; the Agda port is the +next body of work. + +. *Agda source.* Port the groups above to Agda in this repository +(`--safe --without-K`, no postulates, the §2.1 canonical invocation), group +by group in ROADMAP order. Each group moves from `OPEN` to `PROVEN` with an +Agda receipt; that is `PWG-3`. +. *Lean leg.* Compare each Lean statement with its Agda statement and record +the comparison here. The existing Lean file is then the `re-proved` Lean +leg, `RECONCILED`. It counts towards `PWG-2i` only when, in addition, each +axiom it rests on is admissible under disposition (c) of +`TRUSTED-BASE-REDUCTION-POLICY.adoc` (§8.4, "axioms travel with the +grade"). For the `PROVEN-WITH-AXIOMS` groups that means `propext`, and +`Quot.sound` for the tropical adapter, each with its `docs/proof-debt.md` +entry, or a standards ruling on Lean's built-in axioms. A `PROVEN` group +needs no such step. +. *Rocq leg.* Dedukti transport first, hand re-proof as fallback (§2): this +is `PWG-2ii`, under the same axiom rule (`Print Assumptions`). +. *Receipts.* A pinned headless checker run per commit for each witness, +recording the fields §8.2 lists (checker and version, invocation, input +digest, result, axioms, full commit): `PWG-1`. For the Lean leg this is a +CI job around `lake build` and the axiom census; it is `OPEN`. + +Until step 1 lands for a group, nothing in this repository may be called +graded. `PROVEN` and `PROVEN-WITH-AXIOMS` in `README.adoc` mean "accepted by +the Lean kernel", without or with the named axioms, not "discharged under +the estate policy". diff --git a/README.adoc b/README.adoc index 8d305fa..a0f0184 100644 --- a/README.adoc +++ b/README.adoc @@ -14,8 +14,9 @@ object*: region-crossing well-formedness is a typing judgment on traces (`Marches.Trace`), and ill-typed crossings are *unconstructible* — they have no derivation — rather than detected and filtered. -Machine-checked, in this repository, by `lake build` (Lean 4, v4.35.0, -no dependencies): +Accepted by the Lean kernel through `lake build` (Lean 4, v4.35.0, no +Mathlib; one dependency, tropical-types). This is Lean-leg evidence only; +`PROOF-STATUS.adoc` gives the receipt and its scope: * Every well-typed non-empty cross-region trace strictly worsens (`trace_worsens`, `Marches/Compose.lean`). @@ -49,6 +50,13 @@ graded machinery (see `ROADMAP.adoc`). == Status table +`PROVEN` in this table means the Lean kernel accepted the proof and it uses +no axioms. `PROVEN-WITH-AXIOMS` means the kernel accepted it and it rests on +the Lean built-in axioms named in the row. Under the estate proof policy +marches is theory, so Agda is the source of truth and no theorem here is +graded yet. `PROOF-STATUS.adoc` records each witness leg, the axiom census, +the scope of the Lean receipt, and the plan for the Agda port. + [cols="3,1,2"] |=== |Claim |Status |Discharged by @@ -70,7 +78,7 @@ graded machinery (see `ROADMAP.adoc`). |`Kernel.no_return` |GR table inflationary; strictness gap at `(fromCust, c)`; valley → ⊥ -|PROVEN (finite) +|PROVEN-WITH-AXIOMS (finite; `propext`) |`GaoRexford.gr_inflationary`, `gr_not_strict`, `valley_dies` |DISAGREE rejected by discipline ∧ oscillates @@ -78,7 +86,7 @@ graded machinery (see `ROADMAP.adoc`). |`BadGadget.disagree_not_inflationary`, `disagree_two_cycle`, `#eval orbit` |GR crossings as typing judgment ≡ valley-freedom grammar ≡ non-⊥ table -|PROVEN +|PROVEN; PROVEN-WITH-AXIOMS (`propext`) for `valley_free_iff_gwalk` |`GRTrace.gtrace_iff_valley_free`, `GRTrace.valley_free_iff_gwalk` |GR ill-typed moves (valley, second peer hop, from-⊥) underivable @@ -182,14 +190,14 @@ is open and has already withdrawn one proposed pairing. |Tropical estate integration: tropical-types' `TropicalAdapterPath.lean` builds inside this repo, unparaphrased, and its `pathCost` is marches' grade accumulation under the bottleneck grade -|PROVEN +|PROVEN-WITH-AXIOMS (`propext`, `Quot.sound`) |`lake build` with the `lakefile.toml` `require`; `TropicalAdapter.pathCost_eq_accum`, `pathCost_append_via_accum`, `carried_floor`, `bottleneck_carries_unit` |The bottleneck grade gives no loop-freedom: a non-empty path can carry the unit -|PROVEN (finite) +|PROVEN-WITH-AXIOMS (finite; `propext`) |`TropicalAdapter.bottleneck_carries_unit` |Protocol-level asynchronous convergence @@ -209,7 +217,8 @@ elan default leanprover/lean4:v4.35.0 # or let lake read lean-toolchain lake build ---- -Zero dependencies; no mathlib. CI runs the same build. +No Mathlib; the one dependency is tropical-types, pinned in +`lakefile.toml`. CI runs the same build. `scripts/check-correspondence.sh` fetches the sibling proof repositories at their pinned commits (into `_build/dependencies`). It checks that every diff --git a/ROADMAP.adoc b/ROADMAP.adoc index d7aa668..29bfce3 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -88,6 +88,20 @@ echo-types pinned in `scripts/fetch-siblings.sh` |OPEN — postern not reachable 2026-10-14 |=== +== Agda source of truth (estate proof policy) — OPEN, next + +Owner decision 2026-11-09. The estate policy makes Agda the source for +theory; marches' Lean development is target-only evidence until each group +has an Agda proof and the two statements are reconciled. Port rungs 0–3 to +Agda in this repository group by group (`--safe --without-K`, no +postulates), recording each in `PROOF-STATUS.adoc`: Agda `PROVEN` is +`PWG-3`. The reconciled Lean leg makes it `PWG-2i` once each Lean axiom it +rests on (`propext`, `Quot.sound`) is admissible under disposition (c) of +`TRUSTED-BASE-REDUCTION-POLICY.adoc`. A Rocq leg under the same rule makes +it `PWG-2ii`. +Gate per group: the Agda check passes under the canonical invocation and +the statement comparison is written down. Takes precedence over rung 4. + == Rung 4 — attestation (A2ML bridge) * Announcements as attested claims: RPKI attests origin; this layer diff --git a/STATE.adoc b/STATE.adoc index a71851c..2182877 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,55 @@ = STATE — cross-session log +== 2026-11-09 — proof status under the estate proof policy (not a rung) + +* New `PROOF-STATUS.adoc`, as `standards` `3-practice/PROOF-POLICY.adoc` + §8.5 asks. marches is theory (§1), so Agda is the source of truth; its + Lean files are target-only evidence (§3). Every theorem: Agda `OPEN`, + Rocq `OPEN`, `ungraded`. Owner decision: record now, port to Agda next + (new ROADMAP section, ahead of rung 4). +* Lean leg receipt on `abe636a`, v4.35.0: `lake build` 19 jobs; no + `sorry`, `admit`, `axiom`, `native_decide`, `extern`. `Lean.collectAxioms` + over all 446 `Marches` declarations: 402 none, 41 `propext`, 3 + `propext, Quot.sound`; none on `sorryAx` or `Classical.choice`. The + `propext` cases are generated `injEq` lemmas, the Gao–Rexford `gext` + match, and the tropical-types lemmas the adapter consumes. Groups that + rest on them are recorded `PROVEN-WITH-AXIOMS`, naming them (the policy + does not yet rule on Lean's built-ins). +* `CLAUDE.md` said "Lean 4 for proofs"; it now defers to the estate policy. + `README.adoc`'s status table now says its `PROVEN` means Lean-kernel + accepted, not graded. +* Every theorem name in `PROOF-STATUS.adoc` was checked with `#check` + (all resolve). Issues #54 and #55 closed as false alarms (the stale + tropical-types pin, fixed by #57). +* `secret-scanner.yml` had failed at startup, zero jobs, on every run since + #33 (a job-level call to a remote reusable). Replaced by the template's + inline scanner (rsr-template-repo `2be7b88`, its #295): three jobs, + `scan / gitleaks`, `scan / rust-secrets`, `scan / shell-secrets`, job + bodies unchanged; checkout pinned by marches' tag (`v7.0.1`, which the + lock resolves to the template's commit `3d3c42e`). Lock entry added by + hand in the generator's shape (no new dependency; the relock bot needs + `AUTOMATION_TOKEN`). Run locally first: gitleaks 8.18.4 (checksum OK) + with the estate baseline at standards `e064539`, working tree and full + 68-commit history: no leaks; shell job: none detected; rust job: skips + (no `Cargo.toml`). actionlint clean. +* Review round (CodeRabbit on #59), each checked against PROOF-POLICY + §8.2–§8.4 at standards `d036da3`: +** The grade census uses 211 theorems as the denominator; the 235 + definitions are not obligations. By kind: 171 theorems and 231 + definitions use no axioms, 37 and 4 use `propext`, 3 and 0 use + `propext, Quot.sound`. +** The Lean receipt now gives the full commit and the `Marches/` tree + digest. It is re-run at `6db6c0a` (Lean inputs unchanged) and scoped as + historical, not a §8.4 current receipt. A CI receipt job is `OPEN`. +** `PWG-2i` and `PWG-2ii` now also require each Lean or Rocq axiom to be + admissible under disposition (c). +** In the README, the Gao–Rexford table, `valley_free_iff_gwalk` and both + tropical-adapter rows are `PROVEN-WITH-AXIOMS`, naming their axioms; + this is per-name `#print axioms`, and only `GR.*` and + `TropicalAdapter.*` headline names use any. The README's + "no dependencies" claims were stale (tropical-types) and are corrected. +** The next action below is the Agda port; 3f is deferred. + == 2026-11-04 — rung 3d closed: tropical-types re-pinned to the #65 merge commit * #52 merged before hyperpolymath/tropical-types#65, so `main` kept the @@ -432,6 +482,10 @@ $ lake env lean Marches/BadGadget.lean == Next action -Rung 3 (see ROADMAP.adoc): only 3f remains. File the postern cross-issue -once that repository exists (not found 2026-11-04). 3d and 3e are met. +The Agda port (ROADMAP.adoc, "Agda source of truth"; owner decision +2026-11-09), group by group, each recorded in `PROOF-STATUS.adoc`. It takes +precedence over rung 4. + +Deferred, not the next action: rung 3f, the postern cross-issue. It waits +on hyperpolymath/postern existing (not found 2026-11-09); 3d and 3e are met. Obtain the real files; never reconstruct from memory. One rung only.