diff --git a/.github/workflows/community-batch1047.yml b/.github/workflows/community-batch1047.yml index d34cc7fe9e..abfbf45388 100644 --- a/.github/workflows/community-batch1047.yml +++ b/.github/workflows/community-batch1047.yml @@ -87,6 +87,8 @@ jobs: - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 with: python-version: '3.12' + - name: Fetch immutable tree required by the PR946 historical inventory + run: git fetch --no-tags --depth=1 https://github.com/CrocSwap/integer-mult-bounds.git 407d52ff15b2217b6e22bce44728b4c3907b6515 - name: Install exact native replay dependencies run: | sudo apt-get update diff --git a/.github/workflows/community-reconciliation92.yml b/.github/workflows/community-reconciliation92.yml index 8cdc78c070..3e7991db91 100644 --- a/.github/workflows/community-reconciliation92.yml +++ b/.github/workflows/community-reconciliation92.yml @@ -3,6 +3,9 @@ on: push: paths: - 'research/community-reconciliation92-audit/**' + - 'scripts/replay_historical_check.py' + - 'scripts/historical-ci-inputs/**' + - 'tests/test_historical_check.py' - 'scripts/run_parallel.py' - 'scripts/verify_parallel.py' - 'tests/test_parallel_verification.py' @@ -10,6 +13,9 @@ on: pull_request: paths: - 'research/community-reconciliation92-audit/**' + - 'scripts/replay_historical_check.py' + - 'scripts/historical-ci-inputs/**' + - 'tests/test_historical_check.py' - 'scripts/run_parallel.py' - 'scripts/verify_parallel.py' - 'tests/test_parallel_verification.py' @@ -26,6 +32,6 @@ jobs: with: python-version: '3.12' - name: Check provenance and scoped dispositions (not a mathematical replay) - run: python3 research/community-reconciliation92-audit/verify.py + run: python3 -B scripts/replay_historical_check.py reconciliation92 - name: Check worker isolation and rejection controls run: python3 -m unittest discover -s tests -p test_parallel_verification.py -v diff --git a/.github/workflows/r420-two-sided-basis.yml b/.github/workflows/r420-two-sided-basis.yml index 9fe99e36b0..d0e0df3495 100644 --- a/.github/workflows/r420-two-sided-basis.yml +++ b/.github/workflows/r420-two-sided-basis.yml @@ -4,10 +4,16 @@ on: push: paths: - 'research/r420-two-sided-basis/**' + - 'scripts/replay_historical_check.py' + - 'scripts/historical-ci-inputs/**' + - 'tests/test_historical_check.py' - '.github/workflows/r420-two-sided-basis.yml' pull_request: paths: - 'research/r420-two-sided-basis/**' + - 'scripts/replay_historical_check.py' + - 'scripts/historical-ci-inputs/**' + - 'tests/test_historical_check.py' - '.github/workflows/r420-two-sided-basis.yml' workflow_dispatch: @@ -29,14 +35,14 @@ jobs: - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 with: python-version: ${{ matrix.python-version }} - - run: python -B research/r420-two-sided-basis/verify.py - - run: python -B -m unittest discover -s research/r420-two-sided-basis -p 'test_*.py' - name: Install Boost for unchanged C++ checkers if: matrix.python-version == '3.13' run: | sudo apt-get update -qq sudo apt-get install -y --no-install-recommends libboost-dev - - name: Fresh C++ legality and multistage columns - if: matrix.python-version == '3.13' - run: CXX=g++ python -B research/r420-two-sided-basis/native.py + - name: Replay unchanged Python and native checkers with historical inputs + env: + CXX: g++ + NATIVE: ${{ matrix.python-version == '3.13' && '--native' || '' }} + run: python -B scripts/replay_historical_check.py r420 $NATIVE - run: git diff --exit-code diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index bc1741b08f..4446616e87 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -24,6 +24,9 @@ jobs: - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 with: python-version: ${{ matrix.python-version }} + - name: Fetch immutable baseline required by performance regression tests + if: matrix.group == 'tests' + run: git fetch --no-tags --depth=1 https://github.com/CrocSwap/integer-mult-bounds.git 0b1cccf86e2f5132ed286a26ef0a681a495740ea - name: Install headers for the exact enlarged-frame profiler if: matrix.group == 'positive' run: | @@ -32,7 +35,13 @@ jobs: sudo apt-get install -y libboost-dev fi - name: Check arithmetic, source hashes, finite identities, and patches - run: make verify-${{ matrix.group }} + run: | + if [ "${{ matrix.group }}" = clones ]; then + make skip-clones-verify split-skip-producer + python -B scripts/replay_historical_check.py split-skip + else + make verify-${{ matrix.group }} + fi - name: Require reproducible certificates and patches run: git diff --exit-code diff --git a/certificates/mixed-point-audit.json b/certificates/mixed-point-audit.json index 5b65e2e08a..e97c2e4e24 100644 --- a/certificates/mixed-point-audit.json +++ b/certificates/mixed-point-audit.json @@ -487,7 +487,7 @@ "source_sha256": { "docs/research/mixed-point-audit.md": "c80527f9e98c27bd7f5858a06c7273f84c40e0c41505eb4d16029b61f80fb968", "scripts/experiments/mixed_point_circuit.py": "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc", - "scripts/rational_span_frames.py": "766d342dd73ca5efd784c5733282a93d379a58beea763e703238dfbb4eacce82" + "scripts/rational_span_frames.py": "7386947406d5dc4322a39fb7ccd886876a2fa1d163e823f0f231e11cf9ca0cec" }, "status": "BOUNDED MIXED-POINT RESEARCH; NO NEW KAPPA", "target": "1/1073741824", diff --git a/certificates/rank-product-core.json b/certificates/rank-product-core.json index 63e8c3fa30..d77d7bec90 100644 --- a/certificates/rank-product-core.json +++ b/certificates/rank-product-core.json @@ -6054,7 +6054,7 @@ "docs/research/rank-product-core.md": "1028abd145b367f94960264a874b847cdbeb3b4d84dd6d3a890fe4203922bd41", "scripts/audit_joint_frames.py": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", "scripts/audit_rank_product_core.py": "1471f17e86d6c02d5c288116cc3a53544c881ded47a3500f70dac97b366e46a7", - "scripts/audit_stage_pair.py": "f4823525abb553f76ea33adf61ed51e88ec38dd6c346dbcac86f69ffa8fb0375", + "scripts/audit_stage_pair.py": "67cd9f046e257d7889b7574ca70db983d2414e93dcac34d9a555bc688cff6097", "scripts/experiments/rank_product_core.py": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e", "scripts/finite_bit_contract.py": "3cff26a332cb6056f656b824e3a523fb8937d15206ddcc4118b911ac8df1b2a7" }, diff --git a/certificates/stage-pair-audit.json b/certificates/stage-pair-audit.json index 2e4d46b0a3..57bb620b30 100644 --- a/certificates/stage-pair-audit.json +++ b/certificates/stage-pair-audit.json @@ -903,7 +903,7 @@ ], "source_sha256": { "docs/research/stage-pair-audit.md": "af302999ac2342016bc6d0c5b5e33824cd9eafbb260322a2a6700b309069db9f", - "scripts/audit_stage_pair.py": "f4823525abb553f76ea33adf61ed51e88ec38dd6c346dbcac86f69ffa8fb0375" + "scripts/audit_stage_pair.py": "67cd9f046e257d7889b7574ca70db983d2414e93dcac34d9a555bc688cff6097" }, "status": "BOUNDED TWO-INVOCATION FRAME SEARCH; NO NEW KAPPA", "upstream_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a", diff --git a/scripts/historical-ci-inputs/Makefile b/scripts/historical-ci-inputs/Makefile new file mode 100644 index 0000000000..aff6840902 --- /dev/null +++ b/scripts/historical-ci-inputs/Makefile @@ -0,0 +1,660 @@ +.PHONY: verify note audit-note tuned-note reuse-note incidence-note dag-note shared-point-note paired-note compact-note complex-note ternary-note fetch +.DEFAULT_GOAL := verify + +.PHONY: community-audit-check +community-audit-check: + python3 scripts/audit_community_candidate.py --check docs/research/community-audit-arithmetic.json + +.PHONY: community-followup-check +community-followup-check: + python3 scripts/audit_followup_candidate.py --candidate-root . --check docs/research/community-followup-arithmetic.json + +.PHONY: verify-community verify-producers verify-certificates verify-ternary verify-tests +# CI runs these in separate checkouts. Keep local verification sequential: +# different groups regenerate certificates that another group may read. +verify: + $(MAKE) verify-community + $(MAKE) verify-producers + $(MAKE) verify-partial-gauge + $(MAKE) verify-three-stage-cover + $(MAKE) verify-paired-cube + $(MAKE) verify-recycled-bit + $(MAKE) verify-entrance-banks + $(MAKE) gen4-bank-verify + $(MAKE) frontier741-verify + $(MAKE) verify-certificates + $(MAKE) verify-ternary + $(MAKE) verify-research + $(MAKE) verify-strips + $(MAKE) verify-clones + $(MAKE) verify-positive + $(MAKE) verify-joint + $(MAKE) verify-pair + $(MAKE) verify-tests + +.PHONY: selected-record-check entrance-bank-verify verify-entrance-banks +selected-record-check: + python3 -B scripts/verify_selected_result.py + +entrance-bank-verify: selected-record-check + python3 -B research/coordinated-frames-and-entrance-banks/verify.py + python3 -B research/community-round8-audit/bank_schedule.py + +verify-entrance-banks: entrance-bank-verify + +.PHONY: gen4-bank-verify +gen4-bank-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-gen4.XXXXXX"); \ + python3 -B research/five-stage-gen4-banks/verify.py --output "$$work/replay" + +.PHONY: frontier531-verify +frontier531-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier531.XXXXXX"); \ + python3 -B scripts/verify_frontier531.py --work "$$work/replay" + +.PHONY: frontier535-verify +frontier535-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier535.XXXXXX"); \ + python3 -B scripts/verify_frontier535.py --work "$$work/replay" + +.PHONY: frontier588-verify +frontier588-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier588.XXXXXX"); \ + python3 -B scripts/verify_frontier588.py --work "$$work/replay" + +.PHONY: source527-record-check source527-verify +source527-record-check: + python3 -B scripts/verify_selected_result.py --record certificates/checkpoints/source527.json + +source527-verify: source527-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-source527.XXXXXX"); \ + python3 -B research/five-stage-source527-banks/verify.py --output "$$work/replay" + +verify-community: community-audit-check community-followup-check copied-reversed-producer copied-reversed-check copied-fixed-reversed-producer copied-fixed-reversed-check + $(MAKE) copied-fixed-verify + $(MAKE) climbed-48-verify + +verify-producers: + $(MAKE) stopped-product-verify + $(MAKE) copied-centers-verify + $(MAKE) structured-bulk-verify + $(MAKE) endpoint-gauge-producer endpoint-gauge-certificate + $(MAKE) partial-swap-producer partial-swap-certificate + +verify-certificates: source527-record-check + python3 scripts/prime_field_network.py + python3 scripts/complex_network.py + python3 scripts/fast_gaussian.py + $(MAKE) batched-certificate batched-patch + python3 scripts/certify.py + python3 scripts/search_network.py + python3 scripts/make_patch.py + python3 scripts/nonadjacent.py + python3 scripts/make_nonadjacent_patch.py + python3 scripts/tune_routing.py + python3 scripts/research_networks.py + python3 scripts/search_network_variants.py + python3 scripts/block_label_targets.py + python3 scripts/audit_block_labels.py + python3 scripts/audit_additive_labels.py + python3 scripts/small_block_witness.py + python3 scripts/incidence_network.py + python3 scripts/make_incidence_patch.py + python3 scripts/search_incidence_partitions.py + python3 scripts/dag_network.py + python3 scripts/make_dag_patch.py + python3 scripts/shared_point_network.py + python3 scripts/make_shared_point_patch.py + python3 scripts/paired_network.py + python3 scripts/make_paired_patch.py + python3 scripts/prepare_layers.py + python3 scripts/audit_sparse_fusion.py + python3 scripts/audit_fused_block.py + python3 scripts/audit_short_guards.py + python3 scripts/audit_gather_schedules.py + python3 scripts/audit_coded_carries.py + python3 scripts/audit_cancellation.py + python3 scripts/audit_joint_frames.py + python3 scripts/audit_compact_controls.py + python3 scripts/compact_control_layer.py + python3 scripts/make_compact_control_patch.py + python3 scripts/audit_scratch_pooling.py + python3 scripts/reuse_network.py + python3 scripts/make_reuse_patch.py + +# Independent verification of the pending PR62/63 rank-first construction. +# The offline check is separate from the pinned-source, C++/CRT replay. +verify-certificates: ranked-pair-check + +.PHONY: ranked-pair-check ranked-pair-verify formal-ranked-pair-verify +ranked-pair-check: + python3 research/ranked-pair-verification/verify.py + +ranked-pair-verify: ranked-pair-check + test -n "$(UPSTREAM)" + python3 research/ranked-pair-verification/audit/ranked-word-audit.py --upstream "$(UPSTREAM)" --generated build/ranked-pair + +formal-ranked-pair-verify: + python3 research/ranked-pair-verification/lean/check.py + +formal-historical-verify: formal-ranked-pair-verify + +# Later source-bound proof and finite-certificate checkpoint from PR64. +verify-certificates: machine-transfer-check + +.PHONY: machine-transfer-check formal-machine-transfer-verify +machine-transfer-check: + python3 research/machine-transfer-verification/verify.py + +LAKE_PROJECT ?= formal/lean +formal-machine-transfer-verify: + python3 research/machine-transfer-verification/verify_lean.py --lake-project "$(LAKE_PROJECT)" --output build/machine-transfer/lean + +formal-historical-verify: formal-machine-transfer-verify + +verify-ternary: + python3 scripts/complex_compression.py + python3 scripts/make_complex_compression_patch.py + python3 scripts/audit_ternary_side.py + python3 scripts/make_ternary_patch.py + +verify-tests: + python3 scripts/run_isolated_tests.py + git apply --check --directory=upstream patches/frozen-154.patch + git apply --check --directory=upstream patches/balanced-153.patch + git apply --check --directory=upstream patches/same-network-129.patch + git apply --check --directory=upstream patches/h46-111.patch + git apply --check --directory=upstream patches/h46-109.patch + git apply --check --directory=upstream patches/h46-108.patch + git apply --check --directory=upstream patches/h46-rational.patch + git apply --check --directory=upstream patches/nonadjacent-layout.patch + git apply --check --directory=upstream patches/frozen-nonadjacent-107.patch + git apply --check --directory=upstream patches/h46-nonadjacent-78.patch + git apply --check --directory=upstream patches/h46-nonadjacent-76.patch + git apply --check --directory=upstream patches/h46-shared-side-75.patch + git apply --check --directory=upstream patches/h46-incidence-67.patch + git apply --check --directory=upstream patches/h46-dag-63.patch + git apply --check --directory=upstream patches/h46-shared-point.patch + git apply --check --directory=upstream patches/h50-paired-59.patch + git apply --check --directory=upstream patches/compact-control-34.patch + git apply --check --directory=upstream patches/complex-compression-31.patch + git apply --check --directory=upstream patches/ternary-30.patch + git apply --check --directory=upstream patches/batched-23.patch + +note: + mkdir -p artifacts + tectonic --outdir artifacts notes/parameter-note.tex + +audit-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/nonadjacent-axis-note.tex + +tuned-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/routing-tuned-note.tex + +reuse-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/stage-reuse-note.tex + +incidence-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/incidence-note.tex + +dag-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/dag-note.tex + +shared-point-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/shared-point-note.tex + +paired-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/paired-note.tex + +compact-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/compact-control-note.tex + +complex-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/complex-compression-note.tex + +ternary-note: + mkdir -p artifacts + tectonic --outdir artifacts notes/ternary-note.tex + +fetch: + python3 scripts/fetch_upstream.py + +.PHONY: batched-certificate batched-patch batched-note +PDFLATEX ?= pdflatex +TEX_ENGINE ?= pdflatex +TECTONIC ?= tectonic + +batched-certificate: + python3 scripts/controlled_bit_rank_moment.py --output certificates/controlled-bit-rank-moment.json > /dev/null + python3 scripts/batched_network.py --output certificates/batched-network.json --summary + +batched-patch: + python3 scripts/make_batched_patch.py + +batched-note: + mkdir -p artifacts +ifeq ($(TEX_ENGINE),tectonic) + $(TECTONIC) -Z search-path=$(CURDIR) --outdir artifacts notes/batched-23-note.tex +else + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/batched-23-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/batched-23-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/batched-23-note.tex +endif + +.PHONY: partial-swap-producer partial-swap-certificate partial-swap-note +partial-swap-producer: + python3 scripts/partial_swap_producer.py + +partial-swap-certificate: + python3 scripts/partial_swap_network.py + +partial-swap-note: + mkdir -p artifacts +ifeq ($(TEX_ENGINE),tectonic) + $(TECTONIC) -Z search-path=$(CURDIR) --outdir artifacts notes/partial-swap-note.tex +else + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/partial-swap-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/partial-swap-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/partial-swap-note.tex +endif + +.PHONY: endpoint-gauge-producer endpoint-gauge-certificate endpoint-gauge-note +endpoint-gauge-producer: + python3 scripts/endpoint_gauge_producer.py + +endpoint-gauge-certificate: + python3 scripts/endpoint_gauge_network.py + +endpoint-gauge-note: + mkdir -p artifacts +ifeq ($(TEX_ENGINE),tectonic) + $(TECTONIC) -Z search-path=$(CURDIR) --outdir artifacts notes/endpoint-gauge-note.tex +else + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/endpoint-gauge-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/endpoint-gauge-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/endpoint-gauge-note.tex +endif + +.PHONY: endpoint-gauge-verify +endpoint-gauge-verify: endpoint-gauge-producer endpoint-gauge-certificate + python3 -m unittest discover -s tests -p 'test_endpoint_gauge.py' -v + +.PHONY: structured-bulk-producer structured-bulk-certificate structured-bulk-verify structured-bulk-note +structured-bulk-producer: + python3 scripts/structured_bulk_producer.py + +structured-bulk-certificate: + python3 scripts/structured_bulk_network.py + +structured-bulk-verify: structured-bulk-producer structured-bulk-certificate + +structured-bulk-note: + mkdir -p artifacts +ifeq ($(TEX_ENGINE),tectonic) + $(TECTONIC) -Z search-path=$(CURDIR) --outdir artifacts notes/structured-bulk-note.tex +else + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/structured-bulk-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/structured-bulk-note.tex + $(PDFLATEX) -interaction=nonstopmode -halt-on-error -output-directory=artifacts notes/structured-bulk-note.tex +endif + +.PHONY: copied-centers-producer copied-centers-certificate copied-centers-verify +copied-centers-producer: + python3 scripts/copied_centers_producer.py + +copied-centers-certificate: + python3 scripts/copied_centers_network.py + +copied-centers-verify: copied-centers-producer copied-centers-certificate + +.PHONY: copied-reversed-check copied-reversed-producer +copied-reversed-check: + python3 research/copied-reversed/geometry.py + python3 research/copied-reversed/witness.py + python3 -m unittest discover -s tests -p 'test_copied_reversed.py' -v + +copied-reversed-producer: + mkdir -p build/copied-reversed/producer + python3 scripts/copied_centers_producer.py --work-dir build/copied-reversed/producer --output build/copied-reversed/producer.json + + +.PHONY: copied-fixed-reversed-check copied-fixed-reversed-producer +copied-fixed-reversed-check: + python3 research/copied-fixed-reversed/geometry.py --full + python3 research/copied-fixed-reversed/witness.py + python3 -m unittest discover -s tests -p 'test_copied_fixed_reversed.py' + +copied-fixed-reversed-producer: + mkdir -p build/copied-fixed-reversed/producer + python3 research/copied-fixed-reversed/producer.py --work-dir build/copied-fixed-reversed/producer --output build/copied-fixed-reversed/producer.json + python3 research/copied-fixed-reversed/review/fixed25_copied_crt_audit.py --work-dir build/copied-fixed-reversed/producer --record build/copied-fixed-reversed/producer.json --profiler-source research/copied-fixed-reversed/full_profiles25.cpp --output build/copied-fixed-reversed/crt-audit.json + + +.PHONY: copied-fixed-verify copied-fixed-producer copied-fixed-check +copied-fixed-producer: + python3 research/copied-fixed/producer.py + +copied-fixed-check: + python3 research/copied-fixed/audit.py + python3 research/copied-fixed/verify.py --output research/copied-fixed/certificate.json + python3 -m unittest discover -s tests -p 'test_copied_fixed.py' -v + +copied-fixed-verify: copied-fixed-producer copied-fixed-check + +.PHONY: climbed-48-verify climbed-48-producer climbed-48-check +climbed-48-producer: + python3 research/climbed-48/producer.py + +climbed-48-check: + python3 research/climbed-48/witness.py --output research/climbed-48/certificate.json + python3 -m unittest discover -s tests -p 'test_climbed_48.py' -v + +climbed-48-verify: climbed-48-producer climbed-48-check + +.PHONY: formal-verify formal-historical-verify formal-gaussian-verify +formal-verify: formal-historical-verify formal-gaussian-verify + +formal-historical-verify: + cd formal/lean && lake build + python3 scripts/check_lean_axioms.py --project formal/lean --audit formal/lean/AuditAll.lean + python3 formal/lean/sources.py + python3 formal/open-prs/drift_A.py + python3 formal/open-prs/drift_B.py --selftest + python3 formal/open-prs/drift_C.py + mkdir -p build/formal + python3 formal/circuit/export_paired.py build/formal/paired50.json + python3 -I formal/circuit/check_paired.py build/formal/paired50.json + +formal-gaussian-verify: + $(MAKE) -C research/gaussian-parity-synthesis verify + python3 scripts/check_lean_axioms.py --project research/gaussian-parity-synthesis --audit research/gaussian-parity-synthesis/AuditAll.lean + +.PHONY: verify-research +# Historical finite searches; no current witness or production certificates change. +verify-research: + python3 scripts/audit_bit_compression.py + python3 scripts/audit_mixed_point.py + python3 scripts/audit_early_sharing.py + python3 scripts/audit_split_centers.py + python3 scripts/audit_stage_pair.py + python3 scripts/audit_block_carry.py + python3 scripts/audit_joint_return.py + python3 scripts/audit_cyclic_topology.py + python3 scripts/audit_fano_completion.py + python3 scripts/audit_fano_permutation.py + python3 scripts/audit_rank_product_core.py + python3 scripts/audit_stronger_screens.py + python3 scripts/audit_subset_cores.py + python3 scripts/audit_cube_cores.py + python3 scripts/audit_single_intersection.py + python3 scripts/audit_shared_core.py + python3 scripts/audit_general_guard.py + python3 scripts/audit_disjoint_tensor.py + python3 scripts/audit_core_limits.py + python3 scripts/audit_affine_vectors.py + python3 scripts/audit_block_core.py + python3 scripts/audit_complex_centers.py + python3 scripts/audit_inplace_side.py + python3 scripts/audit_quadratic_affine.py + python3 scripts/audit_signed_sparse.py + python3 scripts/audit_positive_side.py + python3 scripts/audit_parity_side.py + python3 scripts/audit_prime_subset_limits.py +.PHONY: skip-frame-verify +skip-frame-verify: + python3 scripts/experiments/verify_skip_frame.py + + +.PHONY: joint-dual-verify +joint-dual-verify: + python3 scripts/experiments/verify_joint_dual.py + python3 -m unittest discover -s tests -p 'test_joint_reclaim.py' -v + + +.PHONY: skip-strips-verify skip-strips-producer skip-strips-check +skip-strips-producer: + python3 research/skip-strips/producer.py + +skip-strips-check: + python3 research/skip-strips/audit.py + python3 research/skip-strips/verify.py --output research/skip-strips/certificate.json + cd research/skip-strips && python3 -m unittest discover -s ../../tests -p 'test_skip_strips.py' -v + +skip-strips-verify: skip-strips-producer skip-strips-check + +.PHONY: positive-skip-verify positive-skip-build positive-skip-check +positive-skip-build: + python3 scripts/audit_positive_skip_exact.py + +positive-skip-check: + python3 research/positive-skip/witness.py --output research/positive-skip/certificate.json + python3 -m unittest discover -s tests -p 'test_positive_skip.py' -v + +positive-skip-verify: positive-skip-build positive-skip-check + +.PHONY: split-skip-producer split-skip-check split-skip-verify +split-skip-producer: + python3 research/split-skip/producer.py --work-dir build/split-skip --output build/split-skip-receipt.json + +split-skip-check: + python3 research/split-skip/witness.py + python3 research/split-skip/independent_arithmetic.py + python3 -m unittest discover -s tests -p 'test_split_skip.py' -v + +split-skip-verify: split-skip-producer split-skip-check + +.PHONY: skip-suffix-verify skip-suffix-producer skip-suffix-check +skip-suffix-producer: + python3 research/skip-suffix/producer.py + +skip-suffix-check: + python3 research/skip-suffix/audit.py + python3 research/skip-suffix/verify.py --output research/skip-suffix/certificate.json + cd research/skip-suffix && python3 -m unittest discover -s ../../tests -p 'test_skip_suffix.py' -v + +skip-suffix-verify: skip-suffix-producer skip-suffix-check + +.PHONY: skip-clones-verify skip-clones-producer skip-clones-check +skip-clones-producer: + python3 research/skip-clones/producer.py + +skip-clones-check: + python3 research/skip-clones/witness.py --output research/skip-clones/certificate.json + python3 -m unittest discover -s tests -p 'test_skip_clones.py' -v + +skip-clones-verify: skip-clones-producer skip-clones-check + +.PHONY: verify-strips verify-clones verify-positive verify-joint formal-matrix-verify +verify-strips: skip-strips-verify skip-suffix-verify +verify-clones: skip-clones-verify split-skip-verify +verify-positive: positive-skip-verify +verify-joint: skip-frame-verify joint-dual-verify + python3 scripts/audit_joint_candidate.py --check docs/research/community-round2-arithmetic.json + +formal-verify: formal-matrix-verify +formal-matrix-verify: + mkdir -p build + cd research/matrix-exponent-synthesis && lake build + python3 scripts/check_lean_axioms.py --project research/matrix-exponent-synthesis --audit research/matrix-exponent-synthesis/AuditAll.lean + python3 research/matrix-exponent-synthesis/run_checks.py --work "$$(mktemp -d build/matrix-synthesis.XXXXXX)" + python3 scripts/audit_joint_candidate.py --check docs/research/community-round2-arithmetic.json + python3 scripts/audit_pair_candidate.py --check docs/research/community-pair-arithmetic.json + +.PHONY: pair-assembly-verify pair-assembly-producer pair-assembly-check +pair-assembly-producer: + python3 research/pair-assembly/producer.py + +pair-assembly-check: + python3 research/pair-assembly/audit.py + python3 research/pair-assembly/verify.py --output research/pair-assembly/certificate.json + python3 research/pair-assembly/frame/frame_verify.py + cd research/pair-assembly && python3 -m unittest discover -s ../../tests -p 'test_pair_assembly.py' -v + +pair-assembly-verify: pair-assembly-producer pair-assembly-check + +.PHONY: verify-pair +verify-pair: pair-assembly-verify + python3 scripts/audit_pair_candidate.py --check docs/research/community-pair-arithmetic.json + +.PHONY: stopped-product-producer stopped-product-certificate stopped-product-verify +stopped-product-producer: + python3 scripts/stopped_product_producer.py + +stopped-product-certificate: + python3 scripts/stopped_product_network.py + +stopped-product-verify: stopped-product-producer stopped-product-certificate + +.PHONY: partial-gauge-bit partial-gauge-producer partial-gauge-certificate partial-gauge-verify +partial-gauge-bit: + python3 scripts/partial_gauge_bit.py + +partial-gauge-producer: + python3 scripts/partial_gauge_producer.py + +partial-gauge-certificate: + python3 scripts/partial_gauge_network.py + +partial-gauge-verify: partial-gauge-bit partial-gauge-producer partial-gauge-certificate + +.PHONY: verify-partial-gauge +verify-partial-gauge: partial-gauge-verify + +.PHONY: three-stage-cover-producer three-stage-cover-certificate three-stage-cover-verify verify-three-stage-cover +three-stage-cover-producer: + python3 scripts/three_stage_cover_producer.py + +three-stage-cover-certificate: + python3 scripts/three_stage_cover_network.py + +three-stage-cover-verify: three-stage-cover-producer three-stage-cover-certificate + +verify-three-stage-cover: three-stage-cover-verify + +.PHONY: paired-cube-producer paired-cube-bit paired-cube-certificate paired-cube-verify verify-paired-cube +paired-cube-producer: + python3 scripts/paired_cube_producer.py + +paired-cube-bit: + python3 scripts/paired_cube_bit.py + +paired-cube-certificate: + python3 scripts/paired_cube_network.py + +paired-cube-verify: paired-cube-producer paired-cube-bit paired-cube-certificate + +verify-paired-cube: paired-cube-verify + +.PHONY: recycled-bit-verify recycled-bit-full-verify verify-recycled-bit +recycled-bit-verify: + python3 research/recycled-bit-integration/verify.py + +recycled-bit-full-verify: + python3 research/recycled-bit-integration/verify.py --all + +verify-recycled-bit: recycled-bit-full-verify + python3 -m unittest discover -s tests -p 'test_recycled_bit_integration.py' -v + +.PHONY: frontier596-verify +frontier596-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier596.XXXXXX"); \ + python3 -B scripts/verify_frontier596.py --work "$$work/replay" + +.PHONY: frontier617-verify +frontier617-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier617.XXXXXX"); \ + python3 -B scripts/verify_frontier617.py --work "$$work/replay" + +.PHONY: frontier626-verify +frontier626-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier626.XXXXXX"); \ + python3 -B scripts/verify_frontier626.py --work "$$work/replay" + +.PHONY: frontier741-verify +frontier741-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier741.XXXXXX"); \ + python3 -B scripts/verify_frontier_complete.py --frontier 741 --work "$$work/replay" + +.PHONY: frontier799-verify +frontier799-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier799.XXXXXX"); \ + python3 -B scripts/verify_frontier_complete.py --frontier 799 --work "$$work/replay" + +# Opt-in PR853 scheduling; the sequential replay remains the reference. +.PHONY: complex741-parallel +complex741-parallel: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-parallel741.XXXXXX"); \ + python3 -B scripts/verify_complex741_parallel.py --work "$$work/replay" --jobs 3 + +.PHONY: frontier890-verify +frontier890-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier890.XXXXXX"); \ + python3 -B scripts/verify_frontier890.py --work "$$work/replay" + +.PHONY: frontier942-verify +frontier942-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier942.XXXXXX"); \ + python3 -B scripts/verify_frontier942.py --work "$$work/replay" +# Tooling: opt-in parallel exact U8 phase recipes, byte-identical to the pinned serial step (no new kappa). +.PHONY: phase-recipes-parallel-verify phase-recipes-parallel-benchmark +phase-recipes-parallel-verify: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-phase-parallel.XXXXXX"); \ + python3 -B research/phase-recipes-parallel/verify.py --work "$$work/replay" && \ + python3 -B -m unittest discover -s research/phase-recipes-parallel -p test_package.py +phase-recipes-parallel-benchmark: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-phase-parallel.XXXXXX"); \ + python3 -B research/phase-recipes-parallel/verify.py --work "$$work/replay" --serial + +.PHONY: frontier1042-verify +frontier1042-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier1042.XXXXXX"); \ + python3 -B scripts/verify_frontier1042.py --work "$$work/replay" + +# Independent verification: code-disjoint T37 moment endpoints and kappa reduction (no new kappa). +.PHONY: t37-endpoints-independent-verify +t37-endpoints-independent-verify: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-t37-endpoints.XXXXXX"); \ + python3 -B research/t37-endpoints-independent/verify.py --work "$$work/replay" && \ + python3 -B -m unittest discover -s research/t37-endpoints-independent -p test_package.py + +# Independent verification: code-disjoint pricing of the pending kappa claims (no new kappa). +.PHONY: pending-claims-pricing-verify +pending-claims-pricing-verify: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-pending-claims.XXXXXX"); \ + python3 -B research/pending-claims-independent-pricing/verify.py --work "$$work/replay" && \ + python3 -B -m unittest discover -s research/pending-claims-independent-pricing -p test_package.py + +# Tooling: opt-in parallel U8 layer-end controls with a byte-identical receipt (no new kappa). +.PHONY: layer-end-controls-parallel-verify layer-end-controls-parallel-benchmark +layer-end-controls-parallel-verify: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-layer-end.XXXXXX"); \ + python3 -B research/layer-end-controls-parallel/verify.py --work "$$work/replay" && \ + python3 -B -m unittest discover -s research/layer-end-controls-parallel -p test_package.py +layer-end-controls-parallel-benchmark: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-layer-end.XXXXXX"); \ + python3 -B research/layer-end-controls-parallel/verify.py --work "$$work/replay" --serial + +# Research note: width packing of the selected PR589 bit hosting (no new kappa). +.PHONY: bit589-width-packing-verify +bit589-width-packing-verify: + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-bit589-packing.XXXXXX"); \ + python3 -B research/bit589-width-packing/verify.py --work "$$work/replay" && \ + python3 -B -m unittest discover -s research/bit589-width-packing -p test_package.py + +.PHONY: frontier1094-verify +frontier1094-verify: selected-record-check + @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier1094.XXXXXX"); \ + python3 -B scripts/verify_frontier1094.py --work "$$work/replay" + +.PHONY: verify-parallel +verify-parallel: + python3 scripts/verify_parallel.py diff --git a/scripts/historical-ci-inputs/README.md b/scripts/historical-ci-inputs/README.md new file mode 100644 index 0000000000..c438694334 --- /dev/null +++ b/scripts/historical-ci-inputs/README.md @@ -0,0 +1,32 @@ +# Historical CI input snapshots + +These are exact Git blobs, not new source pins or changes to the selected result. +The maintenance launcher `scripts/replay_historical_check.py` verifies each blob +against its unchanged predecessor manifest, copies tracked working files into a +temporary tree, replaces just the declared historical input there, and executes +the original checkers. It works with shallow CI checkouts and changes no live +source file. The live Makefile must still preserve its entire authenticated +historical prefix; appended targets are allowed, prefix mutations reject. All other inputs remain the current tracked working +bytes, so their +original checker conditions and corruption controls remain active. After replay, +every tracked file in the temporary tree must still have its initial byte hash +(including the authenticated historical replacement), preserving the original +reproducibility gate as well as protecting the live checkout. + +| Snapshot | Original path | Source commit | Consumer | +| --- | --- | --- | --- | +| `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` | + +Use `python3 -B scripts/replay_historical_check.py r420` (add `--native` for +C++17/Boost), `reconciliation92`, 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. + +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. diff --git a/scripts/historical-ci-inputs/audit_fused_block.py b/scripts/historical-ci-inputs/audit_fused_block.py new file mode 100644 index 0000000000..c63869d22c --- /dev/null +++ b/scripts/historical-ci-inputs/audit_fused_block.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Exact parity-butterfly block and a scoped coordinate-recursion obstruction. + +The direct block uses three exact coordinate Hadamard layers plus diagonal +phases. It is not a faster multiplication algorithm. Its recursive call +count fails the all-role contraction requirement. +""" +from fractions import Fraction as Q +from pathlib import Path +import json + +from certify import network, require, verify_sources +from prepare_layers import serializable + +ROOT=Path(__file__).resolve().parents[1] + + +def gadd(a,b):return (a[0]+b[0],a[1]+b[1]) +def gsub(a,b):return (a[0]-b[0],a[1]-b[1]) +def gmul(a,b):return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0]) + + +def phase_i(value,power): + return gmul(value,((1,0),(0,1),(-1,0),(0,-1))[power%4]) + + +def layout(f,K,rho=0,spectator_bits=0): + require(f>=1 and K>=1 and 0<=rho=0,'Invalid layout') + # Two physical slots of f*K bits; any extra high bits are spectators. + # Masks use least-significant-bit indexing; array order is integer order. + x=[rho+j*K for j in range(f)] + y=[f*K+rho+j*K for j in range(f)] + return x,y,2*f*K+spectator_bits + + +def walsh_numerator(state,positions): + """Unnormalized coordinate Walsh layers, with no layout permutation.""" + out=list(state) + for position in positions: + mask=1<>y)&1)-1)*((i>>x)&1) + for x,y in zip(x_positions,y_positions))) + for i,z in enumerate(state)] + + +def validate_positions(state,x_positions,y_positions): + require(len(state)>0 and len(state)&(len(state)-1)==0,'State size must be a power of two') + positions=list(x_positions)+list(y_positions) + require(len(x_positions)==len(y_positions)>0,'Unequal or empty active sets') + require(len(set(positions))==len(positions),'Active coordinates must be distinct') + require(all(0<=p>i&1:value^=col + return value + + +def permute(state,columns): + out=[(0,0)]*len(state) + for x,z in enumerate(state):out[invertible_map(columns,x)]=z + return out + + +def sandwich_numerator(state,x_positions,y_positions,nbits): + """P_M (product C_x) P_M^-1 for M: y_j <- y_j XOR x_j.""" + validate_positions(state,x_positions,y_positions) + require(len(state)==1<>bit&1] + inputs=[i for i in range(len(matrix[0])) if not ((i%addresses)>>bit&1)] + return rational_rank([[matrix[i][j] for j in inputs] for i in output]) + + +def walsh_matrix(e,roles=1,active=None,role=None): + """Integer Walsh operator, optionally restricted to one role and axis set.""" + size=1<