diff --git a/.github/verify-groups.json b/.github/verify-groups.json new file mode 100644 index 0000000000..2fddc194dc --- /dev/null +++ b/.github/verify-groups.json @@ -0,0 +1,811 @@ +{ + "_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": "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/**", + "upstream/build/sections/03-motifs.tex", + "upstream/build/sections/05-layers.tex", + "upstream/build/sections/08-assembly.tex" + ] + }, + "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 0b88bd2639..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,19 +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 - python -B scripts/replay_historical_check.py skip-clones - make 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: @@ -63,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: @@ -87,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..689b40c29d --- /dev/null +++ b/docs/ci.md @@ -0,0 +1,439 @@ +# 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 + +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. +- 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 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). 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 + +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 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 + 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 (`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 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. +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. + +## Estimated effect + +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 | +|---|---| +| 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/`. 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 + +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. + +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, 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. + +## 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. +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 + +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. +Cancellation API failures make the maintenance workflow fail and identify the +affected run IDs; a dry run never sends cancellation requests. + +## 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 -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 +``` + +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. + +## 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. + +After merging current main, the exclusion and shared-point inputs come from +Wentao Li's retained research baselines, with the same authenticated bytes as +the reference snapshots above. The adapter also retains main's checks that +each baseline is tracked and that live helpers match an explicitly accepted +successor, including the newer shared-point initialization and frame cache. +Unknown live source changes reject before a replay tree is created. + +Main's partial-swap digest/initialization changes also affect both historical +clone manifests. Their additional `scripts/partial_swap/shared.py` input is +restored from `research/partial-swap-digest/baseline.py`, which matches the +original `0b1cccf86e2f5132ed286a26ef0a681a495740ea` bytes. The accepted live +digests come from Wentao Li's retained digest and initialization packages; +their live optimization tests continue to use the current implementation. + +The subsequent sparse-fusion optimization is handled the same way: split-skip +uses `research/sparse-fusion-orbits-production/baseline.py` for its original +`scripts/audit_sparse_fusion.py` pin and accepts only the retained production +successor. The optimized live checker stays unchanged. + +The clones group now runs: + +```sh +python3 -B scripts/replay_historical_check.py skip-clones +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 native +producer (with the original Makefile arguments), witness, +independent arithmetic and unit tests, now with all five historical inputs +authenticated. The producer runs inside the replay copy because its inherited +skip-strips source check also pins the original partial-swap helper. +The original source-bound Makefile targets remain frozen; use these adapters +to replay those checkpoints against a modern checkout. + +`make verify-tests` retains main's isolated runner dispatch to `skip-clones-tests`. +`test_skip_clones.py` also uses this isolated context during direct unittest +discovery. 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. + +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. + +## Conflict-resolution validation + +The conflict refresh merges PR head +`91669e2a3316751ceba6330d19b09fdf5e6b95aa` with canonical main +`ab4fcd39c74effa88d464ed1d80ec832f6020e51`. It keeps main's authenticated +research baselines, accepted-live-source checks and isolated test-runner +dispatch, alongside the PR's traced CI selection and temporary-tree cleanup. +The partial-swap and sparse-fusion additions above cover the newer source +optimizations without editing their implementations or frozen manifests. + +On Linux x86_64 / Python 3.14.4, the complete traced clones group passed both +native reconstructions, all 4,073,300 data pairs, 21 package tests, the copied +artifact integrity gates and declared-input coverage. The six focused CI +modules passed 120 tests; the three updated upstream compatibility modules +passed another 21. Workflow lint (actionlint 1.7.12), selected-record checks, +selected CI input checks and the PR diff whitespace check also passed. + +```sh +python3 -B scripts/trace_verify_inputs.py --group clones --check --output build/verify-trace/pr2361-updated-base-clones.json +for module in historical_check plan_verify_groups trace_verify_inputs cancel_superseded_runs selected_ci_inputs isolated_test_runner disjoint_tensor_support_masks exclusion_embedding_masks exclusion_support_masks; do + python3 -B -m unittest discover -s tests -p "test_${module}.py" -v || exit +done +``` + +The full `tests` group was also run on the initial merge with main +`c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5`: all 139 modules executed, but ten +failed, so the subsequent patch-application checks were not reached. Updated +main fixed the disjoint-tensor and two exclusion compatibility modules; their +reruns are included above. The other seven failures were independently +reproduced in an untouched worktree at `ab4fcd39c`: + +- `test_copied_fixed.py`, `test_copied_fixed_reversed.py`, + `test_pair_assembly.py`, `test_skip_strips.py` and `test_skip_suffix.py` + reject the updated live `scripts/partial_swap/shared.py` source pin. +- `test_shared_point_digest.py` still expects the earlier production digest. +- `test_split_skip.py` encounters a tuple-shape mismatch with the live helper. + +These existing upstream failures are not suppressed. The full tests group was +not rerun after the base refresh, and this resolution does not claim a green +full suite. Logs and recordings under `build/pr2361-*.log` and +`build/verify-trace/pr2361-*.json` are local-only evidence, including the +untouched-upstream reproduction in `build/pr2361-upstream-failures.log`. +Tracked artifacts did not drift. The selected cold replay and Python 3.11/3.13 +were not rerun; the selected record, supplier sources and frozen evidence are +unchanged by this PR. + +## 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 new file mode 100644 index 0000000000..830b84c8f4 --- /dev/null +++ b/scripts/cancel_superseded_runs.py @@ -0,0 +1,164 @@ +#!/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) + if args.limit < 0: + ap.error('--limit must be nonnegative') + + 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) + 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: + 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 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/scripts/historical-ci-inputs/README.md b/scripts/historical-ci-inputs/README.md index 60fc82c1e2..cb06332015 100644 --- a/scripts/historical-ci-inputs/README.md +++ b/scripts/historical-ci-inputs/README.md @@ -18,25 +18,54 @@ 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` | -The split-skip replay restores all three exact helpers named by its unchanged +The split-skip replay restores all five changed helpers named by its unchanged manifest: the fused-block snapshot above, the exclusion circuit preserved in -`research/exclusion-embedding-masks/baseline.py`, and the shared-point circuit -preserved in `research/shared-point-digest/baseline.py`. The latter two are -Wentao Li's retained baselines for the accepted support-mask and digest -optimizations. Both also match the PR53 parent `3ffd4021995c959ac02d12920e0279ae97dd03c7`. +`research/exclusion-embedding-masks/baseline.py`, the shared-point circuit +preserved in `research/shared-point-digest/baseline.py`, the partial-swap +shared-point helper in `research/partial-swap-digest/baseline.py`, and the sparse +fusion checker in `research/sparse-fusion-orbits-production/baseline.py`. These are +Wentao Li's retained baselines for the accepted support-mask, digest, +initialization and spectator-orbit optimizations. The sparse-fusion package +retains ToikY's orbit argument and Douglas R. Colkitt's original screen credit. +The exclusion and canonical shared-point copies +also match the PR53 parent `3ffd4021995c959ac02d12920e0279ae97dd03c7`. +The partial-swap baseline matches `0b1cccf86e2f5132ed286a26ef0a681a495740ea` +and both clone manifests. The exclusion and shared-point snapshots in this +directory are retained exact reference copies; the replay uses the attributed +research baselines above. The skip-clones replay restores both its exclusion +and partial-swap dependencies. Each replacement and reviewed live successor is independently authenticated; missing pins, corrupted baselines, duplicate paths, untracked dependencies and unknown live source changes reject before copying. No original checker is edited. 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. +formally verify the full multiplication theorem. The native R420 checks remain +required in their CI job; the split-skip replay includes its native producer. + +The `skip-clones` replay includes the complete native producer, certificate +regeneration and adversarial tests. `split-skip` authenticates all five of +its historical replacements before copying anything. Its original native +producer command runs inside the same authenticated tree before the witnesses, +because its inherited skip-strips checker also pins the partial-swap helper. +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</`` 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' 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: + 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/replay_historical_check.py b/scripts/replay_historical_check.py index 32ca230832..f35a1899e3 100644 --- a/scripts/replay_historical_check.py +++ b/scripts/replay_historical_check.py @@ -5,6 +5,7 @@ The checkers, their pins, and the live selected record remain unchanged. """ import argparse +from contextlib import contextmanager import hashlib import json from pathlib import Path, PurePosixPath @@ -41,7 +42,9 @@ 'path': 'scripts/audit_fused_block.py', 'input': 'audit_fused_block.py', 'sha256': '2afb83ca8e5f193ca8a4c242becf267ad1d9dc2578ba238b820e98d5185f6288', - 'commands': [['research/split-skip/witness.py'], + 'commands': [['research/split-skip/producer.py', '--work-dir', 'build/split-skip', + '--output', 'build/split-skip-receipt.json'], + ['research/split-skip/witness.py'], ['research/split-skip/independent_arithmetic.py'], ['-m', 'unittest', 'discover', '-s', 'tests', '-p', 'test_split_skip.py', '-v']], }, @@ -62,6 +65,17 @@ 'accepted_live_sha256': [ 'f9fbcd6e85e442cbd0926ac0887414e20735b2dc923d2d5822c803ceb46726d3', ], + 'additional_inputs': [{ + 'manifest': 'research/skip-clones/SOURCE.json', 'field': 'files', + 'path': 'scripts/partial_swap/shared.py', 'input_from_root': True, + 'input': 'research/partial-swap-digest/baseline.py', + 'sha256': '81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34', + # Wentao Li's retained digest and initialization successors. + 'accepted_live_sha256': [ + 'b27c8bfe1de3f7d2d5fb19ac742adf11597c2aaa7add68430443119997e646e8', + '7290bd639600aecff11941d3faf95c9ce95589125cc6a7f7440fb86af7a0f17c', + ], + }], 'commands': [ ['research/skip-clones/producer.py'], ['research/skip-clones/witness.py', '--output', @@ -76,13 +90,24 @@ } -# The split-skip manifest binds three historical helpers. Restore each exact -# dependency, retaining Wentao Li's two optimized live successors unchanged. +# The split-skip manifest binds five historical helpers. Restore each exact +# dependency, retaining Wentao Li's optimized live successors unchanged. CONFIG['split-skip']['accepted_live_sha256'] = [ '6fe64f886309d9154e33a3d67a16e8714cebc424a7a248b3080f8cab7d94179b', ] CONFIG['split-skip']['additional_inputs'] = [ {**CONFIG['skip-clones'], 'manifest': 'research/split-skip/SOURCE.json'}, + {**CONFIG['skip-clones']['additional_inputs'][0], + 'manifest': 'research/split-skip/SOURCE.json'}, + { + 'manifest': 'research/split-skip/SOURCE.json', 'field': 'files', + 'path': 'scripts/audit_sparse_fusion.py', 'input_from_root': True, + 'input': 'research/sparse-fusion-orbits-production/baseline.py', + 'sha256': 'bbaa32f9786f083409e363b081bfb7a1e597c8d32e4183c13a4105c2170934ce', + 'accepted_live_sha256': [ + '6d1997fba802a8fc41099996b29e3add5d2b4f904da02548a98bed32c50aa773', + ], + }, { 'manifest': 'research/split-skip/SOURCE.json', 'field': 'files', 'path': 'scripts/shared_point_circuit.py', 'input_from_root': True, @@ -135,18 +160,25 @@ def tracked_paths(root): return [p.decode('utf-8') for p in raw.split(b'\0') if p] +def input_configs(config): + """Each replacement has an explicit pin in the same predecessor manifest.""" + result = [config] + result.extend(dict(item, manifest=config['manifest'], field=config['field']) + for item in config.get('additional_inputs', [])) + require(len({item['path'] for item in result}) == len(result), + 'Duplicate historical replacement') + return result + + def materialize(root, destination, config, paths, inputs=INPUTS): """Copy tracked working bytes only; never share writable links with the checkout.""" - configurations = [config, *config.get('additional_inputs', [])] - replacements = {} - for entry in configurations: - require(entry['path'] not in replacements, 'Duplicate historical replacement') - data = authenticated_input(root, entry, inputs) - require(entry['path'] in paths and entry['manifest'] in paths, + replacements = [(item, authenticated_input(root, item, inputs)) + for item in input_configs(config)] + for item, _ in replacements: + require(item['path'] in paths and item['manifest'] in paths, 'Historical input or manifest is not tracked') - if entry.get('input_from_root'): - require(entry['input'] in paths, 'Historical baseline is not tracked') - replacements[entry['path']] = data + if item.get('input_from_root'): + require(item['input'] in paths, 'Historical baseline is not tracked') require(not destination.exists(), 'Replay destination already exists') destination.mkdir(parents=True) expected = {} @@ -157,12 +189,12 @@ def materialize(root, destination, config, paths, inputs=INPUTS): target.parent.mkdir(parents=True, exist_ok=True) shutil.copyfile(source, target) expected[name] = hashlib.sha256(target.read_bytes()).hexdigest() - for entry in configurations: - safe_path(destination, entry['path']).write_bytes(replacements[entry['path']]) - expected[entry['path']] = entry['sha256'] + for item, data in replacements: + safe_path(destination, item['path']).write_bytes(data) + expected[item['path']] = item['sha256'] # Authenticate every replacement again before executing any checker. - for entry in configurations: - authenticated_input(destination, entry, inputs) + for item, _ in replacements: + authenticated_input(destination, item, inputs) return expected @@ -174,6 +206,26 @@ def verify_unchanged(snapshot, expected): 'Replay changed tracked artifact: ' + name) +@contextmanager +def replay_tree(package, root=ROOT): + """Yield an isolated historical checkout, checking tracked bytes on exit. + + The tracked tree is several GB. Keep the copy on the checkout's build + filesystem, rather than consuming a memory-backed /tmp in concurrent tests. + """ + config = CONFIG[package] + paths = tracked_paths(root) + scratch = root / 'build' + scratch.mkdir(exist_ok=True) + with tempfile.TemporaryDirectory(prefix='historical-ci-', dir=scratch) as temporary: + snapshot = Path(temporary) / 'repo' + expected = materialize(root, snapshot, config, paths) + try: + yield snapshot + finally: + verify_unchanged(snapshot, expected) + + def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('package', choices=CONFIG) @@ -181,17 +233,13 @@ def main(): args = parser.parse_args() require(not args.native or args.package == 'r420', '--native applies only to r420') config = CONFIG[args.package] - paths = tracked_paths(ROOT) - with tempfile.TemporaryDirectory(prefix='historical-ci-') as temporary: - snapshot = Path(temporary) / 'repo' - print('REPLAY_HISTORICAL_CHECK', args.package, 'copying tracked inputs', flush=True) - expected = materialize(ROOT, snapshot, config, paths) + print('REPLAY_HISTORICAL_CHECK', args.package, 'copying tracked inputs', flush=True) + with replay_tree(args.package) as snapshot: commands = list(config['commands']) if args.native: commands.append(['research/r420-two-sided-basis/native.py']) for command in commands: subprocess.run([sys.executable, '-B'] + command, cwd=snapshot, check=True) - verify_unchanged(snapshot, expected) print('PASS_HISTORICAL_CHECK', args.package, 'input_sha256=' + config['sha256'], flush=True) diff --git a/scripts/trace_verify_inputs.py b/scripts/trace_verify_inputs.py new file mode 100644 index 0000000000..795fb63d0d --- /dev/null +++ b/scripts/trace_verify_inputs.py @@ -0,0 +1,761 @@ +#!/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': ['python3 -B scripts/replay_historical_check.py skip-clones', + '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 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') + 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: + 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: + 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_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_historical_check.py b/tests/test_historical_check.py index 0f9c8f732d..1e6a33772a 100644 --- a/tests/test_historical_check.py +++ b/tests/test_historical_check.py @@ -3,6 +3,7 @@ import importlib.util import json from pathlib import Path +import shlex import tempfile import unittest from unittest.mock import patch @@ -175,15 +176,115 @@ def test_all_split_skip_dependencies_match_frozen_manifest(self): entries = [config, *config['additional_inputs']] self.assertEqual({entry['path'] for entry in entries}, { 'scripts/audit_fused_block.py', 'scripts/exclusion_circuit.py', - 'scripts/shared_point_circuit.py'}) + 'scripts/partial_swap/shared.py', 'scripts/shared_point_circuit.py', + 'scripts/audit_sparse_fusion.py'}) for entry in entries: with self.subTest(path=entry['path']): checker.authenticated_input(ROOT, entry) + def test_clone_overlays_cover_every_changed_frozen_input(self): + for package in ('skip-clones', 'skip-clones-tests', 'split-skip'): + config = checker.CONFIG[package] + replacements = { + entry['path']: checker.authenticated_input(ROOT, entry) + for entry in checker.input_configs(config) + } + pins = json.loads((ROOT / config['manifest']).read_bytes())['files'] + for path, digest in pins.items(): + with self.subTest(package=package, path=path): + data = replacements[path] if path in replacements else (ROOT / path).read_bytes() + self.assertEqual(hashlib.sha256(data).hexdigest(), digest) + + def test_split_skip_replay_preserves_native_make_recipe(self): + makefile = (ROOT / 'Makefile').read_text() + recipe = makefile.split('\nsplit-skip-producer:\n', 1)[1].splitlines()[0] + command = shlex.split(recipe) + self.assertEqual(command[0], 'python3') + self.assertEqual(checker.CONFIG['split-skip']['commands'][0], command[1:]) + + def test_root_baselines_must_be_tracked_before_copy(self): + for additional in (False, True): + with self.subTest(additional=additional), tempfile.TemporaryDirectory() as td: + root, inputs, config, paths = self.multi_fixture(td) + entry = config['additional_inputs'][0] if additional else config + original = (inputs / entry['input']).read_bytes() + (root / 'baseline.txt').write_bytes(original) + entry.update(input='baseline.txt', input_from_root=True) + target = Path(td) / 'copy' + with self.assertRaisesRegex(ValueError, 'Historical baseline is not tracked'): + checker.materialize(root, target, config, paths, inputs) + self.assertFalse(target.exists()) + expected = checker.materialize(root, target, config, paths + ['baseline.txt'], inputs) + self.assertEqual((target / entry['path']).read_bytes(), original) + checker.verify_unchanged(target, expected) + def test_real_snapshots_match_unchanged_predecessor_pins(self): for name, config in checker.CONFIG.items(): - with self.subTest(package=name): - checker.authenticated_input(ROOT, config) + for item in checker.input_configs(config): + with self.subTest(package=name, path=item['path']): + checker.authenticated_input(ROOT, item) + + def add_input(self, root, inputs, config, paths): + data = b'second historical input\n' + (inputs/'second.txt').write_bytes(data) + (root/'second.py').write_bytes(b'current optimized implementation\n') + digest = hashlib.sha256(data).hexdigest() + manifest = json.loads((root/'manifest.json').read_text()) + manifest['files']['second.py'] = digest + (root/'manifest.json').write_text(json.dumps(manifest)) + config['additional_inputs'] = [dict(path='second.py', input='second.txt', sha256=digest)] + paths.append('second.py') + + def test_every_replacement_is_authenticated_and_drift_checked(self): + with tempfile.TemporaryDirectory() as td: + root, inputs, config, paths = self.fixture(td) + self.add_input(root, inputs, config, paths) + before = {p: (root/p).read_bytes() for p in paths} + target = Path(td)/'copy' + expected = checker.materialize(root, target, config, paths, inputs) + for item in checker.input_configs(config): + self.assertEqual((target/item['path']).read_bytes(), (inputs/item['input']).read_bytes()) + checker.verify_unchanged(target, expected) + (target/'second.py').write_bytes(b'corrupted replacement') + with self.assertRaisesRegex(ValueError, 'Replay changed tracked artifact: second.py'): + checker.verify_unchanged(target, expected) + self.assertEqual({p: (root/p).read_bytes() for p in paths}, before) + + def test_bad_additional_input_pin_or_tracking_rejects_before_copy(self): + for corruption in ('blob', 'pin', 'untracked', 'duplicate'): + with self.subTest(corruption=corruption), tempfile.TemporaryDirectory() as td: + root, inputs, config, paths = self.fixture(td) + self.add_input(root, inputs, config, paths) + if corruption == 'blob': + (inputs/'second.txt').write_bytes(b'changed historical input') + elif corruption == 'pin': + manifest = json.loads((root/'manifest.json').read_text()) + del manifest['files']['second.py'] + (root/'manifest.json').write_text(json.dumps(manifest)) + elif corruption == 'untracked': + paths.remove('second.py') + else: + config['additional_inputs'].append(config['additional_inputs'][0]) + target = Path(td)/'copy' + with self.assertRaises(ValueError): + checker.materialize(root, target, config, paths, inputs) + self.assertFalse(target.exists()) + + def test_context_checks_drift_and_removes_scratch_tree(self): + with tempfile.TemporaryDirectory() as td: + root, inputs, config, paths = self.fixture(td) + materialize = checker.materialize + def copy(*args): + return materialize(*args, inputs=inputs) + with patch.dict(checker.CONFIG, fixture=config), \ + patch.object(checker, 'tracked_paths', return_value=paths), \ + patch.object(checker, 'materialize', side_effect=copy): + with self.assertRaisesRegex(ValueError, 'Replay changed tracked artifact'): + with checker.replay_tree('fixture', root) as snapshot: + self.assertEqual(snapshot.parent.parent, root/'build') + (snapshot/'unrelated.py').write_bytes(b'changed during replay') + self.assertFalse(snapshot.exists()) + self.assertEqual((root/'unrelated.py').read_bytes(), b'unchanged checker bytes\n') if __name__ == '__main__': diff --git a/tests/test_plan_verify_groups.py b/tests/test_plan_verify_groups.py new file mode 100644 index 0000000000..1d9dd99f25 --- /dev/null +++ b/tests/test_plan_verify_groups.py @@ -0,0 +1,418 @@ +"""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 runpy +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(['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') + + 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_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']) + 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_skip_clones.py b/tests/test_skip_clones.py index 7c76dfbc00..f80f971830 100644 --- a/tests/test_skip_clones.py +++ b/tests/test_skip_clones.py @@ -3,12 +3,25 @@ from copy import copy, deepcopy from pathlib import Path from fractions import Fraction as Q +from hashlib import sha256 from unittest.mock import patch import importlib.util import sys import unittest ROOT = Path(__file__).resolve().parents[1] +# This is a frozen source-bound certificate. Modern circuit optimizations are +# tested against the live checkout in their own modules; these controls use +# the exact predecessor input without changing either implementation or pin. +spec = importlib.util.spec_from_file_location('clone_historical_replay', ROOT/'scripts/replay_historical_check.py') +historical = importlib.util.module_from_spec(spec) +spec.loader.exec_module(historical) +configs = historical.input_configs(historical.CONFIG['skip-clones']) +for config in configs: + historical.authenticated_input(ROOT, config) +if any(sha256((ROOT/config['path']).read_bytes()).hexdigest() != config['sha256'] + for config in configs): + ROOT = unittest.enterModuleContext(historical.replay_tree('skip-clones', ROOT)) HERE = ROOT/'research/skip-clones' sys.path.insert(0, str(HERE)) spec = importlib.util.spec_from_file_location('skip_clones_tests_module', HERE/'cloned_graph.py') diff --git a/tests/test_trace_verify_inputs.py b/tests/test_trace_verify_inputs.py new file mode 100644 index 0000000000..2d0fa016bd --- /dev/null +++ b/tests/test_trace_verify_inputs.py @@ -0,0 +1,391 @@ +"""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 + +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'), + ['python3 -B scripts/replay_historical_check.py skip-clones', + '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']) + + +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()