Skip to content

proofs: check the receipt-boundary theory in Agda, Lean and Rocq, and gate it in CI #195

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 11 commits into from
Nov 10, 2026
Merged

proofs: check the receipt-boundary theory in Agda, Lean and Rocq, and gate it in CI #195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
0bf5959
fix(api)!: authenticate and authorize the GraphQL API; bind loopback …
claude Nov 4, 2026
e40f537
fix(deps): bump four crates past RustSec advisories in Cargo.lock
claude Nov 4, 2026
63cc6de
fix(api): apply env config without a file, bound the limiter, trim cr…
claude Nov 5, 2026
b664f99
proofs: check the receipt-boundary theory in all three kernels, in CI
claude Nov 9, 2026
6b9cd68
Merge the merged #192 branch history (no content change) so this bran…
claude Nov 9, 2026
b9691cf
ci(theory): restrict toolchain downloads to HTTPS; name the required …
claude Nov 9, 2026
8acc85e
proofs(theory): controls fail for the right reason; reword correspond…
claude Nov 9, 2026
6397426
proofs(theory): judge recheck legs by the checker's output
claude Nov 9, 2026
6b86775
proofs(theory): query named theorems from the script, not the proof file
claude Nov 9, 2026
8947051
docs(proof-status): record why both T-RECEIPT recheck legs are re-proved
claude Nov 9, 2026
797276d
docs(proof-status): correct the Lambdapi export failure
claude Nov 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions .github/workflows/proof-safety.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,3 +26,45 @@ jobs:
cargo test --locked --test protocol_contract
cargo test --locked --bin echidnabot clone_contract_tests
cargo test --locked --lib git_process_tests

theory:
# Receipt-boundary theory (docs/PROOF-STATUS.adoc T-RECEIPT): the Agda
# source and its Lean and Rocq re-proofs, each checked by its own kernel
# at this commit. Toolchains come from pinned upstream release archives,
# not the Guix manifest: this is the recorded PROOF-POLICY §6 deviation
# D-THEORY-TOOLS in docs/PROOF-STATUS.adoc. Each archive is verified by
# digest, and each script fails if the version it observes differs.
name: Theory proofs (Agda, Lean, Rocq)
runs-on: ubuntu-24.04
timeout-minutes: 20
env:
AGDA_URL: https://github.com/agda/agda/releases/download/v2.8.0.2/Agda-v2.8.0.2-linux.tar.xz
AGDA_SHA256: 2bcf24bb561b1be859bba841e5d67962d1616b3251bc147f878e4f60a2fbd9f7
LEAN_URL: https://releases.lean-lang.org/lean4/v4.35.0/lean-4.35.0-linux.tar.zst
LEAN_SHA256: 7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d
steps:
- uses: actions/checkout@v7.0.1
with:
persist-credentials: false
- name: Install Agda 2.8.0.2 (digest-verified release)
run: |
mkdir -p "$RUNNER_TEMP/agda"
curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$AGDA_URL"
echo "$AGDA_SHA256 $RUNNER_TEMP/agda.tar.xz" | sha256sum -c -
tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP/agda"
echo "$RUNNER_TEMP/agda" >> "$GITHUB_PATH"
- name: Install Lean 4.35.0 (digest-verified release)
run: |
mkdir -p "$RUNNER_TEMP/lean"
curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/lean.tar.zst" "$LEAN_URL"
echo "$LEAN_SHA256 $RUNNER_TEMP/lean.tar.zst" | sha256sum -c -
tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" --strip-components=1
echo "$RUNNER_TEMP/lean/bin" >> "$GITHUB_PATH"
- name: Install Coq 8.18.0 (Ubuntu 24.04 archive)
run: |
sudo apt-get update -q
sudo apt-get install -y -q coq
Comment thread
hyperpolymath marked this conversation as resolved.
Resolved
- name: Agda source (strict profile)
run: ./scripts/check-agda-proofs.sh
- name: Lean and Rocq recheck legs (with negative controls)
run: ./scripts/check-theory-rechecks.sh
Loading
Loading