diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 38a4947..17db74f 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -81,3 +81,35 @@ jobs: run: | bash scripts/grade-receipt.sh --write --commit "$(git rev-parse --short=12 HEAD)" sed -n '1,80p' verification/receipts/agda_praxis.deed + + # The Rocq and Lean recheck legs (PROOF-POLICY §2), re-proved by hand from + # the Agda statements (verification/legs/README.adoc gives the route and the + # statement correspondence). Both provers are pinned: Coq by its Ubuntu + # package version, Lean by its release tarball's sha256. Neither leg may use + # an axiom or a library; scripts/check-legs.sh refuses either. + legs: + name: Rocq and Lean recheck legs (no axioms, no libraries) + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + - name: Install the pinned Coq + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -y coq=8.18.0+dfsg-1build2 zstd + - name: Install the pinned Lean (release tarball, sha256-checked) + env: + LEAN_URL: https://github.com/leanprover/lean4/releases/download/v4.24.0/lean-4.24.0-linux.tar.zst + LEAN_SHA256: b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec + run: | + set -euo pipefail + curl --proto '=https' --proto-redir '=https' --tlsv1.2 -fsSL "$LEAN_URL" -o "$RUNNER_TEMP/lean.tar.zst" + echo "$LEAN_SHA256 $RUNNER_TEMP/lean.tar.zst" | sha256sum --check --strict + mkdir -p "$RUNNER_TEMP/lean" + tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" + echo "$RUNNER_TEMP/lean/lean-4.24.0-linux/bin" >> "$GITHUB_PATH" + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Both legs check, with no axioms + run: bash scripts/check-legs.sh diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index eb22b47..eea3bb7 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -26,10 +26,13 @@ invocation, which this repository has met since waiver W-1 closed. |=== | Claim | PWG | Why not higher -| N-1, N-2, N-3, N-7, N-8, N-9 | `PWG-3` | The Agda proof is PROVEN under the §2.1 - invocation (receipt below). No Rocq leg and no Lean leg exists, so no leg - counts (§8.2). No axioms: `--safe`, a postulate scan of the import cone, and the - recorded cone. `foundation-diverse`: no. +| N-1, N-2, N-3, N-7, N-8, N-9 | *`PWG-2ii`* | PROVEN under the canonical + invocation `agda --safe --without-K --cubical-compatible`, with stronger flags + besides (`scripts/proof-flags.sh`), and both §2 legs count: re-proved in Rocq + and in Lean, kernel-checked with no axioms, `RECONCILED` (below). Not + `PWG-1`: that needs a per-commit receipt of each checker's observed result, + and the receipt records the gate, not its result. `foundation-diverse` is + false: Agda, Rocq and Lean are all dependent type theories (§8.3). | N-4, N-5, N-6 | `ungraded` | TESTED demonstrations (refusals, computed witnesses, a law-ablation certificate), not theorems; §8.1 grades theory @@ -40,43 +43,51 @@ N-9 is a proved *refutation*: termination-sensitive noninterference is false for the current typing rules when finishing versus non-finishing is observable. A stronger typing discipline is OPEN, and so is declassification. -A grade is not a discharge (§8.4.1): at `PWG-3` every theorem above still owes -its Rocq and Lean legs (§2). +No theorem rests on an axiom (§8.4, "axioms travel with the grade"). In Agda: +`postulates = 0` and `escape-hatches = 0` in the receipt, under `--safe`. In +Rocq, `Print Assumptions` reports `Closed under the global context` for every +leg theorem; in Lean, `#print axioms` reports `does not depend on any axioms`. -=== The two legs, recorded honestly +=== The two legs `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq and in Lean, by transport through Dedukti first and by hand re-proof as the -fallback, with the route named per theorem. Neither leg exists here, and the -policy is explicit that a policy's adoption is not an execution: each row below -would need its own CI receipt. +fallback, with the route named per theorem. Both legs exist since 2026-11-09. +Their §2.2 record (statements, universe discipline, versions, invocations, +assumptions) is link:verification/legs/README.adoc[`verification/legs/README.adoc`]; +`bash scripts/check-legs.sh` checks them, and CI runs it as the `legs` job. -[cols="1,1,1,3",options="header"] +[cols="1,1,1,1,3",options="header"] |=== -| Claim | Rocq leg | Lean leg | Record - -| N-1, N-2, N-3, N-7, N-8, N-9 | `unavailable` (`OPEN`) | `unavailable` (`OPEN`) -| No Agda→Dedukti transport and no hand re-proof has been attempted from this - repository yet. §2.2 state of each: `AGDA-VERIFIED`. Nothing was skipped - silently: this is the opening state, stated. - -| all rows | — | — -| *A leg that does not exist cannot be evidenced by a file that happens to be - present.* `verification/proofs/coq/TypeSafety.v`, +| Claim | Rocq leg | Lean leg | §2.2 state | Record + +| N-1, N-2, N-3, N-7, N-8, N-9 | `re-proved`, PROVEN | `re-proved`, PROVEN +| `RECONCILED` +| Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork + of Agda and cannot run on 2.6.4.3, and there is no released Dedukti or + Lambdapi exporter to Lean 4. So each leg restates the Agda theorem and proves + it by hand: Coq 8.18.0 with the prelude only, Lean 4.24.0 with core only (no + Mathlib). The statement comparison was written by Claude Code and is + provisional until the owner reviews it (estate doctrine 4). + +| N-4, N-5, N-6 | n/a | n/a | n/a +| Checked demonstrations, not theorems (§8.1). + +| all rows | — | — | — +| *A file that happens to be present is not a leg.* + `verification/proofs/coq/TypeSafety.v`, `verification/proofs/lean4/ApiTypes.lean` and the other skeletons under `verification/proofs/` are RSR template boilerplate ("replace with your project's …"). They prove nothing, they are not the legs, and their - `MANIFEST` lines claiming `gated` are false — no workflow invokes + `MANIFEST` lines claiming `gated` are false: no workflow invokes `scripts/check-proofs.sh`. Recorded as finding F-4 in link:docs/reports/audit/consistency-audit-2026-11-01.adoc. |=== -When a leg is attempted, `PROOF-POLICY` §2.2 fixes the record: exact -proposition, assumptions, universe discipline, source revision, compiler and -library versions, invocation, observed result, and the bridge or statement -correspondence — *transported* or *re-proved* — and the correspondence states -AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED. -Only a RECONCILED leg raises the grade. +The receipt's `(legs)` block records each leg's pinned checker, invocation and +axiom check, and the `sha256` of every leg source, so a change to a leg cannot +leave the receipt intact. `scripts/grade-receipt.sh` also refuses a claim that +counts a leg without a row in the correspondence record, and the reverse. === The §2.1 invocation, and how waiver W-1 closed diff --git a/README.adoc b/README.adoc index 8caf391..031a53c 100644 --- a/README.adoc +++ b/README.adoc @@ -77,14 +77,18 @@ Echo fibre over its outputs does not separate secret inputs — the Echo reading of noninterference, and the first candidate connection Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`. -*Grade.* The proved theorems are at **`PWG-3`** (a Proof Witness Grade, -`standards/3-practice/PROOF-POLICY.adoc` §8) and no higher: they type-check in -Agda under the canonical §2.1 invocation, `--safe --without-K ---cubical-compatible`, plus four stricter flags (`scripts/proof-flags.sh`), with -no axioms. The Rocq and Lean recheck legs that §2 requires do not exist yet, so -no leg counts; they are recorded `unavailable`, not skipped silently, and a grade -is not a discharge. Per-claim evidence is in -link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], the machine record is +*Grade.* The proved claims are at Proof Witness Grade **`PWG-2ii`** +(`PROOF-POLICY.adoc` §8) and no higher. They type-check in Agda under the +canonical §2.1 invocation, `--cubical-compatible` included, with stronger flags +besides (`scripts/proof-flags.sh`). Each is also re-proved by hand in Rocq +(Coq 8.18.0, prelude only) and in Lean (4.24.0, core only, no Mathlib), with no +axioms in either, and the statements are compared in +link:verification/legs/README.adoc[`verification/legs/README.adoc`]. That +comparison was written by Claude Code and is provisional until the owner reviews +it. Not `PWG-1`: no per-commit receipt captures each checker's observed result +yet. Not `+foundation-diverse`: no witness outside dependent type theory. +Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], +the machine record is link:verification/receipts/agda_praxis.deed[`verification/receipts/agda_praxis.deed`] (checked in CI), and link:docs/proof-debt.adoc[proof debt] is empty in all four dispositions. This paragraph states no grade the receipt does not support. diff --git a/build/just/proofs.just b/build/just/proofs.just index 605f71d..fb4db23 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -40,7 +40,7 @@ proof-check-coq: proof-scan-dangerous: @bash scripts/scan-dangerous.sh -# Regenerate the Grade-3 verification receipt (mathesis §6; PROOF-STATUS +# Regenerate the verification receipt (PROOF-POLICY §8 Proof Witness Grades; PROOF-STATUS # "Grade, and the independent-witness legs"). CI runs the --check form, so a # committed receipt that no longer matches the tree fails the gate. proof-receipt: diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index aa4cd95..308621a 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -100,13 +100,17 @@ only tested or still open. Tokens are the standard's closed vocabulary. the public result for finishing. This refutes the current rules, not every possible termination-sensitive typing discipline. -| Independent recheck in Rocq and in Lean (PROOF-POLICY §2) -| open -| — -| `PROOF-STATUS.adoc` "Proof Witness Grades, and the independent-witness legs", - `verification/receipts/agda_praxis.deed` -| No transport has been attempted and no hand re-proof exists, so every proven - theorem above is `PWG-3` (PROOF-POLICY §8) and no higher. The template skeletons under +| Independent recheck of N-1, N-2, N-3, N-7, N-8 and N-9 in Rocq and in Lean + (PROOF-POLICY §2) +| proven +| `bash scripts/check-legs.sh` (Coq 8.18.0 and Lean 4.24.0, each pinned; no + library; every theorem printed with its axioms, and there are none) +| `verification/legs/rocq/SecretTypes.v`, `verification/legs/lean/`; + correspondence in `verification/legs/README.adoc` +| Re-proved by hand, not transported: Agda2Dedukti cannot run on the pinned + Agda. The statement comparison was written by Claude Code and is provisional + until the owner reviews it. With it, every proven row above is at `PWG-2ii` + (PROOF-POLICY §8). The template skeletons under `verification/proofs/{coq,lean4}` are *not* these legs and prove nothing here. | Strengthened termination-sensitive typing discipline diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index e8757a4..897c932 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -67,12 +67,14 @@ _None in the proof development._ Two items are open *obligations* rather than proof debt, and are listed here so that they are not mistaken for either: -* *Rocq and Lean legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof - to be rechecked in Rocq and in Lean. Neither leg exists; both are recorded - `unavailable` in the receipt and in - link:../PROOF-STATUS.adoc[`PROOF-STATUS.adoc`]. An absent recheck is not an - escape hatch in a proof — the proof has no hole — but it bounds every theorem - at `PWG-3` (§8), and that bound is recorded rather than glossed. +* *Recheck legs (`PWG-2ii`, met 2026-11-09).* `PROOF-POLICY.adoc` §2 asks for + every Agda theory proof to be rechecked in Rocq and in Lean. Both legs now + exist, re-proved by hand without a library or an axiom + (link:../verification/legs/README.adoc[`verification/legs/README.adoc`]), + and the receipt records them. The obligation that remains is review: the + statement comparison was written by Claude Code and is provisional until the + owner reviews it. `PWG-1` (a per-commit receipt of each checker's observed + result) is not met. * *Termination-sensitive noninterference.* `Noninterference.OutcomeVisibility.termination-sensitive-fails` refutes TSNI for the current typing rules when finishing versus non-finishing is public. diff --git a/scripts/check-legs.sh b/scripts/check-legs.sh new file mode 100755 index 0000000..eeabcec --- /dev/null +++ b/scripts/check-legs.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-legs.sh — the Rocq and Lean recheck legs (PROOF-POLICY §2). +# +# Checks verification/legs/rocq (Coq, prelude only) and verification/legs/lean +# (Lean core only, no Mathlib, no `require`), then refuses any axiom: +# * every `Print Assumptions` line must read "Closed under the global context"; +# * every `#print axioms` line must read "does not depend on any axioms". +# A leg that does not check, or that rests on an axiom, fails this gate: a +# witness with axioms would have to be recorded PROVEN-WITH-AXIOMS and the +# receipt says it is not (PROOF-POLICY §8.4). +# +# Pins: COQ_VERSION and LEAN_VERSION below, fixed (no environment override); +# scripts/grade-receipt.sh reads them from here into the receipt. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +export LC_ALL="${LC_ALL:-C.UTF-8}" + +COQ_VERSION=8.18.0 +LEAN_VERSION=4.24.0 +fail=0 + +got="$(coqc --version | sed -n 's/^The Coq Proof Assistant, version \([0-9.]*\).*/\1/p')" +[[ "$got" == "$COQ_VERSION" ]] || { echo "ERROR: expected Coq $COQ_VERSION, found '${got:-none}'" >&2; exit 2; } +got="$(lean --version | sed -n 's/^Lean (version \([0-9.]*\),.*/\1/p')" +[[ "$got" == "$LEAN_VERSION" ]] || { echo "ERROR: expected Lean $LEAN_VERSION, found '${got:-none}'" >&2; exit 2; } + +# The Lean leg may not depend on anything: no `require` in the lakefile. +if grep -nE '^\s*\[\[require\]\]|^\s*require\b' verification/legs/lean/lakefile.toml; then + echo 'FAIL: the Lean leg declares a dependency (no Mathlib, no libraries)' >&2; fail=1 +fi +# The Rocq leg may not load the standard library. +if grep -nE '^\s*(From\s+\S+\s+)?Require\b' verification/legs/rocq/*.v; then + echo 'FAIL: the Rocq leg loads a library (prelude only)' >&2; fail=1 +fi +# No escape hatches in either leg. +if grep -nE '\b(sorry|admit|Admitted|Axiom|Parameter|axiom)\b' verification/legs/rocq/*.v verification/legs/lean/SecretTypes/*.lean; then + echo 'FAIL: an escape hatch in a leg' >&2; fail=1 +fi + +rocq_out="$(cd verification/legs/rocq && coqc -q SecretTypes.v 2>&1)" || { echo "$rocq_out" >&2; echo 'FAIL: the Rocq leg does not check' >&2; exit 1; } +n_closed="$(grep -c '^Closed under the global context$' <<< "$rocq_out" || true)" +n_print="$(grep -c '^Print Assumptions ' verification/legs/rocq/SecretTypes.v)" +if [[ "$n_closed" != "$n_print" ]] || grep -vq '^Closed under the global context$' <<< "$rocq_out"; then + echo "$rocq_out" >&2; echo "FAIL: the Rocq leg rests on an axiom ($n_closed of $n_print closed)" >&2; fail=1 +else + echo "PASS: Rocq leg (Coq $COQ_VERSION), $n_print theorems closed under the global context" +fi + +lean_out="$(cd verification/legs/lean && lake build >/dev/null && lake env lean Axioms.lean 2>&1)" \ + || { echo "$lean_out" >&2; echo 'FAIL: the Lean leg does not check' >&2; exit 1; } +n_free="$(grep -c 'does not depend on any axioms$' <<< "$lean_out" || true)" +n_ax="$(grep -c '^#print axioms ' verification/legs/lean/Axioms.lean)" +if [[ "$n_free" != "$n_ax" ]] || grep -vq 'does not depend on any axioms$' <<< "$lean_out"; then + echo "$lean_out" >&2; echo "FAIL: the Lean leg rests on an axiom ($n_free of $n_ax free)" >&2; fail=1 +else + echo "PASS: Lean leg (Lean $LEAN_VERSION, core only), $n_ax theorems depend on no axioms" +fi + +(( fail == 0 )) || exit 1 +echo 'PASS: both recheck legs' diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index 5143d79..82205d6 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -9,7 +9,11 @@ # # Proof Witness Grades: standards/3-practice/PROOF-POLICY.adoc §8 (owner # ruling 2026-11-04). PWG-3: the Agda proof is PROVEN under the §2.1 -# invocation and no Rocq or Lean leg counts yet. The record carries the +# invocation. PWG-2ii: PWG-3, and both the Rocq and the Lean leg count: +# kernel-checked (scripts/check-legs.sh, no axioms) and RECONCILED against +# the Agda statement (verification/legs/README.adoc). Not PWG-1: that needs +# a per-commit receipt of each checker's observed result, which this file +# is not. The record carries the # §8.5 fields: pwg, foundation-diverse, and for each leg its route, its §5 # token and its §2.2 correspondence state. A grade is derived, never # asserted (§8.4): it is computed below from the legs, not typed in. @@ -57,20 +61,20 @@ done # | RECONCILED | COUNTEREXAMPLE | QUARANTINED. Only RECONCILED counts (§8.2). claims() { cat <<'ROWS' -N-1|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED -N-2|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED -N-3|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-1|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED +N-2|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED +N-3|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED N-4|tested-only|demonstration|n/a|n/a|n/a|n/a N-5|tested-only|demonstration|n/a|n/a|n/a|n/a N-6|tested-only|demonstration|n/a|n/a|n/a|n/a -N-7|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED -N-8|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED -N-9|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-7|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED +N-8|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED +N-9|proven|theorem|re-proved|RECONCILED|re-proved|RECONCILED ROWS } # PROOF-POLICY §8.2: derive the grade from the Agda token and the legs. A leg -# counts only when it is RECONCILED (§2.2); none exists yet, so no leg counts. +# counts only when it is RECONCILED (§2.2). # Print the PWG for one claim row's token, kind and two legs' §2.2 states. pwg_of() { local token="$1" kind="$2" coq_state="$3" lean_state="$4" counted=0 @@ -126,6 +130,42 @@ check_claim_ids() { fi } +# The leg sources, in sorted order: everything a leg's kernel reads. +leg_sources() { + find verification/legs/rocq -name '*.v' | LC_ALL=C sort + find verification/legs/lean -name '*.lean' -not -path '*/.lake/*' | LC_ALL=C sort + printf '%s\n' verification/legs/lean/lakefile.toml verification/legs/lean/lean-toolchain +} + +# Print the (legs) block: per leg, the pinned checker, its invocation, the +# axiom check, and the sha256 of every input. The pins are read from +# scripts/check-legs.sh, the one place the gate takes them from. +emit_legs() { + local coq lean + coq="$(sed -n 's/^COQ_VERSION=\(.*\)$/\1/p' scripts/check-legs.sh)" + lean="$(sed -n 's/^LEAN_VERSION=\(.*\)$/\1/p' scripts/check-legs.sh)" + printf ' (legs\n :gate "bash scripts/check-legs.sh"\n :ci ".github/workflows/proofs.yml (job legs)"\n' + printf ' :correspondence "verification/legs/README.adoc"\n' + printf ' :route "re-proved"\n' + printf ' :route-reason "Agda2Dedukti is an Agda backend pinned to a fork (b026db1, GHC 8.10) and cannot run on Agda %s; no released Dedukti/Lambdapi exporter to Lean 4, and no pinned route to Rocq"\n' "$agda_version" + printf ' :state "RECONCILED"\n' + printf ' :review "statement comparison written by Claude Code; provisional until owner review (estate doctrine 4)"\n' + printf ' (leg :prover "rocq" :checker "coqc" :version "%s" :invocation "coqc -q SecretTypes.v (in verification/legs/rocq)" :libraries "none (no Require)" :axioms "none (Print Assumptions: Closed under the global context)")\n' "$coq" + printf ' (leg :prover "lean" :checker "lean" :version "%s" :invocation "lake build; lake env lean Axioms.lean (in verification/legs/lean)" :libraries "none (lakefile has no require; no Mathlib)" :axioms "none (#print axioms: does not depend on any axioms)")\n' "$lean" + printf ' (inputs\n' + while read -r p; do + printf ' (input :path "%s" :sha256 "%s")\n' "$p" "$(sha256sum "$p" | cut -d' ' -f1)" + done < <(leg_sources) + printf ' ))\n' +} + +# A leg's §5 token: a RECONCILED re-proof is kernel-checked with no axiom +# (scripts/check-legs.sh), so it is proven; any other state is still open. +leg_token() { + local state="$1" + [[ "$state" == RECONCILED ]] && printf 'proven' || printf 'open' +} + # Print the derived receipt, including claim rows, module hashes and fixtures. emit() { printf ';; SPDX-License-Identifier: CC-BY-SA-4.0\n' @@ -155,13 +195,14 @@ emit() { printf ' :library-dependencies 0\n :axioms-assumed 0\n' printf ' :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero")\n' printf ' ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded.\n' - printf ' ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts.\n' + printf ' ; Rocq and Lean legs: re-proved by hand (Agda2Dedukti cannot run on the pinned Agda), RECONCILED in verification/legs/README.adoc.\n' + emit_legs printf ' (claims\n' while IFS='|' read -r id token kind coq coq_state lean lean_state; do if [[ "$kind" == theorem ]]; then printf ' (claim :id "%s" :token "%s" :kind "%s" :pwg "%s" :foundation-diverse #f\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")" - printf ' (leg :prover "rocq" :route "%s" :token "open" :state "%s" :receipts ())\n' "$coq" "$coq_state" - printf ' (leg :prover "lean" :route "%s" :token "open" :state "%s" :receipts ()))\n' "$lean" "$lean_state" + printf ' (leg :prover "rocq" :route "%s" :token "%s" :state "%s" :receipts ())\n' "$coq" "$(leg_token "$coq_state")" "$coq_state" + printf ' (leg :prover "lean" :route "%s" :token "%s" :state "%s" :receipts ()))\n' "$lean" "$(leg_token "$lean_state")" "$lean_state" else printf ' (claim :id "%s" :token "%s" :kind "%s" :pwg "%s")\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")" fi @@ -177,7 +218,23 @@ emit() { printf ' )\n)\n' } +# A RECONCILED leg must have a row in the correspondence record, and a claim +# with a correspondence row must count its legs: the grade is derived from +# the §2.2 record, not typed beside it (PROOF-POLICY §8.4). +check_leg_records() { + local rec=verification/legs/README.adoc counted recorded + counted="$(claims | awk -F'|' '$5=="RECONCILED"||$7=="RECONCILED"{print $1}' | LC_ALL=C sort)" + recorded="$(grep -oE '^\| N-[0-9]+$' "$rec" 2>/dev/null | tr -d '| ' | LC_ALL=C sort -u || true)" + if [[ "$counted" != "$recorded" ]]; then + echo "ERROR: claims with a RECONCILED leg differ from the rows of $rec" >&2 + diff <(printf '%s\n' "$recorded") <(printf '%s\n' "$counted") \ + | grep -E '^[<>]' | sed "s|^<| only in $rec:|; s/^>/ only in grade-receipt.sh:/" >&2 + exit 1 + fi +} + check_claim_ids +check_leg_records case "$mode" in --write|"") diff --git a/verification/legs/README.adoc b/verification/legs/README.adoc new file mode 100644 index 0000000..6c748fd --- /dev/null +++ b/verification/legs/README.adoc @@ -0,0 +1,184 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += The Rocq and Lean recheck legs +:revdate: 2026-11-09 + +`standards/3-practice/PROOF-POLICY.adoc` §2 requires every Agda theory proof to +be rechecked in Rocq and in Lean. Transport through Dedukti comes first, and a +hand re-proof without Mathlib is the fallback. This directory holds both legs +for N-1, N-2, N-3, N-7, N-8 and N-9, and this file is their §2.2 +correspondence record. + +`bash scripts/check-legs.sh` checks both. CI runs it as the `legs` job of +`.github/workflows/proofs.yml`. + +== Route: `re-proved`, and why not `transported` + +Transport was tried first, as the policy orders, and is not available today: + +* Agda2Dedukti, the only Agda→Dedukti translator, builds against its own fork + of Agda (pinned commit `b026db1`, GHC 8.10, Stackage LTS 18.21). It is an Agda + backend, so it cannot run on Agda 2.6.4.3, the version the gate pins. +* Even with a Dedukti term, there is no released exporter from Dedukti or + Lambdapi to Lean 4, and no released route to Rocq that this repository + could pin and run in CI. + +So both legs are hand re-proofs of the Agda statements. Each leg was written +from the Agda module, statement by statement and proof by proof, and checked by +its own kernel. Nothing is translated mechanically, so the statements are +compared by hand below. + +== Versions and invocations + +[cols="1,2,3",options="header"] +|=== +| Leg | Version | Invocation + +| Rocq +| Coq 8.18.0 (Ubuntu 24.04 package `coq=8.18.0+dfsg-1build2`) +| `coqc -q SecretTypes.v`, in `rocq/`. + The file loads no library, not even with `Require`: only Coq's prelude. + +| Lean +| Lean 4.24.0 (release tarball, sha256 + `b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec`) +| `lake build`, then `lake env lean Axioms.lean`, in `lean/`. `lakefile.toml` + declares no `require`, so there is no Mathlib and no other package: only + Lean core. +|=== + +`scripts/check-legs.sh` refuses the run if either version differs, if a +`require` or a `Require` appears, or if any source contains `sorry`, `admit`, +`Admitted`, `Axiom` or `Parameter`. + +== Assumptions: none + +Every theorem below is printed with its axioms (§8.4): + +* Rocq: `Print Assumptions` reports `Closed under the global context` for + all 11 theorems. The prelude's classical axioms are not loaded, so none can + enter. +* Lean: `#print axioms` (in `lean/Axioms.lean`) reports + `does not depend on any axioms` for all 11. In particular, no `propext`, + `Quot.sound` or `Classical.choice`. + +`check-legs.sh` fails unless every one of the 22 lines says so. + +== Universe discipline + +Agda's `Set` is `Type` in both legs. The order `_⊑_`, an observer's `sees` and +the typing derivations are `Type`-valued in both, as in Agda, so a proof of +`x ⊑ y` is data in all three systems. A store agreement is an equation between +naturals: `Prop` in the legs and a set in Agda. The naturals have decidable +equality, so the two readings hold the same information. + +The Agda proof of N-7 splits on whether the observer sees a branch label, +under double negation, because agreement is stable (`¬¬ (s ≈ s') → s ≈ s'`). +Both legs make the same move (`agree_stable`, `by_cases_sees`), so neither leg +uses excluded middle. + +== Statement correspondence + +The legs keep the Agda names where the syntax allows. Lean writes `₁`/`₂` and +`'`, Rocq writes `1`/`2` and `0`/`1`. The statements are compared on the +following points; any other difference is notation. + +`exec`:: Agda defines `exec` with two helpers, `execIf` and `execWhile`. Both +legs define one function, `run prev`, structural in the command, with `prev` +the run at one less fuel (`none` at fuel zero), and set `exec 0 = run none` +and `exec (f + 1) = run (some (exec f))`. Clause by clause this is Agda's +definition: sequence and `ifz` keep the fuel, a loop at `f + 1` runs its body +and re-enters at `f`, and a loop at `0` is `nothing`. The legs prove the +clauses as lemmas (`exec_skip`, `exec_assign`, `exec_seq`, `exec_ifz`, +`exec_while_zero` in Lean, `exec_while_succ`), each by `rfl` or by cases. The +split exists so that Lean needs no well-founded recursion. Well-founded +recursion would bring in `propext`. + +`Maybe`:: `Option` in Lean and `option` in Rocq, with `nothing`/`just` as +`none`/`some`. + +The record:: Agda has one record, `Lattice` (`SecretTypes.Lattice.Record`), with +the carrier, `_⊑_`, `_⊔_`, `⊥ₗ` and exactly three laws: `⊑-trans`, +`⊔-upper₁` and `⊔-upper₂`. The legs split it into `Signature`, with the +operations and no laws, and `Lattice`, which extends it with the same three +laws. `TINI` and the typing rules are stated over `Signature`. That is what +the Agda `Statement` and `Typing.Generic` modules are parameterised by, and the +N-8 countermodels need it to state `TINI` where a law fails. The generic proof +(`tini`) takes a `Lattice`. The laws are the same three, so neither leg is +weaker or stronger than Agda here. + +`Observer`:: `sees : Carrier → Type` and down-closure, as in Agda. +`principal L o` sees `· ⊑ o`, and its down-closure is `le_trans`, as in Agda. + +`Vars`:: a type with decidable equality. In Lean, `DecidableEq Var`; in +Rocq, `{x = y} + {x <> y}`. Agda uses `Dec`. All three are the same choice +data. + +== Claim by claim + +The state of every row is `RECONCILED` (§2.2): AGDA-VERIFIED by +`scripts/check.sh`, COQ-CHECKED and LEAN-CHECKED by `scripts/check-legs.sh`, +and the statements compared above with no bridge pending. + +[cols="1,2,2,2",options="header"] +|=== +| Claim | Agda | Lean | Rocq + +| N-1 +| `Noninterference.tini` +| `SecretTypes.Two.tini_two` +| `Two.tini_two` + +| N-2 +| `Noninterference.Generic.eval-low`; `Noninterference.eval-low` +| `SecretTypes.eval_low`; `SecretTypes.Two.eval_low_two` +| `eval_low`; `Two.eval_low_two` + +| N-3 +| `Noninterference.Generic.confine`; `Noninterference.confine` +| `SecretTypes.confine` (with `confine_loop`); `SecretTypes.Two.confine_two` +| `confine` (with `confine_loop`); `Two.confine_two` + +| N-7 +| `Noninterference.Generic.tini : (V : Observer 𝓛) → TINI (Observer.sees V)` +| `SecretTypes.tini` +| `tini : TINI L label (sees O)` + +| N-8 +| `Countermodels.NoUpper₁.refutes`, `NoUpper₂.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes`, each `¬ TINI _` +| `SecretTypes.Countermodels.NoUpper₁.refutes`, `NoUpper₂.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes`, each `TINI … → False` +| `Countermodels.NoUpper1.refutes`, `NoUpper2.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes` + +| N-9 +| `Noninterference.OutcomeVisibility.termination-sensitive-fails : ¬ TSNI` +| `SecretTypes.Two.termination_sensitive_fails : TSNI → False` +| `Two.termination_sensitive_fails : TSNI -> False` +|=== + +Each N-8 countermodel is the Agda one: the same carrier, the same failing law, +the same typed program and the same two stores. For `NoTrans`, the +five-point order and its `join` are Agda's, case by case. N-9 uses the same +`secret-loop`, the same stores `s₀ = (0, 0)` and `s₁ = (0, 1)`, and the same +outcome at fuel 3. + +N-4, N-5 and N-6 have no leg. They are checked demonstrations, not theorems +(§8.1). + +== What the legs do not establish + +* They are re-proofs, not transports. The match between each leg statement + and its Agda statement rests on the comparison above. Claude Code wrote it, + and it is provisional until the owner reviews it (estate doctrine 4). No + tool checks it. +* `foundation_diverse` (§8.3) stays false. Lean's and Rocq's kernels are + independent of Agda's, but all three are dependent type theories. The tag + needs a witness in a different foundation, such as Isabelle/HOL, and none + exists. +* The grade is `PWG-2ii`, not `PWG-1`. `PWG-1` needs a receipt per witness, + per commit, recording the observed result of a pinned checker run on that + commit (§8.2). The receipt here records the legs' versions, invocations and + input digests; the CI log of the `legs` job is the observed result, and it + is not yet captured as a receipt. diff --git a/verification/legs/lean/.gitignore b/verification/legs/lean/.gitignore new file mode 100644 index 0000000..a2524e9 --- /dev/null +++ b/verification/legs/lean/.gitignore @@ -0,0 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +.lake/ +# Written by `lake build`; with no `require` it lists no package, and it is not +# JCS-serialised (estate JSON policy), so it is not committed. +lake-manifest.json diff --git a/verification/legs/lean/Axioms.lean b/verification/legs/lean/Axioms.lean new file mode 100644 index 0000000..34b07ab --- /dev/null +++ b/verification/legs/lean/Axioms.lean @@ -0,0 +1,15 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Prints the axioms every Lean-leg theorem rests on (PROOF-POLICY §8.4). +-- scripts/check-legs.sh requires each line to read "does not depend on any axioms". +import SecretTypes +#print axioms SecretTypes.eval_low +#print axioms SecretTypes.confine +#print axioms SecretTypes.tini +#print axioms SecretTypes.Two.eval_low_two +#print axioms SecretTypes.Two.confine_two +#print axioms SecretTypes.Two.tini_two +#print axioms SecretTypes.Two.termination_sensitive_fails +#print axioms SecretTypes.Countermodels.NoUpper₁.refutes +#print axioms SecretTypes.Countermodels.NoUpper₂.refutes +#print axioms SecretTypes.Countermodels.NoDownClosure.refutes +#print axioms SecretTypes.Countermodels.NoTrans.refutes diff --git a/verification/legs/lean/SecretTypes.lean b/verification/legs/lean/SecretTypes.lean new file mode 100644 index 0000000..3fba1f3 --- /dev/null +++ b/verification/legs/lean/SecretTypes.lean @@ -0,0 +1,4 @@ +-- SPDX-License-Identifier: MPL-2.0 +import SecretTypes.Generic +import SecretTypes.Two +import SecretTypes.Countermodels diff --git a/verification/legs/lean/SecretTypes/Countermodels.lean b/verification/legs/lean/SecretTypes/Countermodels.lean new file mode 100644 index 0000000..3cf8884 --- /dev/null +++ b/verification/legs/lean/SecretTypes/Countermodels.lean @@ -0,0 +1,216 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-8: each law +generic TINI uses is necessary. Mirrors src/SecretTypes/Countermodels.agda +module by module: drop one law, keep the typing rules, and a well-typed +program leaks, so `TINI` is refuted at that signature. Lean core only, no +axioms. +-/ +import SecretTypes.Two + +namespace SecretTypes.Countermodels +open SecretTypes SecretTypes.Two Label Var + +/-- `std`: `lo` public, `hi` secret. -/ +def std : two.Var → Label + | lo => L + | hi => H + +/-- The two-point signature with a given join. -/ +def withJoin (j : Label → Label → Label) : Signature where + Carrier := Label + le := le + join := j + bot := L + +/-- Seen by the observer at `L`: exactly the labels below `L`. -/ +def belowL : Label → Type := fun x => le x L + +theorem agree_s₀_s₁ (S : Signature) (hS : S.Carrier = Label) (lab' : two.Var → S.Carrier) + (sees : S.Carrier → Type) (hhi : sees (lab' hi) → False) : + Agree S lab' sees s₀ s₁ := fun + | lo, _ => rfl + | hi, v => (hhi v).elim + +/-! `NoUpper₁`: the join `x ⊔ʳ y = y` keeps `⊔-upper₂` and drops `⊔-upper₁`. -/ +namespace NoUpper₁ + +def joinR : Label → Label → Label := fun _ y => y + +def S : Signature := withJoin joinR + +def upper₂ : ∀ x y : Label, le y (joinR x y) + | _, L => () + | _, H => () + +theorem not_upper₁ : (∀ x y : Label, le x (joinR x y)) → False := + fun h => nomatch (h H L : Empty) + +/-- `implicit = ifz (var hi) (lo ≔ lit 0) (lo ≔ lit 1)`, typed at `L`. -/ +def implicitFlow : Cmd two := .ifz (.var hi) (.assign lo (.lit 0)) (.assign lo (.lit 1)) + +def typed : Typed S std L implicitFlow := .ifz (.assign ()) (.assign ()) + +theorem refutes : TINI S std belowL → False := fun tini => + nomatch (tini 1 1 typed (agree_s₀_s₁ S rfl std belowL (fun v => nomatch (v : Empty))) + rfl rfl lo () : 0 = 1) + +end NoUpper₁ + +/-! `NoUpper₂`: the join `x ⊔ˡ y = x` keeps `⊔-upper₁` and drops `⊔-upper₂`. -/ +namespace NoUpper₂ + +def joinL : Label → Label → Label := fun x _ => x + +def S : Signature := withJoin joinL + +def upper₁ : ∀ x y : Label, le x (joinL x y) + | L, _ => () + | H, _ => () + +theorem not_upper₂ : (∀ x y : Label, le y (joinL x y)) → False := + fun h => nomatch (h L H : Empty) + +/-- `explicit = lo ≔ var hi`, typed at `L`. -/ +def explicitFlow : Cmd two := .assign lo (.var hi) + +def typed : Typed S std L explicitFlow := .assign () + +theorem refutes : TINI S std belowL → False := fun tini => + nomatch (tini 1 1 typed (agree_s₀_s₁ S rfl std belowL (fun v => nomatch (v : Empty))) + rfl rfl lo () : 0 = 1) + +end NoUpper₂ + +/-! `NoDownClosure`: the observer that sees exactly `H` is not down-closed. -/ +namespace NoDownClosure + +def sees : Label → Type := fun x => PLift (x = H) + +theorem not_down_closed : (∀ {x y : Label}, le x y → sees y → sees x) → False := + fun h => nomatch (h (x := L) (y := H) () ⟨rfl⟩).down + +def S : Signature := withJoin join + +/-- `up = hi ≔ var lo`, typed at `L`. -/ +def up : Cmd two := .assign hi (.var lo) + +def typed : Typed S std L up := .assign () + +def t₀ : Store two := pair 0 0 +def t₁ : Store two := pair 1 0 + +theorem agree : Agree S std sees t₀ t₁ := fun + | lo, v => nomatch v.down + | hi, _ => rfl + +theorem refutes : TINI S std sees → False := fun tini => + nomatch (tini 1 1 typed agree rfl rfl hi ⟨rfl⟩ : 0 = 1) + +end NoDownClosure + +/-! `NoTrans`: without `⊑-trans`, "flows to `o`" can fail to be down-closed, +and TINI fails for that principal observer. -/ +namespace NoTrans + +inductive P where + | B | H' | M | L' | T + +open P + +inductive Le : P → P → Type where + | refl {x} : Le x x + | bot {x} : Le B x + | top {x} : Le x T + | HM : Le H' M + | ML : Le M L' + +def join : P → P → P + | B, y => y + | T, _ => T + | H', B => H' + | H', H' => H' + | H', M => M + | H', L' => T + | H', T => T + | M, B => M + | M, H' => M + | M, M => M + | M, L' => L' + | M, T => T + | L', B => L' + | L', H' => T + | L', M => L' + | L', L' => L' + | L', T => T + +def upper₁ : ∀ x y : P, Le x (join x y) + | B, _ => .bot + | T, _ => .refl + | H', B => .refl + | H', H' => .refl + | H', M => .HM + | H', L' => .top + | H', T => .top + | M, B => .refl + | M, H' => .refl + | M, M => .refl + | M, L' => .ML + | M, T => .top + | L', B => .refl + | L', H' => .top + | L', M => .refl + | L', L' => .refl + | L', T => .top + +def upper₂ : ∀ x y : P, Le y (join x y) + | B, _ => .refl + | T, _ => .top + | H', B => .bot + | H', H' => .refl + | H', M => .refl + | H', L' => .top + | H', T => .refl + | M, B => .bot + | M, H' => .HM + | M, M => .refl + | M, L' => .refl + | M, T => .refl + | L', B => .bot + | L', H' => .top + | L', M => .ML + | L', L' => .refl + | L', T => .refl + +theorem not_trans : (∀ {x y z : P}, Le x y → Le y z → Le x z) → False := + fun t => nomatch (t Le.HM Le.ML : Le H' L') + +def S : Signature where + Carrier := P + le := Le + join := join + bot := B + +def label : two.Var → P + | lo => M + | hi => H' + +/-- `explicit = lo ≔ var hi`, typed at `B` (needs only `H′ ≤ M`). -/ +def explicitFlow : Cmd two := .assign lo (.var hi) + +def typed : Typed S label B explicitFlow := .assign .HM + +def belowL' : P → Type := fun x => Le x L' + +theorem agree : Agree S label belowL' s₀ s₁ := fun + | lo, _ => rfl + | hi, v => nomatch (v : Le H' L') + +theorem refutes : TINI S label belowL' → False := fun tini => + nomatch (tini 1 1 typed agree rfl rfl lo Le.ML : 0 = 1) + +end NoTrans + +end SecretTypes.Countermodels diff --git a/verification/legs/lean/SecretTypes/Generic.lean b/verification/legs/lean/SecretTypes/Generic.lean new file mode 100644 index 0000000..d2e078f --- /dev/null +++ b/verification/legs/lean/SecretTypes/Generic.lean @@ -0,0 +1,411 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-2, N-3 and N-7: +termination-insensitive noninterference over any lattice record and any +down-closed observer. The statements mirror, line for line: + src/SecretTypes/Vars.agda, Lang.agda, Lattice/Record.agda, + Typing/Generic.agda, Noninterference/Statement.agda, Noninterference/Generic.agda. +Lean core only: no Mathlib, no Std, no classical axioms +(see the `#print axioms` lines at the end of this file). + +Universe discipline: Agda's `Set` is Lean's `Type`. The order, an +observer's `sees` and the typing derivations are `Type`-valued here, as in +Agda, so a proof may not use proof irrelevance that the Agda statement does +not grant. Equality of naturals is `Prop` in Lean and a set in Agda; +naturals have decidable equality, so the two readings coincide. +-/ +namespace SecretTypes + +/-- `SecretTypes.Vars`: variables with decidable equality. -/ +structure Vars where + Var : Type + deq : DecidableEq Var + +/-- What `SecretTypes.Noninterference.Statement` and `Typing.Generic` are +parameterised by: a carrier, an order, a join and the label of a literal, with +no laws. The countermodels (N-8) instantiate the statement at signatures +that lack a law, so the statement cannot ask for one. -/ +structure Signature where + Carrier : Type + le : Carrier → Carrier → Type + join : Carrier → Carrier → Carrier + bot : Carrier + +/-- `SecretTypes.Lattice.Record.Lattice`: a signature with the three laws +generic TINI uses (the certified census, N-6). -/ +structure Lattice extends Signature where + le_trans : ∀ {x y z : Carrier}, le x y → le y z → le x z + upper₁ : ∀ x y : Carrier, le x (join x y) + upper₂ : ∀ x y : Carrier, le y (join x y) + +/-- `SecretTypes.Lattice.Record.Observer`: a down-closed set of labels. -/ +structure Observer (L : Lattice) where + sees : L.Carrier → Type + down : ∀ {x y : L.Carrier}, L.le x y → sees y → sees x + +/-- `principal`: the observer at level `o` sees exactly the labels below it. -/ +def principal (L : Lattice) (o : L.Carrier) : Observer L where + sees x := L.le x o + down h v := L.le_trans h v + +section Lang +variable (V : Vars) + +/-- `Store = Var → Nat`. -/ +abbrev Store := V.Var → Nat + +inductive Expr where + | lit : Nat → Expr + | var : V.Var → Expr + | plus : Expr → Expr → Expr + +inductive Cmd where + | skip : Cmd + | assign : V.Var → Expr V → Cmd + | seq : Cmd → Cmd → Cmd + | ifz : Expr V → Cmd → Cmd → Cmd + | «while» : Expr V → Cmd → Cmd + +variable {V} + +def eval (s : Store V) : Expr V → Nat + | .lit n => n + | .var x => s x + | .plus a b => eval s a + eval s b + +/-- `update x n s y = select (x ≟ᵥ y) n (s y)`. -/ +def update (x : V.Var) (n : Nat) (s : Store V) : Store V := fun y => + match V.deq x y with + | .isTrue _ => n + | .isFalse _ => s y + +/-- `bind` of `SecretTypes.Prelude`. -/ +def bind {A : Type} : Option A → (A → Option A) → Option A + | none, _ => none + | some a, f => f a + +/-- One step of fuel: run a command, using `prev` (the run at one less fuel) +to re-enter a loop. `none` is fuel zero, where a loop does not finish. +Structural in the command, so `exec` below is structural in both fuel and +command and its equations hold by `rfl` (no well-founded recursion, hence no +`propext` or `funext` in the proofs). -/ +def run (prev : Option (Cmd V → Store V → Option (Store V))) : + Cmd V → Store V → Option (Store V) + | .skip, s => some s + | .assign x e, s => some (update x (eval s e) s) + | .seq c₁ c₂, s => bind (run prev c₁ s) (run prev c₂) + | .ifz e c₁ c₂, s => + match eval s e with + | 0 => run prev c₁ s + | _ + 1 => run prev c₂ s + | .«while» e c, s => + match prev with + | none => none + | some p => + match eval s e with + | 0 => bind (p c s) (p (.«while» e c)) + | _ + 1 => some s + +/-- `exec` of `SecretTypes.Lang`: `exec fuel c s` is `some t` if `c` finishes +within `fuel`, else `none`. Equal to Agda's `exec`, `execIf` and +`execWhile` clause by clause: sequence and `ifz` keep the fuel, a loop at +`fuel + 1` runs its body and re-enters at `fuel`, a loop at `0` is `none`. -/ +def exec : Nat → Cmd V → Store V → Option (Store V) + | 0 => run none + | f + 1 => run (some (exec f)) + +end Lang + +section Typing +variable {V : Vars} (L : Signature) (label : V.Var → L.Carrier) + +/-- `lab` of `SecretTypes.Typing.Generic`. -/ +def lab : Expr V → L.Carrier + | .lit _ => L.bot + | .var x => label x + | .plus a b => L.join (lab a) (lab b) + +/-- `_⊢_` of `SecretTypes.Typing.Generic`: Volpano–Smith typing with a +program-counter label. -/ +inductive Typed : L.Carrier → Cmd V → Type where + | skip {pc} : Typed pc .skip + | assign {pc x e} : L.le (L.join pc (lab L label e)) (label x) → Typed pc (.assign x e) + | seq {pc c₁ c₂} : Typed pc c₁ → Typed pc c₂ → Typed pc (.seq c₁ c₂) + | ifz {pc e c₁ c₂} : Typed (L.join pc (lab L label e)) c₁ → + Typed (L.join pc (lab L label e)) c₂ → Typed pc (.ifz e c₁ c₂) + | «while» {pc e c} : Typed (L.join pc (lab L label e)) c → Typed pc (.«while» e c) + +/-- `_≈[_]_` of `SecretTypes.Noninterference.Statement`. -/ +def Agree (sees : L.Carrier → Type) (s s' : Store V) : Prop := + ∀ x, sees (label x) → s x = s' x + +/-- `TINI` of `SecretTypes.Noninterference.Statement`. -/ +def TINI (sees : L.Carrier → Type) : Prop := + ∀ {pc : L.Carrier} {c : Cmd V} (fuel fuel' : Nat) {s s' t t' : Store V}, + Typed L label pc c → Agree L label sees s s' → + exec fuel c s = some t → exec fuel' c s' = some t' → Agree L label sees t t' + +end Typing + +section Proof +variable {V : Vars} {L : Lattice} {label : V.Var → L.Carrier} (O : Observer L) + +/-! Unfolding equations for `exec`, one per command form. -/ + +/-- The branch an `ifz` takes on guard value `n`. -/ +def branch (n : Nat) (c₁ c₂ : Cmd V) : Cmd V := + match n with + | 0 => c₁ + | _ + 1 => c₂ + +theorem exec_skip (f : Nat) (s : Store V) : exec f .skip s = some s := by + cases f <;> rfl + +theorem exec_assign (f : Nat) (x : V.Var) (e : Expr V) (s : Store V) : + exec f (.assign x e) s = some (update x (eval s e) s) := by + cases f <;> rfl + +theorem exec_seq (f : Nat) (c₁ c₂ : Cmd V) (s : Store V) : + exec f (.seq c₁ c₂) s = bind (exec f c₁ s) (exec f c₂) := by + cases f <;> rfl + +theorem exec_ifz (f : Nat) (e : Expr V) (c₁ c₂ : Cmd V) (s : Store V) : + exec f (.ifz e c₁ c₂) s = exec f (branch (eval s e) c₁ c₂) s := by + cases f <;> (show run _ _ _ = run _ _ _; simp only [run]; cases eval s e <;> rfl) + +theorem exec_while_zero (e : Expr V) (c : Cmd V) (s : Store V) : + exec 0 (.«while» e c) s = none := rfl + +theorem exec_while_succ (f : Nat) (e : Expr V) (c : Cmd V) (s : Store V) : + exec (f + 1) (.«while» e c) s = + (match eval s e with + | 0 => bind (exec f c s) (exec f (.«while» e c)) + | _ + 1 => some s) := rfl + +theorem bind_some {A : Type} {m : Option A} {f : A → Option A} {t : A} : + bind m f = some t → ∃ a, m = some a ∧ f a = some t := by + cases m with + | none => intro h; cases h + | some a => intro h; exact ⟨a, rfl, h⟩ + +/-- A branch typed under a counter is typed under it, whichever is taken. -/ +def branch_typed {pc : L.Carrier} (n : Nat) {c₁ c₂ : Cmd V} + (d₁ : Typed L.toSignature label pc c₁) (d₂ : Typed L.toSignature label pc c₂) : + Typed L.toSignature label pc (branch n c₁ c₂) := + match n with + | 0 => d₁ + | _ + 1 => d₂ + +/-- `unseen-⊔`. -/ +theorem unseen_join {pc : L.Carrier} (y : L.Carrier) (np : O.sees pc → False) : + O.sees (L.join pc y) → False := + fun v => np (O.down (L.upper₁ pc y) v) + +/-- N-2, `eval-low`: an expression whose label the observer sees reads the +same in agreeing stores. -/ +theorem eval_low : ∀ (e : Expr V) {s s' : Store V}, O.sees (lab L.toSignature label e) → + Agree L.toSignature label O.sees s s' → eval s e = eval s' e + | .lit _, _, _, _, _ => rfl + | .var x, _, _, v, eq => eq x v + | .plus a b, _, _, v, eq => by + show eval _ a + eval _ b = eval _ a + eval _ b + rw [eval_low a (O.down (L.upper₁ _ _) v) eq, eval_low b (O.down (L.upper₂ _ _) v) eq] + +theorem agree_refl {s : Store V} : Agree L.toSignature label O.sees s s := fun _ _ => rfl + +theorem agree_symm {s s' : Store V} (h : Agree L.toSignature label O.sees s s') : + Agree L.toSignature label O.sees s' s := fun x v => (h x v).symm + +theorem agree_trans {s s' s'' : Store V} (h : Agree L.toSignature label O.sees s s') + (k : Agree L.toSignature label O.sees s' s'') : Agree L.toSignature label O.sees s s'' := + fun x v => (h x v).trans (k x v) + +/-- `confine-assign`: an assignment allowed under an unseen counter leaves +every seen variable alone. -/ +theorem confine_assign {pc : L.Carrier} (x : V.Var) (e : Expr V) (n : Nat) (s : Store V) + (np : O.sees pc → False) (ok : L.le (L.join pc (lab L.toSignature label e)) (label x)) : + Agree L.toSignature label O.sees (update x n s) s := by + intro y v + show (match V.deq x y with | .isTrue _ => n | .isFalse _ => s y) = s y + cases V.deq x y with + | isTrue hxy => subst hxy; exact (unseen_join O (lab L.toSignature label e) np (O.down ok v)).elim + | isFalse _ => rfl + +/-- N-3, `confine`: under a program counter the observer cannot see, a +finishing run changes nothing the observer sees. -/ +theorem confine : ∀ (fuel : Nat) {pc : L.Carrier} {c : Cmd V} {s t : Store V}, + (O.sees pc → False) → Typed L.toSignature label pc c → exec fuel c s = some t → + Agree L.toSignature label O.sees t s := by + intro fuel + induction fuel with + | zero => + intro pc c s t np d + induction d generalizing s t with + | skip => intro h; rw [exec_skip] at h; cases h; exact agree_refl O + | @assign pc x e ok => + intro h; rw [exec_assign] at h; cases h; exact confine_assign O x e _ s np ok + | seq d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_seq] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ih₂ np h₂) (ih₁ np h₁) + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_ifz] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => rw [hv] at h; exact ih₁ np' h + | succ _ => rw [hv] at h; exact ih₂ np' h + | «while» d ih => intro h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro pc c s t np d + induction d generalizing s t with + | skip => intro h; rw [exec_skip] at h; cases h; exact agree_refl O + | @assign pc x e ok => + intro h; rw [exec_assign] at h; cases h; exact confine_assign O x e _ s np ok + | seq d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_seq] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ih₂ np h₂) (ih₁ np h₁) + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_ifz] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => rw [hv] at h; exact ih₁ np' h + | succ _ => rw [hv] at h; exact ih₂ np' h + | @«while» pc e c d ih => + intro h; rw [exec_while_succ] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => + rw [hv] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ihf np (Typed.«while» d) h₂) (ihf np' d h₁) + | succ _ => rw [hv] at h; cases h; exact agree_refl O + +/-- `confineL`: re-entering a loop whose body is typed under an unseen +counter changes nothing the observer sees. The loop is not re-typed: `ℓ` is +the body's counter, which need not type the loop itself. -/ +theorem confine_loop : ∀ (fuel : Nat) {ℓ : L.Carrier} {e : Expr V} {c : Cmd V} + {s t : Store V}, (O.sees ℓ → False) → Typed L.toSignature label ℓ c → + exec fuel (.«while» e c) s = some t → Agree L.toSignature label O.sees t s := by + intro fuel + induction fuel with + | zero => intro ℓ e c s t _ _ h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro ℓ e c s t np d h + rw [exec_while_succ] at h + cases hv : eval s e with + | zero => + rw [hv] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ihf np d h₂) (confine O f np d h₁) + | succ _ => rw [hv] at h; cases h; exact agree_refl O + +/-- Agreement is a family of equations between naturals, hence stable under +double negation: what lets the proof split on whether the observer sees a +branch label without deciding it (as the Agda proof does). -/ +theorem agree_stable {s s' : Store V} + (h : (Agree L.toSignature label O.sees s s' → False) → False) : Agree L.toSignature label O.sees s s' := + fun x v => Decidable.byContradiction fun ne => h fun a => ne (a x v) + +/-- `¬¬-dec`: excluded middle under double negation, for any type. -/ +theorem nn_em (P : Type) (k : PSum P (P → False) → False) : False := + k (.inr fun p => k (.inl p)) + +/-- Either the observer sees label `j` or it does not, under double +negation: the shape the `ifz` and `while` cases use. -/ +theorem by_cases_sees {s s' : Store V} (j : L.Carrier) + (yes : O.sees j → Agree L.toSignature label O.sees s s') + (no : (O.sees j → False) → Agree L.toSignature label O.sees s s') : + Agree L.toSignature label O.sees s s' := + agree_stable O fun bad => nn_em (O.sees j) fun + | .inl v => bad (yes v) + | .inr nv => bad (no nv) + +/-- N-7, `tini`: termination-insensitive noninterference for every +down-closed observer of every lattice record. -/ +theorem tini : TINI L.toSignature label O.sees := by + intro pc c fuel + induction fuel generalizing pc c with + | zero => + intro fuel' s s' t t' d + induction d generalizing s s' t t' fuel' with + | skip => + intro eq h h'; rw [exec_skip] at h h'; cases h; cases h'; exact eq + | @assign pc x e ok => + intro eq h h'; rw [exec_assign] at h h'; cases h; cases h' + intro y v + show (match V.deq x y with | .isTrue _ => eval s e | .isFalse _ => s y) = + (match V.deq x y with | .isTrue _ => eval s' e | .isFalse _ => s' y) + cases V.deq x y with + | isTrue hxy => subst hxy; exact eval_low O e (O.down (L.upper₂ _ _) (O.down ok v)) eq + | isFalse _ => exact eq y v + | seq d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_seq] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ih₂ fuel' (ih₁ fuel' eq h₁ h₁') h₂ h₂' + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_ifz] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => rw [hv] at h h'; exact ih₁ fuel' eq h h' + | succ _ => rw [hv] at h h'; exact ih₂ fuel' eq h h' + · exact agree_trans O + (confine O _ nv (branch_typed _ d₁ d₂) h) + (agree_trans O eq (agree_symm O (confine O _ nv (branch_typed _ d₁ d₂) h'))) + | «while» d ih => intro eq h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro fuel' s s' t t' d + induction d generalizing s s' t t' fuel' with + | skip => + intro eq h h'; rw [exec_skip] at h h'; cases h; cases h'; exact eq + | @assign pc x e ok => + intro eq h h'; rw [exec_assign] at h h'; cases h; cases h' + intro y v + show (match V.deq x y with | .isTrue _ => eval s e | .isFalse _ => s y) = + (match V.deq x y with | .isTrue _ => eval s' e | .isFalse _ => s' y) + cases V.deq x y with + | isTrue hxy => subst hxy; exact eval_low O e (O.down (L.upper₂ _ _) (O.down ok v)) eq + | isFalse _ => exact eq y v + | seq d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_seq] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ih₂ fuel' (ih₁ fuel' eq h₁ h₁') h₂ h₂' + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_ifz] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => rw [hv] at h h'; exact ih₁ fuel' eq h h' + | succ _ => rw [hv] at h h'; exact ih₂ fuel' eq h h' + · exact agree_trans O + (confine O _ nv (branch_typed _ d₁ d₂) h) + (agree_trans O eq (agree_symm O (confine O _ nv (branch_typed _ d₁ d₂) h'))) + | @«while» pc e c d ih => + intro eq h h' + cases fuel' with + | zero => rw [exec_while_zero] at h'; cases h' + | succ f' => + rw [exec_while_succ] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => + rw [hv] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ihf f' (Typed.«while» d) (ihf f' d eq h₁ h₁') h₂ h₂' + | succ _ => rw [hv] at h h'; cases h; cases h'; exact eq + · rw [← exec_while_succ] at h h' + exact agree_trans O (confine_loop O _ nv d h) + (agree_trans O eq (agree_symm O (confine_loop O _ nv d h'))) + +end Proof +end SecretTypes diff --git a/verification/legs/lean/SecretTypes/Two.lean b/verification/legs/lean/SecretTypes/Two.lean new file mode 100644 index 0000000..ef8c410 --- /dev/null +++ b/verification/legs/lean/SecretTypes/Two.lean @@ -0,0 +1,158 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-1, N-2, N-3 +at the two-point lattice and N-9. Mirrors src/SecretTypes/Lattice.agda, +Lang/Two.agda, Typing.agda, Noninterference.agda, Witness.agda and +Noninterference/OutcomeVisibility.agda. Lean core only, no axioms. +-/ +import SecretTypes.Generic + +namespace SecretTypes.Two +open SecretTypes + +/-- `Label` of `SecretTypes.Lattice`: `L` public, `H` secret. -/ +inductive Label where + | L + | H +open Label + +/-- `_⊑_` of `SecretTypes.Lattice`: a computed predicate, as there. -/ +def le : Label → Label → Type + | L, _ => Unit + | H, L => Empty + | H, H => Unit + +def join : Label → Label → Label + | L, y => y + | H, _ => H + +def le_trans : ∀ {x y z : Label}, le x y → le y z → le x z + | L, _, _, _, _ => () + | H, H, H, _, _ => () + | H, H, L, _, k => k + | H, L, _, h, _ => nomatch h + +def upper₁ : ∀ x y : Label, le x (join x y) + | L, _ => () + | H, _ => () + +def upper₂ : ∀ x y : Label, le y (join x y) + | L, L => () + | L, H => () + | H, L => () + | H, H => () + +/-- `two-point` of `SecretTypes.Lattice`. -/ +def twoPoint : Lattice where + Carrier := Label + le := le + join := join + bot := L + le_trans := le_trans + upper₁ := upper₁ + upper₂ := upper₂ + +/-- `Var` of `SecretTypes.Lang.Two`. -/ +inductive Var where + | lo + | hi +deriving DecidableEq +open Var + +/-- `two : Vars`. -/ +def two : Vars where + Var := Var + deq := inferInstance + +/-- `label` of `SecretTypes.Typing`. -/ +def label : two.Var → twoPoint.Carrier + | lo => L + | hi => H + +/-- `⟨_,_⟩`, `low` and `_≈_` of `SecretTypes.Lang.Two`. -/ +def pair (l h : Nat) : Store two + | lo => l + | hi => h + +def low (s : Store two) : Nat := s lo + +def LowEq (s s' : Store two) : Prop := low s = low s' + +/-- `public-observer = principal two-point L`. -/ +def publicObserver : Observer twoPoint := principal twoPoint L + +theorem lowEq_agree {s s' : Store two} (eq : LowEq s s') : + Agree twoPoint.toSignature label publicObserver.sees s s' := fun + | lo, _ => eq + | hi, v => Empty.elim (show Empty from v) + +theorem agree_lowEq {s s' : Store two} + (f : Agree twoPoint.toSignature label publicObserver.sees s s') : LowEq s s' := + f lo () + +/-- N-2 at the two-point lattice: a public expression reads the same in +low-equivalent stores. -/ +theorem eval_low_two (e : Expr two) {s s' : Store two} + (p : lab twoPoint.toSignature label e = L) (eq : LowEq s s') : eval s e = eval s' e := + eval_low publicObserver e (p ▸ (() : le L L)) (lowEq_agree eq) + +/-- N-3 at the two-point lattice: under a secret counter the public variable +is unchanged, loops included. -/ +theorem confine_two {c : Cmd two} (fuel : Nat) {s t : Store two} + (d : Typed twoPoint.toSignature label H c) (h : exec fuel c s = some t) : low t = low s := + confine publicObserver fuel (pc := H) (fun v => Empty.elim (show Empty from v)) d h lo () + +/-- N-1, `tini` of `SecretTypes.Noninterference`: TINI at the two-point +lattice, fuels independent. -/ +theorem tini_two {pc : Label} {c : Cmd two} (fuel fuel' : Nat) {s s' t t' : Store two} + (d : Typed twoPoint.toSignature label pc c) (eq : LowEq s s') + (h : exec fuel c s = some t) (h' : exec fuel' c s' = some t') : LowEq t t' := + agree_lowEq (tini publicObserver fuel fuel' d (lowEq_agree eq) h h') + +/-! N-9, `SecretTypes.Noninterference.OutcomeVisibility`. -/ + +/-- `secret-loop = while (var hi) skip` and its typing at `L`. -/ +def secretLoop : Cmd two := .«while» (.var hi) .skip + +def secretLoopTyped : Typed twoPoint.toSignature label L secretLoop := .«while» .skip + +def s₀ : Store two := pair 0 0 +def s₁ : Store two := pair 0 1 + +theorem lowEquivalent : LowEq s₀ s₁ := rfl + +/-- `publicOutcome`: whether a run finished, and if so its public result. -/ +def publicOutcome (fuel : Nat) (c : Cmd two) (s : Store two) : Option Nat := + match exec fuel c s with + | none => none + | some t => some (low t) + +theorem secretLoop_never_finishes : ∀ fuel, exec fuel secretLoop s₀ = none + | 0 => rfl + | f + 1 => by + show bind (exec f .skip s₀) (exec f secretLoop) = none + rw [exec_skip] + exact secretLoop_never_finishes f + +theorem secretLoop_stops (fuel : Nat) : exec (fuel + 1) secretLoop s₁ = some s₁ := rfl + +theorem outcome_spins : publicOutcome 3 secretLoop s₀ = none := rfl +theorem outcome_stops : publicOutcome 3 secretLoop s₁ = some 0 := rfl + +theorem outcome_different : publicOutcome 3 secretLoop s₀ ≠ publicOutcome 3 secretLoop s₁ := + fun h => nomatch h + +/-- `TSNI`: the stronger two-run statement, with termination observable. -/ +def TSNI : Prop := + ∀ {pc : Label} {c : Cmd two} (fuel : Nat) {s s' : Store two}, + Typed twoPoint.toSignature label pc c → LowEq s s' → + publicOutcome fuel c s = publicOutcome fuel c s' + +/-- N-9, `termination-sensitive-fails`: TSNI is false for the current +typing rules. -/ +theorem termination_sensitive_fails : TSNI → False := + fun h => outcome_different (h 3 secretLoopTyped lowEquivalent) + +end SecretTypes.Two diff --git a/verification/legs/lean/lakefile.toml b/verification/legs/lean/lakefile.toml new file mode 100644 index 0000000..51a6b71 --- /dev/null +++ b/verification/legs/lean/lakefile.toml @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 +# The Lean recheck leg of secret-types (PROOF-POLICY §2). Lean core only: +# no Mathlib and no other dependency (no `require` entries). +name = "secret-types-lean-leg" +defaultTargets = ["SecretTypes"] + +[[lean_lib]] +name = "SecretTypes" diff --git a/verification/legs/lean/lean-toolchain b/verification/legs/lean/lean-toolchain new file mode 100644 index 0000000..8e51ca6 --- /dev/null +++ b/verification/legs/lean/lean-toolchain @@ -0,0 +1 @@ +lean-4.24.0 diff --git a/verification/legs/rocq/.gitignore b/verification/legs/rocq/.gitignore new file mode 100644 index 0000000..683abf2 --- /dev/null +++ b/verification/legs/rocq/.gitignore @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +*.vo +*.vok +*.vos +*.glob +.*.aux +.lia.cache diff --git a/verification/legs/rocq/SecretTypes.v b/verification/legs/rocq/SecretTypes.v new file mode 100644 index 0000000..2374e2c --- /dev/null +++ b/verification/legs/rocq/SecretTypes.v @@ -0,0 +1,535 @@ +(* SPDX-License-Identifier: MPL-2.0 + SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + + Rocq leg (PROOF-POLICY §2, route `re-proved`) of secret-types + N-1, N-2, N-3, N-7, N-8 and N-9. Mirrors src/SecretTypes/Vars.agda, + Lang.agda, Lattice/Record.agda, Typing/Generic.agda, + Noninterference/Statement.agda, Noninterference/Generic.agda, + Lattice.agda, Lang/Two.agda, Noninterference.agda, Countermodels.agda and + Noninterference/OutcomeVisibility.agda. + + Prelude only: no `Require` of the standard library, the counterpart of the + Agda gate's --no-libraries. No axioms: the `Print Assumptions` commands + at the end must report "Closed under the global context". + + Universe discipline: Agda's `Set` is `Type` here. The order, an + observer's `sees` and the typing derivations are `Type`-valued, as in + Agda. Equality of naturals is `Prop` here and a set in Agda; naturals + have decidable equality, so the two readings coincide. *) + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Vars and SecretTypes.Lattice.Record *) + +Record Vars := { Var : Type; deq : forall x y : Var, {x = y} + {x <> y} }. + +(* What Statement and Typing.Generic are parameterised by: no laws, so the + countermodels (N-8) can instantiate the statement where a law fails. *) +Record Signature := { + Carrier : Type; + le : Carrier -> Carrier -> Type; + join : Carrier -> Carrier -> Carrier; + bot : Carrier +}. + +Record Lattice := { + sig :> Signature; + le_trans : forall x y z, le sig x y -> le sig y z -> le sig x z; + upper1 : forall x y, le sig x (join sig x y); + upper2 : forall x y, le sig y (join sig x y) +}. + +Record Observer (L : Lattice) := { + sees : Carrier L -> Type; + down : forall x y, le L x y -> sees y -> sees x +}. +Arguments sees {L} o _. +Arguments down {L} o {x y} _ _. + +Definition principal (L : Lattice) (o : Carrier L) : Observer L := + {| sees := fun x => le L x o; + down := fun x y h v => le_trans L x y o h v |}. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Lang *) + +Section Lang. +Variable V : Vars. + +Definition Store := Var V -> nat. + +Inductive Expr := lit (n : nat) | var (x : Var V) | plus (a b : Expr). + +Inductive Cmd := +| skip +| assign (x : Var V) (e : Expr) +| seq (c1 c2 : Cmd) +| ifz (e : Expr) (c1 c2 : Cmd) +| while (e : Expr) (c : Cmd). + +Fixpoint eval (s : Store) (e : Expr) : nat := + match e with + | lit n => n + | var x => s x + | plus a b => eval s a + eval s b + end. + +(* update x n s y = select (x ≟ᵥ y) n (s y) *) +Definition update (x : Var V) (n : nat) (s : Store) : Store := + fun y => if deq V x y then n else s y. + +Definition bind {A : Type} (m : option A) (f : A -> option A) : option A := + match m with None => None | Some a => f a end. + +(* One step of fuel, structural in the command; `prev` is the run at one + less fuel, None at fuel zero (where a loop does not finish). *) +Fixpoint run (prev : option (Cmd -> Store -> option Store)) (c : Cmd) (s : Store) + : option Store := + match c with + | skip => Some s + | assign x e => Some (update x (eval s e) s) + | seq c1 c2 => bind (run prev c1 s) (run prev c2) + | ifz e c1 c2 => match eval s e with 0 => run prev c1 s | S _ => run prev c2 s end + | while e c => + match prev with + | None => None + | Some p => match eval s e with + | 0 => bind (p c s) (p (while e c)) + | S _ => Some s + end + end + end. + +(* exec of SecretTypes.Lang, clause by clause: sequence and ifz keep the + fuel; a loop at S f runs its body and re-enters at f; at 0 it is None. *) +Fixpoint exec (f : nat) : Cmd -> Store -> option Store := + match f with 0 => run None | S f' => run (Some (exec f')) end. + +End Lang. + +Arguments lit {V} n. +Arguments var {V} x. +Arguments plus {V} a b. +Arguments skip {V}. +Arguments assign {V} x e. +Arguments seq {V} c1 c2. +Arguments ifz {V} e c1 c2. +Arguments while {V} e c. +Arguments eval {V} s e. +Arguments update {V} x n s _. +Arguments exec {V} f _ _. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Typing.Generic and Noninterference.Statement *) + +Section Typing. +Context {V : Vars} (S : Signature) (label : Var V -> Carrier S). + +Fixpoint lab (e : Expr V) : Carrier S := + match e with + | lit _ => bot S + | var x => label x + | plus a b => join S (lab a) (lab b) + end. + +Inductive Typed : Carrier S -> Cmd V -> Type := +| t_skip : forall pc, Typed pc skip +| t_assign : forall pc x e, le S (join S pc (lab e)) (label x) -> Typed pc (assign x e) +| t_seq : forall pc c1 c2, Typed pc c1 -> Typed pc c2 -> Typed pc (seq c1 c2) +| t_ifz : forall pc e c1 c2, Typed (join S pc (lab e)) c1 -> + Typed (join S pc (lab e)) c2 -> Typed pc (ifz e c1 c2) +| t_while : forall pc e c, Typed (join S pc (lab e)) c -> Typed pc (while e c). + +Definition Agree (sees : Carrier S -> Type) (s s' : Store V) : Prop := + forall x, sees (label x) -> s x = s' x. + +Definition TINI (sees : Carrier S -> Type) : Prop := + forall pc c fuel fuel' s s' t t', Typed pc c -> Agree sees s s' -> + exec fuel c s = Some t -> exec fuel' c s' = Some t' -> Agree sees t t'. + +End Typing. + +Arguments t_skip {V S label pc}. +Arguments t_assign {V S label pc x e} _. +Arguments t_seq {V S label pc c1 c2} _ _. +Arguments t_ifz {V S label pc e c1 c2} _ _. +Arguments t_while {V S label pc e c} _. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Noninterference.Generic *) + +Section Proof. +Context {V : Vars} (L : Lattice) (label : Var V -> Carrier L) (O : Observer L). + +Notation agree := (Agree L label (sees O)). +Notation typed := (Typed L label). +Notation labe := (lab L label). + +Lemma bind_some {A : Type} (m : option A) (f : A -> option A) t : + bind m f = Some t -> {a : A & (m = Some a) * (f a = Some t)}%type. +Proof. destruct m as [a|]; simpl; intro h; [exists a; split; auto | discriminate]. Defined. + +Definition branch (n : nat) (c1 c2 : Cmd V) : Cmd V := + match n with 0 => c1 | S _ => c2 end. + +Lemma exec_skip f (s : Store V) : exec f skip s = Some s. +Proof. destruct f; reflexivity. Qed. + +Lemma exec_assign f x e (s : Store V) : exec f (assign x e) s = Some (update x (eval s e) s). +Proof. destruct f; reflexivity. Qed. + +Lemma exec_seq f (c1 c2 : Cmd V) (s : Store V) : exec f (seq c1 c2) s = bind (exec f c1 s) (exec f c2). +Proof. destruct f; reflexivity. Qed. + +Lemma exec_ifz f e (c1 c2 : Cmd V) (s : Store V) : exec f (ifz e c1 c2) s = exec f (branch (eval s e) c1 c2) s. +Proof. destruct f; simpl; destruct (eval s e); reflexivity. Qed. + +Lemma exec_while_succ f e (c : Cmd V) (s : Store V) : + exec (S f) (while e c) s = + match eval s e with 0 => bind (exec f c s) (exec f (while e c)) | S _ => Some s end. +Proof. reflexivity. Qed. + +Definition branch_typed pc n c1 c2 (d1 : typed pc c1) (d2 : typed pc c2) + : typed pc (branch n c1 c2) := + match n with 0 => d1 | S _ => d2 end. + +Lemma unseen_join pc y : (sees O pc -> False) -> sees O (join L pc y) -> False. +Proof. intros np v. exact (np (down O (upper1 L pc y) v)). Qed. + +(* N-2, eval-low *) +Lemma eval_low : forall (e : Expr V) (s s' : Store V), sees O (labe e) -> agree s s' -> eval s e = eval s' e. +Proof. + induction e as [n|x|a IHa b IHb]; intros s s' v eq; simpl. + - reflexivity. + - exact (eq x v). + - rewrite (IHa s s' (down O (upper1 L _ _) v) eq). + rewrite (IHb s s' (down O (upper2 L _ _) v) eq). reflexivity. +Qed. + +Lemma agree_refl (s : Store V) : agree s s. +Proof. intros x _; reflexivity. Qed. +Lemma agree_symm (s s' : Store V) : agree s s' -> agree s' s. +Proof. intros h x v; symmetry; exact (h x v). Qed. +Lemma agree_trans (s s' s'' : Store V) : agree s s' -> agree s' s'' -> agree s s''. +Proof. intros h k x v; rewrite (h x v); exact (k x v). Qed. + +Lemma confine_assign pc x e n (s : Store V) : + (sees O pc -> False) -> le L (join L pc (labe e)) (label x) -> agree (update x n s) s. +Proof. + intros np ok y v. unfold update. destruct (deq V x y) as [hxy|hxy]. + - subst y. destruct (unseen_join pc (labe e) np (down O ok v)). + - reflexivity. +Qed. + +(* N-3, confine *) +Lemma confine : forall fuel pc (c : Cmd V) (s t : Store V), + (sees O pc -> False) -> typed pc c -> exec fuel c s = Some t -> agree t s. +Proof. + induction fuel as [|f IHf]; intros pc c s t np d; revert s t np; + induction d as [pc|pc x e ok|pc c1 c2 d1 IH1 d2 IH2|pc e c1 c2 d1 IH1 d2 IH2|pc e c d IH]; + intros s t np h. + all: try (rewrite exec_skip in h; injection h as <-; apply agree_refl). + all: try (rewrite exec_assign in h; injection h as <-; exact (confine_assign pc x e _ s np ok)). + all: try (rewrite exec_seq in h; destruct (bind_some _ _ _ h) as [s1 [h1 h2]]; + exact (agree_trans _ _ _ (IH2 _ _ np h2) (IH1 _ _ np h1))). + all: try (rewrite exec_ifz in h; pose proof (unseen_join pc (labe e) np) as np'; + destruct (eval s e); [exact (IH1 _ _ np' h) | exact (IH2 _ _ np' h)]). + - discriminate h. + - rewrite exec_while_succ in h. pose proof (unseen_join pc (labe e) np) as np'. + destruct (eval s e). + + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + exact (agree_trans _ _ _ (IHf _ _ _ _ np (t_while d) h2) (IHf _ _ _ _ np' d h1)). + + injection h as <-; apply agree_refl. +Qed. + +(* confineL: a loop whose body is typed under an unseen counter, re-entered + without re-typing the loop. *) +Lemma confine_loop : forall fuel l (e : Expr V) (c : Cmd V) (s t : Store V), + (sees O l -> False) -> typed l c -> exec fuel (while e c) s = Some t -> agree t s. +Proof. + induction fuel as [|f IHf]; intros l e c s t np d h. + - discriminate h. + - rewrite exec_while_succ in h. destruct (eval s e). + + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + exact (agree_trans _ _ _ (IHf _ _ _ _ _ np d h2) (confine f _ _ _ _ np d h1)). + + injection h as <-; apply agree_refl. +Qed. + +Fixpoint nat_eq_dec (n m : nat) : {n = m} + {n <> m}. +Proof. decide equality. Defined. + +(* Agreement is a family of equations between naturals, hence stable under + double negation (as in the Agda proof). *) +Lemma agree_stable (s s' : Store V) : ((agree s s' -> False) -> False) -> agree s s'. +Proof. + intros h x v. destruct (nat_eq_dec (s x) (s' x)) as [e|ne]; [exact e|]. + destruct (h (fun a => ne (a x v))). +Qed. + +Lemma by_cases_sees (s s' : Store V) j : + (sees O j -> agree s s') -> ((sees O j -> False) -> agree s s') -> agree s s'. +Proof. + intros yes no. apply agree_stable. intro bad. + apply bad. apply no. intro v. apply bad. exact (yes v). +Qed. + +(* N-7, tini *) +Theorem tini : TINI L label (sees O). +Proof. + intros pc c fuel. revert pc c. + induction fuel as [|f IHf]; intros pc c fuel' s s' t t' d; revert fuel' s s' t t'; + induction d as [pc|pc x e ok|pc c1 c2 d1 IH1 d2 IH2|pc e c1 c2 d1 IH1 d2 IH2|pc e c d IH]; + intros fuel' s s' t t' eq h h'. + all: try (rewrite exec_skip in h, h'; injection h as <-; injection h' as <-; exact eq). + all: try (rewrite exec_assign in h, h'; injection h as <-; injection h' as <-; + intros y v; unfold update; destruct (deq V x y) as [hxy|hxy]; + [subst y; exact (eval_low e s s' (down O (upper2 L _ _) (down O ok v)) eq) + | exact (eq y v)]). + all: try (rewrite exec_seq in h, h'; + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]; + destruct (bind_some _ _ _ h') as [s1' [h1' h2']]; + exact (IH2 _ _ _ _ _ (IH1 _ _ _ _ _ eq h1 h1') h2 h2')). + all: try (rewrite exec_ifz in h, h'; + apply (by_cases_sees _ _ (join L pc (labe e))); + [ intro v; pose proof (eval_low e s s' (down O (upper2 L _ _) v) eq) as ge; + rewrite <- ge in h'; destruct (eval s e); + [exact (IH1 _ _ _ _ _ eq h h') | exact (IH2 _ _ _ _ _ eq h h')] + | intro nv; + exact (agree_trans _ _ _ (confine _ _ _ _ _ nv (branch_typed _ _ _ _ d1 d2) h) + (agree_trans _ _ _ eq + (agree_symm _ _ (confine _ _ _ _ _ nv (branch_typed _ _ _ _ d1 d2) h')))) ]). + - discriminate h. + - destruct fuel' as [|f']; [discriminate h'|]. + apply (by_cases_sees _ _ (join L pc (labe e))). + + intro v. pose proof (eval_low e s s' (down O (upper2 L _ _) v) eq) as ge. + rewrite exec_while_succ in h, h'. rewrite <- ge in h'. destruct (eval s e). + * destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + destruct (bind_some _ _ _ h') as [s1' [h1' h2']]. + exact (IHf _ _ _ _ _ _ _ (t_while d) (IHf _ _ _ _ _ _ _ d eq h1 h1') h2 h2'). + * injection h as <-; injection h' as <-; exact eq. + + intro nv. + exact (agree_trans _ _ _ (confine_loop _ _ _ _ _ _ nv d h) + (agree_trans _ _ _ eq (agree_symm _ _ (confine_loop _ _ _ _ _ _ nv d h')))). +Qed. + +End Proof. + +(* ---------------------------------------------------------------------- *) +(* The two-point lattice (SecretTypes.Lattice, Lang.Two, Typing, *) +(* Noninterference): N-1, and N-2/N-3 at that lattice *) + +Module Two. + +Inductive Label := L | H. + +(* A computed predicate, as in SecretTypes.Lattice. *) +Definition le2 (x y : Label) : Type := + match x, y with L, _ => unit | H, L => Empty_set | H, H => unit end. + +Definition join2 (x y : Label) : Label := match x with L => y | H => H end. + +Definition le2_trans x y z : le2 x y -> le2 y z -> le2 x z := + match x, y, z with + | L, _, _ => fun _ _ => tt + | H, H, H => fun _ _ => tt + | H, H, L => fun _ k => k + | H, L, _ => fun h _ => match h with end + end. + +Definition up1 x y : le2 x (join2 x y) := match x with L => match y with L => tt | H => tt end | H => tt end. +Definition up2 x y : le2 y (join2 x y) := + match x, y with L, L => tt | L, H => tt | H, L => tt | H, H => tt end. + +Definition twoSig : Signature := {| Carrier := Label; le := le2; join := join2; bot := L |}. +Definition twoPoint : Lattice := {| sig := twoSig; le_trans := le2_trans; upper1 := up1; upper2 := up2 |}. + +Inductive TVar := lo | hi. +Definition tdeq (x y : TVar) : {x = y} + {x <> y}. +Proof. decide equality. Defined. +Definition two : Vars := {| Var := TVar; deq := tdeq |}. + +Definition label (x : Var two) : Carrier twoPoint := match x with lo => L | hi => H end. + +Definition pair (l h : nat) : Store two := fun x => match x with lo => l | hi => h end. +Definition low (s : Store two) : nat := s lo. +Definition LowEq (s s' : Store two) : Prop := low s = low s'. + +Definition publicObserver : Observer twoPoint := principal twoPoint L. + +Lemma lowEq_agree s s' : LowEq s s' -> Agree twoPoint label (sees publicObserver) s s'. +Proof. intros eq [|] v; [exact eq | destruct v]. Qed. + +Lemma agree_lowEq s s' : Agree twoPoint label (sees publicObserver) s s' -> LowEq s s'. +Proof. intro f. exact (f lo tt). Qed. + +(* N-2 at the two-point lattice *) +Lemma eval_low_two (e : Expr two) s s' : + lab twoPoint label e = L -> LowEq s s' -> eval s e = eval s' e. +Proof. + intros p eq. apply (eval_low twoPoint label publicObserver e s s'). + - change (le2 (lab twoPoint label e) L). rewrite p. exact tt. + - exact (lowEq_agree _ _ eq). +Qed. + +(* N-3 at the two-point lattice *) +Lemma confine_two (c : Cmd two) fuel s t : + Typed twoPoint label H c -> exec fuel c s = Some t -> low t = low s. +Proof. + intros d h. exact (confine twoPoint label publicObserver fuel H c s t + (fun v : Empty_set => match v with end) d h lo tt). +Qed. + +(* N-1, tini of SecretTypes.Noninterference *) +Theorem tini_two pc (c : Cmd two) fuel fuel' s s' t t' : + Typed twoPoint label pc c -> LowEq s s' -> + exec fuel c s = Some t -> exec fuel' c s' = Some t' -> LowEq t t'. +Proof. + intros d eq h h'. apply agree_lowEq. + exact (tini twoPoint label publicObserver pc c fuel fuel' s s' t t' d (lowEq_agree _ _ eq) h h'). +Qed. + +(* N-9, SecretTypes.Noninterference.OutcomeVisibility *) +Definition secretLoop : Cmd two := while (@var two hi) skip. +Definition secretLoopTyped : Typed twoPoint label L secretLoop := t_while t_skip. +Definition s0 : Store two := pair 0 0. +Definition s1 : Store two := pair 0 1. +Lemma lowEquivalent : LowEq s0 s1. +Proof. reflexivity. Qed. + +Definition publicOutcome fuel (c : Cmd two) s : option nat := + match exec fuel c s with None => None | Some t => Some (low t) end. + +Lemma secretLoop_never_finishes : forall fuel, exec fuel secretLoop s0 = None. +Proof. + induction fuel as [|f IH]; [reflexivity|]. + change (bind (exec f skip s0) (exec f secretLoop) = None). + rewrite exec_skip. exact IH. +Qed. + +Lemma secretLoop_stops fuel : exec (S fuel) secretLoop s1 = Some s1. +Proof. reflexivity. Qed. + +Lemma outcome_different : publicOutcome 3 secretLoop s0 <> publicOutcome 3 secretLoop s1. +Proof. discriminate. Qed. + +Definition TSNI : Prop := + forall pc (c : Cmd two) fuel s s', Typed twoPoint label pc c -> LowEq s s' -> + publicOutcome fuel c s = publicOutcome fuel c s'. + +Theorem termination_sensitive_fails : TSNI -> False. +Proof. intro h. exact (outcome_different (h L secretLoop 3 s0 s1 secretLoopTyped lowEquivalent)). Qed. + +End Two. + +(* ---------------------------------------------------------------------- *) +(* N-8, SecretTypes.Countermodels *) + +Module Countermodels. +Import Two. + +Definition std (x : Var two) : Label := match x with lo => L | hi => H end. +Definition withJoin (j : Label -> Label -> Label) : Signature := + {| Carrier := Label; le := le2; join := j; bot := L |}. +Definition belowL (x : Label) : Type := le2 x L. + +Lemma agree01 (S : Signature) (lb : Var two -> Carrier S) (sees : Carrier S -> Type) : + (sees (lb hi) -> False) -> Agree S lb sees s0 s1. +Proof. intros n [|] v; [reflexivity | destruct (n v)]. Qed. + +Module NoUpper1. + Definition joinR (x y : Label) : Label := y. + Definition S := withJoin joinR. + Lemma not_upper1 : (forall x y, le2 x (joinR x y)) -> False. + Proof. intro h. destruct (h H L). Qed. + Definition implicitFlow : Cmd two := ifz (@var two hi) (@assign two lo (lit 0)) (@assign two lo (lit 1)). + Definition typed : Typed S std L implicitFlow. + Proof. apply t_ifz; apply t_assign; exact tt. Defined. + Theorem refutes : TINI S std belowL -> False. + Proof. + intro tini. pose proof (tini L implicitFlow 1 1 s0 s1 _ _ typed + (agree01 S std belowL (fun v : Empty_set => match v with end)) eq_refl eq_refl lo tt) as e. + discriminate e. + Qed. +End NoUpper1. + +Module NoUpper2. + Definition joinL (x y : Label) : Label := x. + Definition S := withJoin joinL. + Lemma not_upper2 : (forall x y, le2 y (joinL x y)) -> False. + Proof. intro h. destruct (h L H). Qed. + Definition explicitFlow : Cmd two := @assign two lo (@var two hi). + Definition typed : Typed S std L explicitFlow. + Proof. apply t_assign; exact tt. Defined. + Theorem refutes : TINI S std belowL -> False. + Proof. + intro tini. pose proof (tini L explicitFlow 1 1 s0 s1 _ _ typed + (agree01 S std belowL (fun v : Empty_set => match v with end)) eq_refl eq_refl lo tt) as e. + discriminate e. + Qed. +End NoUpper2. + +Module NoDownClosure. + Definition seesH (x : Label) : Type := x = H. + Lemma not_down_closed : (forall x y, le2 x y -> seesH y -> seesH x) -> False. + Proof. intro h. discriminate (h L H tt eq_refl). Qed. + Definition S := withJoin join2. + Definition up : Cmd two := @assign two hi (@var two lo). + Definition typed : Typed S std L up. + Proof. apply t_assign; exact tt. Defined. + Definition t0 : Store two := pair 0 0. + Definition t1 : Store two := pair 1 0. + Lemma agree : Agree S std seesH t0 t1. + Proof. intros [|] v; [discriminate v | reflexivity]. Qed. + Theorem refutes : TINI S std seesH -> False. + Proof. + intro tini. pose proof (tini L up 1 1 t0 t1 _ _ typed agree eq_refl eq_refl hi eq_refl) as e. + discriminate e. + Qed. +End NoDownClosure. + +Module NoTrans. + Inductive P := B | H' | M | L' | T. + Inductive Le : P -> P -> Type := + | le_refl : forall x, Le x x + | le_bot : forall x, Le B x + | le_top : forall x, Le x T + | le_HM : Le H' M + | le_ML : Le M L'. + Definition joinP (x y : P) : P := + match x, y with + | B, y => y | T, _ => T + | H', B => H' | H', H' => H' | H', M => M | H', L' => T | H', T => T + | M, B => M | M, H' => M | M, M => M | M, L' => L' | M, T => T + | L', B => L' | L', H' => T | L', M => L' | L', L' => L' | L', T => T + end. + Lemma not_trans : (forall x y z, Le x y -> Le y z -> Le x z) -> False. + Proof. intro t. pose proof (t _ _ _ le_HM le_ML) as k. inversion k. Qed. + Definition S : Signature := {| Carrier := P; le := Le; join := joinP; bot := B |}. + Definition labelP (x : Var two) : P := match x with lo => M | hi => H' end. + Definition explicitFlow : Cmd two := @assign two lo (@var two hi). + Definition typed : Typed S labelP B explicitFlow. + Proof. apply t_assign; exact le_HM. Defined. + Definition belowL' (x : P) : Type := Le x L'. + Lemma agree : Agree S labelP belowL' s0 s1. + Proof. intros [|] v; [reflexivity | inversion v]. Qed. + Theorem refutes : TINI S labelP belowL' -> False. + Proof. + intro tini. pose proof (tini B explicitFlow 1 1 s0 s1 _ _ typed agree eq_refl eq_refl lo le_ML) as e. + discriminate e. + Qed. +End NoTrans. + +End Countermodels. + +(* Axioms each theorem rests on (PROOF-POLICY §8.4): every line must read + "Closed under the global context". *) +Print Assumptions eval_low. +Print Assumptions confine. +Print Assumptions tini. +Print Assumptions Two.eval_low_two. +Print Assumptions Two.confine_two. +Print Assumptions Two.tini_two. +Print Assumptions Two.termination_sensitive_fails. +Print Assumptions Countermodels.NoUpper1.refutes. +Print Assumptions Countermodels.NoUpper2.refutes. +Print Assumptions Countermodels.NoDownClosure.refutes. +Print Assumptions Countermodels.NoTrans.refutes. diff --git a/verification/receipts/agda_praxis.deed b/verification/receipts/agda_praxis.deed index fb94439..25e526b 100644 --- a/verification/receipts/agda_praxis.deed +++ b/verification/receipts/agda_praxis.deed @@ -13,7 +13,7 @@ :uuid-source "uuid5(URL, github.com/hyperpolymath/secret-types)" :uuid-note "F-1 remains open: template mint-path cause and local scaffolding sweep; see docs/reports/audit/consistency-audit-2026-11-01.adoc" :kind "theory" - :source-commit "eee4e4038503") + :source-commit "ba2484fb7abc") (prover :tool "agda" :version "2.6.4.3" @@ -45,29 +45,49 @@ :axioms-assumed 0 :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero") ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded. - ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts. + ; Rocq and Lean legs: re-proved by hand (Agda2Dedukti cannot run on the pinned Agda), RECONCILED in verification/legs/README.adoc. + (legs + :gate "bash scripts/check-legs.sh" + :ci ".github/workflows/proofs.yml (job legs)" + :correspondence "verification/legs/README.adoc" + :route "re-proved" + :route-reason "Agda2Dedukti is an Agda backend pinned to a fork (b026db1, GHC 8.10) and cannot run on Agda 2.6.4.3; no released Dedukti/Lambdapi exporter to Lean 4, and no pinned route to Rocq" + :state "RECONCILED" + :review "statement comparison written by Claude Code; provisional until owner review (estate doctrine 4)" + (leg :prover "rocq" :checker "coqc" :version "8.18.0" :invocation "coqc -q SecretTypes.v (in verification/legs/rocq)" :libraries "none (no Require)" :axioms "none (Print Assumptions: Closed under the global context)") + (leg :prover "lean" :checker "lean" :version "4.24.0" :invocation "lake build; lake env lean Axioms.lean (in verification/legs/lean)" :libraries "none (lakefile has no require; no Mathlib)" :axioms "none (#print axioms: does not depend on any axioms)") + (inputs + (input :path "verification/legs/rocq/SecretTypes.v" :sha256 "acffaa9b4884b46c61fae6f2c91a34e7005b5d4b6158ebcc83bde25bc573b75e") + (input :path "verification/legs/lean/Axioms.lean" :sha256 "078d9a566e80b9f9701ba1b3f12bd5897e372c41f7d2dcfdf13c2f6d07159ae7") + (input :path "verification/legs/lean/SecretTypes.lean" :sha256 "48d02eea6800f9655c1a1d968cbeb9b8d8aa2594f6ad47915cbc8247e4157b8d") + (input :path "verification/legs/lean/SecretTypes/Countermodels.lean" :sha256 "ef2dc1f54aa0ac76acea9c020c9fa0adecfb864e27caa184339090d233bd6ed5") + (input :path "verification/legs/lean/SecretTypes/Generic.lean" :sha256 "13b10fd744828bc5ea3551346aeaa7795b51f24e8585e26c9dc737805c054cfa") + (input :path "verification/legs/lean/SecretTypes/Two.lean" :sha256 "74387c6eec74dbbfada1c08d5ef96451740c37e439db8aa5a17ece44e4cf318a") + (input :path "verification/legs/lean/lakefile.toml" :sha256 "75b8b79a27ec284d2c383302c88c90248ab56ee9902664068140d014b45bcf34") + (input :path "verification/legs/lean/lean-toolchain" :sha256 "387019dd5f6d8213249f99bfe1bd9f346678bf0d4612938c1e7feae386665335") + )) (claims - (claim :id "N-1" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) - (claim :id "N-2" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) - (claim :id "N-3" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-1" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) + (claim :id "N-2" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) + (claim :id "N-3" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) (claim :id "N-4" :token "tested-only" :kind "demonstration" :pwg "ungraded") (claim :id "N-5" :token "tested-only" :kind "demonstration" :pwg "ungraded") (claim :id "N-6" :token "tested-only" :kind "demonstration" :pwg "ungraded") - (claim :id "N-7" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) - (claim :id "N-8" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) - (claim :id "N-9" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f - (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) - (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-7" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) + (claim :id "N-8" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) + (claim :id "N-9" :token "proven" :kind "theorem" :pwg "2ii" :foundation-diverse #f + (leg :prover "rocq" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ()) + (leg :prover "lean" :route "re-proved" :token "proven" :state "RECONCILED" :receipts ())) ) ; Every module hash is checked against the current tree. (modules