From 7d4b92942d6ea5817577db49e06cb55b388dea76 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 9 Nov 2026 14:22:02 +0000 Subject: [PATCH 1/3] docs(proofs): PROOF-STATUS under the estate proof policy; Agda port next MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit marches is theory under standards PROOF-POLICY §1, so Agda is the source of truth, rechecked in Rocq and Lean. Its Lean development predates that ruling and is target-only evidence (§3): every theorem is Agda OPEN, Rocq OPEN, ungraded. PROOF-STATUS.adoc records that per theorem group with the §8.5 fields, the Lean leg receipt, and the plan to PWG-3/2i/2ii. Lean leg receipt on abe636a (v4.35.0): lake build 19 jobs; no sorry, admit, axiom, native_decide or extern; Lean.collectAxioms over all 446 Marches declarations: 402 none, 41 propext, 3 propext+Quot.sound, none on sorryAx or Classical.choice. Groups resting on propext are recorded PROVEN-WITH-AXIOMS, naming it. Every cited name checked with #check. CLAUDE.md no longer says "Lean 4 for proofs"; README's status table says its PROVEN means Lean-kernel accepted; ROADMAP gains the Agda section ahead of rung 4 (owner decision 2026-11-09). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- CLAUDE.md | 15 +++- PROOF-STATUS.adoc | 191 ++++++++++++++++++++++++++++++++++++++++++++++ README.adoc | 5 ++ ROADMAP.adoc | 11 +++ STATE.adoc | 22 ++++++ 5 files changed, 241 insertions(+), 3 deletions(-) create mode 100644 PROOF-STATUS.adoc 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..5eb89f6 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,191 @@ +// 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. +Denominator: 446 declarations in the `Marches` namespace on `abe636a`, of +which 0 are graded. + +[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 `abe636a`, Lean `v4.35.0` (`lean-toolchain`), +no Mathlib (the only dependency is tropical-types, core Lean). + +---- +$ 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 + 402 × axioms: none + 41 × axioms: propext + 3 × axioms: Quot.sound, propext +---- + +No declaration depends on `sorryAx` or `Classical.choice`. This receipt is a +local run, not a pinned headless CI receipt, so it does not support +`PWG-1` (§8.2) even once the other legs exist. + +== 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. + +[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` (the generated `Pos.*.injEq`, `CLabel.*.injEq` use `propext`) +|`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 then counts as the `re-proved` +Lean leg, `RECONCILED`: `PWG-2i`. +. *Rocq leg.* Dedukti transport first, hand re-proof as fallback (§2): this +is `PWG-2ii`. +. *Receipts.* A pinned headless checker run per commit for each witness: +`PWG-1`. + +Until step 1 lands for a group, nothing in this repository may be called +graded, and "PROVEN" in `README.adoc` means "accepted by the Lean kernel", +not "discharged under the estate policy". diff --git a/README.adoc b/README.adoc index 8d305fa..3123b5b 100644 --- a/README.adoc +++ b/README.adoc @@ -49,6 +49,11 @@ graded machinery (see `ROADMAP.adoc`). == Status table +`PROVEN` in this table means the Lean kernel accepted the proof. 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, and the plan for the Agda port. + [cols="3,1,2"] |=== |Claim |Status |Discharged by diff --git a/ROADMAP.adoc b/ROADMAP.adoc index d7aa668..570f77d 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -88,6 +88,17 @@ 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`, a Rocq leg `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..f2c112b 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,27 @@ = 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). + == 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 From 6db6c0ad3085146ca9d5c519d2b40aef16c4036d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Mon, 9 Nov 2026 14:24:43 +0000 Subject: [PATCH 2/3] ci(secret-scan): run the three scanners inline, from the RSR template secret-scanner.yml called a remote reusable at job level (hyperpolymath/standards secret-scanner-reusable@74d2f66) and failed at startup with zero jobs on every run since #33. This is the template's own fix (hyperpolymath/rsr-template-repo 2be7b88, its #295): three ordinary jobs whose names are the contexts scan / gitleaks, scan / rust-secrets, scan / shell-secrets, baseline pinned to metadatastician/standards e064539. Job bodies unchanged; checkout pinned by marches' lock tag v7.0.1, which resolves to the template's commit 3d3c42e. Header rewritten for marches (the template's ruleset claims do not apply here). actions.lock gains the workflow's entry by hand, in the generator's shape and order, with no new dependency (the relock bot needs AUTOMATION_TOKEN). Run locally first: gitleaks 8.18.4 (sha256 OK), estate baseline, working tree and full history: no leaks; shell job: none; rust job: skips (no Cargo.toml). actionlint 1.7.7 clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- .github/workflows/actions.lock | 2 + .github/workflows/secret-scanner.yml | 321 ++++++++++++++++++++++++++- STATE.adoc | 11 + 3 files changed, 323 insertions(+), 11 deletions(-) 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/STATE.adoc b/STATE.adoc index f2c112b..ac558dc 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -21,6 +21,17 @@ * 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. == 2026-11-04 — rung 3d closed: tropical-types re-pinned to the #65 merge commit From a990ed9e34d9d8829507908c42857d44b883cd39 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:38:05 +0000 Subject: [PATCH 3/3] =?UTF-8?q?docs(proofs):=20answer=20#59=20review=20aga?= =?UTF-8?q?inst=20PROOF-POLICY=20=C2=A78.2=E2=80=93=C2=A78.4=20(not=20a=20?= =?UTF-8?q?rung)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Grade census: denominator is the 211 theorems, not all 446 declarations; census by kind (theorem/definition x axioms). - Lean receipt: full commit and Marches/ tree digest; re-run at 6db6c0a (Lean inputs unchanged); scoped as historical, not a §8.4 current receipt; a CI receipt job is recorded OPEN. - PWG-2i/2ii also need each Lean/Rocq axiom admissible under disposition (c); same in ROADMAP. - README: GR table, valley_free_iff_gwalk and the tropical-adapter rows are PROVEN-WITH-AXIOMS with their axioms (per-name #print axioms); stale "no dependencies" claims corrected. - STATE: next action is the Agda port; 3f deferred. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- PROOF-STATUS.adoc | 68 +++++++++++++++++++++++++++++++++-------------- README.adoc | 26 ++++++++++-------- ROADMAP.adoc | 5 +++- STATE.adoc | 25 +++++++++++++++-- 4 files changed, 90 insertions(+), 34 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 5eb89f6..62dbe1b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -28,8 +28,11 @@ recorded (`RECONCILED`). Until then every Agda row is `OPEN`. Every theorem below is *`ungraded`*: no Agda witness exists, so not even `PWG-3` applies (§8.2). `foundation_diverse` is false throughout. -Denominator: 446 declarations in the `Marches` namespace on `abe636a`, of -which 0 are graded. + +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"] |=== @@ -53,8 +56,14 @@ which 0 are graded. == Lean leg receipt -Taken 2026-11-09 on `main` at `abe636a`, Lean `v4.35.0` (`lean-toolchain`), -no Mathlib (the only dependency is tropical-types, core Lean). +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 @@ -69,15 +78,23 @@ Axiom census, `Lean.collectAxioms` over every theorem and definition in the `Marches` namespace: ---- -declarations audited: 446 - 402 × axioms: none - 41 × axioms: propext - 3 × axioms: Quot.sound, propext +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`. This receipt is a -local run, not a pinned headless CI receipt, so it does not support -`PWG-1` (§8.2) even once the other legs exist. +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 @@ -86,7 +103,9 @@ local run, not a pinned headless CI receipt, so it does not support `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. +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"] |=== @@ -99,7 +118,7 @@ and names them. |Two-region composition (`Compose`) |`trace_worsens`, `wt_cycles_are_empty`, `no_back_cross`, `no_a_label_in_B` -|`PROVEN` (the generated `Pos.*.injEq`, `CLabel.*.injEq` use `propext`) +|`PROVEN` |`OPEN` |Gao–Rexford table (`GaoRexford`, namespace `GR`) @@ -179,13 +198,22 @@ next body of work. 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 then counts as the `re-proved` -Lean leg, `RECONCILED`: `PWG-2i`. +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`. -. *Receipts.* A pinned headless checker run per commit for each witness: -`PWG-1`. +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, and "PROVEN" in `README.adoc` means "accepted by the Lean kernel", -not "discharged under the estate policy". +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 3123b5b..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,10 +50,12 @@ graded machinery (see `ROADMAP.adoc`). == Status table -`PROVEN` in this table means the Lean kernel accepted the proof. 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, and the plan for the Agda port. +`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"] |=== @@ -75,7 +78,7 @@ the axiom census, and the plan for the Agda port. |`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 @@ -83,7 +86,7 @@ the axiom census, and the plan for the Agda port. |`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 @@ -187,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 @@ -214,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 570f77d..29bfce3 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -95,7 +95,10 @@ 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`, a Rocq leg `PWG-2ii`. +`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. diff --git a/STATE.adoc b/STATE.adoc index ac558dc..2182877 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -32,6 +32,23 @@ 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 @@ -465,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.