From 6b0891218a01d8ee76b892a607c45bdf8949ed9f Mon Sep 17 00:00:00 2001 From: illuzen Date: Mon, 13 Jul 2026 17:19:17 +0800 Subject: [PATCH 1/4] upgrade rand --- Cargo.lock | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 025f576..bb1f7da 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -479,9 +479,9 @@ dependencies = [ [[package]] name = "rand" -version = "0.8.5" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +checksum = "22f6172bdec972074665ed81ed53b71da00bfc44b65a753cfde883ec4c702a1a" dependencies = [ "libc", "rand_chacha", From 88f0384a27fec1e45d30ac9755f6051840f9afb1 Mon Sep 17 00:00:00 2001 From: illuzen Date: Mon, 13 Jul 2026 17:33:56 +0800 Subject: [PATCH 2/4] trim criterion --- Cargo.lock | 378 ++++++++++------------------------------------------- Cargo.toml | 2 +- 2 files changed, 68 insertions(+), 312 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index bb1f7da..688e6ac 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 4 [[package]] name = "aho-corasick" -version = "1.1.3" +version = "1.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916" +checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" dependencies = [ "memchr", ] @@ -28,9 +28,9 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.11" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "862ed96ca487e809f1c8e5a8447f6ee2cf102f846893800b20cebdf541fc6bbd" +checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" [[package]] name = "atty" @@ -45,9 +45,9 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.5.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" [[package]] name = "bitflags" @@ -57,9 +57,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.9.4" +version = "2.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2261d10cca569e4643e526d8dc2e62e433cc8aba21ab764233731f8d369bf394" +checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8" [[package]] name = "block2" @@ -70,12 +70,6 @@ dependencies = [ "objc2", ] -[[package]] -name = "bumpalo" -version = "3.19.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46c5e41b57b8bba42a04676d81cb89e9ee8e859a1a66f80a5a72e1cb76b34d43" - [[package]] name = "cast" version = "0.3.0" @@ -84,9 +78,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] name = "cfg-if" -version = "1.0.3" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2fd1289c04a9ea8cb22300a459a72a385d7c73d3259e2ed7dcb2af674838cfa9" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" [[package]] name = "cfg_aliases" @@ -138,18 +132,18 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.48" +version = "4.6.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2134bb3ea021b78629caa971416385309e0131b351b25e01dc16fb54e1b5fae" +checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51" dependencies = [ "clap_builder", ] [[package]] name = "clap_builder" -version = "4.5.48" +version = "4.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2ba64afa3c0a6df7fa517765e31314e983f51dda798ffba27b988194fb65dc9" +checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f" dependencies = [ "anstyle", "clap_lex", @@ -157,9 +151,9 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.7.5" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b94f61472cee1439c0b966b47e3aca9ae07e45d070759512cd390ea2bebc6675" +checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" [[package]] name = "criterion" @@ -170,15 +164,13 @@ dependencies = [ "anes", "cast", "ciborium", - "clap 4.5.48", + "clap 4.6.1", "criterion-plot", "is-terminal", "itertools", "num-traits", "once_cell", "oorandom", - "plotters", - "rayon", "regex", "serde", "serde_derive", @@ -197,31 +189,6 @@ dependencies = [ "itertools", ] -[[package]] -name = "crossbeam-deque" -version = "0.8.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51" -dependencies = [ - "crossbeam-epoch", - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-epoch" -version = "0.9.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2d6914041f254d6e9176c01941b21115dcfb7089e55135a35411081bd106ef3f" -dependencies = [ - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-utils" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" - [[package]] name = "crunchy" version = "0.2.4" @@ -230,13 +197,13 @@ checksum = "460fbee9c2c2f33933d720630a6a0bac33ba7053db5344fac858d4b8952d77d5" [[package]] name = "ctrlc" -version = "3.5.1" +version = "3.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "73736a89c4aff73035ba2ed2e565061954da00d4970fc9ac25dcc85a2a20d790" +checksum = "e0b1fab2ae45819af2d0731d60f2afe17227ebb1a1538a236da84c93e9a60162" dependencies = [ "dispatch2", "nix", - "windows-sys 0.61.0", + "windows-sys", ] [[package]] @@ -245,7 +212,7 @@ version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e0e367e4e7da84520dedcac1901e4da967309406d1e51017ae1abfb97adbd38" dependencies = [ - "bitflags 2.9.4", + "bitflags 2.13.0", "block2", "libc", "objc2", @@ -265,9 +232,9 @@ dependencies = [ [[package]] name = "either" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" +checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e" [[package]] name = "getrandom" @@ -282,12 +249,13 @@ dependencies = [ [[package]] name = "half" -version = "2.6.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "459196ed295495a68f7d7fe1d84f6c4b7ff0e21fe3017b2f283c6fac3ad803c9" +checksum = "6ea2d84b969582b4b1864a92dc5d27cd2b77b622a8d79306834f1be5ba20d84b" dependencies = [ "cfg-if", "crunchy", + "zerocopy", ] [[package]] @@ -313,13 +281,13 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" [[package]] name = "is-terminal" -version = "0.4.16" +version = "0.4.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e04d7f318608d35d4b61ddd75cbdaee86b023ebe2bd5a66ee0915f0bf93095a9" +checksum = "3640c1c38b8e4e43584d8df18be5fc6b0aa314ce6ebf51b53313d4306cca8e46" dependencies = [ "hermit-abi 0.5.2", "libc", - "windows-sys 0.59.0", + "windows-sys", ] [[package]] @@ -333,45 +301,29 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.15" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4a5f13b858c8d314ee3e8f639011f7ccefe71f97f96e50151fb991f267928e2c" - -[[package]] -name = "js-sys" -version = "0.3.80" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "852f13bec5eba4ba9afbeb93fd7c13fe56147f055939ae21c43a29a0ecb2702e" -dependencies = [ - "once_cell", - "wasm-bindgen", -] +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" [[package]] name = "libc" -version = "0.2.175" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a82ae493e598baaea5209805c49bbf2ea7de956d50d7da0da1164f9c6d28543" - -[[package]] -name = "log" -version = "0.4.28" +version = "0.2.186" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34080505efa8e45a4b816c349525ebe327ceaa8559756f0356cba97ef3bf7432" +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" [[package]] name = "memchr" -version = "2.7.5" +version = "2.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a282da65faaf38286cf3be983213fcf1d2e2a58700e808f83f4ea9a4804bc0" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" [[package]] name = "nix" -version = "0.30.1" +version = "0.31.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74523f3a35e05aba87a1d978330aef40f67b0304ac79c1c00b294c9830543db6" +checksum = "cf20d2fde8ff38632c426f1165ed7436270b44f199fc55284c38276f9db47c3d" dependencies = [ - "bitflags 2.9.4", + "bitflags 2.13.0", "cfg-if", "cfg_aliases", "libc", @@ -403,9 +355,9 @@ checksum = "ef25abbcd74fb2609453eb695bd2f860d389e457f67dc17cafc8b8cbc89d0c33" [[package]] name = "once_cell" -version = "1.21.3" +version = "1.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d" +checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" [[package]] name = "oorandom" @@ -413,34 +365,6 @@ version = "11.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e" -[[package]] -name = "plotters" -version = "0.3.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5aeb6f403d7a4911efb1e33402027fc44f29b5bf6def3effcc22d7bb75f2b747" -dependencies = [ - "num-traits", - "plotters-backend", - "plotters-svg", - "wasm-bindgen", - "web-sys", -] - -[[package]] -name = "plotters-backend" -version = "0.3.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "df42e13c12958a16b3f7f4386b9ab1f3e7933914ecea48da7139435263a4172a" - -[[package]] -name = "plotters-svg" -version = "0.3.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51bae2ac328883f7acdfea3d66a7c35751187f870bc81f94563733a154d7a670" -dependencies = [ - "plotters-backend", -] - [[package]] name = "ppv-lite86" version = "0.2.21" @@ -452,9 +376,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.101" +version = "1.0.106" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89ae43fd86e4158d6db51ad8e2b80f313af9cc74f5c0e03ccb87de09998732de" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" dependencies = [ "unicode-ident", ] @@ -470,9 +394,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.40" +version = "1.0.46" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1885c039570dc00dcb4ff087a89e185fd56bae234ddc7f056a945bf36467248d" +checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368" dependencies = [ "proc-macro2", ] @@ -507,31 +431,11 @@ dependencies = [ "getrandom", ] -[[package]] -name = "rayon" -version = "1.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "368f01d005bf8fd9b1206fb6fa653e6c4a81ceb1466406b81792d87c5677a58f" -dependencies = [ - "either", - "rayon-core", -] - -[[package]] -name = "rayon-core" -version = "1.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22e18b0f0062d30d4230b2e85ff77fdfe4326feb054b9783a3460d8435c8ab91" -dependencies = [ - "crossbeam-deque", - "crossbeam-utils", -] - [[package]] name = "regex" -version = "1.11.2" +version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23d7fd106d8c02486a8d64e778353d1cffe08ce79ac2e82f540c86d0facf6912" +checksum = "2a0e75113e14dc5acb068cd0786884f214f1312650a3d36d269f5c4f3cdee8a2" dependencies = [ "aho-corasick", "memchr", @@ -541,9 +445,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.10" +version = "0.4.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b9458fa0bfeeac22b5ca447c63aaf45f28439a709ccd244698632f9aa6394d6" +checksum = "1f388202e4b80542a0921078cc23b6333bcf1409c1e3f86404cae4766a6131db" dependencies = [ "aho-corasick", "memchr", @@ -552,15 +456,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.8.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "caf4aa5b0f434c91fe5c7f1ecb6a5ece2130b02ad2a590589dda5146df959001" - -[[package]] -name = "rustversion" -version = "1.0.22" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" [[package]] name = "same-file" @@ -603,9 +501,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.149" +version = "1.0.150" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83fc039473c5595ace860d8c4fafa220ff474b3fc6bfdb4293327f1a37e94d86" +checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9" dependencies = [ "itoa", "memchr", @@ -622,9 +520,9 @@ checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" [[package]] name = "syn" -version = "2.0.106" +version = "2.0.118" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ede7c438028d4436d71104916910f5bb611972c5cfd7f89b8300a8186e6fada6" +checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422" dependencies = [ "proc-macro2", "quote", @@ -652,9 +550,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.19" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f63a545481291138910575129486daeaf8ac54aee4387fe7906919f7830c7d9d" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" [[package]] name = "unicode-width" @@ -684,75 +582,6 @@ version = "0.11.1+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" -[[package]] -name = "wasm-bindgen" -version = "0.2.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ab10a69fbd0a177f5f649ad4d8d3305499c42bab9aef2f7ff592d0ec8f833819" -dependencies = [ - "cfg-if", - "once_cell", - "rustversion", - "wasm-bindgen-macro", - "wasm-bindgen-shared", -] - -[[package]] -name = "wasm-bindgen-backend" -version = "0.2.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0bb702423545a6007bbc368fde243ba47ca275e549c8a28617f56f6ba53b1d1c" -dependencies = [ - "bumpalo", - "log", - "proc-macro2", - "quote", - "syn", - "wasm-bindgen-shared", -] - -[[package]] -name = "wasm-bindgen-macro" -version = "0.2.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fc65f4f411d91494355917b605e1480033152658d71f722a90647f56a70c88a0" -dependencies = [ - "quote", - "wasm-bindgen-macro-support", -] - -[[package]] -name = "wasm-bindgen-macro-support" -version = "0.2.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ffc003a991398a8ee604a401e194b6b3a39677b3173d6e74495eb51b82e99a32" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "wasm-bindgen-backend", - "wasm-bindgen-shared", -] - -[[package]] -name = "wasm-bindgen-shared" -version = "0.2.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "293c37f4efa430ca14db3721dfbe48d8c33308096bd44d80ebaa775ab71ba1cf" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "web-sys" -version = "0.3.80" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fbe734895e869dc429d78c4b433f8d17d95f8d05317440b4fad5ab2d33e596dc" -dependencies = [ - "js-sys", - "wasm-bindgen", -] - [[package]] name = "winapi" version = "0.3.9" @@ -775,7 +604,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.61.0", + "windows-sys", ] [[package]] @@ -786,106 +615,33 @@ checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" [[package]] name = "windows-link" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45e46c0661abb7180e7b9c281db115305d49ca1709ab8242adf09666d2173c65" - -[[package]] -name = "windows-sys" -version = "0.59.0" +version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" [[package]] name = "windows-sys" -version = "0.61.0" +version = "0.61.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e201184e40b2ede64bc2ea34968b28e33622acdbbf37104f0e4a33f7abe657aa" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" dependencies = [ "windows-link", ] -[[package]] -name = "windows-targets" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" -dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" - -[[package]] -name = "windows_aarch64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[package]] -name = "windows_i686_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" - -[[package]] -name = "windows_x86_64_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" - -[[package]] -name = "windows_x86_64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - [[package]] name = "zerocopy" -version = "0.8.27" +version = "0.8.54" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0894878a5fa3edfd6da3f88c4805f4c8558e2b996227a3d864f47fe11e38282c" +checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.8.27" +version = "0.8.54" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88d2b8d9c68ad2b9e4340d7832716a4d21a22a1154777ad56ea55c51a9cf3831" +checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5" dependencies = [ "proc-macro2", "quote", @@ -894,6 +650,6 @@ dependencies = [ [[package]] name = "zmij" -version = "1.0.21" +version = "1.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" +checksum = "bd2f034a4bebf216c9e4b7083603e024cf930873fd67830cfb083c9fa33129d9" diff --git a/Cargo.toml b/Cargo.toml index 614a764..8ec07ad 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,7 +20,7 @@ categories = ["cryptography", "no-std"] [dev-dependencies] hex = "0.4.3" -criterion = { version = "0.5", features = ["html_reports"] } +criterion = { version = "0.5", default-features = false, features = ["cargo_bench_support"] } dudect-bencher = "0.6" [features] From bf066527d5c9ced092ff5f2f6abd3e5e5629efc9 Mon Sep 17 00:00:00 2001 From: illuzen Date: Mon, 13 Jul 2026 18:46:52 +0800 Subject: [PATCH 3/4] add Lean formal spec for goldilocks.rs arithmetic Co-authored-by: Cursor --- .github/workflows/ci.yml | 60 +++++ formal/.gitignore | 1 + formal/GoldilocksSpec.lean | 2 + formal/GoldilocksSpec/Correctness.lean | 358 +++++++++++++++++++++++++ formal/GoldilocksSpec/Model.lean | 174 ++++++++++++ formal/ci/AxiomsCheck.lean | 12 + formal/lake-manifest.json | 6 + formal/lakefile.toml | 13 + formal/lean-toolchain | 1 + 9 files changed, 627 insertions(+) create mode 100644 formal/.gitignore create mode 100644 formal/GoldilocksSpec.lean create mode 100644 formal/GoldilocksSpec/Correctness.lean create mode 100644 formal/GoldilocksSpec/Model.lean create mode 100644 formal/ci/AxiomsCheck.lean create mode 100644 formal/lake-manifest.json create mode 100644 formal/lakefile.toml create mode 100644 formal/lean-toolchain diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 34a708a..0394bf7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -102,6 +102,66 @@ jobs: - name: Generate documentation (workspace) run: cargo doc --workspace --locked --no-deps --all-features --release + formal-spec: + name: 📐 Formal Spec (Lean) + needs: fast-checks + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@v5 + # Builds the Lean 4 formal spec under `formal/`: machine-checked proofs that + # the hand-optimized Goldilocks arithmetic in `src/goldilocks.rs` (overflow + # tricks, NEG_ORDER corrections, `assume` UB-hints, reduce128) is correct + # mod p on the full non-canonical u64 range. The package is deliberately + # mathlib-free and builds in seconds; `lake build` type-checks every proof + # in the kernel, so an edit that breaks a proof fails CI instead of rotting + # silently. elan/lake are installed from `formal/lean-toolchain` (Lean v4.30). + # + # Defense-in-depth: `leanchecker` re-checks the compiled environment with an + # independent kernel checker (bundled on v4.30). + - name: Build formal spec (lake build) + # Pinned to a full commit SHA (supply-chain hardening). 38fbc41 == v1.5.0. + uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 + with: + lake-package-directory: "formal" + use-mathlib-cache: "false" + leanchecker: "true" + # No-`sorry` gate: the spec must stay gap-free. Fail if any proof term uses a + # `sorry`/`admit`/`sorryAx` placeholder. (Keep the literal words out of + # comments/strings under `formal/` so this stays a clean signal.) + - name: Assert the spec contains no sorry/admit + run: | + if grep -rEn '\b(sorry|admit|sorryAx)\b' --include='*.lean' formal --exclude-dir=.lake; then + echo "::error::formal spec contains a sorry/admit placeholder" + exit 1 + fi + # Axiom-footprint gate: the capstone `goldilocks_tier1` must depend on + # exactly the standard Lean axioms — no placeholder axiom, no + # `Lean.ofReduceBool` (native evaluation), no stray `axiom` declarations. + - name: Assert goldilocks_tier1 axiom footprint + run: | + set -euo pipefail + cd formal + output=$(lake env lean ci/AxiomsCheck.lean 2>&1) + printf '%s\n' "$output" + if ! grep -q 'depends on axioms' <<< "$output"; then + echo "::error::could not read #print axioms for GoldilocksSpec.goldilocks_tier1" + exit 1 + fi + axioms=$(sed -n '/depends on axioms:/,/]/p' <<< "$output" | tr -d '\n' | sed 's/.*\[\(.*\)\].*/\1/' | tr ',' '\n' | sed 's/^[[:space:]]*//;s/[[:space:]]*$//' | grep -v '^$' | sort) + expected=$(printf '%s\n' \ + 'propext' \ + 'Classical.choice' \ + 'Quot.sound' | sort) + if [ "$axioms" != "$expected" ]; then + echo "::error::goldilocks_tier1 axiom footprint mismatch" + echo "expected exactly:" + printf ' %s\n' "$expected" + echo "got:" + printf ' %s\n' "$axioms" + exit 1 + fi + security-audit: name: 🔐 Security Audit (non-blocking) needs: fast-checks diff --git a/formal/.gitignore b/formal/.gitignore new file mode 100644 index 0000000..4080d07 --- /dev/null +++ b/formal/.gitignore @@ -0,0 +1 @@ +/.lake/ diff --git a/formal/GoldilocksSpec.lean b/formal/GoldilocksSpec.lean new file mode 100644 index 0000000..3eeb70a --- /dev/null +++ b/formal/GoldilocksSpec.lean @@ -0,0 +1,2 @@ +import GoldilocksSpec.Model +import GoldilocksSpec.Correctness diff --git a/formal/GoldilocksSpec/Correctness.lean b/formal/GoldilocksSpec/Correctness.lean new file mode 100644 index 0000000..3aeff51 --- /dev/null +++ b/formal/GoldilocksSpec/Correctness.lean @@ -0,0 +1,358 @@ +import GoldilocksSpec.Model + +/-! +# Tier-1 correctness of the optimized Goldilocks arithmetic + +For every operation `op` in `src/goldilocks.rs` (modeled in +`GoldilocksSpec.Model`) we prove, assuming only that the inputs are machine +words (`< 2^64` — canonicality is NOT assumed, since the crate's +representation is non-canonical by design): + + * **congruence**: the result equals the mathematical field operation mod P, + stated as a `Nat` congruence, e.g. `rustAdd a b % P = (a + b) % P`; + * **closure**: the result is again a machine word (`< 2^64`); + * **no silent wrap**: every `+=` / `-=` / `wrapping_*` the Rust annotates + with "Cannot overflow" / "Cannot underflow" really cannot, and each + `assume(..)` UB-hint is implied by its branch condition (so the + `unreachable_unchecked` inside `assume` is never reached). + +On the `ZMod P` reading: casting `Nat → ZMod P` identifies `x` with `x % P`, +so e.g. `rustAdd a b % P = (a + b) % P` is precisely +`(↑(rustAdd a b) : ZMod P) = ↑a + ↑b`. We state the `Nat` form to keep the +package dependency-free (no mathlib), mirroring qp-zk-circuits/formal. + +The capstone `goldilocks_tier1` bundles every theorem; CI asserts its axiom +footprint is exactly the standard Lean axioms. +-/ + +namespace GoldilocksSpec + +/-! ### Numeric literals for `omega` -/ + +theorem two_pow_32 : (2 : Nat) ^ 32 = 4294967296 := by decide +theorem two_pow_64 : (2 : Nat) ^ 64 = 18446744073709551616 := by decide +theorem two_pow_96 : (2 : Nat) ^ 96 = 79228162514264337593543950336 := by decide +theorem two_pow_128 : (2 : Nat) ^ 128 = 340282366920938463463374607431768211456 := by decide + +/-! ### `as_canonical_u64`, `is_zero`, `eq` -/ + +/-- One conditional subtraction fully canonicalizes, because `2 * P` does not +fit in a `u64` (justifying the comment at `goldilocks.rs:92`). -/ +theorem rustCanonical_eq_mod {a : Nat} (ha : a < 2 ^ 64) : + rustCanonical a = a % P := by + simp only [rustCanonical, P, two_pow_64] at * + split <;> omega + +theorem rustCanonical_lt_P {a : Nat} (ha : a < 2 ^ 64) : rustCanonical a < P := by + simp only [rustCanonical, P, two_pow_64] at * + split <;> omega + +/-- `is_zero` recognizes exactly the two representatives of `0`. -/ +theorem rustIsZero_iff {a : Nat} (ha : a < 2 ^ 64) : rustIsZero a ↔ a % P = 0 := by + simp only [rustIsZero, P, two_pow_64] at * + omega + +/-- `==` on `Goldilocks` decides equality of residues mod P. -/ +theorem rustEq_iff {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : + rustEq a b ↔ a % P = b % P := by + simp only [rustEq, rustCanonical, P, two_pow_64] at * + split <;> split <;> omega + +/-! ### Addition -/ + +theorem rustAdd_lt (a b : Nat) : rustAdd a b < 2 ^ 64 := by + simp only [rustAdd] + exact Nat.mod_lt _ (by decide) + +theorem rustAdd_mod {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : + rustAdd a b % P = (a + b) % P := by + simp only [rustAdd, P, NEG_ORDER, two_pow_64] at * + split <;> split <;> omega + +/-- The `assume(self.value > P && rhs.value > P)` at `goldilocks.rs:203` is +sound: whenever the double-overflow branch is taken (first `overflowing_add` +carried — `h1` — and the `NEG_ORDER` correction carried again — `h2`), both +inputs necessarily exceed P, so `assume`'s `unreachable_unchecked` is dead. -/ +theorem rustAdd_assume_sound {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) + (h1 : 2 ^ 64 ≤ a + b) (h2 : 2 ^ 64 ≤ (a + b) % 2 ^ 64 + NEG_ORDER) : + P < a ∧ P < b := by + simp only [P, NEG_ORDER, two_pow_64] at * + omega + +/-- The `sum += NEG_ORDER; // Cannot overflow.` at `goldilocks.rs:205` indeed +cannot: in the double-overflow branch (`_h1`, `h2` as in +`rustAdd_assume_sound`) the wrapped sum plus `NEG_ORDER` still fits. -/ +theorem rustAdd_fixup_no_overflow {a b : Nat} (_h1 : 2 ^ 64 ≤ a + b) + (h2 : 2 ^ 64 ≤ (a + b) % 2 ^ 64 + NEG_ORDER) : + ((a + b) % 2 ^ 64 + NEG_ORDER) % 2 ^ 64 + NEG_ORDER < 2 ^ 64 := by + simp only [NEG_ORDER, two_pow_64] at * + omega + +/-! ### Subtraction -/ + +theorem rustSub_lt (a b : Nat) : rustSub a b < 2 ^ 64 := by + simp only [rustSub] + exact Nat.mod_lt _ (by decide) + +/-- `sub` computes `a - b` in the field: adding `b` back recovers `a` mod P. -/ +theorem rustSub_mod {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : + (rustSub a b + b) % P = a % P := by + simp only [rustSub, P, NEG_ORDER, two_pow_64] at * + split <;> split <;> omega + +/-- The `assume(self.value < NEG_ORDER - 1 && rhs.value > P)` at +`goldilocks.rs:232` is sound: `h1` is the first borrow, `h2` the second +(`(a + 2^64 - b) % 2^64` is the wrapped first difference). -/ +theorem rustSub_assume_sound {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) + (h1 : a < b) (h2 : (a + 2 ^ 64 - b) % 2 ^ 64 < NEG_ORDER) : + a < NEG_ORDER - 1 ∧ P < b := by + simp only [P, NEG_ORDER, two_pow_64] at * + omega + +/-- The `diff -= NEG_ORDER; // Cannot underflow.` at `goldilocks.rs:234` +indeed cannot: after the double-borrow wrap, the intermediate difference is at +least `NEG_ORDER`. -/ +theorem rustSub_fixup_no_underflow {a b : Nat} (_h1 : a < b) + (h2 : (a + 2 ^ 64 - b) % 2 ^ 64 < NEG_ORDER) : + NEG_ORDER ≤ ((a + 2 ^ 64 - b) % 2 ^ 64 + 2 ^ 64 - NEG_ORDER) % 2 ^ 64 := by + simp only [NEG_ORDER, two_pow_64] at * + omega + +/-! ### Negation -/ + +theorem rustNeg_lt (a : Nat) : rustNeg a < 2 ^ 64 := by + simp only [rustNeg, P, two_pow_64] + omega + +theorem rustNeg_mod {a : Nat} (ha : a < 2 ^ 64) : (rustNeg a + a) % P = 0 := by + simp only [rustNeg, rustCanonical, P, two_pow_64] at * + split <;> omega + +/-! ### Halving -/ + +theorem rustHalve_lt (a : Nat) : rustHalve a < 2 ^ 64 := by + simp only [rustHalve] + exact Nat.mod_lt _ (by decide) + +/-- The `wrapping_add` in `halve` (`goldilocks.rs:114`) never wraps. -/ +theorem rustHalve_no_wrap {a : Nat} (ha : a < 2 ^ 64) : + a / 2 + a % 2 * HALF_P_PLUS_1 < 2 ^ 64 := by + simp only [HALF_P_PLUS_1, two_pow_64] at * + omega + +/-- `halve` inverts doubling: `2 * halve(a) ≡ a (mod P)`. -/ +theorem rustHalve_mod {a : Nat} (ha : a < 2 ^ 64) : + 2 * rustHalve a % P = a % P := by + simp only [rustHalve] + rw [Nat.mod_eq_of_lt (rustHalve_no_wrap ha)] + simp only [P, HALF_P_PLUS_1, two_pow_64] at * + omega + +/-! ### 128-bit reduction (used by `mul`) + +`reduce128` is decomposed as `reducePieces (x % 2^64) (x / 2^96) (bits 64..96)` +in the model; we prove the straight-line body correct first, then reassemble. +Throughout, `lo` is `x_lo`, `hh` is `x_hi_hi`, `hl` is `x_hi_lo`. -/ + +theorem addNoCanonicalize_lt (x y : Nat) : addNoCanonicalize x y < 2 ^ 64 := by + simp only [addNoCanonicalize] + exact Nat.mod_lt _ (by decide) + +/-- The safety contract of `add_no_canonicalize_trashing_input` +(`goldilocks.rs:312`, "Only correct if x + y < 2^64 + P"): under it, the +result is a correct non-canonical mod-P sum. We use it with `y < P`. -/ +theorem addNoCanonicalize_mod {x y : Nat} (hx : x < 2 ^ 64) (hy : y < P) : + addNoCanonicalize x y % P = (x + y) % P := by + simp only [addNoCanonicalize, P, NEG_ORDER, two_pow_64] at * + split <;> omega + +/-- Under the same contract, the trailing plain `+` of the portable fallback +(`goldilocks.rs:338`) never overflows. -/ +theorem addNoCanonicalize_fixup_no_overflow {x y : Nat} (hx : x < 2 ^ 64) + (hy : y < P) (h : 2 ^ 64 ≤ x + y) : + (x + y) % 2 ^ 64 + NEG_ORDER < 2 ^ 64 := by + simp only [P, NEG_ORDER, two_pow_64] at * + omega + +/-- The `u64` product `t1 = x_hi_lo * NEG_ORDER` at `goldilocks.rs:298` never +wraps — in fact it stays below P, which feeds the safety contract above. -/ +theorem reduce_t1_lt_P {hl : Nat} (hhl : hl < 2 ^ 32) : hl * NEG_ORDER < P := by + simp only [P, NEG_ORDER, two_pow_32] at * + omega + +/-- The `t0 -= NEG_ORDER; // Cannot underflow` at `goldilocks.rs:296` indeed +cannot: when the borrow fires (`h`), the wrapped difference exceeds +`NEG_ORDER`. -/ +theorem reduce_borrow_fixup_no_underflow {lo hh : Nat} (hlo : lo < 2 ^ 64) + (hhh : hh < 2 ^ 32) (h : lo < hh) : + NEG_ORDER ≤ (lo + 2 ^ 64 - hh) % 2 ^ 64 := by + simp only [NEG_ORDER, two_pow_32, two_pow_64] at * + omega + +/-- The borrow-corrected `t0` (`goldilocks.rs:293–297`) equals `lo - hh` +shifted into `[0, 2^64)` by at most one multiple of P: `t0 + hh` is `lo` or +`lo + P`. -/ +theorem reduce_t0_spec {lo hh : Nat} (hlo : lo < 2 ^ 64) (hhh : hh < 2 ^ 32) : + ((lo + 2 ^ 64 - hh) % 2 ^ 64 + 2 ^ 64 + - (if lo < hh then 1 else 0) * NEG_ORDER) % 2 ^ 64 < 2 ^ 64 ∧ + (((lo + 2 ^ 64 - hh) % 2 ^ 64 + 2 ^ 64 + - (if lo < hh then 1 else 0) * NEG_ORDER) % 2 ^ 64 + hh = lo ∨ + ((lo + 2 ^ 64 - hh) % 2 ^ 64 + 2 ^ 64 + - (if lo < hh then 1 else 0) * NEG_ORDER) % 2 ^ 64 + hh = lo + P) := by + simp only [P, NEG_ORDER, two_pow_32, two_pow_64] at * + split <;> omega + +/-- Combining step, with `t0` abstract so the arithmetic stays small: if +`t0 ≡ lo - hh (mod P)` then `add_no_canonicalize(t0, hl * NEG_ORDER)` is +`lo - hh + 2^64·hl (mod P)`, which matches `2^96·hh + 2^64·hl + lo` because +`P ∣ 2^96 + 1` (Goldilocks: `2^96 ≡ -1`). -/ +theorem reduce_combine {t0 lo hh hl : Nat} (ht0lt : t0 < 2 ^ 64) + (ht0 : t0 + hh = lo ∨ t0 + hh = lo + P) (hhl : hl < 2 ^ 32) : + addNoCanonicalize t0 (hl * NEG_ORDER % 2 ^ 64) % P + = (lo + 2 ^ 96 * hh + 2 ^ 64 * hl) % P := by + have ht1P : hl * NEG_ORDER < P := reduce_t1_lt_P hhl + have ht1 : hl * NEG_ORDER % 2 ^ 64 = hl * NEG_ORDER := + Nat.mod_eq_of_lt (Nat.lt_trans ht1P (by decide)) + rw [ht1, addNoCanonicalize_mod ht0lt ht1P] + simp only [P, NEG_ORDER, two_pow_32, two_pow_64, two_pow_96] at * + rcases ht0 with h | h <;> omega + +/-- The straight-line body of `reduce128` is a correct mod-P reduction of +`lo + 2^96·hh + 2^64·hl`. -/ +theorem reducePieces_mod {lo hh hl : Nat} (hlo : lo < 2 ^ 64) + (hhh : hh < 2 ^ 32) (hhl : hl < 2 ^ 32) : + reducePieces lo hh hl % P = (lo + 2 ^ 96 * hh + 2 ^ 64 * hl) % P := by + obtain ⟨ht0lt, ht0⟩ := reduce_t0_spec hlo hhh + simp only [reducePieces] + exact reduce_combine ht0lt ht0 hhl + +theorem reducePieces_lt (lo hh hl : Nat) : reducePieces lo hh hl < 2 ^ 64 := by + simp only [reducePieces] + exact addNoCanonicalize_lt _ _ + +theorem reduce128_lt (x : Nat) : reduce128 x < 2 ^ 64 := + reducePieces_lt _ _ _ + +/-- `reduce128` is a correct mod-P reduction on the FULL `u128` range — no +bound tighter than `x < 2^128` is needed. (The three pieces recompose exactly: +`x = lo + 2^96·hh + 2^64·hl`, so this is `reducePieces_mod` plus an identity.) -/ +theorem reduce128_mod {x : Nat} (hx : x < 2 ^ 128) : reduce128 x % P = x % P := by + have hlo : x % 2 ^ 64 < 2 ^ 64 := Nat.mod_lt _ (by decide) + have hhh : x / 2 ^ 64 / 2 ^ 32 < 2 ^ 32 := by + simp only [two_pow_32, two_pow_64, two_pow_128] at * + omega + have hhl : x / 2 ^ 64 % 2 ^ 32 < 2 ^ 32 := Nat.mod_lt _ (by decide) + have hsplit : x % 2 ^ 64 + 2 ^ 96 * (x / 2 ^ 64 / 2 ^ 32) + + 2 ^ 64 * (x / 2 ^ 64 % 2 ^ 32) = x := by + simp only [two_pow_32, two_pow_64, two_pow_96] + omega + simp only [reduce128] + rw [reducePieces_mod hlo hhh hhl, hsplit] + +/-! ### Multiplication, squaring, doubling, the x^7 S-box -/ + +theorem rustMul_lt (a b : Nat) : rustMul a b < 2 ^ 64 := + reduce128_lt _ + +theorem rustMul_mod {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : + rustMul a b % P = a * b % P := by + have hab : a * b < 2 ^ 128 := by + calc a * b ≤ (2 ^ 64 - 1) * (2 ^ 64 - 1) := + Nat.mul_le_mul (by omega) (by omega) + _ < 2 ^ 128 := by decide + exact reduce128_mod hab + +theorem rustSquare_lt (a : Nat) : rustSquare a < 2 ^ 64 := + rustMul_lt a a + +theorem rustSquare_mod {a : Nat} (ha : a < 2 ^ 64) : + rustSquare a % P = a * a % P := + rustMul_mod ha ha + +theorem rustDouble_lt (a : Nat) : rustDouble a < 2 ^ 64 := + rustAdd_lt a a + +theorem rustDouble_mod {a : Nat} (ha : a < 2 ^ 64) : + rustDouble a % P = 2 * a % P := by + show rustAdd a a % P = 2 * a % P + rw [rustAdd_mod ha ha] + simp only [P] + omega + +theorem rustExp7_lt (a : Nat) : rustExp7 a < 2 ^ 64 := + rustMul_lt _ _ + +/-- The Poseidon2 S-box: `exp7(a) ≡ a^7 (mod P)` (the seventh power written +as an explicit product to stay `Nat.pow`-free). -/ +theorem rustExp7_mod {a : Nat} (ha : a < 2 ^ 64) : + rustExp7 a % P = a * a * a * a * a * a * a % P := by + have h2lt : rustSquare a < 2 ^ 64 := rustSquare_lt a + have h3lt : rustMul (rustSquare a) a < 2 ^ 64 := rustMul_lt _ _ + have h4lt : rustSquare (rustSquare a) < 2 ^ 64 := rustSquare_lt _ + have h2 : rustSquare a % P = a * a % P := rustSquare_mod ha + have h3 : rustMul (rustSquare a) a % P = a * a * a % P := by + rw [rustMul_mod h2lt ha, Nat.mul_mod, h2, ← Nat.mul_mod] + have h4 : rustSquare (rustSquare a) % P = a * a * (a * a) % P := by + rw [rustSquare_mod h2lt, Nat.mul_mod, h2, ← Nat.mul_mod] + show rustMul (rustMul (rustSquare a) a) (rustSquare (rustSquare a)) % P = _ + rw [rustMul_mod h3lt h4lt, Nat.mul_mod, h3, h4, ← Nat.mul_mod] + simp only [← Nat.mul_assoc] + +/-! ### Capstone -/ + +/-- Every Tier-1 claim in one statement, so a single `#print axioms` in CI +certifies the whole package (see `ci/AxiomsCheck.lean`). Hypotheses are only +`< 2^64` — correctness holds for every (possibly non-canonical) `u64` +representative, which is the crate's actual invariant. -/ +theorem goldilocks_tier1 : + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → + rustAdd a b < 2 ^ 64 ∧ rustAdd a b % P = (a + b) % P) ∧ + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → + rustSub a b < 2 ^ 64 ∧ (rustSub a b + b) % P = a % P) ∧ + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → + rustMul a b < 2 ^ 64 ∧ rustMul a b % P = a * b % P) ∧ + (∀ a : Nat, a < 2 ^ 64 → rustNeg a < 2 ^ 64 ∧ (rustNeg a + a) % P = 0) ∧ + (∀ a : Nat, a < 2 ^ 64 → rustHalve a < 2 ^ 64 ∧ 2 * rustHalve a % P = a % P) ∧ + (∀ a : Nat, a < 2 ^ 64 → + rustExp7 a < 2 ^ 64 ∧ rustExp7 a % P = a * a * a * a * a * a * a % P) ∧ + (∀ a : Nat, a < 2 ^ 64 → rustCanonical a < P ∧ rustCanonical a = a % P) ∧ + (∀ a : Nat, a < 2 ^ 64 → (rustIsZero a ↔ a % P = 0)) ∧ + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → (rustEq a b ↔ a % P = b % P)) := + ⟨fun a b ha hb => ⟨rustAdd_lt a b, rustAdd_mod ha hb⟩, + fun a b ha hb => ⟨rustSub_lt a b, rustSub_mod ha hb⟩, + fun a b ha hb => ⟨rustMul_lt a b, rustMul_mod ha hb⟩, + fun _ ha => ⟨rustNeg_lt _, rustNeg_mod ha⟩, + fun _ ha => ⟨rustHalve_lt _, rustHalve_mod ha⟩, + fun _ ha => ⟨rustExp7_lt _, rustExp7_mod ha⟩, + fun _ ha => ⟨rustCanonical_lt_P ha, rustCanonical_eq_mod ha⟩, + fun _ ha => rustIsZero_iff ha, + fun _ _ ha hb => rustEq_iff ha hb⟩ + +/-! ### Cross-checks against the crate's own test vectors + +Kernel-evaluated instances of `test_against_p3_expected_values` +(`goldilocks.rs:404–432`). These pin the hand-transcribed model to the same +concrete values the Rust test suite pins the implementation to, guarding +against transcription drift. -/ + +example : rustCanonical (rustAdd 13835875475997267463 13593300247443167546) = + 8982431654025850688 := by decide +example : rustCanonical (rustSub 13835875475997267463 13593300247443167546) = + 242575228554099917 := by decide +example : rustCanonical (rustMul 13835875475997267463 13593300247443167546) = + 16746386726560462281 := by decide +example : rustCanonical (rustHalve 13835875475997267463) = + 16141309772705925892 := by decide +example : rustCanonical (rustExp7 13835875475997267463) = + 5716687150516714629 := by decide +example : rustCanonical (rustMul 18446744069414584319 9223372034707292161) = + 18446744069414584320 := by decide +example : rustCanonical (rustHalve 18446744069414584319) = + 18446744069414584320 := by decide +-- `(2^32)^2 = 2^64 ≡ 2^32 - 1 (mod P)` (`test_multiplication_large`). +example : rustCanonical (rustMul 4294967296 4294967296) = 4294967295 := by decide +-- `P` is a non-canonical representative of zero (`test_canonical_reduction`). +example : rustCanonical P = 0 := by decide +example : rustIsZero P := Or.inr rfl + +end GoldilocksSpec diff --git a/formal/GoldilocksSpec/Model.lean b/formal/GoldilocksSpec/Model.lean new file mode 100644 index 0000000..3600759 --- /dev/null +++ b/formal/GoldilocksSpec/Model.lean @@ -0,0 +1,174 @@ +/- + A faithful transcription of the hand-optimized Goldilocks arithmetic in + `src/goldilocks.rs` (qp-poseidon-core), at the `u64` level. + + MODELING. A `u64` is a `Nat` together with the side condition `< 2^64` + (carried as a hypothesis by every correctness theorem, never baked into the + definitions). Wrapping operations are modeled explicitly: + + * `x.overflowing_add y` ↦ value `(x + y) % 2^64`, flag `2^64 ≤ x + y` + * `x.overflowing_sub y` ↦ value `(x + 2^64 - y) % 2^64`, flag `x < y` + * `x >> k` ↦ `x / 2^k` + * `x & (2^k - 1)` ↦ `x % 2^k` + + Carry/borrow flags are `{0,1}`-valued `Nat`s (`if c then 1 else 0`) so each + definition reads line-for-line against the Rust. The trailing fix-up + additions/subtractions that the Rust performs with plain `+=`/`-=` (annotated + "Cannot overflow"/"Cannot underflow") are modeled as WRAPPING operations: + if those annotations were wrong, the model would compute the same wrong value + as the machine, and the correctness theorems in `GoldilocksSpec.Correctness` + would be unprovable. Separate lemmas there certify that the wraps never fire, + i.e. the Rust comments and the `assume` UB-hints are sound. + + The crate stores field elements in a NON-canonical representation: the + internal `u64` may be ≥ P, and every operation must be correct for every + representative. Accordingly the correctness theorems assume only `< 2^64` — + never canonicality — and conclude congruence mod P plus closure + (`result < 2^64`). + + FIDELITY. This model is a hand transcription (there is no symbolic exporter + for straight-line u64 Rust, unlike the gate-constraint exporter in + qp-plonky2/formal). Two mitigations: each definition cites the + `goldilocks.rs` lines it mirrors so the correspondence is auditable side by + side, and `Correctness.lean` ends with kernel-evaluated cross-checks of the + model against the crate's own `test_against_p3_expected_values` vectors. +-/ + +namespace GoldilocksSpec + +/-- The Goldilocks prime `P = 2^64 - 2^32 + 1` (`goldilocks.rs:51`). -/ +def P : Nat := 0xFFFF_FFFF_0000_0001 + +/-- `NEG_ORDER = P.wrapping_neg() = 2^64 - P = 2^32 - 1` (`goldilocks.rs:54`). -/ +def NEG_ORDER : Nat := 0xFFFF_FFFF + +/-- `HALF_P_PLUS_1 = (P + 1) >> 1` (`goldilocks.rs:110`). -/ +def HALF_P_PLUS_1 : Nat := 0x7FFFFFFF80000001 + +theorem P_eq : P = 2 ^ 64 - 2 ^ 32 + 1 := by decide +theorem NEG_ORDER_eq : NEG_ORDER = 2 ^ 64 - P := by decide +theorem HALF_P_PLUS_1_eq : HALF_P_PLUS_1 = (P + 1) / 2 := by decide + +/-- `impl Add for Goldilocks` (`goldilocks.rs:189–208`): +```rust +let (sum, over) = self.value.overflowing_add(rhs.value); +let (mut sum, over) = sum.overflowing_add(u64::from(over) * NEG_ORDER); +if over { sum += NEG_ORDER; } // "Cannot overflow." +Self::new(sum) +``` -/ +def rustAdd (a b : Nat) : Nat := + let sum1 := (a + b) % 2 ^ 64 + let over1 : Nat := if 2 ^ 64 ≤ a + b then 1 else 0 + let sum2 := (sum1 + over1 * NEG_ORDER) % 2 ^ 64 + let over2 : Nat := if 2 ^ 64 ≤ sum1 + over1 * NEG_ORDER then 1 else 0 + (sum2 + over2 * NEG_ORDER) % 2 ^ 64 + +/-- `impl Sub for Goldilocks` (`goldilocks.rs:218–237`): +```rust +let (diff, under) = self.value.overflowing_sub(rhs.value); +let (mut diff, under) = diff.overflowing_sub(u64::from(under) * NEG_ORDER); +if under { diff -= NEG_ORDER; } // "Cannot underflow." +Self::new(diff) +``` -/ +def rustSub (a b : Nat) : Nat := + let diff1 := (a + 2 ^ 64 - b) % 2 ^ 64 + let under1 : Nat := if a < b then 1 else 0 + let diff2 := (diff1 + 2 ^ 64 - under1 * NEG_ORDER) % 2 ^ 64 + let under2 : Nat := if diff1 < under1 * NEG_ORDER then 1 else 0 + (diff2 + 2 ^ 64 - under2 * NEG_ORDER) % 2 ^ 64 + +/-- `as_canonical_u64` (`goldilocks.rs:88–97`): one conditional subtraction. -/ +def rustCanonical (a : Nat) : Nat := + if P ≤ a then a - P else a + +/-- `is_zero` (`goldilocks.rs:100–103`): `value == 0 || value == P`. -/ +def rustIsZero (a : Nat) : Prop := + a = 0 ∨ a = P + +/-- `impl PartialEq` (`goldilocks.rs:143–147`): canonical representatives equal. -/ +def rustEq (a b : Nat) : Prop := + rustCanonical a = rustCanonical b + +/-- `impl Neg` (`goldilocks.rs:247–254`): `P - as_canonical_u64()`. -/ +def rustNeg (a : Nat) : Nat := + P - rustCanonical a + +/-- `halve` (`goldilocks.rs:105–115`): +```rust +let lo_bit = self.value & 1; +let half = self.value >> 1; +let mask = 0u64.wrapping_sub(lo_bit); // all-ones when odd, zero when even +Self::new(half.wrapping_add(mask & HALF_P_PLUS_1)) +``` +`mask & HALF_P_PLUS_1` is `HALF_P_PLUS_1` when `lo_bit = 1` and `0` when +`lo_bit = 0`, i.e. `lo_bit * HALF_P_PLUS_1`. The `wrapping_add` wraps. -/ +def rustHalve (a : Nat) : Nat := + let loBit := a % 2 + let half := a / 2 + (half + loBit * HALF_P_PLUS_1) % 2 ^ 64 + +/-- `add_no_canonicalize_trashing_input` (`goldilocks.rs:336–339`, the portable +fallback; the x86_64 asm at :315–328 computes the same function): +```rust +let (res_wrapped, carry) = x.overflowing_add(y); +res_wrapped + NEG_ORDER * u64::from(carry) // safety doc: needs x + y < 2^64 + P +``` +The trailing plain `+` is modeled wrapping; `Correctness` proves it never wraps +under the documented safety precondition. -/ +def addNoCanonicalize (x y : Nat) : Nat := + let resWrapped := (x + y) % 2 ^ 64 + let carry : Nat := if 2 ^ 64 ≤ x + y then 1 else 0 + (resWrapped + carry * NEG_ORDER) % 2 ^ 64 + +/-- The straight-line body of `reduce128` (`goldilocks.rs:293–299`), after the +input has been split into `lo = x_lo` (low 64 bits), `hh = x_hi_hi` (bits +96..128) and `hl = x_hi_lo` (bits 64..96): +```rust +let (mut t0, borrow) = x_lo.overflowing_sub(x_hi_hi); +if borrow { t0 -= NEG_ORDER; } // "Cannot underflow" +let t1 = x_hi_lo * NEG_ORDER; +let t2 = unsafe { add_no_canonicalize_trashing_input(t0, t1) }; +``` +The `u64` product `x_hi_lo * NEG_ORDER` is modeled wrapping (`Correctness` +proves `(2^32 - 1)^2 < 2^64`, so it never does). -/ +def reducePieces (lo hh hl : Nat) : Nat := + let t0a := (lo + 2 ^ 64 - hh) % 2 ^ 64 + let borrow : Nat := if lo < hh then 1 else 0 + let t0 := (t0a + 2 ^ 64 - borrow * NEG_ORDER) % 2 ^ 64 + let t1 := hl * NEG_ORDER % 2 ^ 64 + addNoCanonicalize t0 t1 + +/-- `reduce128` (`goldilocks.rs:288–307`): `split` (:305) yields +`x_lo = x % 2^64` and `x_hi = x / 2^64`; then `x_hi >> 32` and +`x_hi & NEG_ORDER` (:290–291) select the two 32-bit halves of `x_hi`. -/ +def reduce128 (x : Nat) : Nat := + reducePieces (x % 2 ^ 64) (x / 2 ^ 64 / 2 ^ 32) (x / 2 ^ 64 % 2 ^ 32) + +/-- `impl Mul` (`goldilocks.rs:256–263`): widen to u128, multiply, reduce. +The u128 product `u128::from(a) * u128::from(b)` cannot wrap +(`(2^64 - 1)^2 < 2^128`), so it is a plain product. -/ +def rustMul (a b : Nat) : Nat := + reduce128 (a * b) + +/-- `square` (`goldilocks.rs:117–121`). -/ +def rustSquare (a : Nat) : Nat := + rustMul a a + +/-- `double` (`goldilocks.rs:123–127`). -/ +def rustDouble (a : Nat) : Nat := + rustAdd a a + +/-- `exp7` — the Poseidon2 S-box (`goldilocks.rs:129–136`): +```rust +let x2 = self.square(); +let x3 = x2 * *self; +let x4 = x2.square(); +x3 * x4 +``` -/ +def rustExp7 (a : Nat) : Nat := + let x2 := rustSquare a + let x3 := rustMul x2 a + let x4 := rustSquare x2 + rustMul x3 x4 + +end GoldilocksSpec diff --git a/formal/ci/AxiomsCheck.lean b/formal/ci/AxiomsCheck.lean new file mode 100644 index 0000000..a81baa4 --- /dev/null +++ b/formal/ci/AxiomsCheck.lean @@ -0,0 +1,12 @@ +/- + CI axiom-footprint gate for the capstone `goldilocks_tier1` theorem. + + The shell step in `.github/workflows/ci.yml` runs this file and parses + `#print axioms` output, asserting the complete allow-list of standard Lean + axioms: `{propext, Classical.choice, Quot.sound}` — in particular no + placeholder axiom and no `Lean.ofReduceBool`. Import-only; not part of + `defaultTargets`. +-/ +import GoldilocksSpec + +#print axioms GoldilocksSpec.goldilocks_tier1 diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json new file mode 100644 index 0000000..17faa02 --- /dev/null +++ b/formal/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "goldilocksSpec", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/lakefile.toml b/formal/lakefile.toml new file mode 100644 index 0000000..502b788 --- /dev/null +++ b/formal/lakefile.toml @@ -0,0 +1,13 @@ +# Lean 4 formal-spec package for qp-poseidon-core's hand-optimized Goldilocks +# field arithmetic (`src/goldilocks.rs`). +# +# Deliberately dependency-free (core Lean + `omega`/`decide` only), mirroring +# qp-zk-circuits/formal: it builds in seconds and stays hermetic — no mathlib +# cache to fetch in CI. Correctness is stated as mod-p congruences over `Nat` +# (`result % P = spec % P`), which is definitionally what a `ZMod p` statement +# unfolds to; see GoldilocksSpec/Correctness.lean for the equivalence note. +defaultTargets = ["GoldilocksSpec"] +name = "goldilocksSpec" + +[[lean_lib]] +name = "GoldilocksSpec" diff --git a/formal/lean-toolchain b/formal/lean-toolchain new file mode 100644 index 0000000..af9e5d3 --- /dev/null +++ b/formal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0 From c5ce1202660c4c96a64fef20f58ddd438239cc13 Mon Sep 17 00:00:00 2001 From: illuzen Date: Mon, 13 Jul 2026 21:24:38 +0800 Subject: [PATCH 4/4] gate axiom footprint of safety theorems via safety capstone Co-authored-by: Cursor --- .github/workflows/ci.yml | 40 ++++++++++--------- formal/GoldilocksSpec/Correctness.lean | 53 ++++++++++++++++++++++++-- formal/ci/AxiomsCheck.lean | 16 +++++--- 3 files changed, 83 insertions(+), 26 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0394bf7..c326355 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -135,32 +135,38 @@ jobs: echo "::error::formal spec contains a sorry/admit placeholder" exit 1 fi - # Axiom-footprint gate: the capstone `goldilocks_tier1` must depend on - # exactly the standard Lean axioms — no placeholder axiom, no - # `Lean.ofReduceBool` (native evaluation), no stray `axiom` declarations. - - name: Assert goldilocks_tier1 axiom footprint + # Axiom-footprint gate: both capstones — `goldilocks_tier1` (functional + # congruence + closure) and `goldilocks_tier1_safety` (no-UB/no-wrap) — + # must depend on exactly the standard Lean axioms: no placeholder axiom, + # no `Lean.ofReduceBool` (native evaluation), no stray `axiom` + # declarations anywhere in their proof trees. Together the two theorems + # bundle every claim the spec makes, so this covers the whole package. + - name: Assert capstone axiom footprints run: | set -euo pipefail cd formal output=$(lake env lean ci/AxiomsCheck.lean 2>&1) printf '%s\n' "$output" - if ! grep -q 'depends on axioms' <<< "$output"; then - echo "::error::could not read #print axioms for GoldilocksSpec.goldilocks_tier1" - exit 1 - fi - axioms=$(sed -n '/depends on axioms:/,/]/p' <<< "$output" | tr -d '\n' | sed 's/.*\[\(.*\)\].*/\1/' | tr ',' '\n' | sed 's/^[[:space:]]*//;s/[[:space:]]*$//' | grep -v '^$' | sort) expected=$(printf '%s\n' \ 'propext' \ 'Classical.choice' \ 'Quot.sound' | sort) - if [ "$axioms" != "$expected" ]; then - echo "::error::goldilocks_tier1 axiom footprint mismatch" - echo "expected exactly:" - printf ' %s\n' "$expected" - echo "got:" - printf ' %s\n' "$axioms" - exit 1 - fi + for thm in goldilocks_tier1 goldilocks_tier1_safety; do + line=$(grep "'GoldilocksSpec.${thm}' depends on axioms" <<< "$output" || true) + if [ -z "$line" ]; then + echo "::error::could not read #print axioms for GoldilocksSpec.${thm}" + exit 1 + fi + axioms=$(sed 's/.*\[\(.*\)\].*/\1/' <<< "$line" | tr ',' '\n' | sed 's/^[[:space:]]*//;s/[[:space:]]*$//' | grep -v '^$' | sort) + if [ "$axioms" != "$expected" ]; then + echo "::error::${thm} axiom footprint mismatch" + echo "expected exactly:" + printf ' %s\n' "$expected" + echo "got:" + printf ' %s\n' "$axioms" + exit 1 + fi + done security-audit: name: 🔐 Security Audit (non-blocking) diff --git a/formal/GoldilocksSpec/Correctness.lean b/formal/GoldilocksSpec/Correctness.lean index 3aeff51..aa76d55 100644 --- a/formal/GoldilocksSpec/Correctness.lean +++ b/formal/GoldilocksSpec/Correctness.lean @@ -298,10 +298,16 @@ theorem rustExp7_mod {a : Nat} (ha : a < 2 ^ 64) : rw [rustMul_mod h3lt h4lt, Nat.mul_mod, h3, h4, ← Nat.mul_mod] simp only [← Nat.mul_assoc] -/-! ### Capstone -/ +/-! ### Capstones -/-- Every Tier-1 claim in one statement, so a single `#print axioms` in CI -certifies the whole package (see `ci/AxiomsCheck.lean`). Hypotheses are only +Two bundle theorems cover the package's full assurance surface, so CI can +certify it with `#print axioms` on exactly these two names +(see `ci/AxiomsCheck.lean`): `goldilocks_tier1` for the functional claims +(congruence + closure) and `goldilocks_tier1_safety` for the no-UB/no-wrap +claims. A safety lemma that silently grew a custom axiom would flunk the +footprint gate, because both capstones are inspected. -/ + +/-- Every Tier-1 functional claim in one statement. Hypotheses are only `< 2^64` — correctness holds for every (possibly non-canonical) `u64` representative, which is the crate's actual invariant. -/ theorem goldilocks_tier1 : @@ -328,6 +334,47 @@ theorem goldilocks_tier1 : fun _ ha => rustIsZero_iff ha, fun _ _ ha hb => rustEq_iff ha hb⟩ +/-- Every Tier-1 no-UB/no-wrap claim in one statement, in source order of the +Rust it certifies: + +1. `add` (`goldilocks.rs:196–205`): in the double-overflow branch, the + `assume(self.value > P && rhs.value > P)` holds and the + `sum += NEG_ORDER; // Cannot overflow.` fits; +2. `sub` (`goldilocks.rs:225–234`): in the double-borrow branch, the + `assume(self.value < NEG_ORDER - 1 && rhs.value > P)` holds and the + `diff -= NEG_ORDER; // Cannot underflow.` does not go below zero; +3. `halve` (`goldilocks.rs:114`): the `wrapping_add` never wraps; +4. `reduce128` (`goldilocks.rs:293–296`): when the borrow fires, the + `t0 -= NEG_ORDER; // Cannot underflow` does not go below zero; +5. `reduce128` (`goldilocks.rs:298`): the `u64` product + `t1 = x_hi_lo * NEG_ORDER` stays below P (a fortiori never wraps), which + establishes the safety contract of the `unsafe` call at :299; +6. `add_no_canonicalize_trashing_input` (`goldilocks.rs:338`): under that + contract, the trailing plain `+` never overflows. -/ +theorem goldilocks_tier1_safety : + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → 2 ^ 64 ≤ a + b → + 2 ^ 64 ≤ (a + b) % 2 ^ 64 + NEG_ORDER → + (P < a ∧ P < b) ∧ + ((a + b) % 2 ^ 64 + NEG_ORDER) % 2 ^ 64 + NEG_ORDER < 2 ^ 64) ∧ + (∀ a b : Nat, a < 2 ^ 64 → b < 2 ^ 64 → a < b → + (a + 2 ^ 64 - b) % 2 ^ 64 < NEG_ORDER → + (a < NEG_ORDER - 1 ∧ P < b) ∧ + NEG_ORDER ≤ ((a + 2 ^ 64 - b) % 2 ^ 64 + 2 ^ 64 - NEG_ORDER) % 2 ^ 64) ∧ + (∀ a : Nat, a < 2 ^ 64 → a / 2 + a % 2 * HALF_P_PLUS_1 < 2 ^ 64) ∧ + (∀ lo hh : Nat, lo < 2 ^ 64 → hh < 2 ^ 32 → lo < hh → + NEG_ORDER ≤ (lo + 2 ^ 64 - hh) % 2 ^ 64) ∧ + (∀ hl : Nat, hl < 2 ^ 32 → hl * NEG_ORDER < P) ∧ + (∀ x y : Nat, x < 2 ^ 64 → y < P → 2 ^ 64 ≤ x + y → + (x + y) % 2 ^ 64 + NEG_ORDER < 2 ^ 64) := + ⟨fun _ _ ha hb h1 h2 => + ⟨rustAdd_assume_sound ha hb h1 h2, rustAdd_fixup_no_overflow h1 h2⟩, + fun _ _ ha hb h1 h2 => + ⟨rustSub_assume_sound ha hb h1 h2, rustSub_fixup_no_underflow h1 h2⟩, + fun _ ha => rustHalve_no_wrap ha, + fun _ _ hlo hhh h => reduce_borrow_fixup_no_underflow hlo hhh h, + fun _ hhl => reduce_t1_lt_P hhl, + fun _ _ hx hy h => addNoCanonicalize_fixup_no_overflow hx hy h⟩ + /-! ### Cross-checks against the crate's own test vectors Kernel-evaluated instances of `test_against_p3_expected_values` diff --git a/formal/ci/AxiomsCheck.lean b/formal/ci/AxiomsCheck.lean index a81baa4..3c480b9 100644 --- a/formal/ci/AxiomsCheck.lean +++ b/formal/ci/AxiomsCheck.lean @@ -1,12 +1,16 @@ /- - CI axiom-footprint gate for the capstone `goldilocks_tier1` theorem. + CI axiom-footprint gate for the two capstone theorems that together cover + the package's full assurance surface: `goldilocks_tier1` (functional + congruence + closure) and `goldilocks_tier1_safety` (no-UB/no-wrap). - The shell step in `.github/workflows/ci.yml` runs this file and parses - `#print axioms` output, asserting the complete allow-list of standard Lean - axioms: `{propext, Classical.choice, Quot.sound}` — in particular no - placeholder axiom and no `Lean.ofReduceBool`. Import-only; not part of - `defaultTargets`. + The shell step in `.github/workflows/ci.yml` runs this file and parses each + `#print axioms` line, asserting for BOTH theorems the complete allow-list of + standard Lean axioms: `{propext, Classical.choice, Quot.sound}` — in + particular no placeholder axiom, no `Lean.ofReduceBool`, and no custom + `axiom` declaration smuggled into any lemma either capstone depends on. + Import-only; not part of `defaultTargets`. -/ import GoldilocksSpec #print axioms GoldilocksSpec.goldilocks_tier1 +#print axioms GoldilocksSpec.goldilocks_tier1_safety