From a0129e57a4aa185fcaf3dcec9d297b715d5494df Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 09:27:33 +0530 Subject: [PATCH 1/3] Select verification groups from recorded inputs instead of running all 52 jobs per push Every pull-request revision and every push ran the full artifact matrix (48 Python jobs, the finite replay, three formal packages) plus four unfiltered package workflows, about 232 runner-minutes per sync, while 23 of 30 recent pull requests only add a new research package. With about 925 runs a day the queue reached 20 hours. A plan job now diffs the pull request's merge commit against its base (or a push's before..after), classifies each changed path with .github/verify-groups.json and runs only the groups it reaches, on every supported Python. The declarations are recorded, not guessed: scripts/trace_verify_inputs.py runs each group's unchanged command under strace and records the tracked files read, directories listed, existence checks, probes and whole-tree git queries; every job runs under it and fails on an undeclared input. Paths nobody declared, the root attribute files, scripts/, the Makefile, symlink or submodule changes and ignored-but-tracked paths run everything; scheduled and manual runs and the ci:full-verify label run everything; pull-request revisions supersede each other, pushes never do. The four package verifiers become a planner-selected job (native paths filters stop at a few hundred changed files), verify-summary gives one status that requires success for every selected job, and a manual workflow can cancel superseded pull-request runs from the backlog. Replaying the planner over the 60 most recently updated pull requests gives a mean of 63 runner-minutes per sync (27% of before); a research-only pull request runs the two whole-tree groups and the plan job, about 25 minutes. Not changed: pinned sources, frozen evidence, the selected result, or any verification command. Known, pre-existing: d7d8bfcb and 6178dede changed pinned sources without updating their pins, so the clones group and the tests group fail on main (documented in docs/ci.md, not fixed here). Co-Authored-By: Claude Fable 5.1 --- .github/verify-groups.json | 793 +++++++++++++++++++ .github/workflows/bit-elim-144.yml | 29 - .github/workflows/bit-reuse-147.yml | 29 - .github/workflows/ci-cancel-superseded.yml | 50 ++ .github/workflows/early-reset-reuse.yml | 20 - .github/workflows/graded-box-convolution.yml | 17 - .github/workflows/verify.yml | 217 ++++- docs/ci.md | 247 ++++++ scripts/cancel_superseded_runs.py | 155 ++++ scripts/plan_verify_groups.py | 438 ++++++++++ scripts/trace_verify_inputs.py | 735 +++++++++++++++++ tests/test_plan_verify_groups.py | 370 +++++++++ tests/test_trace_verify_inputs.py | 342 ++++++++ 13 files changed, 3333 insertions(+), 109 deletions(-) create mode 100644 .github/verify-groups.json delete mode 100644 .github/workflows/bit-elim-144.yml delete mode 100644 .github/workflows/bit-reuse-147.yml create mode 100644 .github/workflows/ci-cancel-superseded.yml delete mode 100644 .github/workflows/early-reset-reuse.yml delete mode 100644 .github/workflows/graded-box-convolution.yml create mode 100644 docs/ci.md create mode 100644 scripts/cancel_superseded_runs.py create mode 100644 scripts/plan_verify_groups.py create mode 100644 scripts/trace_verify_inputs.py create mode 100644 tests/test_plan_verify_groups.py create mode 100644 tests/test_trace_verify_inputs.py diff --git a/.github/verify-groups.json b/.github/verify-groups.json new file mode 100644 index 0000000000..7183c6ffe0 --- /dev/null +++ b/.github/verify-groups.json @@ -0,0 +1,793 @@ +{ + "_comment": "Declared CI inputs per verification group, recorded by scripts/trace_verify_inputs.py and consumed by scripts/plan_verify_groups.py. Patterns: exact path; dir/** (any change below); dir/* or * (an entry added to or removed from a listed directory); dir/ (the directory created or removed); ** (the whole tree). Declared group inputs take precedence over skip_safe; a path matching neither runs everything.", + "python": [ + "3.11", + "3.13", + "3.14" + ], + "full_label": "ci:full-verify", + "all": [ + "Makefile", + "scripts/**", + ".github/workflows/verify.yml", + ".github/verify-groups.json", + ".gitattributes", + ".gitignore" + ], + "skip_safe": [ + "research/**", + "docs/**", + ".github/workflows/**", + "README.md", + "AGENTS.md", + "CONTRIBUTING.md", + "CONTRIBUTORS.md", + "PATCHING.md", + "autoresearch.md", + "LICENSE", + "NOTICE", + "docs/ci.md" + ], + "groups": { + "community": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-bit-axes.json", + "certificates/copied-centers-complex-input.json", + "certificates/copied-centers-corner-25-23.json", + "certificates/copied-centers-input.json", + "certificates/copied-centers-network.json", + "certificates/partial-swap-input.json", + "docs/research/community-audit-arithmetic.json", + "docs/research/community-followup-arithmetic.json", + "notes/*", + "notes/copied-centers-assembly.tex", + "notes/copied-centers-bit.tex", + "notes/copied-centers-complex.tex", + "notes/copied-centers-lemma.tex", + "notes/copied-centers-note.tex", + "notes/structured-bulk-bit.tex", + "references/copied-centers/**", + "references/copied-fixed/pr34/**", + "references/copied-fixed/pr35/**", + "references/copied-fixed/pr41/**", + "references/copied-fixed/pr44/**", + "references/semantic-bulk/rad20/LICENSE", + "references/semantic-bulk/rad20/NOTICE", + "references/semantic-bulk/rad20/SOURCE.json", + "references/semantic-bulk/rad20/code/**", + "references/semantic-bulk/rad20/reports/**", + "research/", + "research/climbed-48/**", + "research/copied-fixed-reversed/**", + "research/copied-fixed/**", + "research/copied-reversed/**", + "tests/**" + ], + "declared": "recorded" + }, + "producers": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-bit-axes.json", + "certificates/copied-centers-complex-input.json", + "certificates/copied-centers-corner-25-23.json", + "certificates/copied-centers-input.json", + "certificates/copied-centers-network.json", + "certificates/endpoint-gauge-bit-axes.json", + "certificates/endpoint-gauge-complex-input.json", + "certificates/endpoint-gauge-input.json", + "certificates/endpoint-gauge-network.json", + "certificates/partial-swap-input.json", + "certificates/partial-swap-network.json", + "certificates/stopped-product-bit-axis.json", + "certificates/stopped-product-complex-input.json", + "certificates/stopped-product-input.json", + "certificates/stopped-product-network.json", + "certificates/structured-bulk-bit-axes.json", + "certificates/structured-bulk-complex-input.json", + "certificates/structured-bulk-input.json", + "certificates/structured-bulk-network.json", + "certificates/structured-bulk-rankone-exactness.json", + "certificates/structured-bulk-rankone-profiles.json", + "notes/*", + "notes/copied-centers-assembly.tex", + "notes/copied-centers-bit.tex", + "notes/copied-centers-complex.tex", + "notes/copied-centers-lemma.tex", + "notes/copied-centers-note.tex", + "notes/endpoint-gauge-assembly.tex", + "notes/endpoint-gauge-basis.tex", + "notes/endpoint-gauge-complex.tex", + "notes/endpoint-gauge-construction.tex", + "notes/endpoint-gauge-note.tex", + "notes/partial-swap-assembly.tex", + "notes/partial-swap-basis.tex", + "notes/partial-swap-complex.tex", + "notes/partial-swap-construction.tex", + "notes/partial-swap-note.tex", + "notes/stopped-product-assembly.tex", + "notes/stopped-product-complex.tex", + "notes/stopped-product-factorization.tex", + "notes/stopped-product-interface.tex", + "notes/stopped-product-note.tex", + "notes/structured-bulk-assembly.tex", + "notes/structured-bulk-bit.tex", + "notes/structured-bulk-complex.tex", + "notes/structured-bulk-crt.tex", + "notes/structured-bulk-note.tex", + "references/copied-centers/**", + "references/semantic-bulk/MANIFEST.json", + "references/semantic-bulk/pr21/translated-partial-complex.tex", + "references/semantic-bulk/pr23/**", + "references/semantic-bulk/rad20/LICENSE", + "references/semantic-bulk/rad20/NOTICE", + "references/semantic-bulk/rad20/SOURCE.json", + "references/semantic-bulk/rad20/reports/**" + ], + "declared": "recorded" + }, + "certificates": { + "paths": [ + "*", + "certificates/", + "certificates/additive-label-audit.json", + "certificates/batched-network.json", + "certificates/block-label-audit.json", + "certificates/block-label-target.json", + "certificates/cancellation-audit.json", + "certificates/checkpoints/source527.json", + "certificates/coded-carry-audit.json", + "certificates/compact-control-audit.json", + "certificates/compact-control-layer.json", + "certificates/complex-network.json", + "certificates/controlled-bit-rank-moment.json", + "certificates/dag-network.json", + "certificates/fast-gaussian.json", + "certificates/fused-block-audit.json", + "certificates/gather-schedule-audit.json", + "certificates/incidence-network.json", + "certificates/incidence-partition-screen.json", + "certificates/joint-frame-audit.json", + "certificates/layer-preparation.json", + "certificates/network-research.json", + "certificates/network-search.json", + "certificates/network-variants.json", + "certificates/nonadjacent-axis.json", + "certificates/paired-network.json", + "certificates/parameters.json", + "certificates/prime-field28.json", + "certificates/routing-tuned.json", + "certificates/scratch-pooling-audit.json", + "certificates/shared-point-network.json", + "certificates/short-guard-audit.json", + "certificates/small-block-witness.json", + "certificates/sparse-fusion-audit.json", + "certificates/stage-reuse.json", + "docs/", + "docs/research/", + "docs/research/community-pr210-integration.json", + "docs/research/community-pr210-review.md", + "notes/batched-23-note.tex", + "notes/batched-algorithms.tex", + "notes/batched-assembly.tex", + "notes/batched-bit-rank-accounting.tex", + "notes/batched-bit-rows.tex", + "notes/batched-complex-rows.tex", + "notes/batched-path-budget.tex", + "notes/bulk-complex-guard.tex", + "notes/chirp-scaling-correction.tex", + "notes/compact-control-guard.tex", + "notes/compact-control-layout.tex", + "notes/compact-control-movement.tex", + "notes/complex-circuit-construction.tex", + "notes/controlled-projector-basis.tex", + "notes/dag-construction.tex", + "notes/fast-gaussian-resampling.tex", + "notes/incidence-construction.tex", + "notes/independent-complex.tex", + "notes/paired-construction.tex", + "notes/prime-field28-construction.tex", + "notes/projector-batching.tex", + "notes/shared-point-construction.tex", + "notes/stopped-guard.tex", + "patches/**", + "research/", + "research/community-round9-audit/", + "research/community-round9-audit/pr210-certificate.json", + "research/five-stage-source527-banks/**", + "research/machine-transfer-verification/**", + "research/ranked-pair-verification/**", + "upstream/**" + ], + "declared": "recorded" + }, + "ternary": { + "paths": [ + "*", + "certificates/complex-compression.json", + "certificates/ternary-side.json", + "notes/compact-control-guard.tex", + "notes/compact-control-layout.tex", + "notes/compact-control-movement.tex", + "notes/complex-compression.tex", + "notes/finite-alphabet-transfer.tex", + "notes/independent-complex.tex", + "notes/paired-construction.tex", + "notes/stopped-guard.tex", + "notes/ternary-five-subsets.tex", + "patches/complex-compression-31.patch", + "patches/ternary-30.patch", + "upstream/**" + ], + "declared": "recorded" + }, + "research": { + "paths": [ + "*", + "certificates/affine-vector-screens.json", + "certificates/bit-compression-audit.json", + "certificates/block-carry-audit.json", + "certificates/block-core.json", + "certificates/complex-compression.json", + "certificates/core-limits.json", + "certificates/cube-core-family.json", + "certificates/cyclic-topology-audit.json", + "certificates/disjoint-tensor-compression.json", + "certificates/dyadic-central-factor.json", + "certificates/early-sharing-audit.json", + "certificates/fano-completion-audit.json", + "certificates/fano-permutation-audit.json", + "certificates/general-network-guard.json", + "certificates/inplace-side.json", + "certificates/joint-return-audit.json", + "certificates/mixed-point-audit.json", + "certificates/paired-network.json", + "certificates/parity-side.json", + "certificates/positive-side-core.json", + "certificates/prime-subset-limits.json", + "certificates/quadratic-affine-vectors.json", + "certificates/rank-product-core.json", + "certificates/shared-core.json", + "certificates/signed-sparse-core.json", + "certificates/single-intersection.json", + "certificates/split-centers-audit.json", + "certificates/stage-pair-audit.json", + "certificates/stronger-rank-screens.json", + "certificates/subset-core-family.json", + "docs/research/affine-vector-screens.md", + "docs/research/bit-compression-audit.md", + "docs/research/block-carry-audit.md", + "docs/research/block-core.md", + "docs/research/core-limits.md", + "docs/research/cube-core-family.md", + "docs/research/cyclic-topology-audit.md", + "docs/research/disjoint-tensor-compression.md", + "docs/research/dyadic-central-factor.md", + "docs/research/early-sharing-and-centers.md", + "docs/research/fano-completion-audit.md", + "docs/research/fano-permutation-audit.md", + "docs/research/general-network-guard.md", + "docs/research/inplace-side.md", + "docs/research/joint-return-audit.md", + "docs/research/mixed-point-audit.md", + "docs/research/parity-side.md", + "docs/research/positive-side-core.md", + "docs/research/prime-subset-limits.md", + "docs/research/quadratic-affine-vectors.md", + "docs/research/rank-product-core.md", + "docs/research/shared-core.md", + "docs/research/signed-sparse-core.md", + "docs/research/single-intersection.md", + "docs/research/stage-pair-audit.md", + "docs/research/stronger-rank-screens.md", + "docs/research/subset-core-family.md", + "notes/complex-compression.tex", + "notes/disjoint-tensor-compression.tex", + "notes/dyadic-central-factor.tex", + "notes/general-network-guard.tex", + "upstream/**" + ], + "declared": "recorded" + }, + "tests": { + "paths": [ + "**" + ], + "declared": "recorded (whole tree; the run fails on main because of a pre-existing pin drift, see docs/ci.md)" + }, + "strips": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-bit-axes.json", + "certificates/copied-centers-complex-input.json", + "certificates/copied-centers-corner-25-23.json", + "certificates/copied-centers-input.json", + "certificates/copied-centers-network.json", + "notes/*", + "notes/copied-centers-assembly.tex", + "notes/copied-centers-bit.tex", + "notes/copied-centers-complex.tex", + "notes/copied-centers-lemma.tex", + "notes/copied-centers-note.tex", + "notes/structured-bulk-bit.tex", + "references/copied-centers/**", + "references/copied-fixed/pr34/**", + "references/copied-fixed/pr35/**", + "references/copied-fixed/pr41/**", + "references/copied-fixed/pr44/**", + "research/", + "research/copied-fixed/**", + "research/skip-strips/**", + "research/skip-suffix/**", + "tests/**" + ], + "declared": "recorded" + }, + "clones": { + "paths": [ + "**" + ], + "declared": "recorded" + }, + "positive": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-bit-axes.json", + "certificates/copied-centers-complex-input.json", + "certificates/copied-centers-corner-25-23.json", + "certificates/copied-centers-input.json", + "notes/*", + "notes/copied-centers-assembly.tex", + "notes/copied-centers-bit.tex", + "notes/copied-centers-complex.tex", + "notes/copied-centers-lemma.tex", + "notes/copied-centers-note.tex", + "references/copied-centers/**", + "research/", + "research/positive-skip/**", + "research/skip-strips/*", + "research/skip-strips/balanced_assembly.py", + "research/skip-strips/data-corners.json", + "research/skip-strips/data_recovery.py", + "research/skip-strips/skip_graph.py", + "research/skip-strips/verify.py", + "tests/**" + ], + "declared": "recorded" + }, + "joint": { + "paths": [ + "*", + "certificates/joint-dual-compiler.json", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-profiles-23.json", + "certificates/joint-dual-profiles-25.json", + "certificates/joint-dual-transitions-23.json", + "certificates/joint-dual-transitions-25.json", + "certificates/joint-dual-validation.json", + "certificates/joint-dual-word-23.json.gz", + "certificates/joint-dual-word-25.json.gz", + "certificates/skip-frame-compiler.json", + "certificates/skip-frame-kappa.json", + "certificates/skip-frame-profiles-23.json", + "certificates/skip-frame-profiles-25.json", + "certificates/skip-frame-transitions-23.json", + "certificates/skip-frame-transitions-25.json", + "certificates/skip-frame-validation.json", + "certificates/skip-frame-word-23.json.gz", + "certificates/skip-frame-word-25.json.gz", + "docs/research/community-round2-arithmetic.json", + "references/", + "references/frame-compiler/", + "references/frame-compiler/pr48/SOURCE.json", + "references/frame-compiler/pr48/research/copied-fixed/**", + "references/frame-compiler/pr48/scripts/*", + "references/frame-compiler/pr48/scripts/exclusion_circuit.py", + "references/frame-compiler/pr48/scripts/partial_swap/*", + "references/frame-compiler/pr48/scripts/partial_swap/binary_io.hpp", + "references/frame-compiler/pr48/scripts/partial_swap/paired.py", + "references/frame-compiler/pr48/scripts/partial_swap/shared.py", + "references/frame-compiler/pr53/LICENSE", + "references/frame-compiler/pr53/NOTICE", + "references/frame-compiler/pr53/SOURCE.json", + "references/frame-compiler/pr53/research/skip-strips/skip_graph.py", + "references/frame-compiler/pr55/", + "references/frame-compiler/pr55/LICENSE", + "references/frame-compiler/pr55/NOTICE", + "references/frame-compiler/pr55/SOURCE.json", + "references/frame-compiler/pr55/research/", + "references/frame-compiler/pr55/research/skip-suffix/", + "references/frame-compiler/pr55/research/skip-suffix/skip_graph.py", + "references/frame-compiler/pr58/**", + "research/", + "research/joint-dual/PROOF.md", + "research/joint-dual/README.md", + "research/joint-dual/SOURCE.json", + "research/matrix-exponent-synthesis/", + "research/matrix-exponent-synthesis/history/", + "research/matrix-exponent-synthesis/history/pr60/", + "research/matrix-exponent-synthesis/history/pr60/RefinedFrontierCertificate.lean", + "research/matrix-exponent-synthesis/history/pr60/candidate/*", + "research/matrix-exponent-synthesis/history/pr60/candidate/arithmetic.json", + "research/matrix-exponent-synthesis/history/pr60/candidate/generate_frontier_case.py", + "research/matrix-exponent-synthesis/history/pr60/candidate/pinned60-certificate.json", + "research/matrix-exponent-synthesis/history/pr60/candidate/weighted-lean-input.json", + "tests/**" + ], + "declared": "recorded" + }, + "pair": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-bit-axes.json", + "certificates/copied-centers-complex-input.json", + "certificates/copied-centers-corner-25-23.json", + "certificates/copied-centers-input.json", + "certificates/copied-centers-network.json", + "docs/research/community-pair-arithmetic.json", + "notes/*", + "notes/copied-centers-assembly.tex", + "notes/copied-centers-bit.tex", + "notes/copied-centers-complex.tex", + "notes/copied-centers-lemma.tex", + "notes/copied-centers-note.tex", + "notes/structured-bulk-bit.tex", + "references/copied-centers/**", + "references/copied-fixed/pr34/**", + "references/copied-fixed/pr35/**", + "references/copied-fixed/pr41/**", + "references/copied-fixed/pr44/**", + "references/frame-compiler/pr48/SOURCE.json", + "references/frame-compiler/pr48/research/copied-fixed/**", + "references/frame-compiler/pr48/scripts/exclusion_circuit.py", + "references/frame-compiler/pr48/scripts/partial_swap/", + "references/frame-compiler/pr48/scripts/partial_swap/*", + "references/frame-compiler/pr48/scripts/partial_swap/binary_io.hpp", + "references/frame-compiler/pr48/scripts/partial_swap/paired.py", + "references/frame-compiler/pr48/scripts/partial_swap/shared.py", + "research/", + "research/copied-fixed/**", + "research/matrix-exponent-synthesis/", + "research/matrix-exponent-synthesis/RefinedFrontierCertificate.lean", + "research/matrix-exponent-synthesis/candidate/*", + "research/matrix-exponent-synthesis/candidate/arithmetic.json", + "research/matrix-exponent-synthesis/candidate/generate_frontier_case.py", + "research/matrix-exponent-synthesis/candidate/pinned62-certificate.json", + "research/matrix-exponent-synthesis/candidate/weighted-lean-input.json", + "research/pair-assembly/**", + "research/skip-strips/PROOF.md", + "research/skip-strips/comparison-pr48.json", + "research/skip-strips/links-23.uses", + "research/skip-strips/links-25.uses", + "research/skip-strips/optimize_matching.py", + "research/skip-strips/original-23.json", + "research/skip-strips/original-25.json", + "research/skip-strips/profiles-23.json", + "research/skip-strips/profiles-25.json", + "research/skip-strips/scalar-23.json", + "research/skip-strips/scalar-25.json", + "research/skip-strips/skip_graph.py", + "research/skip-strips/timeline-23.json", + "research/skip-strips/timeline-25.json", + "tests/**" + ], + "declared": "recorded" + }, + "partial-gauge": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-network.json", + "certificates/partial-gauge-bit-input.json", + "certificates/partial-gauge-complex-input.json", + "certificates/partial-gauge-input.json", + "certificates/partial-gauge-network.json", + "certificates/stopped-product-network.json", + "notes/*", + "notes/partial-gauge-assembly.tex", + "notes/partial-gauge-construction.tex", + "notes/partial-gauge-frames.tex", + "notes/partial-gauge-note.tex", + "references/partial-gauge/*", + "references/partial-gauge/pr62/**", + "references/partial-gauge/pr97/**" + ], + "declared": "recorded" + }, + "three-stage-cover": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-network.json", + "certificates/partial-gauge-bit-input.json", + "certificates/partial-gauge-network.json", + "certificates/stopped-product-network.json", + "certificates/three-stage-cover-bit-input.json", + "certificates/three-stage-cover-complex-input.json", + "certificates/three-stage-cover-input.json", + "certificates/three-stage-cover-network.json", + "notes/*", + "notes/general-clifford-frames.tex", + "notes/three-stage-cover-assembly.tex", + "notes/three-stage-cover-bit.tex", + "notes/three-stage-cover-complex.tex", + "notes/three-stage-cover-note.tex", + "notes/three-stage-cover-rows.tex", + "references/partial-gauge/pr97/**", + "references/three-stage-cover/*", + "references/three-stage-cover/pr117/**" + ], + "declared": "recorded" + }, + "paired-cube": { + "paths": [ + "*", + "certificates/*", + "certificates/copied-centers-network.json", + "certificates/paired-cube-bit-input.json", + "certificates/paired-cube-complex-input.json", + "certificates/paired-cube-input.json", + "certificates/paired-cube-network.json", + "certificates/partial-gauge-bit-input.json", + "certificates/three-stage-cover-network.json", + "notes/*", + "notes/general-clifford-frames.tex", + "notes/paired-cube-assembly.tex", + "notes/paired-cube-bit.tex", + "notes/paired-cube-construction.tex", + "notes/paired-cube-note.tex", + "notes/paired-cube-sharing.tex", + "references/paired-cube/*", + "references/paired-cube/pr97-subset/*", + "references/paired-cube/pr97-subset/selection.json", + "references/paired-cube/selected-module/*", + "references/paired-cube/selected-module/README.md", + "references/paired-cube/selected-module/SOURCE.json", + "references/paired-cube/selected-module/matching-arcs.json", + "references/partial-gauge/pr97/**", + "references/three-stage-cover/pr117/**" + ], + "declared": "recorded" + }, + "recycled-bit": { + "paths": [ + "*", + "certificates/copied-centers-network.json", + "certificates/paired-cube-bit-input.json", + "certificates/paired-cube-complex-input.json", + "certificates/paired-cube-input.json", + "certificates/paired-cube-network.json", + "certificates/partial-gauge-bit-input.json", + "certificates/three-stage-cover-network.json", + "notes/general-clifford-frames.tex", + "notes/paired-cube-assembly.tex", + "notes/paired-cube-bit.tex", + "notes/paired-cube-construction.tex", + "notes/paired-cube-note.tex", + "notes/paired-cube-sharing.tex", + "references/", + "references/*", + "references/paired-cube/pr97-subset/selection.json", + "references/paired-cube/selected-module/README.md", + "references/paired-cube/selected-module/SOURCE.json", + "references/paired-cube/selected-module/matching-arcs.json", + "references/partial-gauge/pr97/**", + "research/", + "research/bit-elim-144/*", + "research/bit-elim-144/plan.json", + "research/bit-elim-144/price144.py", + "research/bit-elim-144/verify.py", + "research/bit-reuse-147/**", + "research/gauge-recycling/**", + "research/recycled-bit-integration/**", + "tests/**" + ], + "declared": "recorded" + }, + "entrance-banks": { + "paths": [ + "*", + ".github/", + ".github/workflows/", + ".github/workflows/t37-owners.yml", + "certificates/", + "certificates/replay-coverage/", + "certificates/replay-coverage/pr741-sw4-v1.json", + "certificates/selected-result.json", + "docs/", + "docs/research/", + "docs/research/community-batch1047-review.md", + "docs/research/community-batch1099-integration.json", + "docs/research/community-batch1099-review.md", + "docs/research/community-batch952-review.md", + "docs/research/community-cold617-review.md", + "docs/research/community-frontier741-review.md", + "docs/research/community-frontier799-review.md", + "docs/research/community-frontier890-review.md", + "docs/research/community-hyperplane599-review.md", + "docs/research/community-k492-review.md", + "research/", + "research/community-batch1099-audit/", + "research/community-batch1099-audit/check_frontier1094.py", + "research/community-frontier1094-audit/", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-round8-audit/*", + "research/community-round8-audit/bank_schedule.py", + "research/complex-571-cold14-b3/", + "research/complex-571-cold14-b3/PROOF-NOTE.md", + "research/complex-571-cold14-b3/README.md", + "research/complex-571-free4fc8/", + "research/complex-571-free4fc8/NOTICE.md", + "research/complex-571-hpeq5/", + "research/complex-571-hpeq5/README.md", + "research/complex-double-replica-owners/", + "research/complex-double-replica-owners/PROOF.md", + "research/complex-joint-prefix/", + "research/complex-joint-prefix/proof/", + "research/complex-joint-prefix/proof/CONSTRUCTION.md", + "research/complex-k492-owner-repair/", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md", + "research/complex-k492-owner-repair/PROOF-NOTE.md", + "research/complex-k492-owner-repair/README.md", + "research/complex-multicold/", + "research/complex-multicold/proof/", + "research/complex-multicold/proof/CONSTRUCTION.md", + "research/complex-multicold/vendor/", + "research/complex-multicold/vendor/pr559/", + "research/complex-multicold/vendor/pr559/PROOF.md", + "research/complex-sw4-frame8/**", + "research/complex-t16-rare-pattern-exchanges/**", + "research/complex-t21-owner-bound/**", + "research/complex-t21-owners/**", + "research/complex-t37-owners/**", + "research/coordinated-frames-and-entrance-banks/**", + "research/direct-delivery504-global/**", + "research/e8-bit-carrier-skeleton/**", + "research/e8-bit-p111-tuned/**", + "research/e8-bit-r420/", + "research/e8-bit-r420/README.md", + "research/gauge44-barch/", + "research/gauge44-barch/PROOF-NOTE-BARCH.md", + "research/gauge44-frames-x/**", + "research/gauge44-leaver/**", + "research/gauge44-leaver8/**", + "research/gauge44-slots-t16/**", + "research/gauge44-slots/**", + "research/hyperplane-end-lean/", + "research/hyperplane-end-lean/HyperplaneEnd/", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "research/hyperplane-end-lean/PROOF.md", + "research/kernel-frame-coalescing/", + "research/kernel-frame-coalescing/PROOF.md", + "research/structural-gain/", + "research/structural-gain/frontier-composition/", + "research/structural-gain/frontier-composition/README.md" + ], + "declared": "recorded" + }, + "ranked-pair-finite": { + "job": "ranked-pair-finite", + "paths": [ + "*", + "research/", + "research/ranked-pair-verification/**" + ], + "declared": "recorded" + }, + "formal-historical": { + "job": "formal", + "package": "historical", + "declared": "static", + "paths": [ + "formal/**", + "research/machine-transfer-verification/**", + "research/ranked-pair-verification/**" + ] + }, + "formal-gaussian": { + "job": "formal", + "package": "gaussian", + "declared": "recorded+static", + "paths": [ + "*", + "research/", + "research/gaussian-parity-synthesis/**" + ] + }, + "formal-matrix": { + "job": "formal", + "package": "matrix", + "declared": "recorded", + "paths": [ + "*", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-profiles-23.json", + "certificates/joint-dual-profiles-25.json", + "docs/research/community-pair-arithmetic.json", + "docs/research/community-round2-arithmetic.json", + "references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py", + "research/", + "research/matrix-exponent-synthesis/**", + "research/pair-assembly/frame/frame-certificate.json", + "research/pair-assembly/frame/frame-profiles-23.json", + "research/pair-assembly/frame/frame-profiles-25.json" + ] + }, + "pkg-bit-elim-144": { + "job": "package", + "package": "bit-elim-144", + "python": [ + "3.11", + "3.14" + ], + "command": "python3 research/bit-elim-144/verify.py", + "paths": [ + "certificates/copied-centers-network.json", + "certificates/paired-cube-bit-input.json", + "certificates/paired-cube-complex-input.json", + "references/paired-cube/pr97-subset/selection.json", + "references/partial-gauge/pr97/**", + "research/", + "research/bit-elim-144/**" + ], + "declared": "recorded" + }, + "pkg-bit-reuse-147": { + "job": "package", + "package": "bit-reuse-147", + "python": [ + "3.11", + "3.14" + ], + "command": "python3 research/bit-reuse-147/verify.py", + "paths": [ + "certificates/copied-centers-network.json", + "certificates/paired-cube-bit-input.json", + "certificates/paired-cube-complex-input.json", + "references/paired-cube/pr97-subset/selection.json", + "references/partial-gauge/pr97/**", + "research/", + "research/bit-reuse-147/**" + ], + "declared": "recorded" + }, + "pkg-early-reset-reuse": { + "job": "package", + "package": "early-reset-reuse", + "python": [ + "3.11", + "3.14" + ], + "command": "python -B research/e8-early-reset-kernel/verify.py \"$RUNNER_TEMP/early-reset-reuse\"", + "artifact": "early-reset-reuse", + "paths": [ + "research/", + "research/e8-early-reset-kernel/**", + "research/e8-early-reset-reuse/**", + "research/split-centres-global/**" + ], + "declared": "recorded" + }, + "pkg-graded-box-convolution": { + "job": "package", + "package": "graded-box-convolution", + "python": [ + "3.11", + "3.14" + ], + "command": "python -B research/graded-box-convolution/verify.py \"$RUNNER_TEMP/graded-box\"", + "paths": [ + "research/", + "research/graded-box-convolution/**" + ], + "declared": "recorded" + } + } +} diff --git a/.github/workflows/bit-elim-144.yml b/.github/workflows/bit-elim-144.yml deleted file mode 100644 index f136614637..0000000000 --- a/.github/workflows/bit-elim-144.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: Verify terminal elimination on the paired-cube bit word - -on: - push: - pull_request: - workflow_dispatch: - -permissions: - contents: read - -jobs: - certificate: - runs-on: ubuntu-24.04 - timeout-minutes: 30 - strategy: - fail-fast: false - matrix: - python-version: ['3.11', '3.14'] - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 - with: - persist-credentials: false - - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 - with: - python-version: ${{ matrix.python-version }} - - name: Reproduce PR144, regenerate the elimination, replay and reprice - run: python3 research/bit-elim-144/verify.py - - name: Require committed files to remain unchanged - run: git diff --exit-code diff --git a/.github/workflows/bit-reuse-147.yml b/.github/workflows/bit-reuse-147.yml deleted file mode 100644 index 6a8d3a27ec..0000000000 --- a/.github/workflows/bit-reuse-147.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: Verify recycled bit registers on the paired-cube bit word - -on: - push: - pull_request: - workflow_dispatch: - -permissions: - contents: read - -jobs: - certificate: - runs-on: ubuntu-24.04 - timeout-minutes: 30 - strategy: - fail-fast: false - matrix: - python-version: ['3.11', '3.14'] - steps: - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 - with: - persist-credentials: false - - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 - with: - python-version: ${{ matrix.python-version }} - - name: Reproduce PR144, run the ledger, check exact nesting, replay and reprice - run: python3 research/bit-reuse-147/verify.py - - name: Require committed files to remain unchanged - run: git diff --exit-code diff --git a/.github/workflows/ci-cancel-superseded.yml b/.github/workflows/ci-cancel-superseded.yml new file mode 100644 index 0000000000..dcbce6fd64 --- /dev/null +++ b/.github/workflows/ci-cancel-superseded.yml @@ -0,0 +1,50 @@ +name: Cancel superseded pull-request runs + +# Maintenance, run by hand. Runs queued before a workflow gained its +# concurrency group keep their old definition and are never cancelled +# automatically. This cancels queued or running pull-request runs that a +# newer commit of the same pull request has superseded (same workflow, same +# pull request, different head commit). Pushes, scheduled and manual runs, +# runs sharing the newest head commit, and runs whose pull request cannot +# be identified unambiguously are never touched. No pull-request code is +# checked out: the script comes from the branch this workflow runs on. +on: + workflow_dispatch: + inputs: + cancel: + description: Set to "yes" to cancel; anything else only reports. + default: 'no' + required: true + limit: + description: Cancel at most this many runs (0 = no limit). + default: '0' + required: true + created: + description: Created-at window to inspect (the API lists at most the newest 1000 runs per query), e.g. 2026-10-14T00:00:00Z..2026-10-14T06:00:00Z + required: true + +permissions: + actions: write + contents: read + +concurrency: + group: ci-cancel-superseded + cancel-in-progress: false + +jobs: + cancel: + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - name: Report or cancel superseded runs + env: + GH_TOKEN: ${{ github.token }} + CANCEL: ${{ inputs.cancel }} + LIMIT: ${{ inputs.limit }} + CREATED: ${{ inputs.created }} + run: | + if [ "$CANCEL" = yes ]; then set -- --cancel; else set --; fi + python3 -B scripts/cancel_superseded_runs.py --repo "$GITHUB_REPOSITORY" --limit "$LIMIT" --created "$CREATED" "$@" diff --git a/.github/workflows/early-reset-reuse.yml b/.github/workflows/early-reset-reuse.yml deleted file mode 100644 index ad7aeacfde..0000000000 --- a/.github/workflows/early-reset-reuse.yml +++ /dev/null @@ -1,20 +0,0 @@ -name: Verify early reset and kernel composition -on: [push, pull_request] -jobs: - verify: - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - python: ['3.11', '3.14'] - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 - with: - python-version: ${{ matrix.python }} - - run: python -B research/e8-early-reset-kernel/verify.py "$RUNNER_TEMP/early-reset-reuse" - - uses: actions/upload-artifact@v4 - if: always() - with: - name: early-reset-reuse-${{ matrix.python }} - path: ${{ runner.temp }}/early-reset-reuse diff --git a/.github/workflows/graded-box-convolution.yml b/.github/workflows/graded-box-convolution.yml deleted file mode 100644 index 716feacb76..0000000000 --- a/.github/workflows/graded-box-convolution.yml +++ /dev/null @@ -1,17 +0,0 @@ -name: Graded box convolution -on: - pull_request: - push: -jobs: - verify: - runs-on: ubuntu-latest - timeout-minutes: 10 - strategy: - matrix: - python: ['3.11', '3.14'] - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 - with: - python-version: ${{ matrix.python }} - - run: python -B research/graded-box-convolution/verify.py "$RUNNER_TEMP/graded-box" diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4446616e87..524d238b32 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -3,20 +3,88 @@ name: Verify research artifacts on: push: pull_request: + # `labeled` lets a maintainer request the full matrix on a fork pull + # request with the ci:full-verify label; see docs/ci.md. + types: [opened, synchronize, reopened, labeled] + schedule: + # Full matrix with input recording on main, so the declared inputs in + # .github/verify-groups.json are re-checked against the tree four times + # a day regardless of what individual pushes selected. + - cron: '23 */6 * * *' workflow_dispatch: permissions: contents: read +# A newer revision of a pull request supersedes its queued or running +# automatic run. Pushes (main, branches, tags), label-requested runs, +# scheduled and manual runs each keep their own run and are never cancelled +# by this policy. +concurrency: + group: verify-${{ github.event_name }}-${{ (github.event_name == 'pull_request' && github.event.action != 'labeled') && github.event.pull_request.number || github.run_id }} + cancel-in-progress: ${{ github.event_name == 'pull_request' && github.event.action != 'labeled' }} + jobs: + plan: + # Decide which groups this run must execute. Every check still runs for + # any change that can reach it: see scripts/plan_verify_groups.py and + # the declared, strace-recorded inputs in .github/verify-groups.json. + runs-on: ubuntu-24.04 + timeout-minutes: 10 + outputs: + matrix: ${{ steps.plan.outputs.matrix }} + count: ${{ steps.plan.outputs.count }} + formal: ${{ steps.plan.outputs.formal }} + formal_count: ${{ steps.plan.outputs.formal_count }} + packages: ${{ steps.plan.outputs.packages }} + package_count: ${{ steps.plan.outputs.package_count }} + jobs: ${{ steps.plan.outputs.jobs }} + groups: ${{ steps.plan.outputs.groups }} + mode: ${{ steps.plan.outputs.mode }} + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + # Depth 2 keeps both parents of the pull request merge commit. + fetch-depth: 2 + persist-credentials: false + - name: Fetch the commit this push started from + if: github.event_name == 'push' && github.event.before != '0000000000000000000000000000000000000000' + env: + BEFORE: ${{ github.event.before }} + # A missing commit (force push) leaves the planner without a diff; it + # then verifies everything. + run: git fetch --no-tags --depth=1 origin "$BEFORE" || true + - name: Select verification groups from the changed paths + id: plan + env: + EVENT: ${{ github.event_name }} + ACTION: ${{ github.event.action }} + LABEL: ${{ github.event.label.name }} + LABELS: ${{ toJSON(github.event.pull_request.labels.*.name) }} + BEFORE: ${{ github.event.before }} + run: | + case "$EVENT" in + pull_request) + # The checkout is the merge of the pull request into its base; + # the first parent is the base tip it was merged onto. + if git rev-parse --verify -q 'HEAD^2' >/dev/null; then BASE='HEAD^1'; else BASE=''; fi ;; + push) BASE="$BEFORE" ;; + *) BASE='' ;; + esac + if [ -n "$BASE" ]; then set -- --diff "$BASE" HEAD; else set --; fi + python3 -B scripts/plan_verify_groups.py --event "$EVENT" --action "$ACTION" --label "$LABEL" \ + --labels "$LABELS" "$@" --github-output "$GITHUB_OUTPUT" --summary "$GITHUB_STEP_SUMMARY" + verify: + needs: plan + if: needs.plan.outputs.count != '0' runs-on: ubuntu-24.04 timeout-minutes: 35 strategy: fail-fast: false - matrix: - python-version: ['3.11', '3.13', '3.14'] - group: [community, producers, certificates, ternary, research, tests, strips, clones, positive, joint, pair, partial-gauge, three-stage-cover, paired-cube, recycled-bit, entrance-banks] + # Selected groups on every supported Python; full runs are the same + # 48 combinations as before. + matrix: ${{ fromJSON(needs.plan.outputs.matrix) }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 with: @@ -34,18 +102,25 @@ jobs: sudo apt-get update sudo apt-get install -y libboost-dev fi - - name: Check arithmetic, source hashes, finite identities, and patches + - name: Install strace to record the inputs this group reads run: | - if [ "${{ matrix.group }}" = clones ]; then - make skip-clones-verify split-skip-producer - python -B scripts/replay_historical_check.py split-skip - else - make verify-${{ matrix.group }} + if ! command -v strace >/dev/null; then + sudo apt-get install -y strace || { sudo apt-get update && sudo apt-get install -y strace; } fi + - name: Check arithmetic, source hashes, finite identities, and patches + env: + GROUP: ${{ matrix.group }} + # The group's unchanged commands (see GROUP_COMMANDS in the tracer), + # run under strace: the verification verdict is the same, and the + # step additionally fails if the group read an input that + # .github/verify-groups.json does not declare. + run: python3 -B scripts/trace_verify_inputs.py --group "$GROUP" --check - name: Require reproducible certificates and patches run: git diff --exit-code ranked-pair-finite: + needs: plan + if: contains(needs.plan.outputs.jobs, 'ranked-pair-finite') runs-on: ubuntu-24.04 timeout-minutes: 20 steps: @@ -62,18 +137,26 @@ jobs: ref: ad0f25ff7b23cff7f08ad237c2254e6ecf74257e path: build/ranked-pair-upstream persist-credentials: false + - name: Install strace to record the inputs this replay reads + run: | + if ! command -v strace >/dev/null; then + sudo apt-get install -y strace || { sudo apt-get update && sudo apt-get install -y strace; } + fi - name: Independently replay words and rebuild exact CRT profiles - run: make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream + # `make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream` under + # strace, failing on undeclared inputs. + run: python3 -B scripts/trace_verify_inputs.py --group ranked-pair-finite --check - name: Require unchanged tracked artifacts run: git diff --exit-code formal: + needs: plan + if: needs.plan.outputs.formal_count != '0' runs-on: ubuntu-24.04 timeout-minutes: 45 strategy: fail-fast: false - matrix: - package: [historical, gaussian, matrix] + matrix: ${{ fromJSON(needs.plan.outputs.formal) }} steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 with: @@ -86,9 +169,115 @@ jobs: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh sh /tmp/elan-init.sh -y --default-toolchain none echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: Fetch pinned Mathlib build cache + - name: Restore pinned Mathlib dependencies if: matrix.package == 'historical' + id: mathlib-cache + uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5 + with: + # Cache dependencies only; project compilation and axiom audits + # still run. Exact keys prevent reuse across toolchain/lock changes + # and across runner images. + path: formal/lean/.lake/packages + key: mathlib-v1-ubuntu-24.04-${{ runner.arch }}-${{ hashFiles('formal/lean/lean-toolchain', 'formal/lean/lake-manifest.json', 'formal/lean/lakefile.toml') }} + - name: Fetch pinned Mathlib build cache + if: matrix.package == 'historical' && steps.mathlib-cache.outputs.cache-hit != 'true' working-directory: formal/lean run: lake exe cache get + - name: Install strace to record the inputs this package reads + run: | + if ! command -v strace >/dev/null; then + sudo apt-get install -y strace || { sudo apt-get update && sudo apt-get install -y strace; } + fi - name: Check formal package and theorem axiom dependencies - run: make formal-${{ matrix.package }}-verify + env: + PACKAGE: ${{ matrix.package }} + # `make formal--verify` under strace, failing on undeclared inputs. + run: python3 -B scripts/trace_verify_inputs.py --group "formal-$PACKAGE" --command "make formal-$PACKAGE-verify" --check + - name: Save pinned Mathlib dependencies from successful main runs + # PRs can restore main's cache, but do not fill storage with one copy + # per merge ref. Do not cache verification verdicts or certificates. + if: matrix.package == 'historical' && github.event_name != 'pull_request' && github.ref == 'refs/heads/main' && steps.mathlib-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@caa296126883cff596d87d8935842f9db880ef25 # v5 + with: + path: formal/lean/.lake/packages + key: ${{ steps.mathlib-cache.outputs.cache-primary-key }} + + packages: + # Historical package verifiers that previously had their own unfiltered + # workflows (bit-elim-144, bit-reuse-147, early-reset-reuse, + # graded-box-convolution). Same commands and Python versions; selected by + # the planner from their recorded inputs instead of native paths filters, + # which only inspect the first few hundred changed files. + needs: plan + if: needs.plan.outputs.package_count != '0' + runs-on: ubuntu-24.04 + timeout-minutes: 30 + strategy: + fail-fast: false + matrix: ${{ fromJSON(needs.plan.outputs.packages) }} + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - name: Install strace to record the inputs this verifier reads + run: | + if ! command -v strace >/dev/null; then + sudo apt-get install -y strace || { sudo apt-get update && sudo apt-get install -y strace; } + fi + - name: Reproduce, replay and reprice the package + env: + PACKAGE: ${{ matrix.package }} + COMMAND: ${{ matrix.command }} + # The package's own command under strace, failing on undeclared inputs. + run: python3 -B scripts/trace_verify_inputs.py --group "pkg-$PACKAGE" --command "$COMMAND" --check + - name: Require committed files to remain unchanged + run: git diff --exit-code + - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + if: always() && matrix.artifact != '' + with: + name: ${{ matrix.artifact }}-${{ matrix.python-version }} + path: ${{ runner.temp }}/${{ matrix.artifact }} + + verify-summary: + # One stable status for the whole run. It fails when planning failed, + # when a job the plan selected did not succeed, or when any job failed + # or was cancelled; only jobs the planner skipped on purpose may be + # skipped. + needs: [plan, verify, ranked-pair-finite, formal, packages] + if: always() + runs-on: ubuntu-24.04 + timeout-minutes: 5 + steps: + - name: Report the plan and the results + env: + RESULTS: ${{ toJSON(needs) }} + run: | + echo "$RESULTS" | python3 -c ' + import json, sys + needs = json.load(sys.stdin) + plan = needs["plan"] + if plan["result"] != "success": + sys.exit("planning did not succeed: " + plan["result"]) + out = plan["outputs"] + expected = { + "verify": out.get("count", "0") != "0", + "formal": out.get("formal_count", "0") != "0", + "packages": out.get("package_count", "0") != "0", + "ranked-pair-finite": "ranked-pair-finite" in out.get("jobs", "").split(","), + } + problems = {} + for job, selected in expected.items(): + result = needs[job]["result"] + if selected and result != "success": + problems[job] = "selected but " + result + elif not selected and result not in ("skipped", "success"): + problems[job] = "not selected but " + result + print("plan mode=%s groups=%s" % (out.get("mode"), out.get("groups"))) + if problems: + sys.exit("verification incomplete: " + json.dumps(problems)) + print("every selected job succeeded: " + + ", ".join("%s=%s" % (k, needs[k]["result"]) for k in sorted(expected))) + ' diff --git a/docs/ci.md b/docs/ci.md new file mode 100644 index 0000000000..2b49e41363 --- /dev/null +++ b/docs/ci.md @@ -0,0 +1,247 @@ +# CI execution policy + +The general artifact workflow is +[verify.yml](../.github/workflows/verify.yml). It verifies 16 Makefile groups +on Python 3.11, 3.13 and 3.14, the ranked-pair finite replay, the three +formal Lean packages and four historical package verifiers. Nothing in that +list was removed or thinned. What changed is *when* each job runs: a cheap +`plan` job first decides which of them the run's changed paths can reach. + +## Why + +Measured with the GitHub API on 2026-10-13/14 (details in the +[contribution PR](https://github.com/CrocSwap/integer-mult-bounds/pulls)): + +- The repository had about 4,700 queued runs and 20 to 22 hours of queue + wait, growing since 2026-10-13 06:00 UTC. +- The runner concurrency available to the repository fell from more than + 134 jobs on 2026-10-13 morning to 60 on 2026-10-14 evening and 30 to 38 + at 22:30 UTC. That is outside the repository's control. +- Demand was about 222,000 runner-minutes per day against 86,400 per day + at 60 concurrent jobs. `verify.yml` accounted for 86% of the minutes: + 52 jobs and about 207 runner-minutes per run, 925 runs a day. +- A verify job spends 3.6 of its 3.9 minutes inside `make verify-`; + checkout and interpreter setup are 0.3 minutes. Merging jobs or caching + setup cannot help; the verification work itself is the cost. +- 23 of 30 recently updated pull requests only added a new + `research//` directory. Only two groups depend on the whole + tree (`clones` copies and hashes every tracked file; `tests` walks every + research package), so the other 50 jobs of those runs re-verified a tree + the pull request did not change. +- 25% of the queued runs had already been superseded by a newer push. + +## What runs + +1. **Planning.** For a pull request the checkout is GitHub's merge of the + pull request into its base, and the planner diffs that merge against its + first parent (`git diff --no-renames --name-status`). For a push to main + it diffs `before..after`. Each changed path is classified with + [.github/verify-groups.json](../.github/verify-groups.json): + - a path in the manifest's `all` list (Makefile, `scripts/**`, the + workflow, the manifest, and any `.gitattributes`, `.gitignore` or + `.gitmodules` at any depth) runs everything; + - a path matching a group's declared inputs selects that group, on every + Python version; + - a path in `skip_safe` (research packages, documentation prose, other + workflow files, top-level prose) selects nothing; a declared group + input always takes precedence over `skip_safe`; + - any other path is *unclassified* and runs everything. Silence has to be + declared; it is never assumed. + Scheduled and manually dispatched runs, pull requests carrying the + `ci:full-verify` label, any run whose diff cannot be computed (force + push, missing parent), any change to a symbolic link, any tracked path + that `.gitignore` would ignore, and any entry added to or removed from + the repository root run everything. A group declared `**` depends on + the whole tree and runs on every change (the `clones` group copies and + hashes every tracked file; the `tests` group walks every research + package), but a whole-tree match never counts as understanding a path: + an otherwise undeclared path still runs everything. +2. **Verification.** Selected groups run exactly the commands they ran + before, under `strace`, and the step also fails if a group read an input + its declaration does not cover. Full runs are the same 48 Python + combinations, the finite replay, the three formal packages and the four + package verifiers as before. +3. **Summary.** `verify-summary` is one stable status: it fails if planning + failed, if any job the plan selected did not succeed, or if any job + failed or was cancelled; only jobs the planner skipped on purpose may be + skipped. + +## Expected effect + +Measured by replaying the planner over the changed-file lists of the 60 +most recently updated open pull requests (2026-10-15) with the recorded +manifest, using the Oct 14 per-job durations: + +| | Runner-minutes per pull-request sync | +|---|---| +| Before (52 verify jobs plus the four package workflows) | 232 | +| After, mean over the 60 pull requests | 63 | +| After, a pull request that only adds a research package | 25 (`tests` and `clones` on three Pythons, plus the plan job) | + +51 of the 60 pull requests select only the groups they reach; 9 run +everything, 6 of them because they edit the root `.gitattributes` and 3 +because they change files under `scripts/`. At the Oct 14 arrival rate +(792 syncs and 133 main pushes a day) that is about 55,000 runner-minutes +a day including the scheduled full runs, against 86,400 available at 60 +concurrent jobs. If the concurrency available to the repository stays at +the 30 to 38 jobs observed on the evening of Oct 14, the queue still +clears but with little headroom; that capacity question is outside this +change. + +## How the declared inputs are known to be complete + +The manifest is recorded, not guessed. +[scripts/trace_verify_inputs.py](../scripts/trace_verify_inputs.py) runs a +group's exact CI command under `strace` and records every tracked file it +opened, every directory it listed, every path whose existence it probed and +every whole-tree Git query it made (`git ls-files`, `git status`, ...). +`--check` fails when a recorded input is not covered by the group's patterns. + +Pattern semantics are small on purpose: + +| Pattern | Matches | +|---|---| +| `path/to/file` | any change to that file | +| `dir/**` (`**` alone: the whole tree) | any change at or below `dir` | +| `dir/*` (`*`: the repository root) | an entry added to or removed from the listed directory; editing an existing entry is covered by its own read | +| `dir/` | the directory was only checked for existence (path resolution, `mkdir -p`, `os.path.isdir`); only creating or removing it matters | + +An added path changes the listing of its deepest ancestor that already +existed in the base tree, and a deleted path the listing of its deepest +surviving ancestor; the planner computes that from `git ls-tree` of both +trees, so adding `research/new-package/verify.py` changes the listing of +`research`, not of the root, and creates only `research/new-package`. +Listing and existence are recorded separately because they differ in +practice: every Python process resolves its script path through +`research`, which proves nothing about that directory's entries, while a +glob or a directory walk does. GNU make lists the repository root before every +rule, so a new or removed entry directly at the root always verifies +everything. + +Every verification job, selected or full, runs under the tracer and fails +on undeclared inputs, on every Python version. A change that makes a +verifier read a new input therefore fails until the declaration is updated, +and the scheduled full runs re-validate the whole manifest against main +four times a day. The Lean builds of the formal packages run under the +tracer too; their project trees are declared whole because Lake reads them +densely. + +Regenerate a group's patterns locally with: + +```sh +python3 -B scripts/trace_verify_inputs.py --group community --output build/community.json --check --suggest +``` + +The initial declarations were recorded locally on Python 3.14 (the +`gaussian` and `matrix` formal packages with their real Make targets; the +`historical` package's Python audits, with `formal/**` declared whole since +its Mathlib-backed build was not run locally). The first hosted runs on +3.11 and 3.13 are the check that nothing version-specific was missed; an +undeclared input fails that job with the exact pattern to add. + +## Requesting the full matrix on a pull request + +Fork pull requests cannot be targeted by **Run workflow** in this +repository. Add the `ci:full-verify` label instead: the label event starts a +full run on the pull request's merge commit, with its own concurrency group +so it is not cancelled by later pushes, and every later push to a labelled +pull request also runs everything. Remove and re-add the label to re-run. + +## Pushes and the schedule + +Every push (main, other branches, tags) runs the groups its own diff +reaches, with no cancellation and no shared concurrency group, so each +pushed change is verified for what it touched; a push whose previous +commit is unavailable (new branch, tag, force push) verifies everything. The scheduled full run every six hours +re-establishes whole-tree verification independently of any selection and +re-checks the manifest; manual dispatch does the same on demand. A schedule +is an audit, not a guarantee: a transient bad commit reverted before the +next schedule is caught by its own push run, not by the schedule. + +## Superseded runs + +A newer revision of a pull request cancels that pull request's queued or +running automatic run. Runs created before this policy keep their old +definition; [ci-cancel-superseded.yml](../.github/workflows/ci-cancel-superseded.yml) +is a manually dispatched, report-only-by-default maintenance workflow that +cancels, through the API and without checking out any pull-request code, +pull-request runs that a newer commit of the same pull request has +superseded. It never touches pushes, scheduled or manual runs, runs that +share the newest head commit (re-runs, label-requested runs) or runs whose +pull request it cannot identify unambiguously, and it inspects one +created-at window per dispatch because the API lists at most 1000 runs. + +## Trust boundary + +A pull request runs its own copy of the workflow, planner and manifest with +a read-only token and no secrets, exactly as before. "Changing the planner +runs everything" guards against mistakes, not against a hostile pull +request; pushes to main and scheduled runs, which execute reviewed code +only, remain the trust anchor. + +## Dependency caching + +Only `formal/lean/.lake/packages` is cached, with an exact key derived from +the runner image, architecture, Lean toolchain, Lake manifest and Lake +configuration. Successful non-PR runs on `main` populate the cache; pull +requests restore it. Project compilation, source checks and theorem axiom +audits still run on cache hits. The cache contains dependency sources and +builds, never verification results, regenerated certificates or replay +receipts. + +## Earlier verification speedups + +The following contributions are merged, but their accelerated +implementations remain opt-in and are not used by the matrix: + +- Sagar Thakrar's [#1041](https://github.com/CrocSwap/integer-mult-bounds/pull/1041) + parallel phase recipes, [#1059](https://github.com/CrocSwap/integer-mult-bounds/pull/1059) + parallel U8 layer-end controls, and + [#1151](https://github.com/CrocSwap/integer-mult-bounds/pull/1151) + frontier1042 layer-end controls. Their equivalence checks are separate from + adopting them in the selected cold replay. +- Sagar's [#1433](https://github.com/CrocSwap/integer-mult-bounds/pull/1433) + packed omission replay and [#1584](https://github.com/CrocSwap/integer-mult-bounds/pull/1584) + finite-bit transition cache are also opt-in. +- Josie Elliston's + [selected-chain phase comparison](../research/frontier1042-phase-fastpath/README.md) + documents the remaining integration points in pinned scripts. + +This CI change leaves those sources and their attribution intact. It does +not alter pinned verifiers, frozen evidence, the selected result or +mathematical claims. + +## Validation + +Local validation uses Linux, Python 3.14.4, strace 6.x and actionlint 1.7.12: + +```sh +actionlint .github/workflows/*.yml +python3 -B -m unittest discover -s tests -p 'test_plan_verify_groups.py' -v +python3 -B -m unittest discover -s tests -p 'test_trace_verify_inputs.py' -v +python3 -B scripts/check_selected_ci_inputs.py +python3 -B -m unittest discover -s tests -p test_selected_ci_inputs.py -v +git diff --check +``` + +The planner tests assert that the manifest's verification groups are +exactly the Makefile's `verify-*` targets, that a full plan is the fixed +48-pair universe without duplicates, and that a pull request adding only a +new research package selects exactly the whole-tree groups, on every +Python version. Hosted execution and the first scheduled tracer run are not +claimed by local checks. + +## Known failures on main at the time of this change + +Two tooling commits of 2026-10-14 changed sources that historical packages +pin by hash without updating the pins: d7d8bfcb (`scripts/exclusion_circuit.py`, +pinned by `research/skip-clones`) and 6178dede (`scripts/shared_point_circuit.py`, +pinned by `research/skip-strips`). The `clones` group and the +`test_skip_clones` module fail on that tree, while +`test_exclusion_embedding_masks` and `test_exclusion_support_masks` expect +the new bytes, so the `tests` group cannot pass in either state. This change +does not touch pins or frozen evidence. The input recordings for `clones` +and `tests` were made with the pinned versions of those two files +temporarily restored in a scratch checkout (the set of paths a group reads +does not depend on those bytes); both groups depend on the whole tree and +are declared `**`, so the recordings are not evidence that main passes. diff --git a/scripts/cancel_superseded_runs.py b/scripts/cancel_superseded_runs.py new file mode 100644 index 0000000000..8e30881a89 --- /dev/null +++ b/scripts/cancel_superseded_runs.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Cancel queued or running pull-request runs that a newer commit of the same +pull request has superseded. + +Runs created before a workflow gained a concurrency group keep their old +definition, so a backlog of superseded runs can only be cleared explicitly. +This script is deliberately narrow: + +* only ``pull_request`` runs are candidates; pushes, scheduled and manually + dispatched runs are never touched; +* a run is superseded only if its head commit is no longer the pull + request's current head commit (read from the pull request itself, not + from whichever runs are listed). Runs for the current head (a re-run, a + label-requested full run) are kept; +* the pull request is identified by number when the API provides it, and + otherwise (fork pull requests) by looking up the single open pull request + for the run's head repository and branch; ambiguous or unknown identities + are skipped; +* a ``--created`` window is required because the API lists at most the + newest 1000 runs per query. + +Everything goes through the GitHub REST API via ``gh``; no pull-request +code is checked out. Dry run by default; pass ``--cancel`` to act. +""" +import argparse +import json +import subprocess +import sys +import urllib.parse + + +def api(path): + out = subprocess.run(['gh', 'api', '--paginate', path], check=True, stdout=subprocess.PIPE) + text = out.stdout.decode() + decoder = json.JSONDecoder() + items, pos = [], 0 + while pos < len(text): + while pos < len(text) and text[pos].isspace(): + pos += 1 + if pos >= len(text): + break + obj, pos = decoder.raw_decode(text, pos) + items.append(obj) + return items + + +def list_runs(repo, status, created): + runs = [] + for page in api('repos/%s/actions/runs?status=%s&created=%s&per_page=100' % (repo, status, created)): + runs += page.get('workflow_runs', []) + return runs + + +def identify(repo, run, cache): + """(workflow path, pull request number) or None when not unambiguous.""" + prs = run.get('pull_requests') or [] + if len(prs) == 1: + return run['path'], prs[0]['number'] + if len(prs) > 1: + return None + head_repo = (run.get('head_repository') or {}).get('full_name') + branch = run.get('head_branch') + if not head_repo or not branch: + return None + key = (head_repo, branch) + if key not in cache: + owner = head_repo.split('/')[0] + found = [] + query = urllib.parse.urlencode({'state': 'open', 'head': owner + ':' + branch, 'per_page': 100}) + for page in api('repos/%s/pulls?%s' % (repo, query)): + found += [pr for pr in page + if (pr.get('head') or {}).get('ref') == branch + and ((pr.get('head') or {}).get('repo') or {}).get('full_name') == head_repo] + cache[key] = found[0]['number'] if len(found) == 1 else None + number = cache[key] + return (run['path'], number) if number is not None else None + + +def current_head(repo, number, cache): + """The pull request's head commit right now, from the pull request itself + rather than from whichever runs happen to be listed.""" + if number not in cache: + pages = api('repos/%s/pulls/%d' % (repo, number)) + cache[number] = pages[0].get('head', {}).get('sha') if pages else None + return cache[number] + + +def superseded(runs, identities, heads): + """Runs to cancel: active runs whose head commit is no longer the pull + request's head commit.""" + cancel = [] + for run in runs: + if run['event'] != 'pull_request': + continue + identity = identities.get(run['id']) + if identity is None: + continue + head = heads.get(identity[1]) + if head and run['head_sha'] != head: + cancel.append(run) + return cancel + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--repo', required=True, help='owner/name') + ap.add_argument('--created', required=True, + help='GitHub created filter, e.g. 2026-10-14T00:00:00Z..2026-10-14T06:00:00Z (the API lists ' + 'at most the newest 1000 runs per query, so use windows for a deep backlog)') + ap.add_argument('--workflow', action='append', default=[], + help='workflow file name to consider (repeatable); default: every workflow') + ap.add_argument('--cancel', action='store_true', help='actually cancel (default: report only)') + ap.add_argument('--limit', type=int, default=0, help='cancel at most this many runs (0 = no limit)') + args = ap.parse_args(argv) + + runs = [] + for status in ('queued', 'in_progress', 'waiting', 'pending'): + runs += list_runs(args.repo, status, args.created) + if args.workflow: + wanted = set(args.workflow) + runs = [r for r in runs if r['path'].rsplit('/', 1)[-1] in wanted] + seen, unique = set(), [] + for run in runs: + if run['id'] not in seen and run['event'] == 'pull_request': + seen.add(run['id']); unique.append(run) + cache, identities, unidentified, heads = {}, {}, 0, {} + for run in unique: + identity = identify(args.repo, run, cache) + if identity is None: + unidentified += 1 + else: + identities[run['id']] = identity + head_cache = {} + for identity in set(identities.values()): + heads[identity[1]] = current_head(args.repo, identity[1], head_cache) + targets = superseded(unique, identities, heads) + if args.limit: + targets = targets[:args.limit] + print('pull-request runs considered: %d; without an unambiguous pull request (kept): %d; superseded: %d' + % (len(unique), unidentified, len(targets))) + for number, head in sorted(heads.items()): + if head is None: + print('pull request #%d: current head unknown; its runs are kept' % number) + for run in targets: + print('%s run %d %s PR #%d head %s created %s (%s)' % ( + 'CANCEL' if args.cancel else 'would cancel', run['id'], run['path'].rsplit('/', 1)[-1], + identities[run['id']][1], run['head_sha'][:8], run['created_at'], run['status'])) + if args.cancel: + subprocess.run(['gh', 'api', '-X', 'POST', 'repos/%s/actions/runs/%d/cancel' % (args.repo, run['id'])], + check=False, stdout=subprocess.DEVNULL) + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/scripts/plan_verify_groups.py b/scripts/plan_verify_groups.py new file mode 100644 index 0000000000..e1650e9912 --- /dev/null +++ b/scripts/plan_verify_groups.py @@ -0,0 +1,438 @@ +#!/usr/bin/env python3 +"""Select which verification groups a CI run must execute. + +The artifact workflow (.github/workflows/verify.yml) verifies 16 Makefile +groups on three Python versions plus the ranked-pair finite replay and the +formal Lean packages. Running all of that for every pull-request revision is +what saturates the shared runners: most revisions only add a new +``research//`` directory that no group reads. + +This planner keeps every check for anything that can affect it, and skips a +group only when the run's changed paths provably cannot reach it: + +* ``.github/verify-groups.json`` declares each group's inputs as exact paths + or ``dir/**`` prefixes. The declaration is recorded and checked by + ``scripts/trace_verify_inputs.py``; it is not a guess. +* Any changed path in the manifest's ``all`` list (Makefile, ``scripts/**``, + the workflow, the manifest itself, the root Git attribute and ignore + files) runs everything; a nested ``.gitattributes`` or ``.gitignore`` + counts as a change to every path under its directory. +* A changed path that matches no group and is not in ``skip_safe`` is + *unclassified* and also runs everything. Silence must be declared. +* ``schedule`` and ``workflow_dispatch`` runs, a diff that cannot be computed, + and pull requests carrying the ``full_label`` label always run everything. + +Selected groups keep all Python versions. Every job then runs its commands +under scripts/trace_verify_inputs.py, which fails on inputs the manifest does +not declare, so the declarations are re-validated by every run. +""" +import argparse +import json +import os +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[1] +MANIFEST = ROOT / '.github/verify-groups.json' +ZERO_SHA = '0' * 40 +FULL_EVENTS = ('schedule', 'workflow_dispatch') +CLASSES = ('all', 'group', 'skip_safe', 'unclassified') + + +ANY_ANCESTOR = object() + + +def directories_changed_by(path, status, base_dirs=None, head_dirs=None): + """Directories that an added or deleted ``path`` creates or removes: the + ancestors absent from the base tree (addition) or from the head tree + (deletion). ANY_ANCESTOR without tree information; None for edits.""" + if status == 'M': + return None + dirs = base_dirs if status == 'A' else head_dirs + if dirs is None: + return ANY_ANCESTOR + changed, parent = set(), path + while '/' in parent: + parent = parent.rsplit('/', 1)[0] + if parent not in dirs: + changed.add(parent) + return changed + + +def listing_changed_by(path, status, base_dirs=None, head_dirs=None): + """Which directory's listing an added or deleted ``path`` changes. + + Adding ``a/b/c.txt`` changes the listing of the deepest ancestor that + already existed in the base tree (``a`` if ``a/b`` is new, else ``a/b``). + Deleting changes the listing of the deepest ancestor that still exists + afterwards. Without tree information, return ANY_ANCESTOR: every ancestor + listing is then treated as changed (conservative). ``''`` is the root. + """ + if status == 'M': + return None + dirs = base_dirs if status == 'A' else head_dirs + if dirs is None: + return ANY_ANCESTOR + parent = path + while '/' in parent: + parent = parent.rsplit('/', 1)[0] + if parent in dirs: + return parent + return '' + + +def pattern_matches(pattern, path, status='A', listing=ANY_ANCESTOR, created=ANY_ANCESTOR): + """Does a change of ``status`` (A, M or D as in git diff --name-status) to + ``path`` match ``pattern``? + + * exact path: any status; + * ``dir/**`` (``**`` for everything): any status at or below ``dir``; + * ``dir/*`` (``*`` for the repository root): the group only listed the + directory, so the change matters only if it adds or removes an entry + of that directory; ``listing`` names the directory whose listing the + change alters (see listing_changed_by), or ANY_ANCESTOR when unknown; + * ``dir/``: the group only checked that the directory exists, so the + change matters only if it creates or removes that directory; + ``created`` is the set of directories the change creates or removes + (see directories_changed_by), or ANY_ANCESTOR when unknown. + """ + if pattern == '**': + return True + if pattern.endswith('/**'): + prefix = pattern[:-3] + return path == prefix or path.startswith(prefix + '/') + if pattern == '*' or pattern.endswith('/*'): + if status == 'M' or listing is None: + return False + directory = '' if pattern == '*' else pattern[:-2] + if listing is ANY_ANCESTOR or created is ANY_ANCESTOR: + return directory == '' or path.startswith(directory + '/') + # The directory whose listing gains or loses an entry, or a directory + # that the change creates or removes outright (a group that listed it + # will now find it missing, or newly present). + return listing == directory or (created is not None and directory in created) + if pattern.endswith('/'): + if status == 'M' or created is None: + return False + directory = pattern[:-1] + if created is ANY_ANCESTOR: + return path.startswith(directory + '/') + return directory in created + return pattern == path + + +def validate_pattern(pattern): + if not isinstance(pattern, str) or not pattern or pattern.startswith('/') or '\\' in pattern: + raise ValueError('Bad manifest pattern: ' + repr(pattern)) + if pattern in ('*', '**'): + return + body = (pattern[:-3] if pattern.endswith('/**') else pattern[:-2] if pattern.endswith('/*') + else pattern[:-1] if pattern.endswith('/') else pattern) + if '*' in body or not body or '..' in body.split('/') or body.endswith('/'): + raise ValueError('Only exact paths, dir/, dir/* or dir/** are allowed: ' + pattern) + + +def load_manifest(path=MANIFEST): + manifest = json.loads(Path(path).read_text(encoding='utf-8')) + for key in ('python', 'full_label', 'all', 'skip_safe', 'groups'): + if key not in manifest: + raise ValueError('Manifest lacks ' + key) + for pattern in list(manifest['all']) + list(manifest['skip_safe']): + validate_pattern(pattern) + for group, spec in manifest['groups'].items(): + if not isinstance(spec.get('paths'), list): + raise ValueError('Group ' + group + ' needs a paths list') + for pattern in spec['paths']: + validate_pattern(pattern) + job = spec.get('job', 'verify') + if job not in ('verify', 'ranked-pair-finite', 'formal', 'package'): + raise ValueError('Group ' + group + ' has unknown job ' + job) + if job in ('formal', 'package') and not spec.get('package'): + raise ValueError('Group ' + group + ' needs a package name') + if job == 'package' and not spec.get('command'): + raise ValueError('Group ' + group + ' needs a command') + return manifest + + +GIT_CONFIG_NAMES = ('.gitattributes', '.gitignore') + + +def subtree_matches(pattern, directory): + """Could ``pattern`` match some path at or below ``directory``? Used for + a nested .gitattributes or .gitignore, whose effect (checkout bytes, + git's view of untracked files) covers everything under its directory.""" + if pattern == '**' or pattern == '*': + return True + body = pattern[:-3] if pattern.endswith('/**') else pattern[:-2] if pattern.endswith('/*') else ( + pattern[:-1] if pattern.endswith('/') else pattern) + return body == directory or body.startswith(directory + '/') or ( + pattern.endswith('/**') and directory.startswith(body + '/')) + + +def specific(pattern): + """Patterns that say something about a particular path. A whole-tree ``**`` + selects its group but does not establish that an otherwise unknown path + is understood. A listing pattern does: it only ever matches an added or + removed entry, which no group could have read before (probes and + listings are recorded), and a removed entry some group did read is also + covered by that group's exact or ``dir/**`` pattern.""" + return pattern != '**' + + +def classify(manifest, path, status='A', listing=ANY_ANCESTOR, ignored=False, created=ANY_ANCESTOR): + """Return (class, groups) for one changed path with its git status letter. + + ``groups`` are every group whose patterns match (they all run). The + class says whether the path is understood: ``all`` runs everything, + ``group`` means a specific declared input matched, ``skip_safe`` means + the path is declared inert, ``unclassified`` means nobody declared it and + the planner must run everything.""" + name = path.rsplit('/', 1)[-1] + if name == '.gitmodules' or (name in GIT_CONFIG_NAMES and '/' not in path): + return 'all', [] # the root attribute and ignore files change checkout bytes and git views everywhere + if name in GIT_CONFIG_NAMES: + # A nested one affects every path under its directory: treat the + # change as touching all of them, with any status. + directory = path.rsplit('/', 1)[0] + if any(subtree_matches(p, directory) for p in manifest['all']): + return 'all', [] + groups = [g for g, spec in manifest['groups'].items() + if any(subtree_matches(p, directory) for p in spec['paths'])] + explained = any(subtree_matches(p, directory) for g, spec in manifest['groups'].items() + for p in spec['paths'] if specific(p)) + if explained: + return 'group', groups + if any(subtree_matches(p, directory) for p in manifest['skip_safe']): + return 'skip_safe', groups + return 'unclassified', groups + if ignored: + return 'all', [] # a tracked path that .gitignore would ignore is never a declared input + if listing == '' or (listing is ANY_ANCESTOR and '/' not in path): + # A new or removed entry directly at the repository root: make, the + # import system and compilers probe root names, and the tracer does + # not record root-level probes, so this always verifies everything. + return 'all', [] + if any(pattern_matches(p, path, status, listing, created) for p in manifest['all']): + return 'all', [] + groups = [g for g, spec in manifest['groups'].items() + if any(pattern_matches(p, path, status, listing, created) for p in spec['paths'])] + explained = any(pattern_matches(p, path, status, listing, created) for g, spec in manifest['groups'].items() + for p in spec['paths'] if specific(p)) + if explained: + return 'group', groups + if any(pattern_matches(p, path, status, listing, created) for p in manifest['skip_safe']): + return 'skip_safe', groups + return 'unclassified', groups + + +def split_status(item): + """``A:path`` / ``M:path`` / ``D:path``; a bare path is treated as added (the + most conservative status, since it also matches listing patterns).""" + if len(item) > 2 and item[1] == ':' and item[0] in 'AMD': + return item[0], item[2:] + return 'A', item + + +def plan(manifest, event, changed=None, action=None, label=None, labels=(), diff_error=None, + force_full=False, base_dirs=None, head_dirs=None, ignored=()): + """Decide the run. Returns a dict with mode, reason, groups, jobs and the classification. + + ``base_dirs``/``head_dirs`` are the directory sets of the two trees; without + them, listing patterns are matched conservatively at every ancestor.""" + full_label = manifest['full_label'] + classification = [] + mode, reason = None, None + if force_full: + mode, reason = 'full', 'full run requested' + elif event in FULL_EVENTS: + mode, reason = 'full', event + ' runs always verify everything' + elif event == 'pull_request' and action == 'labeled': + if label == full_label: + mode, reason = 'full', 'label ' + full_label + ' requests the full matrix' + else: + mode, reason = 'none', 'label event without ' + full_label + '; the regular run stands' + elif full_label in labels: + mode, reason = 'full', 'pull request carries ' + full_label + elif diff_error: + mode, reason = 'full', 'changed paths unavailable: ' + diff_error + elif event not in ('pull_request', 'push'): + mode, reason = 'full', 'unexpected event ' + str(event) + elif changed is None: + mode, reason = 'full', 'changed paths were not provided' + else: + selected = [] + full_reasons = [] + for item in sorted(set(changed or [])): + status, path = split_status(item) + listing = listing_changed_by(path, status, base_dirs, head_dirs) + created = directories_changed_by(path, status, base_dirs, head_dirs) + kind, groups = classify(manifest, path, status, listing, path in ignored, created) + classification.append((status + ':' + path, kind, groups)) + if kind == 'all': + full_reasons.append(path + ' affects every group') + elif kind == 'unclassified': + full_reasons.append(path + ' is not declared as an input or as inert') + elif kind == 'symlink': + full_reasons.append(path + ' is or was a symbolic link') + for g in groups: + if g not in selected: + selected.append(g) + if full_reasons: + mode, reason = 'full', '; '.join(full_reasons[:5]) + elif selected: + mode, reason = 'selected', 'changed paths reach %d group(s)' % len(selected) + else: + mode, reason = 'none', 'no changed path is an input of any verification group' + order = list(manifest['groups']) + if mode == 'full': + groups = order + elif mode == 'selected': + groups = [g for g in order if g in selected] + else: + groups = [] + specs = manifest['groups'] + job_of = lambda g: specs[g].get('job', 'verify') + matrix_groups = [g for g in groups if job_of(g) == 'verify'] + jobs = sorted({job_of(g) for g in groups} - {'verify'}) + include = [{'python-version': v, 'group': g} for g in matrix_groups for v in manifest['python']] + formal = [{'package': specs[g]['package']} for g in groups if job_of(g) == 'formal'] + packages = [{'python-version': v, 'package': specs[g]['package'], 'command': specs[g]['command'], + 'artifact': specs[g].get('artifact', '')} + for g in groups if job_of(g) == 'package' for v in specs[g].get('python', manifest['python'])] + return { + 'mode': mode, 'reason': reason, 'groups': groups, 'matrix_groups': matrix_groups, + 'jobs': jobs, 'include': include, 'formal': formal, 'packages': packages, + 'classification': classification, + } + + +SYMLINK_MODE = '120000' +GITLINK_MODE = '160000' + + +def git_changed(base, head='HEAD', cwd=ROOT): + """``STATUS:path`` for every path changed between two commits, plus the + set of paths that are or were symbolic links or submodule pointers. + Renames and copies are reported as a delete plus an add; type changes + count as both.""" + if base == ZERO_SHA: + raise ValueError('base is the all-zero SHA (new branch or force push)') + out = subprocess.run(['git', 'diff', '--no-renames', '--raw', '-z', base, head], cwd=cwd, + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if out.returncode != 0: + raise ValueError(out.stderr.decode(errors='replace').strip() or 'git diff failed') + fields = out.stdout.decode().split('\0') + changed, links = [], set() + i = 0 + while i + 1 < len(fields) and fields[i]: + meta, path = fields[i], fields[i + 1] + i += 2 + parts = meta.lstrip(':').split() # src_mode dst_mode src_sha dst_sha status + if len(parts) < 5: + raise ValueError('unexpected git diff --raw record: ' + meta) + status = parts[4][0] + if SYMLINK_MODE in (parts[0], parts[1]) or GITLINK_MODE in (parts[0], parts[1]): + links.add(path) # symbolic links and submodule pointers always verify everything + if status in ('A', 'M', 'D'): + changed.append(status + ':' + path) + else: # T (type change), U, X or anything unexpected: treat as add + delete + changed += ['A:' + path, 'D:' + path] + return changed, links + + +def git_ignored(paths, cwd=ROOT): + """Paths among ``paths`` that .gitignore rules would ignore.""" + if not paths: + return set() + out = subprocess.run(['git', 'check-ignore', '-z', '--stdin', '--no-index'], cwd=cwd, + input='\0'.join(paths).encode(), stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if out.returncode not in (0, 1): + raise ValueError(out.stderr.decode(errors='replace').strip() or 'git check-ignore failed') + return set(p for p in out.stdout.decode().split('\0') if p) + + +def git_dirs(rev, cwd=ROOT): + """Every directory of a tree, as paths relative to the root.""" + out = subprocess.run(['git', 'ls-tree', '-r', '-d', '--name-only', '-z', rev], cwd=cwd, + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if out.returncode != 0: + raise ValueError(out.stderr.decode(errors='replace').strip() or 'git ls-tree failed') + return set(p for p in out.stdout.decode().split('\0') if p) + + +def summary_markdown(result, event): + lines = ['## Verification plan', '', + '- Event: `%s`' % event, '- Mode: **%s**' % result['mode'], '- Reason: %s' % result['reason']] + if result['groups']: + lines.append('- Groups: ' + ', '.join('`%s`' % g for g in result['groups'])) + if result['jobs']: + lines.append('- Extra jobs: ' + ', '.join('`%s`' % j for j in result['jobs'])) + lines.append('- Matrix jobs: %d verify, %d formal, %d package' % ( + len(result['include']), len(result['formal']), len(result['packages']))) + if result['classification']: + lines += ['', '| Changed path | Class | Groups |', '|---|---|---|'] + for path, kind, groups in result['classification'][:300]: + lines.append('| `%s` | %s | %s |' % (path, kind, ', '.join(groups))) + if len(result['classification']) > 300: + lines.append('| … %d more | | |' % (len(result['classification']) - 300)) + return '\n'.join(lines) + '\n' + + +def write_outputs(result, path): + with open(path, 'a', encoding='utf-8') as out: + out.write('matrix=' + json.dumps({'include': result['include']}, separators=(',', ':')) + '\n') + out.write('count=%d\n' % len(result['include'])) + out.write('formal=' + json.dumps({'include': result['formal']}, separators=(',', ':')) + '\n') + out.write('formal_count=%d\n' % len(result['formal'])) + out.write('packages=' + json.dumps({'include': result['packages']}, separators=(',', ':')) + '\n') + out.write('package_count=%d\n' % len(result['packages'])) + out.write('groups=' + ','.join(result['groups']) + '\n') + out.write('jobs=' + ','.join(result['jobs']) + '\n') + out.write('mode=' + result['mode'] + '\n') + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--manifest', type=Path, default=MANIFEST) + ap.add_argument('--event', required=True, help='GitHub event name') + ap.add_argument('--action', default=None, help='GitHub event action, e.g. labeled') + ap.add_argument('--label', default=None, help='label name for labeled events') + ap.add_argument('--labels', default='[]', help='JSON list of the pull request labels') + ap.add_argument('--diff', nargs=2, metavar=('BASE', 'HEAD'), help='compute changed paths with git') + ap.add_argument('--changed', nargs='*', help='changed paths (instead of --diff)') + ap.add_argument('--full', action='store_true', help='force the full matrix') + ap.add_argument('--github-output', type=Path) + ap.add_argument('--summary', type=Path, help='append a Markdown summary (e.g. $GITHUB_STEP_SUMMARY)') + args = ap.parse_args(argv) + + manifest = load_manifest(args.manifest) + changed, diff_error, base_dirs, head_dirs, ignored = args.changed, None, None, None, set() + if args.diff: + try: + changed, links = git_changed(args.diff[0], args.diff[1]) + if links: + diff_error = 'symbolic links or submodules changed: ' + ', '.join(sorted(links)[:5]) + base_dirs, head_dirs = git_dirs(args.diff[0]), git_dirs(args.diff[1]) + ignored = git_ignored([split_status(c)[1] for c in changed]) + except ValueError as error: + changed, diff_error = None, str(error) + labels = json.loads(args.labels) if args.labels else None + result = plan(manifest, args.event, changed, action=args.action or None, label=args.label or None, + labels=labels if isinstance(labels, list) else [], diff_error=diff_error, + force_full=args.full, base_dirs=base_dirs, head_dirs=head_dirs, ignored=ignored) + print('PLAN mode=%s groups=%d verify_jobs=%d formal_jobs=%d package_jobs=%d extra=%s reason=%s' % ( + result['mode'], len(result['groups']), len(result['include']), len(result['formal']), + len(result['packages']), ','.join(result['jobs']) or '-', result['reason'])) + for path, kind, groups in result['classification']: + print(' %-12s %s%s' % (kind, path, (' -> ' + ','.join(groups)) if groups else '')) + if args.github_output: + write_outputs(result, args.github_output) + if args.summary: + with open(args.summary, 'a', encoding='utf-8') as out: + out.write(summary_markdown(result, args.event)) + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/scripts/trace_verify_inputs.py b/scripts/trace_verify_inputs.py new file mode 100644 index 0000000000..6581a05b47 --- /dev/null +++ b/scripts/trace_verify_inputs.py @@ -0,0 +1,735 @@ +#!/usr/bin/env python3 +"""Record which repository paths a verification group reads, and check the +declared CI input manifest against that record. + +The CI planner (scripts/plan_verify_groups.py) skips a verification group on +a pull request only when none of the pull request's changed paths match the +group's declared inputs in .github/verify-groups.json. That is sound only if +the declaration is complete. This tool makes the declaration checkable: + +* ``--group G`` runs the same command CI runs for group ``G`` under + ``strace`` and records every tracked file, listed directory, existence + probe and whole-tree Git query inside the repository. The verification + outcome is propagated unchanged; tracing adds no claim and removes no check. +* ``--check MANIFEST`` additionally fails when a recorded input is not + covered by the group's declared patterns (or the ``all`` patterns). +* ``--suggest`` prints a minimal pattern set covering a recording. + +Pattern syntax is deliberately small (shared with scripts/plan_verify_groups.py): + +* an exact repository path: any change to that file matters; +* ``dir/**`` (``**`` for the whole tree): any change at or below ``dir``; +* ``dir/*`` (``*`` for the repository root): the group listed that + directory, so an entry added to or removed from it matters, while editing + an existing entry does not (a read of that entry is recorded separately). + +Coverage rules: a recorded file read needs an exact or ``**`` pattern; a +listed directory needs ``dir/*``, ``dir/**`` or an ancestor ``**``; an +existence check of a directory needs ``dir/``, ``dir/*``, ``dir/**`` or an +ancestor ``**``; a probe of a path that does not exist needs an exact +pattern, a ``**`` pattern or a listing pattern on its deepest existing +ancestor; a whole-tree Git query (``git ls-files``, ``git status``, +``git diff``, ...) needs ``**``. + +What is deliberately not recorded, and why it is still safe: + +* paths outside the repository and ``.git`` internals (``git show REV:path`` + and friends are interpreted from the git command line instead); +* untracked files that ``.gitignore`` ignores (``build/`` outputs, caches): + a pull request that tracks such a path is an addition the planner cannot + classify, so it verifies everything; +* probes of names directly at the repository root (GNU make's version-control + and makefile probes, compiler search paths): an undeclared new root entry + likewise makes the planner verify everything. + +Paths are kept lexical (not symlink-resolved) so that a dependency on a +tracked symlink is recorded on the link; the link's target inside the +repository is recorded as well. + +Assumption: a ``stat`` of a directory is an existence check. Directory +metadata (mtime, link count) is not a reproducible input of a fresh CI +checkout, so no verifier here may depend on it; ``git diff --exit-code`` +after every group would expose a verifier that did. +""" +import argparse +import json +import os +from pathlib import Path +import re +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[1] +MANIFEST = ROOT / '.github/verify-groups.json' +TRACE_SYSCALLS = '%file,chdir,fchdir,%process' +MAKE_PROBES = {'RCS', 'SCCS', 'GNUmakefile', 'makefile'} + +# The commands CI runs per matrix group (see .github/workflows/verify.yml). +GROUP_COMMANDS = { + 'clones': ['make skip-clones-verify split-skip-producer', + 'python3 -B scripts/replay_historical_check.py split-skip'], + 'ranked-pair-finite': ['make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream'], +} + + +def group_commands(group): + return GROUP_COMMANDS.get(group, ['make verify-' + group]) + + +# ---------------------------------------------------------------- strace parsing + +_LINE = re.compile(r'^(?P\d+)\s+(?P.*)$') +_CALL = re.compile(r'^(?P\w+)\((?P.*)$') +_RESUMED = re.compile(r'^<\.\.\. (?P\w+) resumed>(?P.*)$') +_RESULT = re.compile(r'=\s+(?P-?\d+|\?)(?:\s|$)') +_FD = re.compile(r'^(?:AT_FDCWD|\d+)<(?P[^>]*)>$') +_SHA = re.compile(r'^[0-9a-f]{40}$') +THIS_CHECKOUT = '' +FORK_CALLS = {'clone', 'clone3', 'fork', 'vfork'} +# Calls whose second (and third) quoted operand is also a path. +TWO_PATH = {'rename': (0, 1), 'link': (0, 1), 'symlink': (1,), 'renameat': (0, 1), 'renameat2': (0, 1), + 'linkat': (0, 1), 'symlinkat': (1,)} +SKIP_CALLS = FORK_CALLS | {'wait4', 'waitid', 'kill', 'exit', 'exit_group', 'execveat', 'getcwd', + 'arch_prctl', 'tgkill', 'tkill', 'rt_sigreturn', 'prlimit64', 'set_tid_address'} + + +_ESCAPES = {'n': b'\n', 't': b'\t', 'r': b'\r', 'a': b'\a', 'b': b'\b', 'f': b'\f', 'v': b'\v', + '\\': b'\\', '"': b'"', "'": b"'", '?': b'?'} + + +def _unescape(text): + """Decode strace's C-style string escapes (\\ooo octal, \\xhh, \\n ...) into + bytes and then with the filesystem encoding, so UTF-8 names survive.""" + out, i = bytearray(), 0 + while i < len(text): + c = text[i] + if c != '\\' or i + 1 >= len(text): + out += c.encode('utf-8', 'surrogateescape'); i += 1 + continue + n = text[i + 1] + if n in '01234567': + j = i + 1 + while j < len(text) and j < i + 4 and text[j] in '01234567': + j += 1 + out.append(int(text[i + 1:j], 8) & 0xFF); i = j + elif n == 'x': + j = i + 2 + while j < len(text) and j < i + 4 and text[j] in '0123456789abcdefABCDEF': + j += 1 + out.append(int(text[i + 2:j], 16) if j > i + 2 else 0); i = j + else: + out += _ESCAPES.get(n, n.encode('utf-8', 'surrogateescape')); i += 2 + return os.fsdecode(bytes(out)) + + +def tokens(args): + """Split strace argument text into top-level comma-separated tokens.""" + out, depth, cur, i, quote = [], 0, [], 0, False + while i < len(args): + c = args[i] + if quote: + cur.append(c) + if c == '\\': + cur.append(args[i + 1]); i += 1 + elif c == '"': + quote = False + elif c == '"': + quote = True; cur.append(c) + elif c in '([{': + depth += 1; cur.append(c) + elif c in ')]}': + if depth == 0: + break # end of the call's argument list + depth -= 1; cur.append(c) + elif c == ',' and depth == 0: + out.append(''.join(cur).strip()); cur = [] + elif c == '<' and depth == 0 and args.startswith('= 2: + return _unescape(token[1:-1]) + if token.startswith('"') and token.endswith('...'): # truncated string + return None + return None + + +def argv_strings(token): + """Strings of an argv array token such as ``["git", "show", "HEAD:x"]``.""" + if not token.startswith('['): + return [] + return [s for s in (string_value(t) for t in tokens(token[1:])) if s is not None] + + +def git_semantics(argv): + """Inputs implied by a git command line: (paths, tree, directory) where + paths is a list of repository-relative (path, kind), tree means the whole + tree of the repository that ``directory`` belongs to (None: the process + cwd), and ``directory`` is the ``-C`` operand if any.""" + args = argv[1:] + i, directory = 0, None + while i < len(args) and args[i].startswith('-'): + if args[i] == '-C' and i + 1 < len(args): + directory = args[i + 1] if directory is None else os.path.join(directory, args[i + 1]) + i += 2 + continue + if args[i] in ('--git-dir', '--work-tree') or args[i].startswith(('--git-dir=', '--work-tree=')): + # Explicit repository selection bypasses discovery: assume this + # checkout's whole tree rather than guessing which one it targets. + return [], True, THIS_CHECKOUT + if args[i] in ('-c',): + i += 1 + i += 1 + if i >= len(args): + return [], False, directory + sub, rest = args[i], args[i + 1:] + inert = {'config', 'version', '--version', 'hash-object', 'check-ignore', 'merge-base', + 'fetch', 'init', 'remote', 'describe', 'var', 'help', 'symbolic-ref'} + if sub == 'rev-parse': + paths = [] + for arg in rest: + if ':' in arg and not arg.startswith('-'): + rev, _, path = arg.partition(':') + if _SHA.match(rev): + continue + if not path: + return [], True, directory + paths.append((path, 'git')) # the object id of a live path changes with it + return paths, False, directory + if sub in ('show', 'cat-file'): + if any(a.startswith('--batch') for a in rest): + return [], True, directory # requests arrive on stdin, which the trace does not see + operands = [a for a in rest if not a.startswith('-')] + if not operands: + return [], True, directory # `git show` alone prints the whole HEAD commit + paths = [] + for arg in operands: + if ':' in arg: + rev, _, path = arg.partition(':') + if _SHA.match(rev): + continue # an immutable object cannot change with the tree + if path: + paths.append((path, 'git')) # repository-relative, see parse_strace + else: + return [], True, directory + elif _SHA.match(arg): + continue + else: + return [], True, directory # a ref alone: a commit, tree or blob of the live history + return paths, False, directory + if sub == 'apply': + if any(a in ('--cached', '--index') or a.startswith('--index') for a in rest): + return [], True, directory # the index and object database are not traced + return [], False, directory # the patch and the target files are read from the tree: traced + if sub in inert: + return [], False, directory + if sub in ('restore', 'checkout'): + paths = [(a, 'file') for a in rest if not a.startswith('-')] + return (paths, False, directory) if paths else ([], True, directory) + return [], True, directory + + +def parse_strace(log_lines, start_cwd): + """Yield (path, kind, syscall) with kind in {'file', 'dir', 'tree', 'gitpath'}. + ``log_lines`` is a callable returning a fresh iterable of lines (the log + is read twice: once for the process tree, once for the paths), or a + string.""" + if isinstance(log_lines, str): + text = log_lines + log_lines = lambda: text.splitlines() + parent = {} + for line in log_lines(): + m = _LINE.match(line) + if not m: + continue + rest = m.group('rest') + call = _CALL.match(rest) or _RESUMED.match(rest) + if call and call.group('name') in FORK_CALLS: + ret = _RESULT.search(rest) + if ret and ret.group('ret').isdigit(): + parent[ret.group('ret')] = m.group('pid') + cwd, pending_chdir, fd_pending = {}, {}, {} + + def current(pid): + if pid not in cwd: + cwd[pid] = current(parent[pid]) if pid in parent else start_cwd + return cwd[pid] + + def resolve(pid, path, base=None): + if os.path.isabs(path): + return os.path.normpath(path) + return os.path.normpath(os.path.join(base if base else current(pid), path)) + + for line in log_lines(): + m = _LINE.match(line) + if not m: + continue + pid, rest = m.group('pid'), m.group('rest') + call = _CALL.match(rest) + resumed = _RESUMED.match(rest) if not call else None + if resumed: + name = resumed.group('name') + ret = _RESULT.search(rest) + if name in FORK_CALLS and ret and ret.group('ret').isdigit(): + cwd.setdefault(ret.group('ret'), current(pid)) + elif name in ('chdir', 'fchdir') and ret and ret.group('ret') == '0' and pid in pending_chdir: + cwd[pid] = pending_chdir.pop(pid) + continue + if not call: + continue + name, args = call.group('name'), call.group('args') + unfinished = args.rstrip().endswith('') + ret = None if unfinished else _RESULT.search(rest) + toks = tokens(args) + if name in FORK_CALLS: + if ret and ret.group('ret').isdigit(): + cwd.setdefault(ret.group('ret'), current(pid)) + continue + if name in ('chdir', 'fchdir'): + target = None + if toks: + if name == 'chdir': + s = string_value(toks[0]) + target = resolve(pid, s) if s is not None else None + else: + fd = _FD.match(toks[0]) + target = fd.group('path') if fd else None + if target is None: + continue + if unfinished: + pending_chdir[pid] = target + elif ret and ret.group('ret') == '0': + cwd[pid] = target + continue + if name in SKIP_CALLS: + continue + if name == 'execve': + if toks: + prog = string_value(toks[0]) + if prog is not None: + yield resolve(pid, prog), 'file', name + argv = argv_strings(toks[1]) if len(toks) > 1 else [] + if argv and os.path.basename(argv[0]) == 'git': + paths, tree, directory = git_semantics(argv) + # The repository git operates on is the one containing the + # process cwd, or the -C operand; classify() checks whether + # that is this repository or a nested checkout. + where = (start_cwd if directory == THIS_CHECKOUT else + resolve(pid, directory) if directory else current(pid)) + if tree: + yield where, 'tree', name + for path, kind in paths: + if kind == 'git': # REV:path is repository-relative unless ./ or ../ + yield where + '\0' + path, 'gitpath', name + else: + yield resolve(pid, path), kind, name + continue + # Generic file syscall: quoted operands are paths, each relative to the + # preceding dirfd operand (``AT_FDCWD`` or ``N``) if any. + operands, base = [], None + for tok in toks: + fd = _FD.match(tok) + if fd: + base = fd.group('path'); continue + s = string_value(tok) + if s is not None: + operands.append((s, base)); base = None + if not operands: + continue + wanted = TWO_PATH.get(name, (0,)) + kind = 'dir' if 'O_DIRECTORY' in args else 'file' + for index in wanted: + if index < len(operands): + path, b = operands[index] + yield resolve(pid, path, b), kind, name + + +# ---------------------------------------------------------------- classification + +def git_lines(*args, cwd=ROOT): + return subprocess.run(['git', *args], cwd=cwd, check=True, stdout=subprocess.PIPE + ).stdout.decode().split('\0' if '-z' in args else '\n') + + +def tracked_files(root=ROOT): + return set(p for p in git_lines('ls-files', '-z', cwd=Path(root)) if p) + + +def tracked_dirs(tracked): + """Every directory that contains a tracked file, at any depth.""" + dirs = set() + for path in tracked: + parent = path + while '/' in parent: + parent = parent.rsplit('/', 1)[0] + if parent in dirs: + break + dirs.add(parent) + return dirs + + +def nearest_tracked(directory, dirs): + """The directory itself if git knows it, else its deepest ancestor that + git knows ('' for the root). The planner attributes additions to tracked + directories only, so declarations must not name runtime-only ones.""" + while directory and directory not in dirs: + directory = directory.rsplit('/', 1)[0] if '/' in directory else '' + return directory + + +def classify(paths, root=ROOT): + """Split (lexical absolute path, kind) records into tracked files, listed + directories, existence checks, probes, git tree objects and a + whole-tree flag.""" + root = Path(root).resolve() + tracked = tracked_files(root) + known_dirs = tracked_dirs(tracked) + inside, tree, subtrees = {}, False, set() + + def this_repository(directory): + """Is ``directory`` inside this checkout and not a nested repository?""" + d = Path(os.path.normpath(directory)) + try: + d.relative_to(root) + except ValueError: + return False + probe = d + while True: + if (probe / '.git').exists(): + return probe == root + if probe == root or probe.parent == probe: + return probe == root + probe = probe.parent + + for path, kind in paths: + if kind == 'tree': + if this_repository(path): + tree = True + continue + if kind == 'gitpath': + where, _, rel_path = path.partition('\0') + if not this_repository(where): + continue + if rel_path.startswith(('./', '../')): + path = os.path.normpath(os.path.join(where, rel_path)) + else: + path = os.path.normpath(os.path.join(str(root), rel_path)) + try: + rel = Path(path).relative_to(root).as_posix() + except ValueError: + continue + if rel in known_dirs or rel == '.': + subtrees.add('' if rel == '.' else rel) # a tree object: names and hashes of everything below + continue + kind = 'file' + try: + rel = Path(os.path.normpath(path)).relative_to(root).as_posix() + except ValueError: + continue + if rel == '.': + rel = '' + parts = rel.split('/') if rel else [] + if parts and parts[0] == '.git': + continue + inside.setdefault(rel, set()).add(kind) + # Every symbolic link on the lexical path is an input (a link is a + # tracked entry), and so is the resolved target when it is inside. + prefix = root + for part in parts: + prefix = prefix / part + if os.path.islink(prefix): + link_rel = prefix.relative_to(root).as_posix() + inside.setdefault(link_rel, set()).add('file') + try: + target = Path(os.path.realpath(prefix)).relative_to(root).as_posix() + inside.setdefault(target, set()).add('file' if target != rel else kind) + except ValueError: + pass + if rel: + real = os.path.realpath(root / rel) + if real != os.path.normpath(str(root / rel)): + try: + target = Path(real).relative_to(root).as_posix() + inside.setdefault(target, set()).add(kind) + except ValueError: + pass + candidates = [rel for rel in inside if rel and rel not in tracked] + ignored = set() + if candidates: + out = subprocess.run(['git', 'check-ignore', '-z', '--stdin', '--no-index'], cwd=root, + input='\0'.join(candidates).encode(), stdout=subprocess.PIPE) + ignored = set(p for p in out.stdout.decode().split('\0') if p) + files, dirs, exists, probes = set(), set(), set(), set() + for rel, kinds in inside.items(): + full = root / rel if rel else root + if rel in tracked: + files.add(rel) + elif rel in ignored: + continue # build outputs and caches: tracking one is an undeclared addition, which runs everything + elif os.path.isdir(full) and not os.path.islink(full): + # A directory git does not know (created at run time) is declared + # at its nearest tracked ancestor, which is where the planner + # attributes additions below it. + anchored = nearest_tracked(rel, known_dirs) + if 'dir' in kinds: + dirs.add(anchored) # opened as a directory: its entries were listed + else: + exists.add(anchored) # only stat/readlink/access: its existence was checked + elif not rel or rel in MAKE_PROBES or '/' not in rel: + continue # root-level probe: an undeclared new root entry runs everything + else: + probes.add(rel) # missing path, or an untracked unignored file a PR could track + return sorted(files), sorted(dirs), sorted(probes), tree, sorted(exists), sorted(subtrees) + + +# ---------------------------------------------------------------- running + +def seccomp_supported(): + """strace >= 5.3 can filter unselected syscalls in the kernel, which cuts + the tracing overhead without changing what is recorded.""" + try: + probe = subprocess.run(['strace', '--seccomp-bpf', '-f', '-e', 'trace=%file', '-o', os.devnull, '--', 'true'], + stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL) + return probe.returncode == 0 + except OSError: + return False + + +def run_traced(commands, cwd=ROOT, env=None): + """Run shell commands under strace; return (exit_code, log path).""" + log = Path(cwd) / 'build' / 'verify-trace' / 'strace.log' + log.parent.mkdir(parents=True, exist_ok=True) + if log.exists(): + log.unlink() + # Each command runs in its own subshell from the repository root, so a + # `cd` in one command cannot change where the next one resolves paths. + script = ' && '.join('( ' + c + ' )' for c in commands) + cmd = ['strace', '-f', '-qq', '-s', '65536', '-e', 'signal=none', '-e', 'trace=' + TRACE_SYSCALLS, + '-o', str(log), '-y'] + (['--seccomp-bpf'] if seccomp_supported() else []) + ['--', 'sh', '-c', script] + print('TRACE ' + script, flush=True) + code = subprocess.run(cmd, cwd=cwd, env=env).returncode + return code, log + + +RECORDING_VERSION = 5 + + +def record(group, commands, cwd=ROOT): + code, log = run_traced(commands, cwd) + + def lines(): + if not log.exists(): + return iter(()) + return (line.rstrip('\n') for line in open(log, encoding='utf-8', errors='replace')) + # Deduplicate while streaming: the log of a large group exceeds 100 MB. + paths = set((p, k) for p, k, _ in parse_strace(lines, str(Path(cwd).resolve()))) + files, dirs, probes, tree, exists, subtrees = classify(paths, cwd) + return code, {'group': group, 'commands': commands, 'files': files, 'dirs': dirs, 'exists': exists, + 'probes': probes, 'subtrees': subtrees, 'tree': tree, 'exit_code': code, + 'recording_version': RECORDING_VERSION, 'python': sys.version.split()[0]} + + +# ---------------------------------------------------------------- coverage + +def pattern_matches(pattern, path): + """Does an edit of the existing file ``path`` match ``pattern``?""" + if pattern == '**': + return True + if pattern.endswith('/**'): + prefix = pattern[:-3] + return path == prefix or path.startswith(prefix + '/') + if pattern == '*' or pattern.endswith('/*') or pattern.endswith('/'): + return False # listing and existence patterns only cover added or removed entries + return pattern == path + + +def dir_covered(pattern, directory): + """A listed directory needs dir/*, dir/** or an ancestor ** pattern.""" + if pattern == '**': + return True + if pattern == '*': + return directory == '' + if pattern.endswith('/**'): + prefix = pattern[:-3] + return directory == prefix or directory.startswith(prefix + '/') + if pattern.endswith('/*'): + return directory == pattern[:-2] + return False + + +def exists_covered(pattern, directory): + """An existence check of a directory needs dir/, or anything that covers + its listing.""" + if pattern.endswith('/') and not pattern.endswith('/**'): + return directory == pattern[:-1] + return dir_covered(pattern, directory) + + +_TRACKED_DIRS = {} + + +def anchor(path, root=ROOT): + """The deepest ancestor directory of a probed path that git knows (it + contains a tracked file): adding the path, with any missing intermediate + directories, changes that listing in the tree the planner inspects.""" + key = str(root) + if key not in _TRACKED_DIRS: + _TRACKED_DIRS[key] = tracked_dirs(tracked_files(root)) + return nearest_tracked(path.rsplit('/', 1)[0] if '/' in path else '', _TRACKED_DIRS[key]) + + +def probe_covered(pattern, path, root=ROOT): + """A probed (absent or untracked) path can only be added: exact, ** or a + listing pattern on its anchor directory all cover that.""" + return pattern_matches(pattern, path) or dir_covered(pattern, anchor(path, root)) + + +def uncovered(recording, patterns, root=ROOT): + missing = [] + if recording.get('tree') and '**' not in patterns: + missing.append('**') + for path in recording['files']: + if not any(pattern_matches(p, path) for p in patterns): + missing.append(path) + for path in recording.get('probes', []): + if not any(probe_covered(p, path, root) for p in patterns): + missing.append(path) + for directory in recording['dirs']: + if not any(dir_covered(p, directory) for p in patterns): + missing.append((directory + '/*') if directory else '*') + for directory in recording.get('exists', []): + if directory and not any(exists_covered(p, directory) for p in patterns): + missing.append(directory + '/') + for directory in recording.get('subtrees', []): + if not any(p == '**' or (p.endswith('/**') and dir_covered(p, directory)) for p in patterns): + missing.append((directory + '/**') if directory else '**') + return missing + + +DENSE = 4 +WALK_FRACTION = 0.5 + + +def suggest(recording, covered_by=(), root=ROOT): + """Covering patterns: ** for whole-tree queries; dir/** where most of a + directory's tracked files are read or most of its subdirectories are + listed (a walk); dir/* for other listings and for probes, at the probe's + anchor; dir/ for existence checks; exact paths otherwise. Patterns + already implied by ``covered_by`` (the manifest's ``all`` list) are + omitted.""" + covered_by = list(covered_by) + if recording.get('tree'): + return [] if '**' in covered_by else ['**'] + files = sorted(set(recording['files'])) + by_dir = {} + for path in files: + by_dir.setdefault(path.rsplit('/', 1)[0] if '/' in path else '', []).append(path) + key = str(root) + if key not in _TRACKED_DIRS: + _TRACKED_DIRS[key] = tracked_dirs(tracked_files(root)) + tracked_by_dir = {} + for path in tracked_files(root): + tracked_by_dir.setdefault(path.rsplit('/', 1)[0] if '/' in path else '', 0) + tracked_by_dir[path.rsplit('/', 1)[0] if '/' in path else ''] += 1 + chosen = [] + # A directory most of whose tracked files were read is declared whole; + # a few files out of many stay exact, so unrelated additions to a shared + # directory (a note, a certificate) do not select the group. + for d in sorted(d for d, items in by_dir.items() + if d and len(items) >= DENSE and len(items) > WALK_FRACTION * tracked_by_dir.get(d, len(items))): + if not any(dir_covered(c, d) and c.endswith('**') for c in chosen + covered_by): + chosen.append(d + '/**') + # A directory most of whose subdirectories are listed was walked: any + # change below it may add or remove listed entries, so declare it whole. + listed_children = {} + for d in recording['dirs']: + if d: + listed_children.setdefault(d.rsplit('/', 1)[0] if '/' in d else '', []).append(d) + for parent, items in sorted(listed_children.items()): + if not parent or len(items) < DENSE: + continue + try: + total = sum(1 for e in os.scandir(Path(root) / parent) if e.is_dir(follow_symlinks=False)) + except OSError: + total = len(items) + if len(items) > WALK_FRACTION * total and not any( + dir_covered(c, parent) and c.endswith('**') for c in chosen + covered_by): + chosen.append(parent + '/**') + chosen = [c for c in chosen if not any(o != c and o.endswith('/**') and dir_covered(o, c[:-3]) for o in chosen)] + for d in sorted(recording['dirs']): + if not any(dir_covered(c, d) for c in chosen + covered_by): + chosen.append((d + '/*') if d else '*') + for directory in sorted(recording.get('subtrees', [])): + pattern = (directory + '/**') if directory else '**' + if not any(c == '**' or (c.endswith('/**') and dir_covered(c, directory)) for c in chosen + covered_by): + chosen.append(pattern) + for directory in sorted(recording.get('exists', [])): + if directory and not any(exists_covered(c, directory) for c in chosen + covered_by): + chosen.append(directory + '/') + for path in files: + if not any(pattern_matches(c, path) for c in chosen + covered_by): + chosen.append(path) + for path in sorted(set(recording.get('probes', []))): + if not any(probe_covered(c, path, root) for c in chosen + covered_by): + a = anchor(path, root) + chosen.append((a + '/*') if a else '*') + return sorted(set(chosen)) + + +def load_manifest(path): + return json.loads(Path(path).read_text(encoding='utf-8')) + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--group', required=True, help='verification group, e.g. community or ranked-pair-finite') + ap.add_argument('--output', type=Path, help='write the recording as JSON') + ap.add_argument('--check', type=Path, nargs='?', const=MANIFEST, + help='fail unless the manifest covers every recorded input (default manifest: %(default)s)') + ap.add_argument('--suggest', action='store_true', help='print the minimal covering patterns') + ap.add_argument('--command', action='append', + help='trace this shell command instead of the group default (repeatable, run in order)') + ap.add_argument('--from-recording', type=Path, help='reuse a recording instead of running the group') + args = ap.parse_args(argv) + + if args.from_recording: + code, recording = 0, json.loads(args.from_recording.read_text(encoding='utf-8')) + else: + code, recording = record(args.group, args.command or group_commands(args.group)) + if args.output: + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(json.dumps(recording, indent=1, sort_keys=True) + '\n', encoding='utf-8') + print('RECORDED group=%s files=%d dirs=%d exists=%d probes=%d subtrees=%d tree=%s' % ( + recording['group'], len(recording['files']), len(recording['dirs']), len(recording.get('exists', [])), + len(recording.get('probes', [])), len(recording.get('subtrees', [])), recording.get('tree', False))) + if code != 0: + print('VERIFICATION_FAILED exit=%d' % code) + return code + status = 0 + if args.check: + manifest = load_manifest(args.check) + patterns = list(manifest['all']) + list(manifest['groups'][args.group]['paths']) + missing = uncovered(recording, patterns, ROOT) + if missing: + print('UNDECLARED_INPUTS group=%s (add to %s):' % (args.group, args.check)) + for item in missing: + print(' ' + item) + status = 2 + else: + print('PASS_DECLARED_INPUTS_COVER_RECORDING group=' + args.group) + if args.suggest: + covered = load_manifest(args.check)['all'] if args.check else () + print(json.dumps(suggest(recording, covered, ROOT), indent=1)) + return status + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/tests/test_plan_verify_groups.py b/tests/test_plan_verify_groups.py new file mode 100644 index 0000000000..e220d72f45 --- /dev/null +++ b/tests/test_plan_verify_groups.py @@ -0,0 +1,370 @@ +"""The CI planner must skip a verification group only when no changed path can reach it.""" +import importlib.util +import json +import os +from pathlib import Path +import re +import subprocess +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +spec = importlib.util.spec_from_file_location('plan_verify_groups', ROOT / 'scripts/plan_verify_groups.py') +planner = importlib.util.module_from_spec(spec) +spec.loader.exec_module(planner) + +MANIFEST = { + 'python': ['3.11', '3.13'], + 'full_label': 'ci:full-verify', + 'all': ['Makefile', 'scripts/**', '.github/workflows/verify.yml', '.github/verify-groups.json'], + 'skip_safe': ['research/**', 'docs/**', 'README.md', '.github/workflows/**'], + 'groups': { + 'alpha': {'paths': ['certificates/alpha.json', 'certificates/*', 'notes/**']}, + 'beta': {'paths': ['research/beta-package/**']}, + 'formal-historical': {'job': 'formal', 'package': 'historical', 'paths': ['formal/**']}, + 'formal-matrix': {'job': 'formal', 'package': 'matrix', 'paths': ['research/matrix-exponent-synthesis/**']}, + 'pkg-bit-elim-144': {'job': 'package', 'package': 'bit-elim-144', 'python': ['3.11', '3.14'], + 'command': 'python3 research/bit-elim-144/verify.py', + 'paths': ['research/bit-elim-144/**', 'certificates/paired-cube-bit-input.json']}, + 'whole': {'paths': ['**']}, + }, +} +ALL_GROUPS = ['alpha', 'beta', 'formal-historical', 'formal-matrix', 'pkg-bit-elim-144', 'whole'] + + +def run_plan(changed, event='pull_request', **kw): + return planner.plan(MANIFEST, event, changed, **kw) + + +class PatternSemantics(unittest.TestCase): + def test_exact_and_recursive_match_any_status(self): + for status in 'AMD': + self.assertTrue(planner.pattern_matches('certificates/alpha.json', 'certificates/alpha.json', status)) + self.assertTrue(planner.pattern_matches('notes/**', 'notes/deep/x.tex', status)) + self.assertTrue(planner.pattern_matches('notes/**', 'notes', status)) + self.assertTrue(planner.pattern_matches('**', 'anything/at/all', status)) + self.assertFalse(planner.pattern_matches('notes/**', 'notes-extra/x', 'A')) + self.assertFalse(planner.pattern_matches('certificates/alpha.json', 'certificates/alpha.json.bak', 'A')) + + def test_listing_patterns_without_tree_information_are_conservative(self): + self.assertTrue(planner.pattern_matches('certificates/*', 'certificates/new.json', 'A')) + self.assertTrue(planner.pattern_matches('certificates/*', 'certificates/old.json', 'D')) + self.assertFalse(planner.pattern_matches('certificates/*', 'certificates/old.json', 'M')) + self.assertTrue(planner.pattern_matches('certificates/*', 'certificates/sub/new.json', 'A')) # any ancestor + self.assertTrue(planner.pattern_matches('*', 'NEWFILE', 'A')) + self.assertTrue(planner.pattern_matches('*', 'dir/file', 'A')) + self.assertFalse(planner.pattern_matches('*', 'README.md', 'M')) + + def test_listing_changed_by_uses_the_deepest_existing_ancestor(self): + base = {'research', 'research/old', 'certificates'} + self.assertEqual(planner.listing_changed_by('research/new/README.md', 'A', base, base), 'research') + self.assertEqual(planner.listing_changed_by('research/old/extra.json', 'A', base, base), 'research/old') + self.assertEqual(planner.listing_changed_by('NEWFILE', 'A', base, base), '') + self.assertEqual(planner.listing_changed_by('brand/new/tree/x', 'A', base, base), '') + self.assertEqual(planner.listing_changed_by('research/old/gone.json', 'D', base, {'research'}), 'research') + self.assertIsNone(planner.listing_changed_by('research/old/x', 'M', base, base)) + self.assertIs(planner.listing_changed_by('research/old/x', 'A'), planner.ANY_ANCESTOR) + + def test_existence_patterns_match_only_creation_or_removal(self): + base = {'research', 'research/old'} + self.assertEqual(planner.directories_changed_by('research/new/x', 'A', base, base), {'research/new'}) + self.assertEqual(planner.directories_changed_by('research/old/x', 'A', base, base), set()) + self.assertEqual(planner.directories_changed_by('research/old/x', 'D', base, {'research'}), {'research/old'}) + self.assertIsNone(planner.directories_changed_by('research/old/x', 'M', base, base)) + self.assertTrue(planner.pattern_matches('research/new/', 'research/new/x', 'A', 'research', {'research/new'})) + self.assertFalse(planner.pattern_matches('research/', 'research/new/x', 'A', 'research', {'research/new'})) + self.assertFalse(planner.pattern_matches('research/old/', 'research/old/x', 'M', None, None)) + self.assertTrue(planner.pattern_matches('research/', 'research/new/x', 'A')) # conservative without trees + manifest = json.loads(json.dumps(MANIFEST)); del manifest['groups']['whole'] + manifest['groups']['alpha']['paths'].append('research/') + dirs = {'research', 'research/old'} + result = planner.plan(manifest, 'pull_request', ['A:research/new/x'], base_dirs=dirs, head_dirs=dirs | {'research/new'}) + self.assertEqual(result['mode'], 'none', result['reason']) + result = planner.plan(manifest, 'pull_request', ['A:research/old/deeper/x'], base_dirs=dirs, head_dirs=dirs | {'research/old/deeper'}) + self.assertEqual(result['mode'], 'none', result['reason']) # research/old still exists; only a subdirectory was created + result = planner.plan(manifest, 'pull_request', ['A:research/new/x']) # no tree information: conservative + self.assertEqual((result['mode'], result['groups']), ('selected', ['alpha'])) + + def test_removing_or_creating_a_listed_directory_matches_its_listing(self): + base = {'research', 'research/pkg'} + # deleting the last file of research/pkg removes that directory: its own listing pattern must match + listing = planner.listing_changed_by('research/pkg/last.json', 'D', base, {'research'}) + removed = planner.directories_changed_by('research/pkg/last.json', 'D', base, {'research'}) + self.assertEqual((listing, removed), ('research', {'research/pkg'})) + self.assertTrue(planner.pattern_matches('research/pkg/*', 'research/pkg/last.json', 'D', listing, removed)) + self.assertTrue(planner.pattern_matches('research/*', 'research/pkg/last.json', 'D', listing, removed)) + self.assertFalse(planner.pattern_matches('research/other/*', 'research/pkg/last.json', 'D', listing, removed)) + manifest = json.loads(json.dumps(MANIFEST)); del manifest['groups']['whole'] + manifest['groups']['alpha']['paths'].append('research/pkg/*') + result = planner.plan(manifest, 'pull_request', ['D:research/pkg/last.json'], base_dirs=base, head_dirs={'research'}) + self.assertEqual(result['groups'], ['alpha']) + + def test_listing_patterns_with_tree_information_are_precise(self): + new = {'research/new'} + self.assertTrue(planner.pattern_matches('research/*', 'research/new/README.md', 'A', 'research', new)) + self.assertFalse(planner.pattern_matches('*', 'research/new/README.md', 'A', 'research', new)) + self.assertTrue(planner.pattern_matches('research/new/*', 'research/new/README.md', 'A', 'research', new)) + self.assertFalse(planner.pattern_matches('research/*', 'research/old/extra.json', 'A', 'research/old', set())) + self.assertTrue(planner.pattern_matches('research/old/*', 'research/old/extra.json', 'A', 'research/old', set())) + self.assertFalse(planner.pattern_matches('research/*', 'research/old/x', 'M', None, None)) + + def test_validate_pattern_rejects_other_globs(self): + for good in ('Makefile', 'scripts/**', 'certificates/*', '*', '**', 'a/b/c.json', 'research/'): + planner.validate_pattern(good) + for bad in ('research/*/x', 'foo//', '../x', '*.md', '', '/abs', 'a\\b', 'a/**/b', '/'): + with self.assertRaises(ValueError, msg=bad): + planner.validate_pattern(bad) + + +class Selection(unittest.TestCase): + def test_research_only_pull_request_runs_only_whole_tree_groups(self): + result = run_plan(['A:research/new-package/README.md', 'A:research/new-package/verify.py']) + self.assertEqual(result['mode'], 'selected') + self.assertEqual(result['groups'], ['whole']) + self.assertEqual(result['include'], [{'python-version': '3.11', 'group': 'whole'}, + {'python-version': '3.13', 'group': 'whole'}]) + self.assertEqual(result['jobs'], []) + + def test_whole_tree_group_does_not_explain_unknown_paths(self): + # `**` selects its group but a path nobody declared still runs everything. + kind, groups = planner.classify(MANIFEST, 'SOURCES.json', 'M', None) + self.assertEqual((kind, groups), ('unclassified', ['whole'])) + self.assertEqual(run_plan(['M:SOURCES.json'])['mode'], 'full') + kind, groups = planner.classify(MANIFEST, 'research/x/y', 'M', None) + self.assertEqual((kind, groups), ('skip_safe', ['whole'])) + + def test_ignored_tracked_path_runs_everything(self): + result = planner.plan(MANIFEST, 'pull_request', ['A:research/x/__pycache__/m.pyc'], + ignored={'research/x/__pycache__/m.pyc'}) + self.assertEqual(result['mode'], 'full') + + def test_declared_package_input_selects_its_group_on_every_python(self): + result = run_plan(['M:research/beta-package/words.json']) + self.assertEqual(result['mode'], 'selected') + self.assertEqual(result['groups'], ['beta', 'whole']) + self.assertEqual(result['include'], [{'python-version': '3.11', 'group': 'beta'}, + {'python-version': '3.13', 'group': 'beta'}, + {'python-version': '3.11', 'group': 'whole'}, + {'python-version': '3.13', 'group': 'whole'}]) + + def test_group_match_takes_precedence_over_skip_safe(self): + kind, groups = planner.classify(MANIFEST, 'research/beta-package/x', 'M') + self.assertEqual((kind, groups), ('group', ['beta', 'whole'])) + + def test_added_entry_in_listed_directory_selects_group(self): + result = run_plan(['A:certificates/brand-new.json']) + self.assertEqual((result['mode'], result['groups']), ('selected', ['alpha', 'whole'])) + + def test_root_listing_is_not_changed_by_a_new_file_in_an_existing_directory(self): + manifest = json.loads(json.dumps(MANIFEST)) + manifest['groups']['alpha']['paths'].append('*') # make lists the root for every group + dirs = {'research', 'research/old', 'certificates'} + result = planner.plan(manifest, 'pull_request', ['A:research/new/README.md'], base_dirs=dirs, head_dirs=dirs) + self.assertEqual((result['mode'], result['groups']), ('selected', ['whole']), result['reason']) + result = planner.plan(manifest, 'pull_request', ['A:brand-new-dir/x'], base_dirs=dirs, head_dirs=dirs) + self.assertEqual(result['mode'], 'full') # a new root entry always verifies everything + self.assertEqual(planner.classify(manifest, 'brand-new-dir/x', 'A', '')[0], 'all') + self.assertEqual(planner.classify(manifest, 'NEWFILE', 'A')[0], 'all') + result = planner.plan(manifest, 'pull_request', ['A:research/new/README.md']) # no tree info + self.assertEqual((result['mode'], result['groups']), ('selected', ['alpha', 'whole'])) + + def test_modified_undeclared_file_in_listed_directory_runs_everything(self): + # Only the listing was recorded, so an edit to an unread file is unclassified: fail closed. + result = run_plan(['M:certificates/other.json']) + self.assertEqual(result['mode'], 'full') + self.assertIn('not declared', result['reason']) + self.assertEqual(result['groups'], ALL_GROUPS) + + def test_root_documentation_edit_is_inert_but_new_root_file_is_not(self): + self.assertEqual(run_plan(['M:README.md'])['groups'], ['whole']) + self.assertEqual(run_plan(['A:NEWFILE.md'])['mode'], 'full') + self.assertEqual(run_plan(['D:NOTICE'])['mode'], 'full') + self.assertEqual(run_plan(['M:SOURCES.json'])['mode'], 'full') # unclassified root file edit + + def test_all_paths_run_everything_and_record_inputs(self): + for path in ('M:Makefile', 'A:scripts/new_tool.py', 'M:.github/workflows/verify.yml', + 'M:.github/verify-groups.json'): + result = run_plan([path, 'A:research/x/y']) + self.assertEqual(result['mode'], 'full', path) + self.assertEqual(len(result['include']), 6, path) # alpha, beta, whole x two Pythons + self.assertEqual(result['jobs'], ['formal', 'package'], path) + self.assertEqual(result['formal'], [{'package': 'historical'}, {'package': 'matrix'}], path) + self.assertEqual([p['python-version'] for p in result['packages']], ['3.11', '3.14'], path) + self.assertEqual(result['packages'][0]['command'], 'python3 research/bit-elim-144/verify.py', path) + + def test_formal_only_change_runs_that_formal_package_without_matrix(self): + manifest = json.loads(json.dumps(MANIFEST)); del manifest['groups']['whole'] + result = planner.plan(manifest, 'pull_request', ['M:formal/lean/Foo.lean']) + self.assertEqual(result['mode'], 'selected') + self.assertEqual(result['include'], []) + self.assertEqual(result['jobs'], ['formal']) + self.assertEqual(result['formal'], [{'package': 'historical'}]) + self.assertEqual(result['packages'], []) + + def test_package_verifier_selected_on_its_pinned_input(self): + result = run_plan(['M:certificates/paired-cube-bit-input.json']) + self.assertEqual(result['groups'], ['pkg-bit-elim-144', 'whole']) + self.assertEqual(len(result['include']), 2) + self.assertEqual(result['jobs'], ['package']) + self.assertEqual([p['package'] for p in result['packages']], ['bit-elim-144', 'bit-elim-144']) + + def test_root_git_configuration_files_run_everything(self): + for path in ('M:.gitattributes', 'A:.gitignore', 'A:x/.gitmodules', 'M:.gitmodules'): + self.assertEqual(run_plan([path])['mode'], 'full', path) + + def test_nested_git_configuration_files_count_as_their_whole_subtree(self): + manifest = json.loads(json.dumps(MANIFEST)); del manifest['groups']['whole'] + # inside a research package: everything below is skip-safe, beta's declared package is unaffected + result = planner.plan(manifest, 'pull_request', ['A:research/new/.gitattributes']) + self.assertEqual(result['mode'], 'none', result['reason']) + # inside beta's declared package: beta runs + result = planner.plan(manifest, 'pull_request', ['A:research/beta-package/.gitattributes']) + self.assertEqual((result['mode'], result['groups']), ('selected', ['beta'])) + # above a declared input (notes/** of alpha): alpha runs + result = planner.plan(manifest, 'pull_request', ['M:notes/.gitignore']) + self.assertEqual((result['mode'], result['groups']), ('selected', ['alpha'])) + # in an undeclared directory: unclassified, everything runs + self.assertEqual(planner.plan(manifest, 'pull_request', ['A:references/.gitattributes'])['mode'], 'full') + # in scripts/: an `all` path + self.assertEqual(planner.plan(manifest, 'pull_request', ['A:scripts/x/.gitattributes'])['mode'], 'full') + self.assertTrue(planner.subtree_matches('research/beta-package/**', 'research')) # pattern below the directory + self.assertTrue(planner.subtree_matches('research/**', 'research/beta-package')) # pattern above it + self.assertFalse(planner.subtree_matches('notes/**', 'research')) + + def test_other_workflow_edits_are_inert(self): + manifest = json.loads(json.dumps(MANIFEST)); del manifest['groups']['whole'] + self.assertEqual(planner.plan(manifest, 'pull_request', ['M:.github/workflows/other.yml'])['mode'], 'none') + + def test_bare_paths_are_treated_as_additions(self): + self.assertEqual(planner.split_status('certificates/x.json'), ('A', 'certificates/x.json')) + self.assertEqual(planner.split_status('M:certificates/x.json'), ('M', 'certificates/x.json')) + self.assertEqual(run_plan(['certificates/new.json'])['groups'], ['alpha', 'whole']) + + +class FullRunTriggers(unittest.TestCase): + def test_schedule_and_dispatch_always_run_everything(self): + for event in ('schedule', 'workflow_dispatch'): + result = run_plan(None, event=event) + self.assertEqual(result['mode'], 'full', event) + self.assertEqual(len(result['include']), 6) + self.assertEqual(len(result['formal']), 2) + self.assertEqual(len(result['packages']), 2) + + def test_missing_or_failed_diff_fails_closed(self): + self.assertEqual(run_plan(None)['mode'], 'full') + self.assertEqual(run_plan(None, diff_error='base is the all-zero SHA')['mode'], 'full') + self.assertEqual(run_plan(None, event='push', diff_error='fetch failed')['mode'], 'full') + + def test_full_label(self): + self.assertEqual(run_plan([], action='labeled', label='ci:full-verify')['mode'], 'full') + self.assertEqual(run_plan([], action='labeled', label='needs-review')['mode'], 'none') + self.assertEqual(run_plan(['A:research/x/y'], labels=['ci:full-verify'])['mode'], 'full') + + def test_unknown_event_runs_everything(self): + self.assertEqual(run_plan(['A:research/x/y'], event='merge_group')['mode'], 'full') + + def test_force_full(self): + self.assertEqual(run_plan(['A:research/x/y'], force_full=True)['mode'], 'full') + + +class GitDiff(unittest.TestCase): + def test_statuses_and_renames(self): + with tempfile.TemporaryDirectory() as tmp: + env = dict(os.environ, GIT_AUTHOR_NAME='t', GIT_AUTHOR_EMAIL='t@x', GIT_COMMITTER_NAME='t', + GIT_COMMITTER_EMAIL='t@x', GIT_CONFIG_GLOBAL='/dev/null', GIT_CONFIG_NOSYSTEM='1') + git = lambda *a: subprocess.run(['git', *a], cwd=tmp, env=env, check=True, stdout=subprocess.PIPE, + stderr=subprocess.PIPE).stdout.decode().strip() + git('init', '-q') + Path(tmp, 'keep.txt').write_text('a') + Path(tmp, 'gone.txt').write_text('b') + Path(tmp, 'moved.txt').write_text('c' * 100) + git('add', '.'); git('commit', '-qm', 'base'); base = git('rev-parse', 'HEAD') + Path(tmp, 'keep.txt').write_text('a2') + Path(tmp, 'gone.txt').unlink() + Path(tmp, 'moved.txt').rename(Path(tmp, 'renamed.txt')) + Path(tmp, 'new.txt').write_text('d') + git('add', '-A'); git('commit', '-qm', 'change') + changed, links = planner.git_changed(base, 'HEAD', cwd=tmp) + self.assertEqual(sorted(changed), ['A:new.txt', 'A:renamed.txt', 'D:gone.txt', 'D:moved.txt', 'M:keep.txt']) + self.assertEqual(links, set()) + os.symlink('keep.txt', Path(tmp, 'alias.txt')) + Path(tmp, '.gitignore').write_text('*.log\n'); Path(tmp, 'noise.log').write_text('x') + git('add', '-A'); git('add', '-f', 'noise.log'); git('commit', '-qm', 'link') + changed, links = planner.git_changed('HEAD^', 'HEAD', cwd=tmp) + self.assertEqual(links, {'alias.txt'}) + self.assertEqual(planner.git_ignored(['noise.log', 'keep.txt'], cwd=tmp), {'noise.log'}) + with self.assertRaises(ValueError): + planner.git_changed(planner.ZERO_SHA, 'HEAD', cwd=tmp) + with self.assertRaises(ValueError): + planner.git_changed('0123456789abcdef0123456789abcdef01234567', 'HEAD', cwd=tmp) + Path(tmp, 'sub/deeper').mkdir(parents=True); Path(tmp, 'sub/deeper/f').write_text('x') + git('add', '-A'); git('commit', '-qm', 'dirs') + self.assertEqual(planner.git_dirs('HEAD', cwd=tmp), {'sub', 'sub/deeper'}) + self.assertEqual(planner.git_dirs(base, cwd=tmp), set()) + + +class Outputs(unittest.TestCase): + def test_github_output_and_summary(self): + result = run_plan(['M:research/beta-package/words.json']) + with tempfile.TemporaryDirectory() as tmp: + out = Path(tmp, 'out') + planner.write_outputs(result, out) + text = out.read_text() + values = dict(line.split('=', 1) for line in text.strip().splitlines()) + self.assertEqual(json.loads(values['matrix']), {'include': result['include']}) + self.assertEqual(values['count'], '4') + self.assertEqual(values['groups'], 'beta,whole') + self.assertEqual(values['jobs'], '') + self.assertEqual(json.loads(values['formal']), {'include': []}) + self.assertEqual(values['formal_count'], '0') + self.assertEqual(json.loads(values['packages']), {'include': []}) + self.assertEqual(values['package_count'], '0') + self.assertEqual(values['mode'], 'selected') + self.assertNotIn('trace', values) + summary = planner.summary_markdown(result, 'pull_request') + self.assertIn('**selected**', summary) + self.assertIn('M:research/beta-package/words.json', summary) + + +class RepositoryManifest(unittest.TestCase): + """The committed manifest must match the Makefile's CI groups and validate.""" + def test_manifest_loads_and_groups_match_makefile(self): + manifest = planner.load_manifest(ROOT / '.github/verify-groups.json') + self.assertEqual(manifest['python'], ['3.11', '3.13', '3.14']) + makefile = (ROOT / 'Makefile').read_text() + targets = set(re.findall(r'^verify-([a-z0-9-]+):', makefile, re.M)) + verify_groups = {g for g, spec in manifest['groups'].items() if spec.get('job', 'verify') == 'verify'} + self.assertEqual(verify_groups, targets - {'parallel'}) + self.assertEqual({spec.get('job', 'verify') for spec in manifest['groups'].values()}, + {'verify', 'ranked-pair-finite', 'formal', 'package'}) + formal = {spec['package'] for spec in manifest['groups'].values() if spec.get('job') == 'formal'} + self.assertEqual(formal, set(re.findall(r'^formal-([a-z]+)-verify:', makefile, re.M))) + packages = {spec['package'] for spec in manifest['groups'].values() if spec.get('job') == 'package'} + self.assertEqual(packages, {'bit-elim-144', 'bit-reuse-147', 'early-reset-reuse', 'graded-box-convolution'}) + full = planner.plan(manifest, 'workflow_dispatch') + self.assertEqual(len(full['include']), 48) + self.assertEqual(len({(i['python-version'], i['group']) for i in full['include']}), 48) + self.assertEqual(len(full['formal']), 3) + self.assertEqual(len(full['packages']), 8) + for key in ('Makefile', 'scripts/**', '.github/workflows/verify.yml', '.github/verify-groups.json', + '.gitattributes'): + self.assertIn(key, manifest['all']) + + def test_a_new_research_package_runs_only_whole_tree_groups(self): + manifest = planner.load_manifest(ROOT / '.github/verify-groups.json') + dirs = planner.git_dirs('HEAD') + result = planner.plan(manifest, 'pull_request', + ['A:research/zz-new-package/README.md', 'A:research/zz-new-package/verify.py', + 'A:research/zz-new-package/VERIFY.json', 'A:.github/workflows/zz-new-package.yml'], + base_dirs=dirs, head_dirs=dirs | {'research/zz-new-package'}) + self.assertNotEqual(result['mode'], 'full', result['reason']) + broad = {g for g, spec in manifest['groups'].items() + if '**' in spec['paths'] or 'research/**' in spec['paths'] or 'research/*' in spec['paths']} + self.assertEqual(set(result['groups']), broad, result['reason']) + for group in result['matrix_groups']: + self.assertEqual([i['python-version'] for i in result['include'] if i['group'] == group], + manifest['python']) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_trace_verify_inputs.py b/tests/test_trace_verify_inputs.py new file mode 100644 index 0000000000..65e6990e3f --- /dev/null +++ b/tests/test_trace_verify_inputs.py @@ -0,0 +1,342 @@ +"""Recorded verification inputs must be parsed, classified and covered correctly.""" +import importlib.util +import os +from pathlib import Path +import subprocess +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +spec = importlib.util.spec_from_file_location('trace_verify_inputs', ROOT / 'scripts/trace_verify_inputs.py') +tracer = importlib.util.module_from_spec(spec) +spec.loader.exec_module(tracer) + +LOG = '''100 execve("/usr/bin/sh", ["sh", "-c", "make verify-x"], 0x1 /* 3 vars */) = 0 +100 openat(AT_FDCWD, "Makefile", O_RDONLY|O_CLOEXEC) = 3 +100 openat(AT_FDCWD, ".", O_RDONLY|O_NONBLOCK|O_CLOEXEC|O_DIRECTORY) = 4 +100 vfork( +101 execve("/usr/bin/python3", ["python3", "scripts/x.py"], 0x2 /* 3 vars */) = 0 +101 newfstatat(AT_FDCWD, "scripts/x.py", {st_mode=S_IFREG|0644, st_size=10, ...}, 0) = 0 +100 <... vfork resumed>) = 101 +101 chdir("certificates") = 0 +101 openat(AT_FDCWD, "alpha.json", O_RDONLY|O_CLOEXEC) = 3 +101 openat(AT_FDCWD, "../notes", O_RDONLY|O_NONBLOCK|O_CLOEXEC|O_DIRECTORY) = 5 +101 openat(5, "deep.tex", O_RDONLY|O_CLOEXEC) = 6 +101 newfstatat(AT_FDCWD, "missing.json", 0x7ffd, 0) = -1 ENOENT (No such file or directory) +101 openat(AT_FDCWD, "/repo/build/out.json", O_WRONLY|O_CREAT|O_TRUNC|O_CLOEXEC, 0666) = 7 +101 openat(AT_FDCWD, "/usr/lib/python3/json/__init__.py", O_RDONLY|O_CLOEXEC) = 8 +101 readlink("/repo/scripts/x.py", 0x7ffd, 4096) = -1 EINVAL (Invalid argument) +101 <... openat resumed>) = 9 +101 exit_group(0) = ? +100 +++ exited with 0 +++ +''' + + +class Parsing(unittest.TestCase): + def test_paths_resolve_against_each_process_cwd(self): + seen = {(p, k) for p, k, _ in tracer.parse_strace(LOG, '/repo')} + self.assertIn(('/repo/Makefile', 'file'), seen) + self.assertIn(('/repo', 'dir'), seen) + self.assertIn(('/repo/scripts/x.py', 'file'), seen) + self.assertIn(('/repo/certificates/alpha.json', 'file'), seen) # after chdir in the child + self.assertIn(('/repo/notes', 'dir', ), seen) + self.assertIn(('/repo/notes/deep.tex', 'file'), seen) # relative to an open directory fd + self.assertIn(('/repo/certificates/missing.json', 'file'), seen) + self.assertIn(('/repo/build/out.json', 'file'), seen) + self.assertIn(('/usr/lib/python3/json/__init__.py', 'file'), seen) + self.assertNotIn(('/repo/certificates/scripts/x.py', 'file'), seen) + self.assertIn(('/repo/scripts/x.py', 'file'), seen) # readlink operand + + def test_child_inherits_cwd_before_parent_resume_line(self): + log = ('1 chdir("sub") = 0\n1 vfork( \n2 openat(AT_FDCWD, "f", O_RDONLY) = 3\n' + '1 <... vfork resumed>) = 2\n') + self.assertIn(('/r/sub/f', 'file'), {(p, k) for p, k, _ in tracer.parse_strace(log, '/r')}) + + +class Classification(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory() + self.root = Path(self.tmp.name).resolve() + env = dict(os.environ, GIT_AUTHOR_NAME='t', GIT_AUTHOR_EMAIL='t@x', GIT_COMMITTER_NAME='t', + GIT_COMMITTER_EMAIL='t@x', GIT_CONFIG_GLOBAL='/dev/null', GIT_CONFIG_NOSYSTEM='1') + git = lambda *a: subprocess.run(['git', *a], cwd=self.root, env=env, check=True, stdout=subprocess.PIPE) + git('init', '-q') + (self.root / 'certificates').mkdir() + (self.root / 'certificates/alpha.json').write_text('{}') + (self.root / 'Makefile').write_text('all:\n') + (self.root / '.gitignore').write_text('build/\n__pycache__/\n') + git('add', '.'); git('commit', '-qm', 'base') + (self.root / 'build').mkdir(); (self.root / 'build/out.json').write_text('x') + (self.root / 'certificates/untracked.json').write_text('{}') + (self.root / 'certificates/__pycache__').mkdir() + + def tearDown(self): + self.tmp.cleanup() + + def test_tracked_files_listed_dirs_and_probes(self): + r = str(self.root) + paths = [(r + '/Makefile', 'file'), (r + '/certificates/alpha.json', 'file'), (r, 'dir'), + (r + '/certificates', 'dir'), (r + '/certificates/missing.json', 'file'), + (r + '/build/out.json', 'file'), (r + '/certificates/untracked.json', 'file'), + (r + '/certificates/__pycache__/x.pyc', 'file'), (r + '/.git/index', 'file'), + ('/usr/lib/python3/json.py', 'file'), (r + '/RCS', 'dir'), (r + '/SCCS', 'file'), + (r + '/-lc', 'file'), (r + '/algorithm', 'file'), (r + '/certificates', 'file')] + files, dirs, probes, tree, exists, subtrees = tracer.classify(paths, self.root) + self.assertEqual(files, ['Makefile', 'certificates/alpha.json']) + self.assertEqual(dirs, ['', 'certificates']) + self.assertEqual(exists, []) + # ignored outputs, caches, .git, system files, make's VCS probes and root-level probes are dropped; + # an untracked but unignored file and a missing path inside the repo are kept. + self.assertEqual(probes, ['certificates/missing.json', 'certificates/untracked.json']) + self.assertFalse(tree) + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/build', 'dir'), (r + '/build/out.json', 'file')], self.root) + self.assertEqual((files, dirs, probes, exists), ([], [], [], [])) # ignored directories are not listings + + def test_existence_checks_are_not_listings(self): + r = str(self.root) + files, dirs, probes, tree, exists, subtrees = tracer.classify( + [(r + '/certificates', 'file'), (r, 'file'), (r + '/certificates', 'dir')], self.root) + self.assertEqual((dirs, exists), (['certificates'], [''])) # listed wins over a bare stat; root stat is existence + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/certificates', 'file')], self.root) + self.assertEqual((dirs, exists), ([], ['certificates'])) + + def test_runtime_directories_are_declared_at_their_tracked_ancestor(self): + r = str(self.root) + (self.root / 'certificates/scratch').mkdir() + files, dirs, probes, tree, exists, subtrees = tracer.classify( + [(r + '/certificates/scratch', 'dir'), (r + '/certificates/scratch/input.json', 'file')], self.root) + self.assertEqual(dirs, ['certificates']) # git does not know scratch; additions below it change certificates + self.assertEqual(probes, ['certificates/scratch/input.json']) + self.assertEqual(tracer.anchor('certificates/scratch/input.json', self.root), 'certificates') + self.assertEqual(tracer.anchor('nowhere/deep/x', self.root), '') + + def test_git_tree_objects_are_subtrees(self): + r = str(self.root) + files, dirs, probes, tree, exists, subtrees = tracer.classify( + [(r + '\0certificates', 'gitpath'), (r + '\0certificates/alpha.json', 'gitpath')], self.root) + self.assertEqual((files, subtrees), (['certificates/alpha.json'], ['certificates'])) + rec = {'group': 'g', 'commands': [], 'files': [], 'dirs': [], 'probes': [], 'subtrees': ['certificates']} + self.assertEqual(tracer.uncovered(rec, ['certificates/*'], self.root), ['certificates/**']) + self.assertEqual(tracer.suggest(rec, root=self.root), ['certificates/**']) + + def test_escaped_utf8_and_dash_names_survive(self): + r = str(self.root) + (self.root / 'certificates/caf\u00e9.json').write_text('{}') + subprocess.run(['git', 'add', 'certificates/caf\u00e9.json'], cwd=self.root, check=True) + self.assertEqual(tracer._unescape('caf\\303\\251.json'), 'caf\u00e9.json') + self.assertEqual(tracer._unescape('a\\nb\\x41\\"'), 'a\nbA"') + files, dirs, probes, tree, exists, subtrees = tracer.classify( + [(r + '/certificates/caf\u00e9.json', 'file'), (r + '/certificates/-dashed.json', 'file')], self.root) + self.assertEqual(files, ['certificates/caf\u00e9.json']) + self.assertEqual(probes, ['certificates/-dashed.json']) + + def test_tracked_cache_files_and_tree_queries_are_kept(self): + r = str(self.root) + (self.root / 'certificates/__pycache__/keep.pyc').write_text('x') + subprocess.run(['git', 'add', '-f', 'certificates/__pycache__/keep.pyc'], cwd=self.root, check=True, + stdout=subprocess.PIPE) + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/certificates/__pycache__/keep.pyc', 'file'), (r, 'tree')], self.root) + self.assertEqual(files, ['certificates/__pycache__/keep.pyc']) + self.assertTrue(tree) + + def test_git_in_a_nested_checkout_or_outside_is_not_this_tree(self): + r = str(self.root) + nested = self.root / 'build/upstream' + nested.mkdir(parents=True) + subprocess.run(['git', 'init', '-q'], cwd=nested, check=True) + files, dirs, probes, tree, exists, subtrees = tracer.classify( + [(r + '/build/upstream', 'tree'), ('/elsewhere', 'tree'), (r + '/build/upstream\0certificates/alpha.json', 'gitpath'), + (r + '/certificates\0Makefile', 'gitpath'), (r + '/certificates\0./alpha.json', 'gitpath')], self.root) + self.assertFalse(tree) + self.assertEqual(files, ['Makefile', 'certificates/alpha.json']) + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/certificates', 'tree')], self.root) + self.assertTrue(tree) + + def test_symlink_records_link_and_target(self): + r = str(self.root) + os.symlink('alpha.json', self.root / 'certificates/link.json') + os.symlink('certificates', self.root / 'linkdir') + subprocess.run(['git', 'add', 'certificates/link.json', 'linkdir'], cwd=self.root, check=True) + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/certificates/link.json', 'file')], self.root) + self.assertEqual(files, ['certificates/alpha.json', 'certificates/link.json']) + files, dirs, probes, tree, exists, subtrees = tracer.classify([(r + '/linkdir/alpha.json', 'file')], self.root) + self.assertEqual(files, ['certificates/alpha.json', 'linkdir']) # the directory link and the real input + + +class GitSemantics(unittest.TestCase): + def test_show_of_a_tree_path_is_that_path(self): + self.assertEqual(tracer.git_semantics(['git', 'show', 'HEAD:certificates/x.json']), + ([('certificates/x.json', 'git')], False, None)) + self.assertEqual(tracer.git_semantics(['git', '-c', 'core.quotepath=off', 'show', 'HEAD:a/b']), + ([('a/b', 'git')], False, None)) + self.assertEqual(tracer.git_semantics(['git', 'cat-file', '-p', 'HEAD:a/b']), ([('a/b', 'git')], False, None)) + self.assertEqual(tracer.git_semantics(['git', '-C', 'up', 'ls-tree', '-r', 'HEAD']), ([], True, 'up')) + self.assertEqual(tracer.git_semantics(['git', 'rev-parse', 'HEAD:certificates/x.json']), + ([('certificates/x.json', 'git')], False, None)) + self.assertEqual(tracer.git_semantics(['git', 'rev-parse', 'HEAD:']), ([], True, None)) + self.assertEqual(tracer.git_semantics(['git', '--git-dir=/x/.git', 'show', 'HEAD'])[1:], (True, tracer.THIS_CHECKOUT)) + + def test_object_paths_carry_the_git_directory(self): + log = ('7 chdir("sub") = 0\n' + '7 execve("/usr/bin/git", ["git", "show", "HEAD:certificates/x.json"], 0x1 /* 3 vars */) = 0\n' + '7 execve("/usr/bin/git", ["git", "-C", "../up", "ls-files"], 0x1 /* 3 vars */) = 0\n') + seen = {(p, k) for p, k, _ in tracer.parse_strace(log, '/r')} + self.assertIn(('/r/sub\0certificates/x.json', 'gitpath'), seen) + self.assertIn(('/r/up', 'tree'), seen) + + def test_immutable_objects_and_inert_commands(self): + sha = '0123456789abcdef0123456789abcdef01234567' + self.assertEqual(tracer.git_semantics(['git', 'show', sha + ':certificates/x.json'])[:2], ([], False)) + for argv in (['git', 'rev-parse', 'HEAD'], ['git', 'cat-file', '-e', sha], ['git', 'hash-object', 'f'], + ['git', 'apply', '--check', '--directory=upstream', 'patches/x.patch'], ['git', 'fetch', 'x'], + ['git', 'cat-file', '-p', sha + ':certificates/x.json'], ['git', '-C', 'up', 'rev-parse', 'HEAD']): + self.assertEqual(tracer.git_semantics(argv)[:2], ([], False), argv) + + def test_whole_tree_commands(self): + for argv in (['git', 'ls-files', '-z'], ['git', 'status', '--porcelain'], ['git', 'diff', '--exit-code'], + ['git', 'show', 'HEAD'], ['git', 'show'], ['git', 'ls-tree', 'HEAD'], ['git', '--git-dir=x', 'log'], + ['git', 'rev-list', 'HEAD'], + ['git', 'clone', '.', '/tmp/x'], ['git', 'frobnicate'], ['git', 'cat-file', '--batch'], + ['git', 'cat-file', '--batch-check'], ['git', 'cat-file', '-p', 'HEAD'], + ['git', 'apply', '--cached', 'p.patch'], ['git', 'apply', '--index', 'p.patch']): + self.assertEqual(tracer.git_semantics(argv)[:2], ([], True), argv) + self.assertEqual(tracer.git_semantics(['git', 'restore', 'certificates/x.json']), + ([('certificates/x.json', 'file')], False, None)) + + +class Tokens(unittest.TestCase): + def test_tokens_respect_quotes_and_nesting(self): + self.assertEqual(tracer.tokens('AT_FDCWD, "a, b", O_RDONLY|O_CLOEXEC) = 3'), + ['AT_FDCWD', '"a, b"', 'O_RDONLY|O_CLOEXEC']) + self.assertEqual(tracer.tokens('"/usr/bin/git", ["git", "show", "HEAD:x,y"], 0x1 /* 3 vars */) = 0'), + ['"/usr/bin/git"', '["git", "show", "HEAD:x,y"]', '0x1 /* 3 vars */']) + self.assertEqual(tracer.argv_strings('["git", "show", "HEAD:x,y"]'), ['git', 'show', 'HEAD:x,y']) + self.assertEqual(tracer.tokens('"x" '), ['"x"']) + + def test_two_path_calls_record_destinations(self): + log = ('7 rename("build/tmp.json", "certificates/out.json") = 0\n' + '7 renameat2(AT_FDCWD, "a", AT_FDCWD, "b", RENAME_NOREPLACE) = 0\n' + '7 symlinkat("target", AT_FDCWD, "linkname") = 0\n') + seen = {(p, k) for p, k, _ in tracer.parse_strace(log, '/r')} + self.assertEqual(seen, {('/r/build/tmp.json', 'file'), ('/r/certificates/out.json', 'file'), + ('/r/a', 'file'), ('/r/b', 'file'), ('/r/linkname', 'file')}) + + def test_git_execve_and_fchdir(self): + log = ('7 execve("/usr/bin/git", ["git", "ls-files", "-z"], 0x1 /* 3 vars */) = 0\n' + '8 fchdir(5) = 0\n8 openat(AT_FDCWD, "f", O_RDONLY) = 3\n' + '9 chdir("deep" \n9 <... chdir resumed>) = 0\n9 stat("g", 0x1) = 0\n') + seen = {(p, k) for p, k, _ in tracer.parse_strace(log, '/r')} + self.assertIn(('/r', 'tree'), seen) + self.assertIn(('/usr/bin/git', 'file'), seen) + self.assertIn(('/r/sub/f', 'file'), seen) + self.assertIn(('/r/deep/g', 'file'), seen) + log2 = '9 chdir("sub") = 0\n9 execve("/usr/bin/git", ["git", "--git-dir=/elsewhere/.git", "show", "HEAD"], 0x1 /* 3 vars */) = 0\n' + self.assertIn(('/r', 'tree'), {(p, k) for p, k, _ in tracer.parse_strace(log2, '/r')}) + # the parser also accepts a callable producing lines, as record() streams the log + self.assertIn(('/r', 'tree'), {(p, k) for p, k, _ in tracer.parse_strace(lambda: iter(log2.splitlines()), '/r')}) + + +class Coverage(unittest.TestCase): + RECORDING = {'group': 'g', 'commands': [], 'files': ['Makefile', 'certificates/alpha.json', 'notes/a.tex'], + 'dirs': ['', 'certificates', 'references/pkg'], 'probes': ['references/pkg/missing.json'], + 'tree': False} + + def setUp(self): + self.tmp = tempfile.TemporaryDirectory() + self.root = Path(self.tmp.name).resolve() + env = dict(os.environ, GIT_AUTHOR_NAME='t', GIT_AUTHOR_EMAIL='t@x', GIT_COMMITTER_NAME='t', + GIT_COMMITTER_EMAIL='t@x', GIT_CONFIG_GLOBAL='/dev/null', GIT_CONFIG_NOSYSTEM='1') + subprocess.run(['git', 'init', '-q'], cwd=self.root, env=env, check=True) + for d in ('certificates', 'notes', 'references/pkg', 'research/p1', 'research/p2', 'research/p3', + 'research/p4', 'research/p5', 'research/p6', 'research/p7', 'research/p8', 'tests/sub'): + (self.root / d).mkdir(parents=True) + (self.root / d / 'tracked.txt').write_text('x') # every directory is known to git + subprocess.run(['git', 'add', '.'], cwd=self.root, env=env, check=True) + subprocess.run(['git', 'commit', '-qm', 'base'], cwd=self.root, env=env, check=True) + + def tearDown(self): + self.tmp.cleanup() + + def test_dir_coverage(self): + self.assertTrue(tracer.dir_covered('certificates/*', 'certificates')) + self.assertTrue(tracer.dir_covered('certificates/**', 'certificates')) + self.assertTrue(tracer.dir_covered('references/**', 'references/pkg')) + self.assertTrue(tracer.dir_covered('*', '')) + self.assertTrue(tracer.dir_covered('**', 'anything')) + self.assertFalse(tracer.dir_covered('certificates/*', 'certificates/sub')) + self.assertFalse(tracer.dir_covered('certificates/alpha.json', 'certificates')) + self.assertFalse(tracer.dir_covered('*', 'certificates')) + + def test_file_reads_need_exact_or_recursive_patterns(self): + self.assertTrue(tracer.pattern_matches('notes/**', 'notes/a.tex')) + self.assertTrue(tracer.pattern_matches('Makefile', 'Makefile')) + self.assertFalse(tracer.pattern_matches('notes/*', 'notes/a.tex')) # listing does not cover an edit + self.assertFalse(tracer.pattern_matches('*', 'Makefile')) + + def test_uncovered_and_suggest(self): + patterns = ['Makefile', 'certificates/alpha.json', 'notes/**', '*', 'certificates/*', 'references/**'] + self.assertEqual(tracer.uncovered(self.RECORDING, patterns, self.root), []) + missing = tracer.uncovered(self.RECORDING, ['Makefile', 'notes/**', 'references/**'], self.root) + self.assertEqual(missing, ['certificates/alpha.json', '*', 'certificates/*']) + suggested = tracer.suggest(self.RECORDING, covered_by=['Makefile'], root=self.root) + self.assertEqual(suggested, ['*', 'certificates/*', 'certificates/alpha.json', 'notes/a.tex', + 'references/pkg/*']) # the probe is covered by its parent's listing + self.assertEqual(tracer.uncovered(self.RECORDING, suggested + ['Makefile'], self.root), []) + + def test_suggest_coarsens_directories_whose_files_are_mostly_read(self): + # tests/ has one tracked file in the fixture: reading five files there is "most of it" + rec = {'group': 'g', 'commands': [], 'files': ['tests/t%d.py' % i for i in range(5)] + ['tests/sub/x.py'], + 'dirs': ['tests'], 'probes': []} + self.assertEqual(tracer.suggest(rec, root=self.root), ['tests/**']) + # notes/ with many tracked files: reading four of them stays exact plus the listing + for i in range(20): + (self.root / ('notes/n%d.tex' % i)).write_text('x') + subprocess.run(['git', 'add', 'notes'], cwd=self.root, check=True) + tracer._TRACKED_DIRS.clear() + rec = {'group': 'g', 'commands': [], 'files': ['notes/n%d.tex' % i for i in range(4)], 'dirs': ['notes'], 'probes': []} + self.assertEqual(tracer.suggest(rec, root=self.root), + ['notes/*', 'notes/n0.tex', 'notes/n1.tex', 'notes/n2.tex', 'notes/n3.tex']) + + def test_suggest_coarsens_walked_directories_but_not_a_few_listed_children(self): + walked = {'group': 'g', 'commands': [], 'files': [], 'probes': [], + 'dirs': ['research'] + ['research/p%d' % i for i in range(1, 9)]} + self.assertEqual(tracer.suggest(walked, root=self.root), ['research/**']) + few = {'group': 'g', 'commands': [], 'files': [], 'probes': [], + 'dirs': ['research', 'research/p1', 'research/p2', 'research/p3', 'research/p4']} + self.assertEqual(tracer.suggest(few, root=self.root), + ['research/*', 'research/p1/*', 'research/p2/*', 'research/p3/*', 'research/p4/*']) + + def test_probe_is_anchored_at_its_deepest_existing_ancestor(self): + rec = {'group': 'g', 'commands': [], 'files': [], 'dirs': ['certificates'], + 'probes': ['certificates/missing.json', 'research/x/missing.json', 'notes/deep/er/missing.h']} + self.assertEqual(tracer.uncovered(rec, ['certificates/*'], self.root), ['research/x/missing.json', 'notes/deep/er/missing.h']) + self.assertEqual(tracer.suggest(rec, root=self.root), ['certificates/*', 'notes/*', 'research/*']) + self.assertEqual(tracer.uncovered(rec, ['certificates/*', 'notes/*', 'research/*'], self.root), []) + + def test_existence_coverage(self): + rec = {'group': 'g', 'commands': [], 'files': [], 'dirs': [], 'probes': [], 'exists': ['research', 'notes']} + self.assertEqual(tracer.uncovered(rec, ['notes/**'], self.root), ['research/']) + self.assertEqual(tracer.uncovered(rec, ['research/', 'notes/*'], self.root), []) + self.assertEqual(tracer.suggest(rec, root=self.root), ['notes/', 'research/']) + self.assertFalse(tracer.pattern_matches('research/', 'research/x/y')) + + def test_whole_tree_dependency(self): + rec = {'group': 'g', 'commands': [], 'files': ['Makefile'], 'dirs': [''], 'probes': [], 'tree': True} + self.assertEqual(tracer.uncovered(rec, ['Makefile', '*'], self.root), ['**']) + self.assertEqual(tracer.uncovered(rec, ['**'], self.root), []) + self.assertEqual(tracer.suggest(rec, root=self.root), ['**']) + self.assertEqual(tracer.suggest(rec, covered_by=['**'], root=self.root), []) + + +class Commands(unittest.TestCase): + def test_group_commands_match_the_workflow(self): + self.assertEqual(tracer.group_commands('community'), ['make verify-community']) + self.assertEqual(tracer.group_commands('clones'), + ['make skip-clones-verify split-skip-producer', + 'python3 -B scripts/replay_historical_check.py split-skip']) + self.assertEqual(tracer.group_commands('ranked-pair-finite'), + ['make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream']) + + +if __name__ == '__main__': + unittest.main() From 31b30326b08348c2af3bd4ed7310d20f65c49030 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 11:15:55 +0530 Subject: [PATCH 2/3] Fix historical clone replays after circuit optimizations --- docs/ci.md | 79 ++++++-- scripts/historical-ci-inputs/README.md | 21 +- .../historical-ci-inputs/exclusion_circuit.py | 184 ++++++++++++++++++ .../shared_point_circuit.py | 149 ++++++++++++++ scripts/replay_historical_check.py | 77 ++++++-- scripts/trace_verify_inputs.py | 3 +- tests/test_historical_check.py | 67 ++++++- tests/test_skip_clones.py | 11 ++ tests/test_trace_verify_inputs.py | 3 +- 9 files changed, 562 insertions(+), 32 deletions(-) create mode 100644 scripts/historical-ci-inputs/exclusion_circuit.py create mode 100644 scripts/historical-ci-inputs/shared_point_circuit.py diff --git a/docs/ci.md b/docs/ci.md index 2b49e41363..8f2bbf2712 100644 --- a/docs/ci.md +++ b/docs/ci.md @@ -231,17 +231,68 @@ new research package selects exactly the whole-tree groups, on every Python version. Hosted execution and the first scheduled tracer run are not claimed by local checks. -## Known failures on main at the time of this change - -Two tooling commits of 2026-10-14 changed sources that historical packages -pin by hash without updating the pins: d7d8bfcb (`scripts/exclusion_circuit.py`, -pinned by `research/skip-clones`) and 6178dede (`scripts/shared_point_circuit.py`, -pinned by `research/skip-strips`). The `clones` group and the -`test_skip_clones` module fail on that tree, while -`test_exclusion_embedding_masks` and `test_exclusion_support_masks` expect -the new bytes, so the `tests` group cannot pass in either state. This change -does not touch pins or frozen evidence. The input recordings for `clones` -and `tests` were made with the pinned versions of those two files -temporarily restored in a scratch checkout (the set of paths a group reads -does not depend on those bytes); both groups depend on the whole tree and -are declared `**`, so the recordings are not evidence that main passes. +## Historical source compatibility repair + +At the investigation base `0fdd7d82`, the exclusion-circuit optimizations in +`d8029ee05` and `d7d8bfcb` change a script pinned by `research/skip-clones` and +`research/split-skip`. The shared-point optimization in `6178dede` also changes +a script pinned by `research/split-skip`. The clone certificate tests and the +clones CI group therefore fail. Reverting the optimizations would instead +break their new source-bound equivalence tests. An earlier version of this +note incorrectly named `skip-strips` as the shared-point pin's consumer; +its unchanged verifier passes. + +The repair extends the existing `scripts/replay_historical_check.py` adapter. +It authenticates exact predecessor blobs from commit +`0b1cccf86e2f5132ed286a26ef0a681a495740ea` against the unchanged historical +source manifests before copying the current tracked tree. Only the declared +historical inputs are replaced inside the temporary tree. The live optimized +scripts, frozen certificates, manifests and selected result remain unchanged. +All tracked bytes in the replay copy are checked again on exit. + +The clones group now runs: + +```sh +python3 -B scripts/replay_historical_check.py skip-clones +make split-skip-producer +python3 -B scripts/replay_historical_check.py split-skip +``` + +The first command retains the complete clone native producer, certificate +regeneration and unit tests. The final command retains the split-skip witness, +independent arithmetic and unit tests, now with all three historical inputs +authenticated. Its native producer still runs separately as before. +The original source-bound Makefile targets remain frozen; use these adapters +to replay those checkpoints against a modern checkout. + +`test_skip_clones.py` also uses this isolated context during ordinary unittest +discovery, so `make verify-tests` keeps the original runner and discovers every +test module. Only this historical module sees the predecessor script; the +optimization tests still exercise the current production code. When already +running inside the historical replay, it uses that tree without nesting a +second copy. Scratch trees live under ignored `build/` and are removed on +exit, avoiding multi-GB allocations in memory-backed `/tmp`. + +Regression controls reject corrupt replacement bytes, missing or changed pins, +duplicate replacement paths, untracked replacements, and modifications to a +replay copy. Both groups retain their conservative whole-tree input declaration. +The earlier workload estimates predate the additional isolated clone replay; +its copying overhead and hosted execution still require measurement. + +Local repair validation on Linux x86_64 / Python 3.14.4 passed: + +```sh +python3 -B scripts/trace_verify_inputs.py --group clones --check --output build/verify-trace/pin-repair-clones.json +python3 -B scripts/trace_verify_inputs.py --group tests --check --output build/verify-trace/pin-repair-tests.json +python3 -B scripts/verify_selected_result.py +python3 -B scripts/check_selected_ci_inputs.py +``` + +Run the groups sequentially in an isolated worktree. The clones run includes +both native reconstructions, all 4,073,300 fixed-basis data pairs, the historical +witnesses and 21 package tests. The tests group passes all 129 discovered test +modules (including the live optimization controls) and all 20 patch-application +checks. Both traced input-coverage audits pass, tracked artifacts remain +unchanged, and temporary historical trees are removed. The recordings and logs +under `build/` are local-only evidence; hosted execution and Python 3.11/3.13 +execution of this repair are not claimed. diff --git a/scripts/historical-ci-inputs/README.md b/scripts/historical-ci-inputs/README.md index c438694334..841587efbb 100644 --- a/scripts/historical-ci-inputs/README.md +++ b/scripts/historical-ci-inputs/README.md @@ -3,7 +3,7 @@ These are exact Git blobs, not new source pins or changes to the selected result. The maintenance launcher `scripts/replay_historical_check.py` verifies each blob against its unchanged predecessor manifest, copies tracked working files into a -temporary tree, replaces just the declared historical input there, and executes +temporary tree, replaces just the declared historical inputs there, and executes the original checkers. It works with shallow CI checkouts and changes no live source file. The live Makefile must still preserve its entire authenticated historical prefix; appended targets are allowed, prefix mutations reject. All other inputs remain the current tracked working @@ -18,15 +18,32 @@ reproducibility gate as well as protecting the live checkout. | `selected-result.json` | `certificates/selected-result.json` | `5c5567d15bd019186519a4db267914257b5f1ac0` | `research/r420-two-sided-basis/SOURCES.json` | | `Makefile` | `Makefile` | `b84ba67156a01f9c2cb34fe1e3cb1dcdeab00d9c` | `research/community-reconciliation92-audit/MANIFEST.json` | | `audit_fused_block.py` | `scripts/audit_fused_block.py` | `6e564879f51ae16f23d392e9e196c605f36d90df` | `research/split-skip/SOURCE.json` | +| `exclusion_circuit.py` | `scripts/exclusion_circuit.py` | `0b1cccf86e2f5132ed286a26ef0a681a495740ea` | `research/skip-clones/SOURCE.json`, `research/split-skip/SOURCE.json` | +| `shared_point_circuit.py` | `scripts/shared_point_circuit.py` | `0b1cccf86e2f5132ed286a26ef0a681a495740ea` | `research/split-skip/SOURCE.json` | Use `python3 -B scripts/replay_historical_check.py r420` (add `--native` for -C++17/Boost), `reconciliation92`, or `split-skip`. These check historical finite +C++17/Boost), `reconciliation92`, `skip-clones`, or `split-skip`. These check historical finite constructions/provenance; they do not recertify the current selected supplier or formally verify the full multiplication theorem. The native R420 checks and the split-skip producer remain required in their CI jobs. +The `skip-clones` replay includes the complete native producer, certificate +regeneration and adversarial tests. `split-skip` authenticates all three of +its historical replacements before copying anything. Its native producer +still runs separately, as in the original CI job. The clone test module also +uses an isolated historical tree when invoked directly by unittest or the +isolated test runner; an already historical tree is used without nesting a +second copy. Other test modules, including Wentao Li's optimization controls, +continue to use the live scripts. No source pin is loosened or rewritten. + +Copies are placed in a unique temporary directory under the checkout's ignored +`build/` directory and removed on exit. This keeps the multi-GB tracked tree +off memory-backed `/tmp` while test modules run concurrently. + Credit Scott Woolsey Biggart and Greer Guthrie for the R420 evidence; the retained reconciliation records and their contributor attribution; Chafik Boukhalfa, RaD/hipotures and Rohan Garg for the split-pair lineage; and the original source headers. The snapshots retain the repository Apache-2.0 license. This maintenance adapter was prepared by Dennis with substantial OpenAI Codex assistance. +The clone/split-skip compatibility extension was prepared with substantial +OpenAI Codex assistance and retains all original source headers and credits. diff --git a/scripts/historical-ci-inputs/exclusion_circuit.py b/scripts/historical-ci-inputs/exclusion_circuit.py new file mode 100644 index 0000000000..aaa99986c4 --- /dev/null +++ b/scripts/historical-ci-inputs/exclusion_circuit.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Cancellation-free circuit for all pair sums avoiding two specified points. + +Every addition has disjoint input supports. Node interning shares equal sums; +support tracking verifies the full linear map, not sampled input values. +""" +from itertools import combinations +from hashlib import sha256 +import json + + +class ExclusionCircuit: + def __init__(self,n): + assert n>=4 + self.n=n + self.inputs=list(combinations(range(n),2)) + self.support=[0]+[1<=6 and h!=9, 'The ambient form I-J/9 must be nondegenerate' + self.h=h + self.local=circuit or ExclusionCircuit(h-1) + assert self.local.n==h-1, 'Pair circuit has the wrong ground size' + self.inputs=list(combinations(range(h),3)) + self.variables={t:i+1 for i,t in enumerate(self.inputs)} + self.args=[None]*(len(self.inputs)+1) + self.core=[0]+[sum(1<=2 and key in lookup: + mapping[node]=lookup[key];self.merged+=1 + continue + new=len(self.args);mapping[node]=new + self.args.append((a,b));self.core.append(core);self.union.append(union) + self.provenance.append((common,node)) + if core.bit_count()>=2:lookup[key]=new + for pair,node in sorted(self.local.outputs.items()): + t=tuple(sorted((common,*(self.points[common][x] for x in pair)))) + self.outputs[common,t]=mapping[node] + self.active=set();stack=list(self.outputs.values()) + while stack: + n=stack.pop() + if n in self.active:continue + self.active.add(n) + if self.args[n]:stack.extend(self.args[n]) + self.additions=sum(self.args[n] is not None for n in self.active) + + @lru_cache(maxsize=16384) + def support_in(self,node,common): + """Exact pair-input support in coordinates with this common point.""" + assert self.core[node]&(1< Date: Thu, 15 Oct 2026 11:59:40 +0530 Subject: [PATCH 3/3] Harden CI selection and failure reporting after independent audit Keep verification active on unrelated PR label events, honor existing full-run requests, and preserve recorded failures when checking saved trace coverage. Reject incompatible or incomplete recordings instead of accepting partial input evidence. Report failed cancellation requests and reject negative limits. Complete the historical formal dependency recording after fetching its pinned Mathlib cache. Preserve whole Lean project trees and explicitly cover external notes, certificates, upstream sections and alternate project discovery. The full target and its traced coverage pass; the original partial recording had missed inputs after a missing dependency stopped compilation. Add regressions for external references, label handling, saved traces and cancellation bounds. Preserve the original Apache-2.0 attribution, frozen archives, all source pins, selected-result record, optimized scripts, and earlier optional speedups. The historical compatibility repair authenticates exact predecessor bytes rather than changing their evidence. Document current workload estimates and the stable required-check gate in docs/ci.md. Validation on Linux/Python 3.14.4: full traced tests group (130 modules and 20 patch checks), complete traced historical formal target, actionlint, selected-result/input checks, and clean tracked-artifact drift checks. Final formal declaration also passed independent review and recorded input coverage. Earlier full clones replay passed with authenticated historical inputs. Hosted execution and Python 3.11/3.13 runs remain unverified. Prepared with substantial OpenAI Codex assistance and independent agent code review. Earlier CI implementation assistance by Claude Fable 5.1 remains credited in the preceding commit and documentation. --- .github/verify-groups.json | 22 ++++- docs/ci.md | 129 +++++++++++++++++++++------ scripts/cancel_superseded_runs.py | 13 ++- scripts/plan_verify_groups.py | 10 +-- scripts/trace_verify_inputs.py | 28 +++++- tests/test_cancel_superseded_runs.py | 128 ++++++++++++++++++++++++++ tests/test_plan_verify_groups.py | 50 ++++++++++- tests/test_trace_verify_inputs.py | 49 ++++++++++ 8 files changed, 391 insertions(+), 38 deletions(-) create mode 100644 tests/test_cancel_superseded_runs.py diff --git a/.github/verify-groups.json b/.github/verify-groups.json index 7183c6ffe0..2fddc194dc 100644 --- a/.github/verify-groups.json +++ b/.github/verify-groups.json @@ -684,11 +684,29 @@ "formal-historical": { "job": "formal", "package": "historical", - "declared": "static", + "declared": "recorded complete Make target; conservative whole Lean project trees", "paths": [ + "*", + "certificates/compact-control-layer.json", + "certificates/paired-network.json", + "certificates/parameters.json", "formal/**", + "notes/compact-control-guard.tex", + "notes/compact-control-layout.tex", + "notes/compact-control-movement.tex", + "notes/compact-control-note.tex", + "notes/independent-complex.tex", + "notes/nonadjacent-axis-note.tex", + "notes/paired-construction.tex", + "notes/paired-note.tex", + "notes/parameter-note.tex", + "research/", + "research/formal/**", "research/machine-transfer-verification/**", - "research/ranked-pair-verification/**" + "research/ranked-pair-verification/**", + "upstream/build/sections/03-motifs.tex", + "upstream/build/sections/05-layers.tex", + "upstream/build/sections/08-assembly.tex" ] }, "formal-gaussian": { diff --git a/docs/ci.md b/docs/ci.md index 8f2bbf2712..6c7c4933ac 100644 --- a/docs/ci.md +++ b/docs/ci.md @@ -9,8 +9,8 @@ list was removed or thinned. What changed is *when* each job runs: a cheap ## Why -Measured with the GitHub API on 2026-10-13/14 (details in the -[contribution PR](https://github.com/CrocSwap/integer-mult-bounds/pulls)): +Observed with the GitHub API on 2026-10-13/14; the downloaded timings are +local investigation evidence, not a retained performance certificate: - The repository had about 4,700 queued runs and 20 to 22 hours of queue wait, growing since 2026-10-13 06:00 UTC. @@ -22,12 +22,13 @@ Measured with the GitHub API on 2026-10-13/14 (details in the 52 jobs and about 207 runner-minutes per run, 925 runs a day. - A verify job spends 3.6 of its 3.9 minutes inside `make verify-`; checkout and interpreter setup are 0.3 minutes. Merging jobs or caching - setup cannot help; the verification work itself is the cost. + setup addresses only a small part of that cost. - 23 of 30 recently updated pull requests only added a new `research//` directory. Only two groups depend on the whole tree (`clones` copies and hashes every tracked file; `tests` walks every - research package), so the other 50 jobs of those runs re-verified a tree - the pull request did not change. + research package). Most remaining jobs re-verified inputs the pull request + did not change. The historical formal job's complete dependency recording + also allows selection without losing its external source checks. - 25% of the queued runs had already been superseded by a newer push. ## What runs @@ -38,8 +39,10 @@ Measured with the GitHub API on 2026-10-13/14 (details in the it diffs `before..after`. Each changed path is classified with [.github/verify-groups.json](../.github/verify-groups.json): - a path in the manifest's `all` list (Makefile, `scripts/**`, the - workflow, the manifest, and any `.gitattributes`, `.gitignore` or - `.gitmodules` at any depth) runs everything; + workflow, the manifest, and the root `.gitattributes` or `.gitignore`) + runs everything; `.gitmodules` at any depth also runs everything; + - a nested `.gitattributes` or `.gitignore` selects every group whose + declared inputs overlap its affected subtree; - a path matching a group's declared inputs selects that group, on every Python version; - a path in `skip_safe` (research packages, documentation prose, other @@ -52,12 +55,12 @@ Measured with the GitHub API on 2026-10-13/14 (details in the push, missing parent), any change to a symbolic link, any tracked path that `.gitignore` would ignore, and any entry added to or removed from the repository root run everything. A group declared `**` depends on - the whole tree and runs on every change (the `clones` group copies and - hashes every tracked file; the `tests` group walks every research - package), but a whole-tree match never counts as understanding a path: + the whole tree and runs on every change (`clones` and `tests`), but a whole-tree + match never counts as understanding a path: an otherwise undeclared path still runs everything. -2. **Verification.** Selected groups run exactly the commands they ran - before, under `strace`, and the step also fails if a group read an input +2. **Verification.** Selected groups retain their checks, using the + authenticated historical adapters described below where source pins + require them. They run under `strace`, and the step also fails if a group read an input its declaration does not cover. Full runs are the same 48 Python combinations, the finite replay, the three formal packages and the four package verifiers as before. @@ -66,11 +69,13 @@ Measured with the GitHub API on 2026-10-13/14 (details in the failed or was cancelled; only jobs the planner skipped on purpose may be skipped. -## Expected effect +## Estimated effect -Measured by replaying the planner over the changed-file lists of the 60 -most recently updated open pull requests (2026-10-15) with the recorded -manifest, using the Oct 14 per-job durations: +Estimated by replaying the planner over the changed-file lists of the 60 +most recently updated open pull requests (2026-10-15) with the audited +manifest, using the Oct 14 per-job durations. These are workload estimates, +not measured hosted durations of the new workflow; they exclude added tracing, +historical-copy and summary-job overhead: | | Runner-minutes per pull-request sync | |---|---| @@ -80,13 +85,10 @@ manifest, using the Oct 14 per-job durations: 51 of the 60 pull requests select only the groups they reach; 9 run everything, 6 of them because they edit the root `.gitattributes` and 3 -because they change files under `scripts/`. At the Oct 14 arrival rate -(792 syncs and 133 main pushes a day) that is about 55,000 runner-minutes -a day including the scheduled full runs, against 86,400 available at 60 -concurrent jobs. If the concurrency available to the repository stays at -the 30 to 38 jobs observed on the evening of Oct 14, the queue still -clears but with little headroom; that capacity question is outside this -change. +because they change files under `scripts/`. The mean estimated workload is +27% of the old workload. Actual queue recovery depends on runner capacity, +new arrivals, trace overhead and the historical replay copies. No queue-drain +time or hosted speedup is established by this model. ## How the declared inputs are known to be complete @@ -126,16 +128,30 @@ four times a day. The Lean builds of the formal packages run under the tracer too; their project trees are declared whole because Lake reads them densely. +Rechecking a saved recording with `--from-recording` requires its matching +group, current recording schema and explicit verification status. A failed +or incomplete recording cannot establish successful input coverage. Reuse +checks the saved observations; it does not rerun the verifier. + Regenerate a group's patterns locally with: ```sh python3 -B scripts/trace_verify_inputs.py --group community --output build/community.json --check --suggest ``` -The initial declarations were recorded locally on Python 3.14 (the -`gaussian` and `matrix` formal packages with their real Make targets; the -`historical` package's Python audits, with `formal/**` declared whole since -its Mathlib-backed build was not run locally). The first hosted runs on +The initial declarations were recorded locally on Python 3.14, including the +`gaussian` and `matrix` formal packages with their real Make targets. The +initial `historical` recording stopped before its source audits because +compiled Mathlib dependencies were unavailable. Those audits read notes, +certificates and upstream paper sources outside `formal/`; a declaration of +`formal/**` alone was insufficient. The pre-push audit fetched the pinned +Mathlib cache and successfully traced the complete `make formal-historical-verify` +target, including ranked-pair and machine-transfer compilation. Its 145 files, +43 directory listings, 3 directory-existence checks and 86 probes are covered +by 21 declared patterns. All three Lean project source trees stay declared +whole; external notes, certificates and upstream sections are explicit inputs. +The alternative `research/formal/` project discovery path is covered too. +No whole-tree Git access was observed in that complete recording. The first hosted runs on 3.11 and 3.13 are the check that nothing version-specific was missed; an undeclared input fails that job with the exact pattern to add. @@ -146,6 +162,18 @@ repository. Add the `ci:full-verify` label instead: the label event starts a full run on the pull request's merge commit, with its own concurrency group so it is not cancelled by later pushes, and every later push to a labelled pull request also runs everything. Remove and re-add the label to re-run. +Other label events follow the ordinary change-based plan and honor any existing +full-verification label; they cannot publish an empty successful replacement +for a real verification run. + +## Required checks + +The stable gate is `verify-summary`. On 2026-10-15 the GitHub branch API reported +`main` unprotected with no required status checks, and the repository ruleset +list was empty. If maintainers enable required checks, use this gate rather +than individual matrix or retired package-workflow check names. Selected-out +matrix combinations do not publish those former check names. This change does +not alter repository protection settings. ## Pushes and the schedule @@ -170,6 +198,8 @@ superseded. It never touches pushes, scheduled or manual runs, runs that share the newest head commit (re-runs, label-requested runs) or runs whose pull request it cannot identify unambiguously, and it inspects one created-at window per dispatch because the API lists at most 1000 runs. +Cancellation API failures make the maintenance workflow fail and identify the +affected run IDs; a dry run never sends cancellation requests. ## Trust boundary @@ -219,6 +249,7 @@ Local validation uses Linux, Python 3.14.4, strace 6.x and actionlint 1.7.12: actionlint .github/workflows/*.yml python3 -B -m unittest discover -s tests -p 'test_plan_verify_groups.py' -v python3 -B -m unittest discover -s tests -p 'test_trace_verify_inputs.py' -v +python3 -B -m unittest discover -s tests -p 'test_cancel_superseded_runs.py' -v python3 -B scripts/check_selected_ci_inputs.py python3 -B -m unittest discover -s tests -p test_selected_ci_inputs.py -v git diff --check @@ -296,3 +327,47 @@ checks. Both traced input-coverage audits pass, tracked artifacts remain unchanged, and temporary historical trees are removed. The recordings and logs under `build/` are local-only evidence; hosted execution and Python 3.11/3.13 execution of this repair are not claimed. + +The pre-push audit also ran the complete historical formal target on Linux +x86_64 / Python 3.14.4, Lean 4.21.0 and the pinned Mathlib revision +`308445d7985027f538e281e18df29ca16ede2ba3`: + +```sh +(cd formal/lean && lake exe cache get) +python3 -B scripts/trace_verify_inputs.py --group formal-historical --command 'make formal-historical-verify' --check --output build/verify-trace/push-audit-formal-historical.json +python3 -B scripts/trace_verify_inputs.py --group formal-historical --from-recording build/verify-trace/push-audit-formal-historical.json --check +``` + +The run passed 45 ranked-pair theorem audits, 298 machine-transfer declaration +audits, the main Lean build, 386 project axiom audits, source/literal consistency +checks and the paired-circuit reconstruction. The narrowed manifest covers the +successful complete recording. These are the existing scoped formal checks, +not a formal verification of the full multiplication theorem. Tracked artifacts +remain unchanged; the log and recording under `build/` are local-only evidence. + +The final staged audit fixes passed the complete test group again, including +all **130 test modules**, all 20 patch-application checks and the traced +input-coverage audit: + +```sh +python3 -B scripts/trace_verify_inputs.py --group tests --check --output build/verify-trace/push-audit-tests.json +git diff --exit-code +``` + +The added module tests cancellation boundaries without making live API writes. +Regression controls also cover unrelated label events, failed/incompatible +saved recordings, all 17 formal source references and both nearer Lean project +discovery paths. Independent review found no remaining input gap in the final +formal declaration. Scratch replay trees were removed and tracked artifacts +remained unchanged. Hosted execution and other Python versions remain unrun. + +## Attribution + +This CI maintenance work is by Sagar Thakrar with substantial Claude Fable 5.1 +and OpenAI Codex assistance, including independent pre-push code reviews. +It builds on Dennis's authenticated historical replay adapter and retains the +source credits listed in +[historical-ci-inputs/README.md](../scripts/historical-ci-inputs/README.md). +The optimized circuit implementations and their source-bound controls remain +Wentao Li's contributions. The earlier optional speedups listed above remain +opt-in. All new maintenance code is under the repository's Apache-2.0 license. diff --git a/scripts/cancel_superseded_runs.py b/scripts/cancel_superseded_runs.py index 8e30881a89..830b84c8f4 100644 --- a/scripts/cancel_superseded_runs.py +++ b/scripts/cancel_superseded_runs.py @@ -112,6 +112,8 @@ def main(argv=None): ap.add_argument('--cancel', action='store_true', help='actually cancel (default: report only)') ap.add_argument('--limit', type=int, default=0, help='cancel at most this many runs (0 = no limit)') args = ap.parse_args(argv) + if args.limit < 0: + ap.error('--limit must be nonnegative') runs = [] for status in ('queued', 'in_progress', 'waiting', 'pending'): @@ -141,13 +143,20 @@ def main(argv=None): for number, head in sorted(heads.items()): if head is None: print('pull request #%d: current head unknown; its runs are kept' % number) + failed = [] for run in targets: print('%s run %d %s PR #%d head %s created %s (%s)' % ( 'CANCEL' if args.cancel else 'would cancel', run['id'], run['path'].rsplit('/', 1)[-1], identities[run['id']][1], run['head_sha'][:8], run['created_at'], run['status'])) if args.cancel: - subprocess.run(['gh', 'api', '-X', 'POST', 'repos/%s/actions/runs/%d/cancel' % (args.repo, run['id'])], - check=False, stdout=subprocess.DEVNULL) + result = subprocess.run( + ['gh', 'api', '-X', 'POST', 'repos/%s/actions/runs/%d/cancel' % (args.repo, run['id'])], + check=False, stdout=subprocess.DEVNULL) + if result.returncode: + failed.append(run['id']) + if failed: + print('Cancellation failed for run(s): ' + ', '.join(map(str, failed)), file=sys.stderr) + return 1 return 0 diff --git a/scripts/plan_verify_groups.py b/scripts/plan_verify_groups.py index e1650e9912..0fe47dbb1d 100644 --- a/scripts/plan_verify_groups.py +++ b/scripts/plan_verify_groups.py @@ -247,11 +247,11 @@ def plan(manifest, event, changed=None, action=None, label=None, labels=(), diff mode, reason = 'full', 'full run requested' elif event in FULL_EVENTS: mode, reason = 'full', event + ' runs always verify everything' - elif event == 'pull_request' and action == 'labeled': - if label == full_label: - mode, reason = 'full', 'label ' + full_label + ' requests the full matrix' - else: - mode, reason = 'none', 'label event without ' + full_label + '; the regular run stands' + elif event == 'pull_request' and action == 'labeled' and label == full_label: + mode, reason = 'full', 'label ' + full_label + ' requests the full matrix' + # Other label events must follow the ordinary plan, including any existing + # full label. An empty successful run would publish the same summary check + # as a real verification run without establishing its result. elif full_label in labels: mode, reason = 'full', 'pull request carries ' + full_label elif diff_error: diff --git a/scripts/trace_verify_inputs.py b/scripts/trace_verify_inputs.py index 6702c152bd..94cf1a202c 100644 --- a/scripts/trace_verify_inputs.py +++ b/scripts/trace_verify_inputs.py @@ -689,6 +689,28 @@ def load_manifest(path): return json.loads(Path(path).read_text(encoding='utf-8')) +def load_recording(path, group): + """Reject incompatible or incomplete evidence before rechecking coverage.""" + recording = json.loads(Path(path).read_text(encoding='utf-8')) + if not isinstance(recording, dict): + raise ValueError('Recording must be an object') + if recording.get('group') != group: + raise ValueError('Recording group does not match --group') + if type(recording.get('recording_version')) is not int or recording['recording_version'] != RECORDING_VERSION: + raise ValueError('Unsupported recording version; record the group again') + if type(recording.get('exit_code')) is not int: + raise ValueError('Recording needs an integer exit_code') + if type(recording.get('tree')) is not bool: + raise ValueError('Recording needs a boolean tree flag') + for field in ('commands', 'files', 'dirs', 'exists', 'probes', 'subtrees'): + values = recording.get(field) + if not isinstance(values, list) or not all(isinstance(value, str) for value in values): + raise ValueError('Recording needs a string list for ' + field) + if not recording['commands']: + raise ValueError('Recording needs at least one command') + return recording + + def main(argv=None): ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) ap.add_argument('--group', required=True, help='verification group, e.g. community or ranked-pair-finite') @@ -702,7 +724,11 @@ def main(argv=None): args = ap.parse_args(argv) if args.from_recording: - code, recording = 0, json.loads(args.from_recording.read_text(encoding='utf-8')) + try: + recording = load_recording(args.from_recording, args.group) + except (OSError, ValueError) as error: + ap.error(str(error)) + code = recording['exit_code'] else: code, recording = record(args.group, args.command or group_commands(args.group)) if args.output: diff --git a/tests/test_cancel_superseded_runs.py b/tests/test_cancel_superseded_runs.py new file mode 100644 index 0000000000..e47211aa13 --- /dev/null +++ b/tests/test_cancel_superseded_runs.py @@ -0,0 +1,128 @@ +"""Cancellation must preserve current work and report failed API requests.""" +from contextlib import redirect_stderr, redirect_stdout +import importlib.util +import io +from pathlib import Path +from types import SimpleNamespace +import unittest +from unittest.mock import patch + + +ROOT = Path(__file__).resolve().parents[1] +spec = importlib.util.spec_from_file_location('cancel_superseded_runs', ROOT / 'scripts/cancel_superseded_runs.py') +cancel = importlib.util.module_from_spec(spec) +spec.loader.exec_module(cancel) + + +def run_record(number, head='old', event='pull_request', **fields): + return dict(id=number, event=event, path='.github/workflows/verify.yml', + head_sha=head, created_at='2026-10-14T00:00:00Z', status='queued', + pull_requests=[{'number': 42}], **fields) + + +class CandidateSelection(unittest.TestCase): + def test_only_identified_outdated_pull_request_heads_are_candidates(self): + records = [run_record(1), run_record(2, head='current'), + run_record(3, event='push'), run_record(4, event='schedule'), + run_record(5, event='workflow_dispatch'), run_record(6), run_record(7)] + identities = {i: ('.github/workflows/verify.yml', 42) for i in range(1, 6)} + identities[7] = ('.github/workflows/verify.yml', 43) + result = cancel.superseded(records, identities, {42: 'current', 43: None}) + self.assertEqual([r['id'] for r in result], [1]) + + def test_direct_identity_requires_exactly_one_pull_request(self): + record = run_record(1) + with patch.object(cancel, 'api') as api: + self.assertEqual(cancel.identify('base/repo', record, {}), (record['path'], 42)) + record['pull_requests'].append({'number': 43}) + self.assertIsNone(cancel.identify('base/repo', record, {})) + record['pull_requests'] = [] + self.assertIsNone(cancel.identify('base/repo', record, {})) + api.assert_not_called() + + def test_fork_lookup_binds_both_repository_and_branch_and_caches(self): + record = run_record(1, head_repository={'full_name': 'fork/repo'}, head_branch='topic') + record['pull_requests'] = [] + wrong_repo = {'number': 50, 'head': {'ref': 'topic', 'repo': {'full_name': 'fork/other'}}} + wrong_branch = {'number': 51, 'head': {'ref': 'other', 'repo': {'full_name': 'fork/repo'}}} + correct = {'number': 52, 'head': {'ref': 'topic', 'repo': {'full_name': 'fork/repo'}}} + cache = {} + with patch.object(cancel, 'api', return_value=[[wrong_repo, wrong_branch, correct]]) as api: + for _ in range(2): + self.assertEqual(cancel.identify('base/repo', record, cache), (record['path'], 52)) + api.assert_called_once() + self.assertIn('head=fork%3Atopic', api.call_args.args[0]) + + def test_ambiguous_fork_lookup_is_kept(self): + record = run_record(1, head_repository={'full_name': 'fork/repo'}, head_branch='topic') + record['pull_requests'] = [] + candidates = [{'number': n, 'head': {'ref': 'topic', 'repo': {'full_name': 'fork/repo'}}} + for n in (42, 43)] + with patch.object(cancel, 'api', return_value=[candidates]): + self.assertIsNone(cancel.identify('base/repo', record, {})) + + def test_current_head_comes_from_pull_request_and_is_cached(self): + cache = {} + with patch.object(cancel, 'api', return_value=[{'head': {'sha': 'current'}}]) as api: + self.assertEqual(cancel.current_head('base/repo', 42, cache), 'current') + self.assertEqual(cancel.current_head('base/repo', 42, cache), 'current') + api.assert_called_once_with('repos/base/repo/pulls/42') + + +class Command(unittest.TestCase): + def execute(self, args, records, returncodes=()): + stdout, stderr = io.StringIO(), io.StringIO() + with patch.object(cancel, 'list_runs', side_effect=[records, [], [], []]), \ + patch.object(cancel, 'current_head', return_value='current'), \ + patch.object(cancel.subprocess, 'run', + side_effect=[SimpleNamespace(returncode=c) for c in returncodes]) as post, \ + redirect_stdout(stdout), redirect_stderr(stderr): + code = cancel.main(['--repo', 'base/repo', '--created', '2026-10-14'] + args) + return code, post.call_args_list, stdout.getvalue(), stderr.getvalue() + + def test_dry_run_never_posts(self): + code, calls, out, err = self.execute([], [run_record(1)]) + self.assertEqual(code, 0) + self.assertEqual(calls, []) + self.assertIn('would cancel run 1', out) + self.assertEqual(err, '') + + def test_limit_bounds_cancellation(self): + code, calls, out, err = self.execute(['--cancel', '--limit', '1'], + [run_record(1), run_record(2)], [0]) + self.assertEqual(code, 0) + self.assertEqual(len(calls), 1) + self.assertEqual(calls[0].args[0], + ['gh', 'api', '-X', 'POST', 'repos/base/repo/actions/runs/1/cancel']) + self.assertNotIn('CANCEL run 2', out) + self.assertEqual(err, '') + + def test_zero_limit_cancels_all_outdated_heads_only(self): + records = [run_record(1), run_record(2, head='current'), run_record(3, event='push'), + run_record(4, event='schedule'), run_record(5, event='workflow_dispatch'), + run_record(6)] + code, calls, out, err = self.execute(['--cancel', '--limit', '0'], records, [0, 0]) + self.assertEqual(code, 0) + self.assertEqual([c.args[0][-1] for c in calls], + ['repos/base/repo/actions/runs/1/cancel', 'repos/base/repo/actions/runs/6/cancel']) + self.assertEqual(err, '') + + def test_failed_post_does_not_prevent_other_cancellations_and_fails_command(self): + code, calls, out, err = self.execute(['--cancel'], [run_record(1), run_record(2)], [1, 0]) + self.assertEqual(code, 1) + self.assertEqual(len(calls), 2) + self.assertIn('Cancellation failed for run(s): 1', err) + self.assertNotIn('run(s): 1, 2', err) + + def test_negative_limit_is_rejected_before_querying_or_posting(self): + with patch.object(cancel, 'list_runs') as query, patch.object(cancel.subprocess, 'run') as post, \ + redirect_stderr(io.StringIO()) as err, self.assertRaises(SystemExit) as error: + cancel.main(['--repo', 'base/repo', '--created', '2026-10-14', '--cancel', '--limit', '-1']) + self.assertEqual(error.exception.code, 2) + self.assertIn('--limit must be nonnegative', err.getvalue()) + query.assert_not_called() + post.assert_not_called() + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_plan_verify_groups.py b/tests/test_plan_verify_groups.py index e220d72f45..1d9dd99f25 100644 --- a/tests/test_plan_verify_groups.py +++ b/tests/test_plan_verify_groups.py @@ -4,6 +4,7 @@ import os from pathlib import Path import re +import runpy import subprocess import tempfile import unittest @@ -257,9 +258,24 @@ def test_missing_or_failed_diff_fails_closed(self): def test_full_label(self): self.assertEqual(run_plan([], action='labeled', label='ci:full-verify')['mode'], 'full') - self.assertEqual(run_plan([], action='labeled', label='needs-review')['mode'], 'none') self.assertEqual(run_plan(['A:research/x/y'], labels=['ci:full-verify'])['mode'], 'full') + def test_unrelated_label_preserves_existing_full_request(self): + result = run_plan(['M:research/beta-package/words.json'], action='labeled', + label='needs-review', labels=['ci:full-verify', 'needs-review']) + self.assertEqual(result['mode'], 'full') + self.assertEqual(result['groups'], ALL_GROUPS) + + def test_unrelated_label_verifies_the_same_changes_as_a_regular_run(self): + for changed, options in ((['M:research/beta-package/words.json'], {}), + (['M:scripts/exclusion_circuit.py'], {}), + (None, {'diff_error': 'merge parent unavailable'})): + with self.subTest(changed=changed, options=options): + expected = run_plan(changed, **options) + result = run_plan(changed, action='labeled', label='needs-review', + labels=['needs-review'], **options) + self.assertEqual(result, expected) + def test_unknown_event_runs_everything(self): self.assertEqual(run_plan(['A:research/x/y'], event='merge_group')['mode'], 'full') @@ -328,6 +344,38 @@ def test_github_output_and_summary(self): class RepositoryManifest(unittest.TestCase): """The committed manifest must match the Makefile's CI groups and validate.""" + def test_new_nearer_lean_project_selects_historical_formal(self): + manifest = planner.load_manifest(ROOT / '.github/verify-groups.json') + base_dirs = {'formal', 'formal/lean', 'research', 'research/ranked-pair-verification', + 'research/ranked-pair-verification/lean'} + # ranked-pair's default_project probes these nearer ancestors before + # formal/lean. Creating a toolchain file can change the project it uses. + for directory in ('research/formal/lean', 'research/ranked-pair-verification/formal/lean'): + head_dirs = base_dirs | {directory, directory.rsplit('/', 1)[0]} + for event in ('pull_request', 'push'): + with self.subTest(directory=directory, event=event): + result = planner.plan(manifest, event, ['A:' + directory + '/lean-toolchain'], + base_dirs=base_dirs, head_dirs=head_dirs) + self.assertEqual(result['mode'], 'selected', result['reason']) + self.assertIn('formal-historical', result['groups']) + self.assertIn({'package': 'historical'}, result['formal']) + + def test_historical_formal_follows_its_external_source_references(self): + manifest = planner.load_manifest(ROOT / '.github/verify-groups.json') + sources = runpy.run_path(str(ROOT / 'formal/lean/sources.py')) + # The source audit runs after compilation and reads notes, certificate + # values and upstream paper lines outside the formal project tree. + paths = {ref.path for row in sources['ROWS'] for ref in row[3]} + self.assertIn('notes/compact-control-note.tex', paths) + self.assertIn('certificates/compact-control-layer.json', paths) + self.assertIn('upstream/build/sections/03-motifs.tex', paths) + for event in ('pull_request', 'push'): + for path in sorted(paths): + with self.subTest(event=event, path=path): + result = planner.plan(manifest, event, ['M:' + path]) + self.assertIn('formal-historical', result['groups'], result['reason']) + self.assertIn({'package': 'historical'}, result['formal']) + def test_manifest_loads_and_groups_match_makefile(self): manifest = planner.load_manifest(ROOT / '.github/verify-groups.json') self.assertEqual(manifest['python'], ['3.11', '3.13', '3.14']) diff --git a/tests/test_trace_verify_inputs.py b/tests/test_trace_verify_inputs.py index 91a59d4072..55376b5134 100644 --- a/tests/test_trace_verify_inputs.py +++ b/tests/test_trace_verify_inputs.py @@ -1,8 +1,10 @@ """Recorded verification inputs must be parsed, classified and covered correctly.""" import importlib.util +import json import os from pathlib import Path import subprocess +import sys import tempfile import unittest @@ -339,5 +341,52 @@ def test_group_commands_match_the_workflow(self): ['make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream']) +class SavedRecordings(unittest.TestCase): + def recording(self): + return dict(group='clones', commands=tracer.group_commands('clones'), + files=[], dirs=[], exists=[], probes=[], subtrees=[], tree=False, + exit_code=0, recording_version=tracer.RECORDING_VERSION) + + def recheck(self, recording): + with tempfile.TemporaryDirectory() as td: + path = Path(td) / 'recording.json' + path.write_text(json.dumps(recording), encoding='utf-8') + return subprocess.run([sys.executable, '-B', str(ROOT / 'scripts/trace_verify_inputs.py'), + '--group', 'clones', '--from-recording', str(path), '--check'], + cwd=ROOT, capture_output=True, text=True) + + def test_successful_recording_can_be_rechecked(self): + result = self.recheck(self.recording()) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('PASS_DECLARED_INPUTS_COVER_RECORDING group=clones', result.stdout) + + def test_partial_recording_keeps_verification_failure(self): + recording = self.recording() + recording['exit_code'] = 7 + result = self.recheck(recording) + self.assertEqual(result.returncode, 7, result.stderr) + self.assertIn('VERIFICATION_FAILED exit=7', result.stdout) + self.assertNotIn('PASS_DECLARED_INPUTS', result.stdout) + + def test_wrong_group_old_schema_and_incomplete_evidence_reject(self): + mutations = [('group', 'community'), ('recording_version', tracer.RECORDING_VERSION - 1), + ('recording_version', True), ('exit_code', False), ('tree', 'false'), + ('files', 'Makefile'), ('probes', [None]), ('commands', [])] + for field, value in mutations: + with self.subTest(field=field, value=value): + recording = self.recording() + recording[field] = value + result = self.recheck(recording) + self.assertEqual(result.returncode, 2, result.stderr) + self.assertNotIn('PASS_DECLARED_INPUTS', result.stdout) + for field in ('exit_code', 'dirs', 'subtrees'): + with self.subTest(missing=field): + recording = self.recording() + del recording[field] + result = self.recheck(recording) + self.assertEqual(result.returncode, 2, result.stderr) + self.assertNotIn('PASS_DECLARED_INPUTS', result.stdout) + + if __name__ == '__main__': unittest.main()