diff --git a/certificates/joint-dual-kappa.json b/certificates/joint-dual-kappa.json index b7f7b89bc2..240efb3da1 100644 --- a/certificates/joint-dual-kappa.json +++ b/certificates/joint-dual-kappa.json @@ -837,12 +837,12 @@ "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669", "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9", "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13", - "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800", + "scripts/experiments/joint_dual_compose.py": "3554e957570e2d3f65c5bd7c945338c9e2fc5f3e79efa2b436a4dfc61899c394", "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", - "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", + "scripts/experiments/pin_joint_dual_sources.py": "5d41535a73ad62fae7acb5365c5b7f40d7c99e52b6bc4266e44572018080acc5", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985" }, - "source_manifest_sha256": "4f3c15b82a2d97335d4fe95fb8bcb96bd2a921087da289d9da16c68213a17f17", + "source_manifest_sha256": "e60f1f78c9729700ef9606a6576163de0b553792e5e8f24591dce5f51597158c", "sources": [ { "files": { diff --git a/certificates/joint-dual-validation.json b/certificates/joint-dual-validation.json index 194861d3c3..a5ee9f485a 100644 --- a/certificates/joint-dual-validation.json +++ b/certificates/joint-dual-validation.json @@ -226,7 +226,7 @@ } }, "bit_saving": "2382370177/50000000000000", - "certificate_sha256": "9801147b1502cf1e43d5fa39aa37f5291f03b48c30c4dd4f272e0877894a1c24", + "certificate_sha256": "a1329d6c5e78cef5c7381d5e5d79c0a8842db7e569892af3b7e763b6c46d6f96", "kappa": "4764513337/100000000000000", "margins": 7, "producer_words_regenerated_and_matched": true, diff --git a/docs/paired-cube.md b/docs/paired-cube.md index 38dc3d30e0..f10c339b2d 100644 --- a/docs/paired-cube.md +++ b/docs/paired-cube.md @@ -64,12 +64,14 @@ sources are included without a PDF. ## Shared source bindings -The final `Makefile`, `README.md` and `NOTICE` changes also update the inherited -joint-dual manifest. Explicitly refresh its hashes, regenerate joint arithmetic -and update the validation receipt's certificate digest. Its mathematical -fields and previous complete replay payload must remain equal when their -producer/verifier inputs are unchanged. The complete affected replay command, -when needed, is `make verify-joint`. +The inherited joint-dual manifest no longer binds `Makefile`, `README.md` or +`NOTICE`, so editing them does not touch it. Earlier round notes describe the +time when it did. If a bound producer, certificate or finite input changes, +explicitly refresh its hashes, regenerate joint arithmetic and update the +validation receipt's certificate digest. Its mathematical fields and previous +complete replay payload must remain equal when their producer/verifier inputs +are unchanged. The complete affected replay command, when needed, is +`make verify-joint`. Stage the final artifacts before the deterministic certificate regeneration and require `git diff --exit-code` to remain clean. CI checks the committed diff --git a/research/joint-dual/SOURCE.json b/research/joint-dual/SOURCE.json index e3a8386b17..e055d5d63d 100644 --- a/research/joint-dual/SOURCE.json +++ b/research/joint-dual/SOURCE.json @@ -3,9 +3,6 @@ "base_pr57_commit": "cd350f76c9bc01489ec83568bded532cb69be938", "base_pr58_commit": "bc2f7ed4c20dc18898305ab17165c0c995cbb804", "files": { - "Makefile": "768131bd4ce18433f6abccdc9812a38c92e11220e3a1019c6d95334b42f529d1", - "NOTICE": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd", - "README.md": "d104c31d5b7e0d3a8d011a0e3517ab615e5b499b3dc05684f7ad3cadcd28bdae", "certificates/joint-dual-compiler.json": "516c4d85158553dabd0a98216a064b2a7397957a9d5dd0df1d6e5aec53a4e805", "certificates/joint-dual-profiles-23.json": "159fa8fee175fc1d24f63e72d3c2f1dc9f4fcd78b938c5e7d2f735fd0fd37209", "certificates/joint-dual-profiles-25.json": "8d190ce42d097e828c5756918c52f2963df576cf4c6600b0fc7f2b7fdb6ad223", @@ -49,9 +46,9 @@ "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669", "scripts/experiments/binary_frame_replay.py": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9", "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13", - "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800", + "scripts/experiments/joint_dual_compose.py": "3554e957570e2d3f65c5bd7c945338c9e2fc5f3e79efa2b436a4dfc61899c394", "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", - "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", + "scripts/experiments/pin_joint_dual_sources.py": "5d41535a73ad62fae7acb5365c5b7f40d7c99e52b6bc4266e44572018080acc5", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985", "tests/test_joint_reclaim.py": "c4e2817bf6e699f462aa3c589ee45e24ab0dcad6bcdb6152ca2a1e16ac7bffeb" }, diff --git a/research/lean-binary-count-dispatcher/ACCEPTED_CHECKS.json b/research/lean-binary-count-dispatcher/ACCEPTED_CHECKS.json new file mode 100644 index 0000000000..f2a83e46cf --- /dev/null +++ b/research/lean-binary-count-dispatcher/ACCEPTED_CHECKS.json @@ -0,0 +1,238 @@ +{ + "kind": "fresh six-module accepted-source checks; package replay separate", + "modules": [ + { + "module": "IntegerConvolution", + "source_sha256": "0bc86f2fa8e68f39df77be603d2a9634bc008745093286903105378ab45938ea", + "receipt_sha256": "9f4041c0a3fec637e8b47686837ec516d133df60b5482ec83d5aa774cf8adc62", + "object_sha256": "72299b15d1bee37af56e1c5d10018d45784213c43461021afc4c213d1863af36", + "log_sha256": "c1aea8c6ec85d16aa991288c1dbd640d2047900b669fb59a79e5d084d150f0c5", + "started_utc": "2026-10-11T20:17:31.900570+00:00", + "finished_utc": "2026-10-11T20:17:33.611709+00:00", + "compile_seconds": 1.7111359120001453, + "queue_seconds": 0.00039078200006770203, + "peak_vm_bytes": 2265174016, + "status": "PASS" + }, + { + "module": "FixedTapeMachine", + "source_sha256": "92dadedc9f6e23d12633549b53ca8f917360e4fedac0b64a58d18feea741a5ed", + "receipt_sha256": "ea1bdd28da97ea51a45eb11bbcbee1dbcf1b835d9c7efc1796e7cbe81f784b55", + "object_sha256": "88fa2e0c9e43f696f53762a345092d19fa3501d7b1de2381dfb335b232b53ff1", + "log_sha256": "36dc8dbc05e17722f16160959d84aea237a472b8a2435c0fd7dc140e3f704559", + "started_utc": "2026-10-11T20:17:34.574845+00:00", + "finished_utc": "2026-10-11T20:17:36.242033+00:00", + "compile_seconds": 1.66718382199997, + "queue_seconds": 0.00032932299995991343, + "peak_vm_bytes": 2063888384, + "status": "PASS" + }, + { + "module": "CarryTape", + "source_sha256": "20d13d9d2da74452e45c0a175b643556615ba14187bf8fb0e4393e44842c17a5", + "receipt_sha256": "c98c833a97cf4f96c38f54ea75e4c9309a6ff17baec4cee7f814627b88fe5041", + "object_sha256": "5ecb25ccf73c61eb5b4be13a69c73d9b7183201a71344e333761af7ea7915c74", + "log_sha256": "a269b42e17b5fd794216654bafc3ee3cc58c39fbbf5c36fa525eb42bfc739b67", + "started_utc": "2026-10-11T20:21:09.928592+00:00", + "finished_utc": "2026-10-11T20:21:12.444412+00:00", + "compile_seconds": 2.51581714200006, + "queue_seconds": 0.00039194500004668953, + "peak_vm_bytes": 2735390720, + "status": "PASS" + }, + { + "module": "CarryTapePass", + "source_sha256": "680b5d16736880ac6a02f27e9503e1cc01479bb2b35bb7546d9108dcb4b4ef2b", + "receipt_sha256": "c2ddc97083ec113da2537650250a961be1e1fb4c76f5c6b53f7fcd137a37ddc9", + "object_sha256": "183f0edf242a2f6ecb9d9a07d62bc977d9fa04b3a32bad75a6c71344583c1147", + "log_sha256": "bf3a993154b0837224b4a4f76d6f48fc6508422904a4371309c777ba6936ddb6", + "started_utc": "2026-10-11T20:21:13.415458+00:00", + "finished_utc": "2026-10-11T20:21:15.922354+00:00", + "compile_seconds": 2.506893128999991, + "queue_seconds": 0.0002887979999286472, + "peak_vm_bytes": 2735984640, + "status": "PASS" + }, + { + "module": "BinaryCarryIncrement", + "source_sha256": "b0f639159e2169c75e6d7a13663adee5107648a32b7ff9203f92792e31012dce", + "receipt_sha256": "dc6bc90c6a70cf077442fb309c012e1d6e6256137074cc1e6cd3e7a1b4a3cea9", + "object_sha256": "07895c550c6298ae2143cca61c53399131f4b5a6a77b71f154c7ec6baa46ddc8", + "log_sha256": "d249a6aaa4e3eec29d84596b492eac68b52d6c14c115df389f20f5b313d1f0ae", + "started_utc": "2026-10-11T20:25:26.593822+00:00", + "finished_utc": "2026-10-11T20:25:28.676028+00:00", + "compile_seconds": 2.082204667000042, + "queue_seconds": 0.0004521139999269508, + "peak_vm_bytes": 2065498112, + "status": "PASS" + }, + { + "module": "BinaryCountDispatcher", + "source_sha256": "ec24af9483d59ce3248802378218d4b478490aa2458e136880f36e7f49356e93", + "receipt_sha256": "c701b66a9f5885ce456e95fc6af33d93d81e32c157ca11a69fa2049ab4840113", + "object_sha256": "6685bcc5f2657f829149fa21e0140e063750680997c072cbe2c661e5190fa97e", + "log_sha256": "514eb1cbe0db0c7bef18f845a35310c63653d757bb691d1cd0bc44c076c1a90f", + "started_utc": "2026-10-11T20:37:41.048046+00:00", + "finished_utc": "2026-10-11T20:37:44.703455+00:00", + "compile_seconds": 3.6554057119997196, + "queue_seconds": 0.0005584489999819198, + "peak_vm_bytes": 2603089920, + "status": "PASS" + } + ], + "axiom_probes": [ + { + "module": "IntegerConvolution", + "line": "'CurrentMain.IntegerConvolution.value_addCoefficients' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "IntegerConvolution", + "line": "'CurrentMain.IntegerConvolution.value_map_mul' depends on axioms: [propext]" + }, + { + "module": "IntegerConvolution", + "line": "'CurrentMain.IntegerConvolution.convolution_value' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "IntegerConvolution", + "line": "'CurrentMain.IntegerConvolution.binary_convolution' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "FixedTapeMachine", + "line": "'CurrentMain.FixedTapeMachine.initial_inputA' depends on axioms: [propext]" + }, + { + "module": "FixedTapeMachine", + "line": "'CurrentMain.FixedTapeMachine.initial_inputB' depends on axioms: [propext]" + }, + { + "module": "FixedTapeMachine", + "line": "'CurrentMain.FixedTapeMachine.initial_output' depends on axioms: [propext]" + }, + { + "module": "FixedTapeMachine", + "line": "'CurrentMain.FixedTapeMachine.run_halted' does not depend on any axioms" + }, + { + "module": "FixedTapeMachine", + "line": "'CurrentMain.FixedTapeMachine.run_add' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.run_add' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.carry_execution' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.rewind_execution' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.carryFinish_rewind' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.increment_execution' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.increment_length' depends on axioms: [propext]" + }, + { + "module": "CarryTape", + "line": "'CurrentMain.CarryTape.all_ones_execution' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.value_bound' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.increment_value' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.increment_mod' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.pass_length' depends on axioms: [propext]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.pass_value' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.pass_even' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.empty_pass_one' does not depend on any axioms" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.complete_pass' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.incrementReceipt_realized' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.pass_successor_realized' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "CarryTapePass", + "line": "'CurrentMain.CarryTape.full_pass24_index_traffic' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "BinaryCarryIncrement", + "line": "'CurrentMain.BinaryCarryIncrement.increment_run' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "BinaryCarryIncrement", + "line": "'CurrentMain.BinaryCarryIncrement.final_halted' depends on axioms: [propext]" + }, + { + "module": "BinaryCarryIncrement", + "line": "'CurrentMain.BinaryCarryIncrement.increment_length' depends on axioms: [propext]" + }, + { + "module": "BinaryCarryIncrement", + "line": "'CurrentMain.BinaryCarryIncrement.value_binding' does not depend on any axioms" + }, + { + "module": "BinaryCarryIncrement", + "line": "'CurrentMain.BinaryCarryIncrement.increment_modular_value' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "BinaryCountDispatcher", + "line": "'CurrentMain.BinaryCountDispatcher.count_run' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "BinaryCountDispatcher", + "line": "'CurrentMain.BinaryCountDispatcher.final_halted' depends on axioms: [propext, Quot.sound]" + }, + { + "module": "BinaryCountDispatcher", + "line": "'CurrentMain.BinaryCountDispatcher.counter_length' depends on axioms: [propext]" + }, + { + "module": "BinaryCountDispatcher", + "line": "'CurrentMain.BinaryCountDispatcher.counter_value' depends on axioms: [propext, Quot.sound]" + } + ], + "all_sources_and_objects_verified": true, + "package_isolated_replay": { + "status": "PASS", + "summary_sha256": "4f38e221f0a048d25b583e0772a58fab4ee171fa786d08c58cefff219cf59782" + }, + "total_compile_seconds": 14.138640383999928, + "total_queue_seconds": 0.0024114109999118227, + "maximum_vm_bytes": 2735984640, + "independent_acceptance_scope_review_sha256": "8648da8a63b6222c0fdf1a156d3fe27580eab71464084b8e41709a4cbff1f6fd" +} diff --git a/research/lean-binary-count-dispatcher/AUTHOR_CHECK.json b/research/lean-binary-count-dispatcher/AUTHOR_CHECK.json new file mode 100644 index 0000000000..a31690c026 --- /dev/null +++ b/research/lean-binary-count-dispatcher/AUTHOR_CHECK.json @@ -0,0 +1,26 @@ +{ + "status": "AUTHOR_CHECKED_COMPLETED_SCOPE_AND_EXPLICIT_CONDITIONAL_KAPPA", + "source_base_commit": "12a4934d15006e8c10f9b2264f13f8f341be802b", + "reviewed_files": { + "README.md": "9f322996b3e82f7cb4aef40f270d130638a80c869e6877bd4c1ab11163858f7e", + "PROVENANCE.json": "aef823808c948bc557eff3ecde8cb0c6257cb1074665c4bbf1428ef343e68b51", + "MANIFEST.json": "cdf44d1089e14f1309dd20a85c0d2fdca050d9a9120b7c1e40862e176447bafb", + "FOUNDATIONS.json": "fcac056292d2fb7aa2e5c8f91523f0255bdeb16f244f8edcec48ff9088949698", + "REPLAY_SUMMARY.json": "4f38e221f0a048d25b583e0772a58fab4ee171fa786d08c58cefff219cf59782" + }, + "source_author_contract_context_readback_sha256": "83b84ecfa2c50d1727d771e9f5286e3d6a4333551fad5bc4ceaba2bf1259de43", + "exact_draft_author_readback_sha256": "e64466b5bc1a24f02ca5dd56cd704d3fdb57ef2675456f3867b113c8c3987e67", + "final_replay_status_author_readback_sha256": "4d5aa5e772511d5392d68177d2c852b2619732c195dc10ce7f668004ca1518fb", + "kappa": "90446448750933/125000000000000000", + "decimal": "0.000723571590007464", + "source_evidence_sha256": "df836c6d34509e980d067bd5678489c968bc6e329af9dd82c6207abf6443da89", + "certificate_sha256": "6a457a34b4db57417e5b253cf1c169da2bd6aff4c21363a31fd85dc931d49589", + "confirmation": "The source-author readback verifies the exact controller endpoint and pass-receipt bound, prior-work attribution, two external PR488 source dependencies, completed flat-layout isolated replay statement, and the explicit conditional project kappa context. These generic machine results do not prove a kappa or multiplication theorem.", + "included_source_hashes": { + "BinaryCarryIncrement.lean": "b0f639159e2169c75e6d7a13663adee5107648a32b7ff9203f92792e31012dce", + "BinaryCountDispatcher.lean": "ec24af9483d59ce3248802378218d4b478490aa2458e136880f36e7f49356e93", + "CarryTape.lean": "20d13d9d2da74452e45c0a175b643556615ba14187bf8fb0e4393e44842c17a5", + "CarryTapePass.lean": "680b5d16736880ac6a02f27e9503e1cc01479bb2b35bb7546d9108dcb4b4ef2b" + }, + "final_flat_layout_author_readback_sha256": "1d7069050a7e667abb691894275768e3487bd61ac904d1ebecbbece6076b3f24" +} diff --git a/research/lean-binary-count-dispatcher/BinaryCarryIncrement.lean b/research/lean-binary-count-dispatcher/BinaryCarryIncrement.lean new file mode 100644 index 0000000000..411667d983 --- /dev/null +++ b/research/lean-binary-count-dispatcher/BinaryCarryIncrement.lean @@ -0,0 +1,220 @@ +import FixedTapeMachine +import CarryTapePass + +/-! A five-state, one-tape implementation of the existing fixed-width carry +incrementer in the explicit three-symbol tape model. Home and end markers both +encode as blank; a dedicated end-return state distinguishes their reachable +uses. Only the well-formed marked interval is simulated. No input-driven count, +width allocation, compact-record conversion, source caller or Budget is claimed. -/ +namespace CurrentMain.BinaryCarryIncrement +open FixedTapeMachine + +private abbrev CT := CarryTape.Tape + +def symbol : CarryTape.Symbol → Symbol + | .home | .stop => .blank + | .zero => .zero + | .one => .one + +def tape (s : CT) : Tape := + ⟨s.left.map symbol, symbol (CarryTape.read s), s.right.tail.map symbol⟩ + +def phase (s : CT) : Fin 5 := + match s.phase with + | .enter => 0 + | .carry => 1 + | .rewind => if CarryTape.read s = .stop then 2 else 3 + | .halt => 4 + +def action (next : Fin 5) (write : Symbol) (move : Move) : Action 1 5 := + ⟨next, fun _ => write, fun _ => move⟩ + +/-- States: enter, carry, return from end, rewind, halt. -/ +def machine : Machine where + tapes := 1 + states := 5 + initial := 0 + transition := fun s read => + match s.val with + | 0 => if read (0 : Fin 1) = .blank then + some (action 1 .blank .right) else none + | 1 => match read (0 : Fin 1) with + | .zero => some (action 3 .one .stay) + | .one => some (action 1 .zero .right) + | .blank => some (action 2 .blank .stay) + | 2 => some (action 3 (read (0 : Fin 1)) .left) + | 3 => if read (0 : Fin 1) = .blank then + some (action 4 .blank .stay) + else some (action 3 (read (0 : Fin 1)) .left) + | _ => none + +def configuration (state : Fin 5) (contents : Tape) : Configuration machine := + ⟨state, fun _ => contents⟩ + +def encode (s : CT) : Configuration machine := configuration (phase s) (tape s) + +/-- Exactly the reachable phase forms of a marker-bounded increment call. The +public theorem below constructs its initial witness for every Boolean word. -/ +private inductive WellFormed : CT → Prop + | enter (bits : List Bool) : WellFormed (CarryTape.homeTape bits .enter) + | carry (pref bits : List Bool) : WellFormed (CarryTape.carryTape pref bits) + | rewind (pref bits : List Bool) : WellFormed (CarryTape.rewindTape pref bits) + | home (bits : List Bool) : WellFormed (CarryTape.homeTape bits .rewind) + | halt (bits : List Bool) : WellFormed (CarryTape.homeTape bits .halt) + +private theorem wellFormed_step (s : CT) (h : WellFormed s) : + WellFormed (CarryTape.step s).1 := by + cases h with + | enter bits => + simpa [CarryTape.step, CarryTape.homeTape, CarryTape.read, CarryTape.right, + CarryTape.carryTape] using WellFormed.carry [] bits + | carry pref bits => + cases bits with + | nil => + simpa [CarryTape.step, CarryTape.carryTape, CarryTape.rewindTape, + CarryTape.read, CarryTape.cells] using WellFormed.rewind pref [] + | cons b bits => + cases b with + | false => + simpa [CarryTape.step, CarryTape.carryTape, CarryTape.rewindTape, + CarryTape.read, CarryTape.cells, CarryTape.encode, CarryTape.write] + using WellFormed.rewind pref (true :: bits) + | true => + simpa [CarryTape.step, CarryTape.carryTape, CarryTape.read, + CarryTape.cells, CarryTape.encode, CarryTape.write, CarryTape.right] + using WellFormed.carry (false :: pref) bits + | rewind pref bits => + cases pref with + | nil => + cases bits with + | nil => + simpa [CarryTape.step, CarryTape.rewindTape, CarryTape.homeTape, + CarryTape.read, CarryTape.cells, CarryTape.left] + using WellFormed.home [] + | cons b bits => + have h := WellFormed.home (b :: bits) + cases b <;> + simpa [CarryTape.step, CarryTape.rewindTape, CarryTape.homeTape, + CarryTape.read, CarryTape.cells, CarryTape.encode, CarryTape.left] using h + | cons b pref => + cases bits with + | nil => + simpa [CarryTape.step, CarryTape.rewindTape, CarryTape.read, + CarryTape.cells, CarryTape.left] using WellFormed.rewind pref [b] + | cons c bits => + have h := WellFormed.rewind pref (b :: c :: bits) + cases c <;> + simpa [CarryTape.step, CarryTape.rewindTape, CarryTape.read, + CarryTape.cells, CarryTape.encode, CarryTape.left] using h + | home bits => + simpa [CarryTape.step, CarryTape.homeTape, CarryTape.read] + using WellFormed.halt bits + | halt bits => + simpa [CarryTape.step, CarryTape.homeTape] using WellFormed.halt bits + +/-- The source halt step is inert, matching the target's saturated run. -/ +private theorem step_simulation (s : CT) (h : WellFormed s) : + run machine 1 (encode s) = encode (CarryTape.step s).1 := by + cases h with + | enter bits => + cases bits with + | nil => rfl + | cons b bits => cases b <;> rfl + | carry pref bits => + cases bits with + | nil => rfl + | cons b bits => + cases b with + | false => rfl + | true => + cases bits with + | nil => rfl + | cons c bits => cases c <;> rfl + | rewind pref bits => + cases pref with + | nil => + cases bits with + | nil => rfl + | cons b bits => cases b <;> rfl + | cons b pref => + cases bits with + | nil => cases b <;> rfl + | cons c bits => cases b <;> cases c <;> rfl + | home bits => rfl + | halt bits => rfl + +private theorem run_simulation (n : Nat) (s : CT) (h : WellFormed s) : + run machine n (encode s) = encode (CarryTape.run n s).1 := by + induction n generalizing s with + | zero => rfl + | succ n ih => + have split : run machine (n + 1) (encode s) = + run machine n (run machine 1 (encode s)) := by + simpa only [Nat.one_add] using run_add machine 1 n (encode s) + rw [split, step_simulation s h, ih _ (wellFormed_step s h)] + rfl + +/-- The home blank and end blank are two distinct represented cells, including +width zero. This is not the canonical Tape.ofWord representation. -/ +def homeTape (bits : List Bool) : Tape := + ⟨[], .blank, bits.map bitSymbol ++ [.blank]⟩ + +def initialConfiguration (bits : List Bool) : Configuration machine := + configuration 0 (homeTape bits) + +def finalConfiguration (bits : List Bool) : Configuration machine := + configuration 4 (homeTape (CarryTape.increment bits)) + +private theorem encode_home (bits : List Bool) (p : CarryTape.Phase) : + tape (CarryTape.homeTape bits p) = homeTape bits := by + change (Tape.mk [] .blank ((bits.map CarryTape.encode ++ [CarryTape.Symbol.stop]).map symbol)) = + Tape.mk [] .blank (bits.map bitSymbol ++ [.blank]) + have maps : (bits.map CarryTape.encode).map symbol = bits.map bitSymbol := by + rw [List.map_map] + apply List.map_congr_left + intro b _ + cases b <;> rfl + simp only [List.map_append, maps, List.map_cons, List.map_nil, symbol] + +/-- Exact target-table run for every width and bit pattern, including overflow. +The cost and logical update are transported from the existing carry proof. -/ +theorem increment_run (bits : List Bool) : + run machine (2 * CarryTape.trailingOnes bits + 4) (initialConfiguration bits) = + finalConfiguration bits := by + have h := run_simulation (2 * CarryTape.trailingOnes bits + 4) + (CarryTape.homeTape bits .enter) (WellFormed.enter bits) + rw [CarryTape.increment_execution] at h + have start : encode (CarryTape.homeTape bits .enter) = initialConfiguration bits := + congrArg (configuration (0 : Fin 5)) (encode_home bits .enter) + have finish : encode (CarryTape.homeTape (CarryTape.increment bits) .halt) = + finalConfiguration bits := + congrArg (configuration (4 : Fin 5)) (encode_home (CarryTape.increment bits) .halt) + exact (congrArg (run machine (2 * CarryTape.trailingOnes bits + 4)) start.symm).trans + (h.trans finish) + +theorem final_halted (bits : List Bool) : Halted machine (finalConfiguration bits) := by + rfl + +theorem increment_length (bits : List Bool) : + (CarryTape.increment bits).length = bits.length := CarryTape.increment_length bits + +/-- A representation identity only; no counter arithmetic is reproved. -/ +theorem value_binding (bits : List Bool) : CarryTape.value bits = wordValue bits := by + induction bits with + | nil => rfl + | cons b bits ih => + simpa only [CarryTape.value, wordValue, IntegerConvolution.binaryValue, + List.map_cons, IntegerConvolution.value] + using congrArg (fun v => (if b then 1 else 0) + 2 * v) ih + +theorem increment_modular_value (bits : List Bool) : + wordValue (CarryTape.increment bits) = (wordValue bits + 1) % 2 ^ bits.length := by + rw [← value_binding, ← value_binding] + exact CarryTape.increment_mod bits + +end CurrentMain.BinaryCarryIncrement +#print axioms CurrentMain.BinaryCarryIncrement.increment_run +#print axioms CurrentMain.BinaryCarryIncrement.final_halted +#print axioms CurrentMain.BinaryCarryIncrement.increment_length +#print axioms CurrentMain.BinaryCarryIncrement.value_binding +#print axioms CurrentMain.BinaryCarryIncrement.increment_modular_value diff --git a/research/lean-binary-count-dispatcher/BinaryCountDispatcher.lean b/research/lean-binary-count-dispatcher/BinaryCountDispatcher.lean new file mode 100644 index 0000000000..4c6719d736 --- /dev/null +++ b/research/lean-binary-count-dispatcher/BinaryCountDispatcher.lean @@ -0,0 +1,271 @@ +import BinaryCarryIncrement + +/-! A finite symbol-driven controller for a preallocated, marked fixed-width +counter. This supplies the restart-controller boundary left explicit by PR64's +RippleCounter/CounterArithmetic and the local CarryTape pass specification. +The counter arithmetic and increment execution are reused, not reproved. + +The seven-state/two-tape table scans an actual input word and dispatches one +increment per bit. Width is tape data, not an instruction argument. The final +input is at its visited right blank; the counter returns to its home blank. +The bound uses the existing pass receipt. Width allocation, amortization, +compact output, source prelude and Plan/Budget are separate obligations. -/ +namespace CurrentMain.BinaryCountDispatcher +open FixedTapeMachine + +private theorem fin1 (i : Fin 1) : i=0 := by + exact (show ∀ j : Fin 1, j=0 by decide) i +private theorem fin2 (i : Fin 2) : i=0 ∨ i=1 := by + exact (show ∀ j : Fin 2, j=0 ∨ j=1 by decide) i +private theorem fin5 (i : Fin 5) : i=0 ∨ i=1 ∨ i=2 ∨ i=3 ∨ i=4 := by + exact (show ∀ j : Fin 5, j=0 ∨ j=1 ∨ j=2 ∨ j=3 ∨ j=4 by decide) i + +def liftState (s : Fin 5) : Fin 7 := ⟨s.val+1, by omega⟩ +def readCounter (r : Fin 2 → Symbol) : Fin 1 → Symbol := fun _ => r 1 + +def stayAction (next : Fin 7) (r : Fin 2 → Symbol) : Action 2 7 := + ⟨next,r,fun _ => .stay⟩ +def advanceAction (r : Fin 2 → Symbol) : Action 2 7 := + ⟨1,r,fun i => if i=0 then .right else .stay⟩ +def liftAction (r : Fin 2 → Symbol) (a : Action 1 5) : Action 2 7 where + state := liftState a.state + writes := fun i => if i=0 then r 0 else a.writes 0 + moves := fun i => if i=0 then .stay else a.moves 0 + +/-- Dispatcher0; renamed increment states1..5; terminal6. -/ +def machine : Machine where + tapes := 2 + states := 7 + initial := 0 + transition := fun s r => + if h : 1≤s.val ∧ s.val≤5 then + match BinaryCarryIncrement.machine.transition (⟨s.val-1,by omega⟩ : Fin 5) + (readCounter r) with + | some a => some (liftAction r a) + | none => some (stayAction 0 r) + else if s.val=0 then + match r (0 : Fin 2) with + | .blank => some (stayAction 6 r) + | .zero | .one => some (advanceAction r) + else none + +def configuration (s : Fin 7) (input counter : Tape) : Configuration machine := + ⟨s,fun i => if i=(0 : Fin 2) then input else counter⟩ +def embed (c : Configuration BinaryCarryIncrement.machine) (input : Tape) : + Configuration machine := configuration (liftState c.state) input (c.tapes (0 : Fin 1)) + +private theorem transition_lift (s : Fin 5) (r : Fin 2 → Symbol) : + machine.transition (liftState s) r = + match BinaryCarryIncrement.machine.transition s (readCounter r) with + | some a => some (liftAction r a) + | none => some (stayAction 0 r) := by + rcases fin5 s with rfl|rfl|rfl|rfl|rfl <;> rfl + +private theorem reads_embed (c : Configuration BinaryCarryIncrement.machine) (input : Tape) : + readCounter (fun i : Fin 2 => ((embed c input).tapes i).head) = + fun j : Fin 1 => (c.tapes j).head := by + funext j + rw [fin1 j] + rfl + +/- The next definitional reduction and successful-prefix induction reuse the +accepted BinaryInputPreparation proof bodies verbatim. They avoid reconstructing +concrete dependent matchers and do not assume a first-halting-time theorem. -/ +private theorem step_of_transition (m : Machine) (c : Configuration m) + (a : Action m.tapes m.states) + (h : m.transition c.state (fun i => (c.tapes i).head) = some a) : + step m c = some (Configuration.mk a.state + (fun i => ((c.tapes i).write (a.writes i)).move (a.moves i))) := by + unfold step + rw [h] + +private theorem step_embed (c d : Configuration BinaryCarryIncrement.machine) (input : Tape) + (h : step BinaryCarryIncrement.machine c = some d) : + step machine (embed c input) = some (embed d input) := by + cases ht : BinaryCarryIncrement.machine.transition c.state (fun i => (c.tapes i).head) with + | none => + simp only [step, ht] at h + cases h + | some a => + simp only [step, ht, Option.some.injEq] at h + subst d + have lifted : BinaryCarryIncrement.machine.transition c.state + (readCounter (fun i : Fin 2 => ((embed c input).tapes i).head)) = some a := + (congrArg (fun reads : Fin 1 → Symbol => + BinaryCarryIncrement.machine.transition c.state reads) (reads_embed c input)).trans ht + have outer : machine.transition (embed c input).state + (fun i : Fin 2 => ((embed c input).tapes i).head) = + some (liftAction (fun i : Fin 2 => ((embed c input).tapes i).head) a) := + (transition_lift c.state (fun i : Fin 2 => ((embed c input).tapes i).head)).trans + (congrArg (fun q : Option (Action 1 5) => + match q with + | some a => some (liftAction (fun i : Fin 2 => ((embed c input).tapes i).head) a) + | none => some (stayAction 0 (fun i : Fin 2 => ((embed c input).tapes i).head))) lifted) + refine (step_of_transition machine (embed c input) _ outer).trans ?_ + dsimp only [liftAction, embed, configuration] + apply congrArg some + apply congrArg (fun tapes : Fin 2 → Tape => + (Configuration.mk (liftState a.state) tapes : Configuration machine)) + funext i + rcases fin2 i with rfl|rfl <;> simp [configuration, Tape.write, Tape.move] + +private theorem halt_embed (c : Configuration BinaryCarryIncrement.machine) (input : Tape) + (h : Halted BinaryCarryIncrement.machine c) : + step machine (embed c input) = some (configuration 0 input (c.tapes (0 : Fin 1))) := by + have ht : BinaryCarryIncrement.machine.transition c.state (fun i => (c.tapes i).head) = none := by + cases he : BinaryCarryIncrement.machine.transition c.state (fun i => (c.tapes i).head) <;> + simp_all [Halted, step] + have lifted : BinaryCarryIncrement.machine.transition c.state + (readCounter (fun i : Fin 2 => ((embed c input).tapes i).head)) = none := + (congrArg (fun reads : Fin 1 → Symbol => + BinaryCarryIncrement.machine.transition c.state reads) (reads_embed c input)).trans ht + have outer : machine.transition (embed c input).state + (fun i : Fin 2 => ((embed c input).tapes i).head) = + some (stayAction 0 (fun i : Fin 2 => ((embed c input).tapes i).head)) := + (transition_lift c.state (fun i : Fin 2 => ((embed c input).tapes i).head)).trans + (congrArg (fun q : Option (Action 1 5) => + match q with + | some a => some (liftAction (fun i : Fin 2 => ((embed c input).tapes i).head) a) + | none => some (stayAction 0 (fun i : Fin 2 => ((embed c input).tapes i).head))) lifted) + refine (step_of_transition machine (embed c input) _ outer).trans ?_ + dsimp only [stayAction, embed, configuration] + apply congrArg some + apply congrArg (fun tapes : Fin 2 → Tape => (Configuration.mk (0 : Fin 7) tapes : Configuration machine)) + funext i + rcases fin2 i with rfl|rfl <;> simp [Tape.write, Tape.move] + +private theorem simulate_to_halt (source target : Machine) + (embed : Configuration source → Configuration target) + (sim : ∀ c d, step source c=some d → step target (embed c)=some (embed d)) + (budget : Nat) (c : Configuration source) (h : Halted source (run source budget c)) : + ∃ k≤budget, run target k (embed c)=embed (run source budget c) := by + induction budget generalizing c with + | zero => exact ⟨0, Nat.le_refl _, rfl⟩ + | succ budget ih => + cases hs : step source c with + | none => + refine ⟨0, Nat.zero_le _, ?_⟩ + simp only [run, hs] + | some d => + have hd : Halted source (run source budget d) := by simpa only [run, hs] using h + obtain ⟨k,hk,he⟩ := ih d hd + refine ⟨k+1, by omega, ?_⟩ + simpa only [run, hs, sim c d hs] using he + +/-- Scanned input is retained nearest-first on the left; the unread finite word +ends at the first blank. This specifies the entire explicit tape footprint. -/ +def inputTape (left : List Symbol) : List Bool → Tape + | [] => ⟨left,.blank,[]⟩ + | b::rest => ⟨left,bitSymbol b,rest.map bitSymbol⟩ + +private theorem inputTape_word (word : List Bool) : inputTape [] word=Tape.ofWord word := by + cases word <;> rfl + +private theorem dispatch_step (b : Bool) (rest : List Bool) (left : List Symbol) (bits : List Bool) : + step machine (configuration 0 (inputTape left (b::rest)) (BinaryCarryIncrement.homeTape bits)) = + some (embed (BinaryCarryIncrement.initialConfiguration bits) + (inputTape (bitSymbol b::left) rest)) := by + have outer : machine.transition (0 : Fin 7) + (fun i : Fin 2 => ((configuration 0 (inputTape left (b::rest)) + (BinaryCarryIncrement.homeTape bits)).tapes i).head) = + some (advanceAction (fun i : Fin 2 => ((configuration 0 (inputTape left (b::rest)) + (BinaryCarryIncrement.homeTape bits)).tapes i).head)) := by + cases b <;> rfl + refine (step_of_transition machine _ _ outer).trans ?_ + dsimp only [advanceAction, embed, configuration, BinaryCarryIncrement.initialConfiguration, + BinaryCarryIncrement.configuration, liftState] + apply congrArg some + apply congrArg (fun tapes : Fin 2 → Tape => (Configuration.mk (1 : Fin 7) tapes : Configuration machine)) + funext i + rcases fin2 i with rfl|rfl <;> + cases rest <;> simp [configuration, inputTape, Tape.write, Tape.move] + +private theorem stop_step (left : List Symbol) (bits : List Bool) : + step machine (configuration 0 (inputTape left []) (BinaryCarryIncrement.homeTape bits)) = + some (configuration 6 (inputTape left []) (BinaryCarryIncrement.homeTape bits)) := by + have outer : machine.transition (0 : Fin 7) + (fun i : Fin 2 => ((configuration 0 (inputTape left []) + (BinaryCarryIncrement.homeTape bits)).tapes i).head) = + some (stayAction 6 (fun i : Fin 2 => ((configuration 0 (inputTape left []) + (BinaryCarryIncrement.homeTape bits)).tapes i).head)) := rfl + refine (step_of_transition machine _ _ outer).trans ?_ + dsimp only [stayAction, configuration] + apply congrArg some + apply congrArg (fun tapes : Fin 2 → Tape => (Configuration.mk (6 : Fin 7) tapes : Configuration machine)) + funext i + rcases fin2 i with rfl|rfl <;> simp [Tape.write, Tape.move] + +private theorem one_increment (bits : List Bool) (input : Tape) : + ∃ k≤2*CarryTape.trailingOnes bits+4, + run machine k (embed (BinaryCarryIncrement.initialConfiguration bits) input) = + embed (BinaryCarryIncrement.finalConfiguration bits) input := by + have halted : Halted BinaryCarryIncrement.machine + (run BinaryCarryIncrement.machine (2*CarryTape.trailingOnes bits+4) + (BinaryCarryIncrement.initialConfiguration bits)) := by + rw [BinaryCarryIncrement.increment_run] + exact BinaryCarryIncrement.final_halted bits + obtain ⟨k,hk,he⟩ := simulate_to_halt BinaryCarryIncrement.machine machine (fun c => embed c input) + (fun c d h => step_embed c d input h) _ _ halted + exact ⟨k,hk,by simpa only [BinaryCarryIncrement.increment_run] using he⟩ + +private theorem loop_run (word : List Bool) (left : List Symbol) (bits : List Bool) : + ∃ t≤(CarryTape.pass word.length bits).2.reads+2*word.length+1, + run machine t (configuration 0 (inputTape left word) (BinaryCarryIncrement.homeTape bits)) = + configuration 6 (inputTape (word.reverse.map bitSymbol++left) []) + (BinaryCarryIncrement.homeTape (CarryTape.pass word.length bits).1) := by + induction word generalizing left bits with + | nil => + refine ⟨1,by simp [CarryTape.pass, CarryTape.Receipt.zero],?_⟩ + simpa only [run, stop_step, List.length_nil, CarryTape.pass, List.reverse_nil, + List.map_nil, List.nil_append] using + (rfl : configuration (6 : Fin 7) (inputTape left []) (BinaryCarryIncrement.homeTape bits) = + configuration (6 : Fin 7) (inputTape left []) (BinaryCarryIncrement.homeTape bits)) + | cons b rest ih => + let next := inputTape (bitSymbol b::left) rest + obtain ⟨k,hk,he⟩ := one_increment bits next + obtain ⟨t,ht,hr⟩ := ih (bitSymbol b::left) (CarryTape.increment bits) + have bridge : step machine (embed (BinaryCarryIncrement.finalConfiguration bits) next) = + some (configuration 0 next (BinaryCarryIncrement.homeTape (CarryTape.increment bits))) := by + simpa only [BinaryCarryIncrement.finalConfiguration, BinaryCarryIncrement.configuration] + using halt_embed (BinaryCarryIncrement.finalConfiguration bits) next (BinaryCarryIncrement.final_halted bits) + refine ⟨1+k+1+t,?_,?_⟩ + · simp only [List.length_cons, CarryTape.pass, CarryTape.incrementReceipt, CarryTape.Receipt.add] + omega + · rw [run_add machine (1+k+1) t, run_add machine (1+k) 1, run_add machine 1 k] + simp only [run, dispatch_step] + rw [he] + simp only [run, bridge] + simpa only [List.length_cons, CarryTape.pass, List.reverse_cons, List.map_append, + List.map_cons, List.map_nil, List.append_assoc, List.singleton_append] using hr + +def initialConfiguration (word bits : List Bool) : Configuration machine := + configuration 0 (Tape.ofWord word) (BinaryCarryIncrement.homeTape bits) +def finalConfiguration (word bits : List Bool) : Configuration machine := + configuration 6 (inputTape (word.reverse.map bitSymbol) []) + (BinaryCarryIncrement.homeTape (CarryTape.pass word.length bits).1) + +/-- Every actual input symbol dispatches one completed increment. The bound +charges the inherited physical receipt plus dispatcher/return/terminal steps. -/ +theorem count_run (word bits : List Bool) : + ∃ t≤(CarryTape.pass word.length bits).2.reads+2*word.length+1, + run machine t (initialConfiguration word bits)=finalConfiguration word bits := by + simpa only [initialConfiguration, finalConfiguration, inputTape_word, List.append_nil] + using loop_run word [] bits + +theorem final_halted (word bits : List Bool) : Halted machine (finalConfiguration word bits) := by + rfl + +theorem counter_length (word bits : List Bool) : + (CarryTape.pass word.length bits).1.length=bits.length := CarryTape.pass_length _ _ + +theorem counter_value (word bits : List Bool) : + wordValue (CarryTape.pass word.length bits).1 = + (wordValue bits+word.length)%2^bits.length := by + rw [← BinaryCarryIncrement.value_binding, ← BinaryCarryIncrement.value_binding] + exact CarryTape.pass_value _ _ + +end CurrentMain.BinaryCountDispatcher +#print axioms CurrentMain.BinaryCountDispatcher.count_run +#print axioms CurrentMain.BinaryCountDispatcher.final_halted +#print axioms CurrentMain.BinaryCountDispatcher.counter_length +#print axioms CurrentMain.BinaryCountDispatcher.counter_value diff --git a/research/lean-binary-count-dispatcher/CarryTape.lean b/research/lean-binary-count-dispatcher/CarryTape.lean new file mode 100644 index 0000000000..4993e9e1d3 --- /dev/null +++ b/research/lean-binary-count-dispatcher/CarryTape.lean @@ -0,0 +1,211 @@ +import Lean + +/-! A finite-alphabet, one-head, two-way tape incrementer. +The program has four control states and four tape symbols. Lists represent +only the two sides of its physical tape; the executable transition inspects +the current symbol and moves at most one cell. There is no Nat address or +remaining-count register in the transition. `run` fuel is proof instrumentation. +-/ +namespace CurrentMain.CarryTape + +inductive Symbol where + | home | zero | one | stop + deriving DecidableEq, Repr +inductive Phase where + | enter | carry | rewind | halt + deriving DecidableEq, Repr + +structure Tape where + left : List Symbol + right : List Symbol + phase : Phase + deriving DecidableEq, Repr + +/-- The current cell is the first right-hand symbol. Missing cells are stop +symbols; well-formed executions below never traverse outside both markers. -/ +def read (s : Tape) : Symbol := s.right.headD .stop +def write (v : Symbol) (s : Tape) : Tape := {s with right := v :: s.right.tail} +def right (s : Tape) : Tape := + {s with left := read s :: s.left, right := s.right.tail} +def left (s : Tape) : Tape := + {s with left := s.left.tail, right := s.left.headD .home :: s.right} + +structure Receipt where + reads : Nat + writes : Nat + moves : Nat + deriving DecidableEq, Repr + +def Receipt.zero : Receipt := ⟨0, 0, 0⟩ +def Receipt.add (a b : Receipt) : Receipt := + ⟨a.reads + b.reads, a.writes + b.writes, a.moves + b.moves⟩ + +/-- Each charge records the actual current-cell inspection, write, and head move. +Halting is inert; malformed enter/carry-home states halt after one inspection. -/ +def step (s : Tape) : Tape × Receipt := + match s.phase, read s with + | .halt, _ => (s, Receipt.zero) + | .enter, .home => ({right s with phase := .carry}, ⟨1, 0, 1⟩) + | .enter, _ => ({s with phase := .halt}, ⟨1, 0, 0⟩) + | .carry, .zero => ({write .one s with phase := .rewind}, ⟨1, 1, 0⟩) + | .carry, .one => (right (write .zero s), ⟨1, 1, 1⟩) + | .carry, .stop => ({s with phase := .rewind}, ⟨1, 0, 0⟩) + | .carry, .home => ({s with phase := .halt}, ⟨1, 0, 0⟩) + | .rewind, .home => ({s with phase := .halt}, ⟨1, 0, 0⟩) + | .rewind, _ => (left s, ⟨1, 0, 1⟩) + +def run : Nat → Tape → Tape × Receipt + | 0, s => (s, Receipt.zero) + | n + 1, s => + let first := step s + let rest := run n first.1 + (rest.1, first.2.add rest.2) + +def encode : Bool → Symbol | false => .zero | true => .one +def cells (bits : List Bool) : List Symbol := bits.map encode ++ [.stop] +def homeTape (bits : List Bool) (phase : Phase) : Tape := + ⟨[], .home :: cells bits, phase⟩ + +def carryTape (pref bits : List Bool) : Tape := + ⟨pref.map encode ++ [.home], cells bits, .carry⟩ +def rewindTape (pref bits : List Bool) : Tape := + ⟨pref.map encode ++ [.home], cells bits, .rewind⟩ + +/-- LSB-first modular increment, used only as the semantic specification. -/ +def increment : List Bool → List Bool + | [] => [] + | false :: bits => true :: bits + | true :: bits => false :: increment bits + +def trailingOnes : List Bool → Nat + | [] => 0 + | false :: _ => 0 + | true :: bits => trailingOnes bits + 1 + +def bitWrites : List Bool → Nat + | [] => 0 + | false :: _ => 1 + | true :: bits => bitWrites bits + 1 + +/-- The carry-stop configuration, preserving its actually live tape pref. -/ +def carryFinish (pref : List Bool) : List Bool → Tape + | [] => rewindTape pref [] + | false :: bits => rewindTape pref (true :: bits) + | true :: bits => carryFinish (false :: pref) bits + +theorem run_add (m n : Nat) (s : Tape) : + run (m + n) s = + let first := run m s + let second := run n first.1 + (second.1, first.2.add second.2) := by + induction m generalizing s with + | zero => simp [run, Receipt.zero, Receipt.add] + | succ m ih => + simp only [Nat.succ_add, run, ih] + congr 1 + simp [Receipt.add, Nat.add_assoc] + +theorem carry_execution (pref bits : List Bool) : + run (trailingOnes bits + 1) (carryTape pref bits) = + (carryFinish pref bits, ⟨trailingOnes bits + 1, bitWrites bits, trailingOnes bits⟩) := by + induction bits generalizing pref with + | nil => rfl + | cons b bits ih => + cases b with + | false => rfl + | true => + simp only [trailingOnes, bitWrites, carryFinish, run] + change (let rest := run (trailingOnes bits + 1) (carryTape (false :: pref) bits) + (rest.1, (Receipt.mk 1 1 1).add rest.2)) = _ + rw [ih] + simp [Receipt.add, Nat.add_comm] + +theorem rewind_execution (pref bits : List Bool) : + run (pref.length + 2) (rewindTape pref bits) = + (homeTape (pref.reverse ++ bits) .halt, ⟨pref.length + 2, 0, pref.length + 1⟩) := by + induction pref generalizing bits with + | nil => + cases bits with + | nil => rfl + | cons b bits => cases b <;> rfl + | cons b pref ih => + have hstep : step (rewindTape (b :: pref) bits) = + (rewindTape pref (b :: bits), ⟨1, 0, 1⟩) := by + cases bits with + | nil => rfl + | cons c bits => cases c <;> rfl + rw [List.length_cons] + change (let first := step (rewindTape (b :: pref) bits) + let rest := run (pref.length + 2) first.1 + (rest.1, first.2.add rest.2)) = _ + simp only [hstep] + rw [ih] + simp [Receipt.add, List.reverse_cons, List.append_assoc, Nat.add_comm, Nat.add_left_comm] + +theorem carryFinish_rewind (pref bits : List Bool) : + run (pref.length + trailingOnes bits + 2) (carryFinish pref bits) = + (homeTape (pref.reverse ++ increment bits) .halt, + ⟨pref.length + trailingOnes bits + 2, 0, pref.length + trailingOnes bits + 1⟩) := by + induction bits generalizing pref with + | nil => simpa [carryFinish, trailingOnes, increment] using rewind_execution pref [] + | cons b bits ih => + cases b with + | false => simpa [carryFinish, trailingOnes, increment] using rewind_execution pref (true :: bits) + | true => + have h := ih (false :: pref) + simpa [carryFinish, trailingOnes, increment, List.reverse_cons, List.append_assoc, + Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h + +/-- Every input width and every bit pattern: exact increment, unchanged end +markers, head back at home, and exact paid tape-operation counts. -/ +theorem increment_execution (bits : List Bool) : + run (2 * trailingOnes bits + 4) (homeTape bits .enter) = + (homeTape (increment bits) .halt, + ⟨2 * trailingOnes bits + 4, bitWrites bits, 2 * trailingOnes bits + 2⟩) := by + have hsplit : 2 * trailingOnes bits + 4 = + 1 + ((trailingOnes bits + 1) + (trailingOnes bits + 2)) := by omega + rw [hsplit, run_add] + have henter : run 1 (homeTape bits .enter) = (carryTape [] bits, ⟨1, 0, 1⟩) := rfl + simp only [henter] + rw [run_add] + simp only [carry_execution] + have hback := carryFinish_rewind [] bits + simp only [List.length_nil, Nat.zero_add, List.reverse_nil, List.nil_append] at hback + simp only [hback] + simp only [Receipt.add] + congr 2 <;> omega + +theorem increment_length (bits : List Bool) : (increment bits).length = bits.length := by + induction bits with + | nil => rfl + | cons b bits ih => cases b <;> simp [increment, ih] + +/-- The exact receipt cannot be charged as O(1) per worst-case increment. -/ +theorem all_ones_execution (n : Nat) : + run (2 * n + 4) (homeTape (List.replicate n true) .enter) = + (homeTape (List.replicate n false) .halt, ⟨2 * n + 4, n, 2 * n + 2⟩) := by + have hi : increment (List.replicate n true) = List.replicate n false := by + induction n with + | zero => rfl + | succ n ih => simp [List.replicate_succ, increment, ih] + have ht : trailingOnes (List.replicate n true) = n := by + clear hi + induction n with + | zero => rfl + | succ n ih => simp [List.replicate_succ, trailingOnes, ih] + have hw : bitWrites (List.replicate n true) = n := by + clear hi ht + induction n with + | zero => rfl + | succ n ih => simp [List.replicate_succ, bitWrites, ih] + simpa [hi, ht, hw] using increment_execution (List.replicate n true) + +end CurrentMain.CarryTape + +#print axioms CurrentMain.CarryTape.run_add +#print axioms CurrentMain.CarryTape.carry_execution +#print axioms CurrentMain.CarryTape.rewind_execution +#print axioms CurrentMain.CarryTape.carryFinish_rewind +#print axioms CurrentMain.CarryTape.increment_execution +#print axioms CurrentMain.CarryTape.increment_length +#print axioms CurrentMain.CarryTape.all_ones_execution diff --git a/research/lean-binary-count-dispatcher/CarryTapePass.lean b/research/lean-binary-count-dispatcher/CarryTapePass.lean new file mode 100644 index 0000000000..720415129e --- /dev/null +++ b/research/lean-binary-count-dispatcher/CarryTapePass.lean @@ -0,0 +1,143 @@ +import CarryTape + +namespace CurrentMain.CarryTape + +/-- Logical overflow is specified separately; the four-state incrementer does +not retain an overflow flag after rewinding. -/ +def overflow : List Bool → Bool + | [] => true + | false :: _ => false + | true :: bits => overflow bits + +def value : List Bool → Nat + | [] => 0 + | b :: bits => (if b then 1 else 0) + 2 * value bits + +theorem value_bound (bits : List Bool) : value bits < 2 ^ bits.length := by + induction bits with + | nil => decide + | cons b bits ih => cases b <;> simp [value, Nat.pow_succ] <;> omega + +theorem increment_value (bits : List Bool) : + value (increment bits) + (if overflow bits then 2 ^ bits.length else 0) = value bits + 1 := by + induction bits with + | nil => rfl + | cons b bits ih => + cases b with + | false => simp [increment, overflow, value]; omega + | true => + cases h : overflow bits <;> + simp [increment, overflow, value, h, Nat.pow_succ] at ih ⊢ <;> omega + +theorem increment_mod (bits : List Bool) : + value (increment bits) = (value bits + 1) % 2 ^ bits.length := by + have hi := increment_value bits + have hx := value_bound bits + have hy := value_bound (increment bits) + rw [increment_length] at hy + cases h : overflow bits with + | false => + simp only [h, Bool.false_eq_true, if_false, Nat.add_zero] at hi + rw [← hi, Nat.mod_eq_of_lt hy] + | true => + simp only [h, if_true] at hi + have hz : value (increment bits) = 0 := by omega + have hp : value bits + 1 = 2 ^ bits.length := by omega + rw [hz, hp, Nat.mod_self] + +/-- Proven physical primitive receipt, including both endpoint-marker reads. -/ +def incrementReceipt (bits : List Bool) : Receipt := + ⟨2 * trailingOnes bits + 4, bitWrites bits, 2 * trailingOnes bits + 2⟩ + +/-- Specification of repeated, head-restored physical increments. +The Nat loop is an iteration proof device; control and client costs are not +claimed to have been compiled to tape by this definition. -/ +def pass : Nat → List Bool → List Bool × Receipt + | 0, bits => (bits, Receipt.zero) + | k + 1, bits => + let tail := pass k (increment bits) + (tail.1, (incrementReceipt bits).add tail.2) + +theorem pass_length (k : Nat) (bits : List Bool) : (pass k bits).1.length = bits.length := by + induction k generalizing bits with + | zero => rfl + | succ k ih => simp only [pass, ih, increment_length] + +theorem pass_value (k : Nat) (bits : List Bool) : + value (pass k bits).1 = (value bits + k) % 2 ^ bits.length := by + induction k generalizing bits with + | zero => simp [pass, Nat.mod_eq_of_lt (value_bound bits)] + | succ k ih => + simp only [pass, ih, increment_length, increment_mod, Nat.mod_add_mod] + congr 1 + omega + +/-- Two actual low-bit increments advance the tail once. This is the +amortization bridge; no list of all addresses is built. -/ +theorem pass_even (k : Nat) (bits : List Bool) : + pass (2 * k) (false :: bits) = + (false :: (pass k bits).1, + ⟨(pass k bits).2.reads + 6 * k, + (pass k bits).2.writes + 2 * k, + (pass k bits).2.moves + 4 * k⟩) := by + induction k generalizing bits with + | zero => rfl + | succ k ih => + have he : 2 * (k + 1) = (2 * k + 1) + 1 := by omega + rw [he] + simp only [pass, increment] + rw [ih] + simp only [incrementReceipt, trailingOnes, bitWrites, Receipt.add] + congr 2 <;> omega + +theorem empty_pass_one : pass 1 [] = ([], ⟨4, 0, 2⟩) := rfl + +/-- Exact all-width index-tape traffic for the full modular pass. This includes +all carry and rewind head movement, but excludes zero initialization, coefficient +evaluation, data-tape/client work and loop-control lowering. -/ +theorem complete_pass (n : Nat) : + pass (2 ^ n) (List.replicate n false) = + (List.replicate n false, + ⟨6 * 2 ^ n - 2, 2 * 2 ^ n - 2, 4 * 2 ^ n - 2⟩) := by + induction n with + | zero => rfl + | succ n ih => + have hp : 1 ≤ 2 ^ n := Nat.one_le_pow n 2 (by decide) + rw [Nat.pow_succ, Nat.mul_comm (2 ^ n) 2, List.replicate_succ, pass_even, ih] + dsimp only + congr 2 <;> omega + +/-- Every primitive used by the pass is bound to the finite-alphabet machine, +not merely assigned the receipt of a desired endpoint. -/ +theorem incrementReceipt_realized (bits : List Bool) : + run (incrementReceipt bits).reads (homeTape bits .enter) = + (homeTape (increment bits) .halt, incrementReceipt bits) := increment_execution bits + +/-- A physical call and its returned head-restored state have exactly the same +logical effect as one step of the repeated-increment specification. -/ +theorem pass_successor_realized (k : Nat) (bits : List Bool) : + let first := run (incrementReceipt bits).reads (homeTape bits .enter) + let tail := pass k (increment bits) + first.1 = homeTape (increment bits) .halt ∧ + pass (k + 1) bits = (tail.1, first.2.add tail.2) := by + simp only [incrementReceipt_realized, pass] + trivial + +theorem full_pass24_index_traffic : + (pass (2 ^ 24) (List.replicate 24 false)).2 = + ⟨100663294, 33554430, 67108862⟩ := by + rw [complete_pass] + +end CurrentMain.CarryTape + +#print axioms CurrentMain.CarryTape.value_bound +#print axioms CurrentMain.CarryTape.increment_value +#print axioms CurrentMain.CarryTape.increment_mod +#print axioms CurrentMain.CarryTape.pass_length +#print axioms CurrentMain.CarryTape.pass_value +#print axioms CurrentMain.CarryTape.pass_even +#print axioms CurrentMain.CarryTape.empty_pass_one +#print axioms CurrentMain.CarryTape.complete_pass +#print axioms CurrentMain.CarryTape.incrementReceipt_realized +#print axioms CurrentMain.CarryTape.pass_successor_realized +#print axioms CurrentMain.CarryTape.full_pass24_index_traffic diff --git a/research/lean-binary-count-dispatcher/FOUNDATIONS.json b/research/lean-binary-count-dispatcher/FOUNDATIONS.json new file mode 100644 index 0000000000..600d7440e0 --- /dev/null +++ b/research/lean-binary-count-dispatcher/FOUNDATIONS.json @@ -0,0 +1,21 @@ +{ + "repository": "https://github.com/jamesyc/integer-mult-bounds", + "commit": "edd3102b415df5b9d6f633ac0a4dedcf69c58525", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/488", + "package_path": "research/lean-binary-input-preparation", + "merge_assumed": false, + "files": [ + { + "repository_path": "research/lean-binary-input-preparation/Lean/IntegerConvolution.lean", + "sha256": "0bc86f2fa8e68f39df77be603d2a9634bc008745093286903105378ab45938ea", + "bytes": 2055, + "module": "IntegerConvolution" + }, + { + "repository_path": "research/lean-binary-input-preparation/Lean/FixedTapeMachine.lean", + "sha256": "92dadedc9f6e23d12633549b53ca8f917360e4fedac0b64a58d18feea741a5ed", + "bytes": 4523, + "module": "FixedTapeMachine" + } + ] +} diff --git a/research/lean-binary-count-dispatcher/LICENSE b/research/lean-binary-count-dispatcher/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/lean-binary-count-dispatcher/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/lean-binary-count-dispatcher/MANIFEST.json b/research/lean-binary-count-dispatcher/MANIFEST.json new file mode 100644 index 0000000000..99fc20ce7d --- /dev/null +++ b/research/lean-binary-count-dispatcher/MANIFEST.json @@ -0,0 +1,73 @@ +{ + "format": "bounded-lean-dispatcher-package-v1", + "lean_version": "4.21.0", + "package_modules": 4, + "dependency_modules": 2, + "source_bytes": 44164, + "package_source_bytes": 37586, + "compile_order": [ + { + "module": "IntegerConvolution", + "sha256": "0bc86f2fa8e68f39df77be603d2a9634bc008745093286903105378ab45938ea", + "bytes": 2055, + "imports": [ + "Lean" + ], + "origin": "pr488", + "file": "Lean/IntegerConvolution.lean" + }, + { + "module": "FixedTapeMachine", + "sha256": "92dadedc9f6e23d12633549b53ca8f917360e4fedac0b64a58d18feea741a5ed", + "bytes": 4523, + "imports": [ + "IntegerConvolution" + ], + "origin": "pr488", + "file": "Lean/FixedTapeMachine.lean" + }, + { + "module": "CarryTape", + "sha256": "20d13d9d2da74452e45c0a175b643556615ba14187bf8fb0e4393e44842c17a5", + "bytes": 8348, + "imports": [ + "Lean" + ], + "origin": "package", + "file": "CarryTape.lean" + }, + { + "module": "CarryTapePass", + "sha256": "680b5d16736880ac6a02f27e9503e1cc01479bb2b35bb7546d9108dcb4b4ef2b", + "bytes": 5662, + "imports": [ + "CarryTape" + ], + "origin": "package", + "file": "CarryTapePass.lean" + }, + { + "module": "BinaryCarryIncrement", + "sha256": "b0f639159e2169c75e6d7a13663adee5107648a32b7ff9203f92792e31012dce", + "bytes": 9032, + "imports": [ + "FixedTapeMachine", + "CarryTapePass" + ], + "origin": "package", + "file": "BinaryCarryIncrement.lean" + }, + { + "module": "BinaryCountDispatcher", + "sha256": "ec24af9483d59ce3248802378218d4b478490aa2458e136880f36e7f49356e93", + "bytes": 14544, + "imports": [ + "BinaryCarryIncrement" + ], + "origin": "package", + "file": "BinaryCountDispatcher.lean" + } + ], + "scope": "Concrete two-tape actual-symbol restart dispatcher with supplied marked counter width and modular value.", + "complete_integer_multiplication_theorem": false +} diff --git a/research/lean-binary-count-dispatcher/NOTICE.source.txt b/research/lean-binary-count-dispatcher/NOTICE.source.txt new file mode 100644 index 0000000000..8853b1b1d6 --- /dev/null +++ b/research/lean-binary-count-dispatcher/NOTICE.source.txt @@ -0,0 +1,9 @@ +Shared-edge supplier and completed entrance banks,2026. Apache-2.0. +Developed with OpenAI model assistance. No personal byline is added. + +This contribution composes the pinnedPR181complex supplier and the actual +PR168v4bit word with completed entrance banks and recomputes the full paid +finite bound. All upstream author attribution and assistance disclosures +remain in UPSTREAM-NOTICE.md and the immutable archive. Copied source files +retain their author notices. No global optimality or exclusive priority +is claimed; the inherited all-size interfaces remain explicit. diff --git a/research/lean-binary-count-dispatcher/PROVENANCE.json b/research/lean-binary-count-dispatcher/PROVENANCE.json new file mode 100644 index 0000000000..efa8b56c66 --- /dev/null +++ b/research/lean-binary-count-dispatcher/PROVENANCE.json @@ -0,0 +1,63 @@ +{ + "status": "Exact accepted sources and isolated six-module package replay passed.", + "source_base_commit": "12a4934d15006e8c10f9b2264f13f8f341be802b", + "foundation_dependency": { + "repository": "https://github.com/jamesyc/integer-mult-bounds", + "commit": "edd3102b415df5b9d6f633ac0a4dedcf69c58525", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/488", + "package_path": "research/lean-binary-input-preparation", + "merge_assumed": false, + "files": [ + { + "repository_path": "research/lean-binary-input-preparation/Lean/IntegerConvolution.lean", + "sha256": "0bc86f2fa8e68f39df77be603d2a9634bc008745093286903105378ab45938ea", + "bytes": 2055, + "module": "IntegerConvolution" + }, + { + "repository_path": "research/lean-binary-input-preparation/Lean/FixedTapeMachine.lean", + "sha256": "92dadedc9f6e23d12633549b53ca8f917360e4fedac0b64a58d18feea741a5ed", + "bytes": 4523, + "module": "FixedTapeMachine" + } + ] + }, + "project_kappa_context": { + "kappa": "90446448750933/125000000000000000", + "decimal": "0.000723571590007464", + "selected_result_repository_path": "certificates/selected-result.json", + "selected_result_sha256": "df836c6d34509e980d067bd5678489c968bc6e329af9dd82c6207abf6443da89", + "certificate_repository_path": "research/community-pr279-audit/certificate.json", + "certificate_sha256": "6a457a34b4db57417e5b253cf1c169da2bd6aff4c21363a31fd85dc931d49589", + "scope": "Current base conditional project parameter only; this generic dispatcher proves no kappa or multiplication theorem." + }, + "prior_work": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/64", + "relationship": "Prior literal counter and stack realization, first-completion and amortized arithmetic. No generic increment novelty or stronger-contract claim. The controller imports local CarryTape/CarryTapePass; direct PR64-to-current-model arithmetic transport remains open." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/488", + "relationship": "Exact two foundation source dependencies; input-preparation reduction proof bodies reused. Merge is not assumed." + } + ], + "author_contract_context_readback_sha256": "83b84ecfa2c50d1727d771e9f5286e3d6a4333551fad5bc4ceaba2bf1259de43", + "accepted_source_manifest_sha256": "cdf44d1089e14f1309dd20a85c0d2fdca050d9a9120b7c1e40862e176447bafb", + "attribution": "Developed with OpenAI assistance; inherited NOTICE and Apache-2.0 license are retained.", + "exclusions": [ + "Width allocation or an input-dependent capacity proof", + "A transported cross-model linear amortized bound", + "Compact or canonical counter output", + "A source-program caller/prelude or Plan/Budget implementation", + "A first-completion theorem", + "A full multiplication theorem or kappa theorem" + ], + "isolated_replay": { + "path": "REPLAY_SUMMARY.json", + "sha256": "4f38e221f0a048d25b583e0772a58fab4ee171fa786d08c58cefff219cf59782", + "module_count": 6, + "all_objects_match_accepted": true, + "all_axiom_outputs_match_accepted": true + }, + "layout": "Flat single-directory source/evidence package, with external PR488 foundation paths unchanged." +} diff --git a/research/lean-binary-count-dispatcher/README.md b/research/lean-binary-count-dispatcher/README.md new file mode 100644 index 0000000000..09398894e1 --- /dev/null +++ b/research/lean-binary-count-dispatcher/README.md @@ -0,0 +1,35 @@ +# A concrete binary count dispatcher in Lean + +This package checks a seven-state, two-tape, three-symbol controller that reads an actual finite input word and dispatches one completed increment per bit. The input bits may be either value; the counter adds their number to its initial value, modulo 2^width for the supplied width. Four Lean sources are included, with two exact source dependencies from [PR488](https://github.com/CrocSwap/integer-mult-bounds/pull/488). PR488 need not be merged. + +## Checked contract + +For every input word and every supplied fixed-width counter bit list, `count_run` reaches the specified halted configuration in at most `(CarryTape.pass word.length bits).2.reads + 2 * word.length + 1` transitions. The input remains represented nearest-first to the left of its visited right blank. The counter returns to its home blank with the same width and value `(initial value + word.length) mod 2^width`. Empty input, zero width and wraparound are included. The counter's home and end blanks are distinct represented cells, including at zero width. + +The five-state one-tape increment adapter realizes the reused carry semantics in `2 * trailingOnes + 4` transitions. The controller lifts that table, detects its completion and restarts it from actual scanned symbols. Successful-prefix simulation is proved internally. It does not require a first-halting-time premise. + +This is a supplied-width modular-count helper. Width allocation, a cross-model linear amortized bound, compact output, the actual source prelude/caller, and Plan/Budget composition remain outside this package. It does not prove a full multiplication theorem or a κ bound. + +## Reuse and contribution + +[PR64](https://github.com/CrocSwap/integer-mult-bounds/pull/64) already supplies literal counter and stack machinery with richer direction, exterior-tape, first-completion and amortized guarantees. Binary increment is not claimed as new or improved here. The additional checked result is the explicit `CurrentMain.FixedTapeMachine` symbol-driven restart controller, its exact two-tape endpoint, and its connection to the existing carry-pass receipt. The controller reuses CarryTape/CarryTapePass; this six-module closure does not yet prove the PR64-to-current-model arithmetic transport. The two foundation files and the successful-prefix reduction pattern are reused from the [exact PR488 head](https://github.com/jamesyc/integer-mult-bounds/tree/edd3102b415df5b9d6f633ac0a4dedcf69c58525/research/lean-binary-input-preparation). + +## Reproduce + +Use Linux, Python3 and Lean4.21.0. The checker uses `/proc` for its memory observations and has no Python package dependencies. Obtain a separate checkout of the foundation repository at the exact commit in `FOUNDATIONS.json`, for example: + +```sh +git clone https://github.com/jamesyc/integer-mult-bounds.git foundation-repo +git -C foundation-repo checkout --detach edd3102b415df5b9d6f633ac0a4dedcf69c58525 +python3 check.py --lean /path/to/lean-4.21.0-linux/bin/lean \ + --foundation-root /path/to/foundation-repo/research/lean-binary-input-preparation \ + --build-dir /tmp/count-dispatcher-check +``` + +The build directory must not exist. The checker is offline: it validates both external source hashes and the four included source hashes, then compiles exactly six modules into that fresh directory. Its Lean search path contains only that output directory and the installed core library. No Mathlib is required. Per-module limits are 60 seconds and 4 GiB address space; a successful check over 40 seconds or 3.5 GiB stops for review. No object files are shipped. `ACCEPTED_CHECKS.json` records the exact source-level acceptance receipts and 36 standard-axiom probes. The isolated flat-layout six-module package replay passed in 8.8320 compiler seconds and 0.00303 queue seconds, with peak virtual memory 2,735,955,968 bytes. All six object hashes and all 36 printed axiom outputs matched the accepted sources; see `REPLAY_SUMMARY.json`. + +## Author-checked project context + +At base commit `12a4934d15006e8c10f9b2264f13f8f341be802b`, the selected conditional project value is κ=`90446448750933/125000000000000000`=`0.000723571590007464`. The captured source and linked certificate agree, as checked by the source author. This project context retains all-size compiler, weighted/common-ancestor chart, restored-row, selector/routing, prime-supply, precision/recovery, complex-symbolic and analytic-transfer assumptions. The generic dispatcher does not discharge those assumptions or prove this κ value. Exact source and dependency pins are in `PROVENANCE.json`, `FOUNDATIONS.json` and `MANIFEST.json`. + +The inherited Apache-2.0 license and source attribution are included. diff --git a/research/lean-binary-count-dispatcher/REPLAY_SUMMARY.json b/research/lean-binary-count-dispatcher/REPLAY_SUMMARY.json new file mode 100644 index 0000000000..69033f0b02 --- /dev/null +++ b/research/lean-binary-count-dispatcher/REPLAY_SUMMARY.json @@ -0,0 +1,163 @@ +{ + "status": "PASS", + "kind": "isolated flat-layout six-module public package reproducibility check", + "started_utc": "2026-10-11T20:52:02.001389+00:00", + "finished_utc": "2026-10-11T20:52:10.847701+00:00", + "manifest_sha256": "cdf44d1089e14f1309dd20a85c0d2fdca050d9a9120b7c1e40862e176447bafb", + "foundations_manifest_sha256": "fcac056292d2fb7aa2e5c8f91523f0255bdeb16f244f8edcec48ff9088949698", + "foundation_commit": "edd3102b415df5b9d6f633ac0a4dedcf69c58525", + "checker_sha256": "f312dcd0efce93383f110635464f2fc83bddd6e1962dbf24280e0f094c75b0a7", + "lean_version": "Lean (version 4.21.0, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)", + "lean_binary_sha256": "cbf5fd536e142ef1beaccf33f788fd8a7f3f29fb214e75c11319a8d8677b4b2b", + "external_library_paths": [], + "source_search_path_policy": "Fresh output directory only; exact two external source dependencies supplied offline.", + "module_count": 6, + "included_module_count": 4, + "external_source_dependency_count": 2, + "compile_seconds": 8.831995109999752, + "queue_seconds": 0.003029640000022482, + "peak_vm_bytes": 2735955968, + "axiom_probes": 36, + "all_objects_match_accepted": true, + "all_axiom_outputs_match_accepted": true, + "modules": [ + { + "module": "IntegerConvolution", + "source_sha256": "0bc86f2fa8e68f39df77be603d2a9634bc008745093286903105378ab45938ea", + "object_sha256": "72299b15d1bee37af56e1c5d10018d45784213c43461021afc4c213d1863af36", + "log_sha256": "c1aea8c6ec85d16aa991288c1dbd640d2047900b669fb59a79e5d084d150f0c5", + "started_utc": "2026-10-11T20:52:02.002274+00:00", + "finished_utc": "2026-10-11T20:52:03.214728+00:00", + "compile_seconds": 1.2121822950002752, + "queue_seconds": 0.0005177090001780016, + "peak_vm_bytes": 2265145344, + "axiom_output": [ + "'CurrentMain.IntegerConvolution.value_addCoefficients' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.IntegerConvolution.value_map_mul' depends on axioms: [propext]", + "'CurrentMain.IntegerConvolution.convolution_value' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.IntegerConvolution.binary_convolution' depends on axioms: [propext, Quot.sound]" + ], + "status": "PASS", + "receipt_sha256": "d1239d9e1ccd44a23ae5eaf2950ca0cd6f2fd6e451069aa362739733743e7060", + "object_matches_accepted": true, + "axioms_match_accepted": true + }, + { + "module": "FixedTapeMachine", + "source_sha256": "92dadedc9f6e23d12633549b53ca8f917360e4fedac0b64a58d18feea741a5ed", + "object_sha256": "88fa2e0c9e43f696f53762a345092d19fa3501d7b1de2381dfb335b232b53ff1", + "log_sha256": "36dc8dbc05e17722f16160959d84aea237a472b8a2435c0fd7dc140e3f704559", + "started_utc": "2026-10-11T20:52:03.216275+00:00", + "finished_utc": "2026-10-11T20:52:04.322622+00:00", + "compile_seconds": 1.1060579390000385, + "queue_seconds": 0.0006542389996866405, + "peak_vm_bytes": 2063859712, + "axiom_output": [ + "'CurrentMain.FixedTapeMachine.initial_inputA' depends on axioms: [propext]", + "'CurrentMain.FixedTapeMachine.initial_inputB' depends on axioms: [propext]", + "'CurrentMain.FixedTapeMachine.initial_output' depends on axioms: [propext]", + "'CurrentMain.FixedTapeMachine.run_halted' does not depend on any axioms", + "'CurrentMain.FixedTapeMachine.run_add' depends on axioms: [propext]" + ], + "status": "PASS", + "receipt_sha256": "d021f25e25165ef3a19fd1c82c4e44c0d33fc82d0748dbcea5530d9037213e62", + "object_matches_accepted": true, + "axioms_match_accepted": true + }, + { + "module": "CarryTape", + "source_sha256": "20d13d9d2da74452e45c0a175b643556615ba14187bf8fb0e4393e44842c17a5", + "object_sha256": "5ecb25ccf73c61eb5b4be13a69c73d9b7183201a71344e333761af7ea7915c74", + "log_sha256": "a269b42e17b5fd794216654bafc3ee3cc58c39fbbf5c36fa525eb42bfc739b67", + "started_utc": "2026-10-11T20:52:04.324868+00:00", + "finished_utc": "2026-10-11T20:52:05.920084+00:00", + "compile_seconds": 1.5950261329999194, + "queue_seconds": 0.0007879919999140839, + "peak_vm_bytes": 2735362048, + "axiom_output": [ + "'CurrentMain.CarryTape.run_add' depends on axioms: [propext]", + "'CurrentMain.CarryTape.carry_execution' depends on axioms: [propext]", + "'CurrentMain.CarryTape.rewind_execution' depends on axioms: [propext]", + "'CurrentMain.CarryTape.carryFinish_rewind' depends on axioms: [propext]", + "'CurrentMain.CarryTape.increment_execution' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.increment_length' depends on axioms: [propext]", + "'CurrentMain.CarryTape.all_ones_execution' depends on axioms: [propext, Quot.sound]" + ], + "status": "PASS", + "receipt_sha256": "e717b1998e34e1f3ec811a9794ce350bc5b4436e7a0d0b09c9c0029e169141b0", + "object_matches_accepted": true, + "axioms_match_accepted": true + }, + { + "module": "CarryTapePass", + "source_sha256": "680b5d16736880ac6a02f27e9503e1cc01479bb2b35bb7546d9108dcb4b4ef2b", + "object_sha256": "183f0edf242a2f6ecb9d9a07d62bc977d9fa04b3a32bad75a6c71344583c1147", + "log_sha256": "bf3a993154b0837224b4a4f76d6f48fc6508422904a4371309c777ba6936ddb6", + "started_utc": "2026-10-11T20:52:05.921859+00:00", + "finished_utc": "2026-10-11T20:52:07.715802+00:00", + "compile_seconds": 1.7935781440000937, + "queue_seconds": 0.0003293780000603874, + "peak_vm_bytes": 2735955968, + "axiom_output": [ + "'CurrentMain.CarryTape.value_bound' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.increment_value' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.increment_mod' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.pass_length' depends on axioms: [propext]", + "'CurrentMain.CarryTape.pass_value' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.pass_even' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.empty_pass_one' does not depend on any axioms", + "'CurrentMain.CarryTape.complete_pass' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.incrementReceipt_realized' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.pass_successor_realized' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.CarryTape.full_pass24_index_traffic' depends on axioms: [propext, Quot.sound]" + ], + "status": "PASS", + "receipt_sha256": "0dbe35d893e32389993037d36648d13498974cbebcd44b2126d8c88552c9c311", + "object_matches_accepted": true, + "axioms_match_accepted": true + }, + { + "module": "BinaryCarryIncrement", + "source_sha256": "b0f639159e2169c75e6d7a13663adee5107648a32b7ff9203f92792e31012dce", + "object_sha256": "07895c550c6298ae2143cca61c53399131f4b5a6a77b71f154c7ec6baa46ddc8", + "log_sha256": "d249a6aaa4e3eec29d84596b492eac68b52d6c14c115df389f20f5b313d1f0ae", + "started_utc": "2026-10-11T20:52:07.719713+00:00", + "finished_utc": "2026-10-11T20:52:09.116429+00:00", + "compile_seconds": 1.3964239449996967, + "queue_seconds": 0.0004314080001677212, + "peak_vm_bytes": 2065469440, + "axiom_output": [ + "'CurrentMain.BinaryCarryIncrement.increment_run' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.BinaryCarryIncrement.final_halted' depends on axioms: [propext]", + "'CurrentMain.BinaryCarryIncrement.increment_length' depends on axioms: [propext]", + "'CurrentMain.BinaryCarryIncrement.value_binding' does not depend on any axioms", + "'CurrentMain.BinaryCarryIncrement.increment_modular_value' depends on axioms: [propext, Quot.sound]" + ], + "status": "PASS", + "receipt_sha256": "10e56ac19d501d0ef81c0d1e0f1fc1d0a2e007f7eace4fbd5180cdaa988665d3", + "object_matches_accepted": true, + "axioms_match_accepted": true + }, + { + "module": "BinaryCountDispatcher", + "source_sha256": "ec24af9483d59ce3248802378218d4b478490aa2458e136880f36e7f49356e93", + "object_sha256": "6685bcc5f2657f829149fa21e0140e063750680997c072cbe2c661e5190fa97e", + "log_sha256": "c54652b47292efff363956e0ec0af2eeb791be77b01213b6adbc7807576f81f1", + "started_utc": "2026-10-11T20:52:09.117578+00:00", + "finished_utc": "2026-10-11T20:52:10.846582+00:00", + "compile_seconds": 1.728726653999729, + "queue_seconds": 0.0003089140000156476, + "peak_vm_bytes": 2603061248, + "axiom_output": [ + "'CurrentMain.BinaryCountDispatcher.count_run' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.BinaryCountDispatcher.final_halted' depends on axioms: [propext, Quot.sound]", + "'CurrentMain.BinaryCountDispatcher.counter_length' depends on axioms: [propext]", + "'CurrentMain.BinaryCountDispatcher.counter_value' depends on axioms: [propext, Quot.sound]" + ], + "status": "PASS", + "receipt_sha256": "97bfafb7e58e7136d6296ef0922307f4790fcf0d0bb833af54d14b509838131d", + "object_matches_accepted": true, + "axioms_match_accepted": true + } + ] +} diff --git a/research/lean-binary-count-dispatcher/SHA256SUMS b/research/lean-binary-count-dispatcher/SHA256SUMS new file mode 100644 index 0000000000..8cc00263e8 --- /dev/null +++ b/research/lean-binary-count-dispatcher/SHA256SUMS @@ -0,0 +1,16 @@ +e6531f162e9381b6c33bfbebfb02cb5be026368d70f6f8a3e40822b9633aeab7 ACCEPTED_CHECKS.json +ee6780dc8a0a7c1ffde3aaf5dede52311ca9b65d49f884bed1aa02074de714ef AUTHOR_CHECK.json +b0f639159e2169c75e6d7a13663adee5107648a32b7ff9203f92792e31012dce BinaryCarryIncrement.lean +ec24af9483d59ce3248802378218d4b478490aa2458e136880f36e7f49356e93 BinaryCountDispatcher.lean +20d13d9d2da74452e45c0a175b643556615ba14187bf8fb0e4393e44842c17a5 CarryTape.lean +680b5d16736880ac6a02f27e9503e1cc01479bb2b35bb7546d9108dcb4b4ef2b CarryTapePass.lean +fcac056292d2fb7aa2e5c8f91523f0255bdeb16f244f8edcec48ff9088949698 FOUNDATIONS.json +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +cdf44d1089e14f1309dd20a85c0d2fdca050d9a9120b7c1e40862e176447bafb MANIFEST.json +2cf3c6e1aaaed287d44d001f55cfd74393c9d9e773e3ea0e3fb359d885b4f6b5 NOTICE.source.txt +aef823808c948bc557eff3ecde8cb0c6257cb1074665c4bbf1428ef343e68b51 PROVENANCE.json +9f322996b3e82f7cb4aef40f270d130638a80c869e6877bd4c1ab11163858f7e README.md +4f38e221f0a048d25b583e0772a58fab4ee171fa786d08c58cefff219cf59782 REPLAY_SUMMARY.json +f312dcd0efce93383f110635464f2fc83bddd6e1962dbf24280e0f094c75b0a7 check.py +d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c lean-toolchain +df836c6d34509e980d067bd5678489c968bc6e329af9dd82c6207abf6443da89 selected-result.json diff --git a/research/lean-binary-count-dispatcher/check.py b/research/lean-binary-count-dispatcher/check.py new file mode 100644 index 0000000000..b8ed4cbef4 --- /dev/null +++ b/research/lean-binary-count-dispatcher/check.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Offline exact six-source replay using two separately pinned PR488 foundations.""" +import argparse,fcntl,hashlib,importlib.util,json,os,re,resource,signal,subprocess,time +from pathlib import Path +from datetime import datetime,timezone +ROOT=Path(__file__).resolve().parent +sha=lambda p:hashlib.sha256(Path(p).read_bytes()).hexdigest() +now=lambda:datetime.now(timezone.utc).isoformat() +def limits(): + resource.setrlimit(resource.RLIMIT_AS,(4*1024**3,4*1024**3)) + resource.setrlimit(resource.RLIMIT_CPU,(60,62));os.setsid() +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--lean',required=True);ap.add_argument('--foundation-root',required=True,help='Path to the exact PR488 research/lean-binary-input-preparation package.');ap.add_argument('--build-dir',default='.build');ap.add_argument('--slot-service',help='Optional existing FIFO slot service exposing acquire(); does not change Lean inputs.');ap.add_argument('--lean-sha256');args=ap.parse_args() + assert Path('/proc/self/status').is_file(),'Linux /proc is required for the stated memory review' + foundation_root=Path(args.foundation_root).resolve();assert foundation_root.is_dir() + source_for=lambda row:(foundation_root if row['origin']=='pr488' else ROOT)/row['file'] + lean=Path(args.lean).resolve();assert lean.is_file() + if args.lean_sha256:assert sha(lean)==args.lean_sha256 + version=subprocess.check_output([str(lean),'--version'],text=True).strip();assert re.search(r'\b4\.21\.0\b',version),version + manifest=json.loads((ROOT/'MANIFEST.json').read_text());rows=manifest['compile_order'];names={r['module']for r in rows};seen=set() + assert len(rows)==6 and manifest['source_bytes']==44164 + assert sum(r['origin']=='pr488' for r in rows)==2 and sum(r['origin']=='package' for r in rows)==4 + foundations=json.loads((ROOT/'FOUNDATIONS.json').read_text());assert foundations['commit']=='edd3102b415df5b9d6f633ac0a4dedcf69c58525' + for dep in foundations['files']: + row=next(r for r in rows if r['module']==dep['module']);assert row['origin']=='pr488' and row['sha256']==dep['sha256'] and row['bytes']==dep['bytes'] + for row in rows: + p=source_for(row);assert p.is_file()and sha(p)==row['sha256']and p.stat().st_size==row['bytes'],row['module'] + imports=[] + for line in p.read_text().splitlines(): + m=re.match(r'^import\s+(.+)$',line) + if m:imports.extend(m[1].split('--',1)[0].split()) + assert imports==row['imports'];assert set(imports)-{'Lean'}<=seen;seen.add(row['module']) + build=Path(args.build_dir);build=build if build.is_absolute()else ROOT/build;build.mkdir(parents=True,exist_ok=False);(build/'logs').mkdir();(build/'receipts').mkdir() + service=None + if args.slot_service: + spec=importlib.util.spec_from_file_location('existing_lean_slot_service',Path(args.slot_service).resolve());service=importlib.util.module_from_spec(spec);spec.loader.exec_module(service) + env=dict(os.environ);env['LEAN_PATH']=str(build);env['LEAN_EXTRA_PATHS']='';env.pop('LEAN_SYSROOT',None);env['MIMALLOC_ARENA_RESERVE']='64MiB' + outcome={'started_utc':now(),'manifest_sha256':sha(ROOT/'MANIFEST.json'),'foundations_manifest_sha256':sha(ROOT/'FOUNDATIONS.json'),'foundation_commit':foundations['commit'],'lean_version':version,'lean_binary_sha256':sha(lean),'external_library_paths':[],'source_search_path':str(build),'status':'RUNNING','receipts':[]};(build/'REPLAY_RESULT.json').write_text(json.dumps(outcome,indent=2)+'\n') + for row in rows: + requested=time.monotonic();slot=None;handle=None;handles=[] + if service:slot,handle,handles=service.acquire('isolated_count_dispatcher_package:'+row['module']) + queue=time.monotonic()-requested;started=time.monotonic();start_utc=now();source=source_for(row);output_path=build/(row['module']+'.olean');log=build/'logs'/(row['module']+'.log');peak=0;samples=0;timed_out=False + try: + assert sha(source)==row['sha256'];cmd=[str(lean),'-s','65536','-j','1','-o',str(output_path),source.name] + proc=subprocess.Popen(cmd,cwd=source.parent,env=env,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,preexec_fn=limits) + while True: + try: + text=Path(f'/proc/{proc.pid}/status').read_text();m=re.search(r'^VmPeak:\s+(\d+)',text,re.M);peak=max(peak,int(m[1])*1024 if m else 0);samples+=1 + except OSError:pass + remaining=60-(time.monotonic()-started) + if remaining<=0: + timed_out=True;os.killpg(proc.pid,signal.SIGKILL);data,_=proc.communicate();break + try:data,_=proc.communicate(timeout=min(.1,remaining));break + except subprocess.TimeoutExpired:pass + elapsed=time.monotonic()-started;log.write_bytes(data);text=data.decode(errors='replace');forbidden=('sorryAx'in text or "declaration uses 'sorry'"in text) + passed=proc.returncode==0 and not timed_out and not forbidden and output_path.is_file()and sha(source)==row['sha256'];review=passed and(elapsed>40 or peak>int(3.5*1024**3)) + rec={'module':row['module'],'source_sha256':row['sha256'],'status':'PASS'if passed else'FAIL','review_stop':review,'exit_code':proc.returncode,'timed_out':timed_out,'started_utc':start_utc,'finished_utc':now(),'compile_seconds':elapsed,'queue_seconds':queue,'peak_vm_bytes':peak,'samples':samples,'slot':slot,'log_sha256':sha(log),'object_sha256':sha(output_path)if passed else None,'imports':row['imports'],'axiom_output':[s for s in text.splitlines()if'depends on axioms:'in s or'does not depend on any axioms'in s]};rp=build/'receipts'/(row['module']+'.json');rp.write_text(json.dumps(rec,indent=2)+'\n');outcome['receipts'].append({'module':row['module'],'receipt_sha256':sha(rp),'status':rec['status']});outcome['status']='REVIEW_STOP'if review else('RUNNING'if passed else'FAIL');(build/'REPLAY_RESULT.json').write_text(json.dumps(outcome,indent=2)+'\n');print(json.dumps(rec),flush=True) + if not passed or review:return 2 + finally: + if handle:fcntl.flock(handle,fcntl.LOCK_UN) + for h in handles:h.close() + outcome['status']='PASS';outcome['finished_utc']=now();outcome['modules']=len(outcome['receipts']);(build/'REPLAY_RESULT.json').write_text(json.dumps(outcome,indent=2)+'\n');print('PASS exact isolated6-module dispatcher closure',flush=True);return 0 +if __name__=='__main__':raise SystemExit(main()) diff --git a/research/lean-binary-count-dispatcher/lean-toolchain b/research/lean-binary-count-dispatcher/lean-toolchain new file mode 100644 index 0000000000..980709bbba --- /dev/null +++ b/research/lean-binary-count-dispatcher/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.21.0 diff --git a/research/lean-binary-count-dispatcher/selected-result.json b/research/lean-binary-count-dispatcher/selected-result.json new file mode 100644 index 0000000000..af3efd2f01 --- /dev/null +++ b/research/lean-binary-count-dispatcher/selected-result.json @@ -0,0 +1,33 @@ +{ + "status": "Published on main: maintainer-reviewed conditional construction", + "kappa": "90446448750933/125000000000000000", + "decimal": "0.000723571590007464", + "source_prs": [ + 279, + 276, + 244, + 234, + 209, + 197, + 237, + 200, + 193, + 168, + 144 + ], + "source_manifest": "research/five-stage-gen4-banks/MANIFEST.json", + "certificate": "research/community-pr279-audit/certificate.json", + "certificate_sha256": "6a457a34b4db57417e5b253cf1c169da2bd6aff4c21363a31fd85dc931d49589", + "proof": "research/five-stage-gen4-banks/PROOF.md", + "proof_supplements": { + "research/five-stage-gen4-banks/BANK-PROOF.md": "bbc328e05848a211c981288514380a4ba12fddaed16c9d23328b5764502be411" + }, + "review": "docs/research/community-pr279-review.md", + "validation": "docs/research/community-pr279-integration.json", + "reproduce": "make gen4-bank-verify", + "scope": "Conditional on retained all-size compiler, weighted/common-ancestor chart, restored rows, selectors/routing, prime supply, precision/recovery, complex symbolic correctness and analytic transfer; finite replay and written review, not a full formal multiplication theorem.", + "previous_kappa": "330942774629799/500000000000000000", + "previous_certificate": "research/coordinated-frames-and-entrance-banks/certificate.json", + "previous_audited_kappa": "710046193349537/1000000000000000000", + "audited_source_head": "4d8c31eec7ae618645cb058101cb4e72a97268d3" +} diff --git a/scripts/experiments/joint_dual_compose.py b/scripts/experiments/joint_dual_compose.py index 1db1f1f606..ae8fdf1248 100644 --- a/scripts/experiments/joint_dual_compose.py +++ b/scripts/experiments/joint_dual_compose.py @@ -60,7 +60,7 @@ def check_sources(): required.update(f'certificates/joint-dual-{kind}-{h}.{extension}' for h in (23,25) for kind, extension in (('word','json.gz'),('profiles','json'),('transitions','json'))) required.update(('certificates/joint-dual-compiler.json', 'certificates/skip-frame-kappa.json', - 'scripts/experiments/pin_joint_dual_sources.py', 'Makefile', 'README.md', 'NOTICE')) + 'scripts/experiments/pin_joint_dual_sources.py')) comparison = ROOT/'references/frame-compiler/pr58' required.add('references/frame-compiler/pr58/SOURCE.json') required.update('references/frame-compiler/pr58/'+name diff --git a/scripts/experiments/pin_joint_dual_sources.py b/scripts/experiments/pin_joint_dual_sources.py index 94ec6bd77b..0b0299088a 100644 --- a/scripts/experiments/pin_joint_dual_sources.py +++ b/scripts/experiments/pin_joint_dual_sources.py @@ -12,7 +12,7 @@ def run(): names = {'scripts/experiments/'+name for name in NAMES} - names.update(('Makefile', 'README.md', 'NOTICE', 'research/joint-dual/README.md', + names.update(('research/joint-dual/README.md', 'research/joint-dual/PROOF.md', 'certificates/joint-dual-compiler.json', 'certificates/skip-frame-kappa.json', 'tests/test_joint_reclaim.py')) for h in (23,25):