From e5d303aa22b239ac3ee0a693651df4a7d7f63df3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 07:15:36 +0000 Subject: [PATCH 1/2] perf(number-field): complete Phase 4 evidence --- libraries.yml | 2 +- ...ld-phase4-final-inversion-comparators.json | 967 ++++++++++++++++++ ...x-number-field-phase4-final-inversion.json | 529 ++++++++++ reports/hex-number-field-performance.md | 165 +-- 4 files changed, 1598 insertions(+), 65 deletions(-) create mode 100644 reports/bench-results/hex-number-field-phase4-final-inversion-comparators.json create mode 100644 reports/bench-results/hex-number-field-phase4-final-inversion.json diff --git a/libraries.yml b/libraries.yml index c8f3d329c..a3677f613 100644 --- a/libraries.yml +++ b/libraries.yml @@ -1016,7 +1016,7 @@ libraries: HexNumberField: deps: [HexPolyZ, HexRoots, HexResultant, HexBerlekampZassenhaus, HexMatrix, HexRowReduce] mathlib: false - done_through: 3 + done_through: 4 status: active phase4: comparators: diff --git a/reports/bench-results/hex-number-field-phase4-final-inversion-comparators.json b/reports/bench-results/hex-number-field-phase4-final-inversion-comparators.json new file mode 100644 index 000000000..42c098e4c --- /dev/null +++ b/reports/bench-results/hex-number-field-phase4-final-inversion-comparators.json @@ -0,0 +1,967 @@ +{"results": + [{"points": + [{"total_nanos": 235052462, + "status": "ok", + "result_hash": "0x0", + "repeat_index": 0, + "peak_rss_kb": 70512, + "inner_repeats": 32768, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 222030970, + "status": "ok", + "result_hash": "0x0", + "repeat_index": 1, + "peak_rss_kb": 70328, + "inner_repeats": 32768, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 226775152, + "status": "ok", + "result_hash": "0x0", + "repeat_index": 2, + "peak_rss_kb": 70508, + "inner_repeats": 32768, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 231456291, + "status": "ok", + "result_hash": "0x0", + "repeat_index": 3, + "peak_rss_kb": 70324, + "inner_repeats": 32768, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 231624260, + "status": "ok", + "result_hash": "0x0", + "repeat_index": 4, + "peak_rss_kb": 70508, + "inner_repeats": 32768, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x0", + "min_nanos": 6775, + "median_nanos": 7063, + "max_nanos": 7173, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodOverhead", + "expected_hash_check": {"status": "match"}, + "env": + {"timestamp_unix_ms": 1788246513786, + "timestamp_iso": "2026-09-01T07:08:33Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": "0x0"}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 399805125, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 0, + "peak_rss_kb": 70100, + "inner_repeats": 16384, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 389748357, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 1, + "peak_rss_kb": 69640, + "inner_repeats": 16384, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 390581442, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 2, + "peak_rss_kb": 70032, + "inner_repeats": 16384, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 390799906, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 3, + "peak_rss_kb": 69824, + "inner_repeats": 16384, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 391829031, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 4, + "peak_rss_kb": 69712, + "inner_repeats": 16384, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xb8302e29a4df3f41", + "min_nanos": 23788, + "median_nanos": 23852, + "max_nanos": 24402, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair4", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246517138, + "timestamp_iso": "2026-09-01T07:08:37Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 271568132, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 0, + "peak_rss_kb": 70176, + "inner_repeats": 8192, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 269101775, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 1, + "peak_rss_kb": 70184, + "inner_repeats": 8192, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 269177117, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 2, + "peak_rss_kb": 69452, + "inner_repeats": 8192, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 271373072, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 3, + "peak_rss_kb": 70516, + "inner_repeats": 8192, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 271658115, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "repeat_index": 4, + "peak_rss_kb": 69640, + "inner_repeats": 8192, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xb8302e29a4df3f41", + "min_nanos": 32849, + "median_nanos": 33126, + "max_nanos": 33161, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv4", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246522139, + "timestamp_iso": "2026-09-01T07:08:42Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 269814491, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 0, + "peak_rss_kb": 70048, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 269375702, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 1, + "peak_rss_kb": 69508, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 271078526, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 2, + "peak_rss_kb": 69844, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 271319243, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 3, + "peak_rss_kb": 69324, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 269945326, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 4, + "peak_rss_kb": 70112, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xc80c3d019e0b9e4c", + "min_nanos": 65765, + "median_nanos": 65904, + "max_nanos": 66240, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair6", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246525955, + "timestamp_iso": "2026-09-01T07:08:45Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 213718798, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 0, + "peak_rss_kb": 69752, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 215285880, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 1, + "peak_rss_kb": 70308, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 213388959, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 2, + "peak_rss_kb": 70196, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 214223226, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 3, + "peak_rss_kb": 69636, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 213651799, + "status": "ok", + "result_hash": "0xc80c3d019e0b9e4c", + "repeat_index": 4, + "peak_rss_kb": 70100, + "inner_repeats": 4096, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xc80c3d019e0b9e4c", + "min_nanos": 52096, + "median_nanos": 52177, + "max_nanos": 52560, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv6", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246529505, + "timestamp_iso": "2026-09-01T07:08:49Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 270721717, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 0, + "peak_rss_kb": 69960, + "inner_repeats": 2048, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 271454092, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 1, + "peak_rss_kb": 69740, + "inner_repeats": 2048, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 269535449, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 2, + "peak_rss_kb": 70176, + "inner_repeats": 2048, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 267788049, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 3, + "peak_rss_kb": 70136, + "inner_repeats": 2048, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 268441717, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 4, + "peak_rss_kb": 70156, + "inner_repeats": 2048, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xd16df20a45d683c7", + "min_nanos": 130755, + "median_nanos": 131609, + "max_nanos": 132545, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair8", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246532642, + "timestamp_iso": "2026-09-01T07:08:52Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 216970418, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 0, + "peak_rss_kb": 70304, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 219325629, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 1, + "peak_rss_kb": 69460, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 216156632, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 2, + "peak_rss_kb": 69964, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 221547563, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 3, + "peak_rss_kb": 69464, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 225576035, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "repeat_index": 4, + "peak_rss_kb": 69808, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xd16df20a45d683c7", + "min_nanos": 211090, + "median_nanos": 214185, + "max_nanos": 220289, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv8", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246536176, + "timestamp_iso": "2026-09-01T07:08:56Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 232898389, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 0, + "peak_rss_kb": 70252, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 227966709, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 1, + "peak_rss_kb": 69832, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 227209577, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 2, + "peak_rss_kb": 70216, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 228135489, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 3, + "peak_rss_kb": 69932, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 227460077, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 4, + "peak_rss_kb": 70152, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x7d0941f1c8c5f9e8", + "min_nanos": 221884, + "median_nanos": 222623, + "max_nanos": 227439, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair10", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246539382, + "timestamp_iso": "2026-09-01T07:08:59Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 217161432, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 0, + "peak_rss_kb": 70200, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 218440828, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 1, + "peak_rss_kb": 69636, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 221090386, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 2, + "peak_rss_kb": 69804, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 216062532, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 3, + "peak_rss_kb": 70128, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 215332730, + "status": "ok", + "result_hash": "0x7d0941f1c8c5f9e8", + "repeat_index": 4, + "peak_rss_kb": 70196, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x7d0941f1c8c5f9e8", + "min_nanos": 210285, + "median_nanos": 212071, + "max_nanos": 215908, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv10", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246542433, + "timestamp_iso": "2026-09-01T07:09:02Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 344325545, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 0, + "peak_rss_kb": 69764, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 344435778, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 1, + "peak_rss_kb": 69972, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 350167735, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 2, + "peak_rss_kb": 69748, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 340626571, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 3, + "peak_rss_kb": 69972, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 341849514, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 4, + "peak_rss_kb": 69784, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x7776688d262fc467", + "min_nanos": 332643, + "median_nanos": 336255, + "max_nanos": 341960, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair12", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246545612, + "timestamp_iso": "2026-09-01T07:09:05Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 243644349, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 0, + "peak_rss_kb": 70136, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 242040151, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 1, + "peak_rss_kb": 70012, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 241148909, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 2, + "peak_rss_kb": 69952, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 243180321, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 3, + "peak_rss_kb": 69788, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 239848021, + "status": "ok", + "result_hash": "0x7776688d262fc467", + "repeat_index": 4, + "peak_rss_kb": 69872, + "inner_repeats": 1024, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x7776688d262fc467", + "min_nanos": 234226, + "median_nanos": 236367, + "max_nanos": 237933, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv12", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246550048, + "timestamp_iso": "2026-09-01T07:09:10Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 363152323, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 0, + "peak_rss_kb": 70332, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 362741604, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 1, + "peak_rss_kb": 70176, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 361973425, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 2, + "peak_rss_kb": 70104, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 365512391, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 3, + "peak_rss_kb": 70176, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 366266319, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 4, + "peak_rss_kb": 69776, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x5820b68b7d69021d", + "min_nanos": 706979, + "median_nanos": 709281, + "max_nanos": 715363, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvPair16", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246553517, + "timestamp_iso": "2026-09-01T07:09:13Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 252200011, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 0, + "peak_rss_kb": 69712, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 264427907, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 1, + "peak_rss_kb": 70380, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 245306412, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 2, + "peak_rss_kb": 69524, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 245318922, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 3, + "peak_rss_kb": 69728, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 244572865, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "repeat_index": 4, + "peak_rss_kb": 70272, + "inner_repeats": 512, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x5820b68b7d69021d", + "min_nanos": 477681, + "median_nanos": 479138, + "max_nanos": 516460, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.NumberFieldBench.runPariPolmodInv16", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1788246558211, + "timestamp_iso": "2026-09-01T07:09:18Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"warmup_first_iter": true, + "warmup": true, + "repeats": 5, + "min_total_seconds": 0.2, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1788246513786, + "timestamp_iso": "2026-09-01T07:08:33Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/bench-results/hex-number-field-phase4-final-inversion.json b/reports/bench-results/hex-number-field-phase4-final-inversion.json new file mode 100644 index 000000000..224a737b8 --- /dev/null +++ b/reports/bench-results/hex-number-field-phase4-final-inversion.json @@ -0,0 +1,529 @@ +{"results": + [{"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.007312, + "param": 4, + "ok_count": 5, + "min_per_call_nanos": 23987.100342, + "median_per_call_nanos": 24122.283447, + "max_per_call_nanos": 24163.482422}, + {"relative_spread": 0.009998, + "param": 8, + "ok_count": 5, + "min_per_call_nanos": 131327.035156, + "median_per_call_nanos": 132100.976562, + "max_per_call_nanos": 132647.763672}, + {"relative_spread": 0.011793, + "param": 16, + "ok_count": 5, + "min_per_call_nanos": 710870.554688, + "median_per_call_nanos": 714157.226562, + "max_per_call_nanos": 719292.335938}, + {"relative_spread": 0.008741, + "param": 32, + "ok_count": 5, + "min_per_call_nanos": 4711823.9375, + "median_per_call_nanos": 4719866.5, + "max_per_call_nanos": 4753080.0625}, + {"relative_spread": 0.018453, + "param": 48, + "ok_count": 5, + "min_per_call_nanos": 14040275, + "median_per_call_nanos": 14163685.75, + "max_per_call_nanos": 14301642.5}, + {"relative_spread": 0.00622, + "param": 64, + "ok_count": 5, + "min_per_call_nanos": 32498564, + "median_per_call_nanos": 32569745, + "max_per_call_nanos": 32701154.5}, + {"relative_spread": 0.0157, + "param": 96, + "ok_count": 5, + "min_per_call_nanos": 95898565, + "median_per_call_nanos": 96551222, + "max_per_call_nanos": 97414403}], + "spawn_floor_nanos": 46798141, + "slope": -0.106331, + "ratios": + [[4, 137.058429], + [8, 137.605184], + [16, 121.29029], + [32, 118.18576], + [48, 111.77151], + [64, 111.994337], + [96, 101.713379]], + "points": + [{"trial_index": 0, + "total_nanos": 98973624, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "per_call_nanos": 24163.482422, + "peak_rss_kb": 69948, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 98490227, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "per_call_nanos": 24045.465576, + "peak_rss_kb": 70040, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 98251163, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "per_call_nanos": 23987.100342, + "peak_rss_kb": 70368, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 98804873, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "per_call_nanos": 24122.283447, + "peak_rss_kb": 69780, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 98886284, + "status": "ok", + "result_hash": "0xb8302e29a4df3f41", + "per_call_nanos": 24142.15918, + "peak_rss_kb": 69312, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 67239442, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "per_call_nanos": 131327.035156, + "peak_rss_kb": 69992, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 67276437, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "per_call_nanos": 131399.291016, + "peak_rss_kb": 70460, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 67915655, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "per_call_nanos": 132647.763672, + "peak_rss_kb": 69336, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 67765552, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "per_call_nanos": 132354.59375, + "peak_rss_kb": 70220, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 67635700, + "status": "ok", + "result_hash": "0xd16df20a45d683c7", + "per_call_nanos": 132100.976562, + "peak_rss_kb": 70220, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 90991431, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "per_call_nanos": 710870.554688, + "peak_rss_kb": 70136, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 91412125, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "per_call_nanos": 714157.226562, + "peak_rss_kb": 69712, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 92069419, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "per_call_nanos": 719292.335938, + "peak_rss_kb": 70216, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 91081845, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "per_call_nanos": 711576.914062, + "peak_rss_kb": 69708, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 91683146, + "status": "ok", + "result_hash": "0x5820b68b7d69021d", + "per_call_nanos": 716274.578125, + "peak_rss_kb": 67952, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 75795045, + "status": "ok", + "result_hash": "0xedc3cce05e5a1c43", + "per_call_nanos": 4737190.3125, + "peak_rss_kb": 70628, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 75389183, + "status": "ok", + "result_hash": "0xedc3cce05e5a1c43", + "per_call_nanos": 4711823.9375, + "peak_rss_kb": 70036, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 75517864, + "status": "ok", + "result_hash": "0xedc3cce05e5a1c43", + "per_call_nanos": 4719866.5, + "peak_rss_kb": 69904, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 75514168, + "status": "ok", + "result_hash": "0xedc3cce05e5a1c43", + "per_call_nanos": 4719635.5, + "peak_rss_kb": 70384, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 76049281, + "status": "ok", + "result_hash": "0xedc3cce05e5a1c43", + "per_call_nanos": 4753080.0625, + "peak_rss_kb": 70460, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 56161100, + "status": "ok", + "result_hash": "0xe03e71220cc369ea", + "per_call_nanos": 14040275, + "peak_rss_kb": 69708, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 56280708, + "status": "ok", + "result_hash": "0xe03e71220cc369ea", + "per_call_nanos": 14070177, + "peak_rss_kb": 69888, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 56789592, + "status": "ok", + "result_hash": "0xe03e71220cc369ea", + "per_call_nanos": 14197398, + "peak_rss_kb": 70848, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 56654743, + "status": "ok", + "result_hash": "0xe03e71220cc369ea", + "per_call_nanos": 14163685.75, + "peak_rss_kb": 70856, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 57206570, + "status": "ok", + "result_hash": "0xe03e71220cc369ea", + "per_call_nanos": 14301642.5, + "peak_rss_kb": 70220, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 65139490, + "status": "ok", + "result_hash": "0x19fd22e45f10c383", + "per_call_nanos": 32569745, + "peak_rss_kb": 70768, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 65213949, + "status": "ok", + "result_hash": "0x19fd22e45f10c383", + "per_call_nanos": 32606974.5, + "peak_rss_kb": 69888, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 65402309, + "status": "ok", + "result_hash": "0x19fd22e45f10c383", + "per_call_nanos": 32701154.5, + "peak_rss_kb": 70280, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 64997128, + "status": "ok", + "result_hash": "0x19fd22e45f10c383", + "per_call_nanos": 32498564, + "peak_rss_kb": 70212, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 65131567, + "status": "ok", + "result_hash": "0x19fd22e45f10c383", + "per_call_nanos": 32565783.5, + "peak_rss_kb": 70760, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 95898565, + "status": "ok", + "result_hash": "0xb97c8f647e1eb8dc", + "per_call_nanos": 95898565, + "peak_rss_kb": 71792, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 96239230, + "status": "ok", + "result_hash": "0xb97c8f647e1eb8dc", + "per_call_nanos": 96239230, + "peak_rss_kb": 71532, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 97414403, + "status": "ok", + "result_hash": "0xb97c8f647e1eb8dc", + "per_call_nanos": 97414403, + "peak_rss_kb": 71812, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 96995712, + "status": "ok", + "result_hash": "0xb97c8f647e1eb8dc", + "per_call_nanos": 96995712, + "peak_rss_kb": 71416, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 96551222, + "status": "ok", + "result_hash": "0xb97c8f647e1eb8dc", + "per_call_nanos": 96551222, + "peak_rss_kb": 71632, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.NumberFieldBench.runQAdjoinInvLadder", + "env": + {"timestamp_unix_ms": 1788246342812, + "timestamp_iso": "2026-09-01T07:05:42Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [4, 8, 16, 32, 48, 64, 96], "kind": "custom"}, + "param_floor": 4, + "param_ceiling": 96, + "outer_trials": 5, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 120, + "cache_mode": "warm"}, + "complexity_formula": "n * n * (n + 7)", + "c_min": 101.713379, + "c_max": 137.605184, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1788246342812, + "timestamp_iso": "2026-09-01T07:05:42Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "c94811435cf219e3c37638e07f1802aa38925067", + "exe_name": "hexnumberfield_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/hex-number-field-performance.md b/reports/hex-number-field-performance.md index 48ff3ee9a..bf7516800 100644 --- a/reports/hex-number-field-performance.md +++ b/reports/hex-number-field-performance.md @@ -5,9 +5,10 @@ Mathlib-free executable computation, so all of its Phase-4 evidence is ordinary LeanBench evidence and none of it is fresh-module proof evidence (`PLAN/Phase4.md` §Evidence tracks). -This snapshot records the current measured evidence. `libraries.yml` still -keeps `HexNumberField` at `done_through: 3`, but the compiled-surface coverage -and Attribution-rule concerns found by the Phase-4 audit are closed here. +This snapshot records the complete Phase-4 evidence. `libraries.yml` records +`HexNumberField` at `done_through: 4`; every direct dependency is also at Phase +4 or later, every advertised compiled operation is registered, and every +profiled dominant cost is attributed to a registration. ## Bench targets @@ -263,7 +264,7 @@ and adds only a constant-time projection. | `QAdjoin.sub` | `runQAdjoinSubLadder` | parametric, `n` | | `QAdjoin.neg` | `runQAdjoinNegLadder` | parametric, `n` | | `QAdjoin.mul` | `runQAdjoinMulLadder` | parametric, `n²` | -| `QAdjoin.inv` / `Inv.inv` | `runQAdjoinInvLadder` | parametric aggregate proxy; model decision #9743 remains scoped separately | +| `QAdjoin.inv` / `Inv.inv` | `runQAdjoinInvLadder` | parametric, `n²(n+7)` aggregate finite-word proxy; the SPEC retains the conservative `O(n³ log n)` worst-case bit-cost bound | | `QAdjoin.div` / `Div.div` | `runQAdjoinDivLadder` | parametric, `n²(n+7)` | | rational `SMul.smul` on `QAdjoin` | `runQAdjoinSmulLadder` | parametric, `n` | | `QAdjoin.toAlgebraicNumber?` | `runQAdjoinCanonical` | fixed quadratic conversion | @@ -386,7 +387,7 @@ runs below give the measurements; this table says which one counts. | `runQAdjoinSmulLadder` | **consistent** | -0.019 | current API-surface audit | | `runQAdjoinMulLadder` | **consistent** | -0.015 | current API-surface audit | | `runQAdjoinApprox` | **fixed: 17.244 ms, hash match** | — | API-surface fixed | -| `runQAdjoinInvLadder` | **consistent** | **-0.113** | current API-surface audit | +| `runQAdjoinInvLadder` | **consistent** | **-0.106** | Phase-4 completion rerun | | `runQAdjoinDivLadder` | **consistent** | -0.102 | current API-surface audit | | `runAddEliminantLadder` | **consistent** | +0.116 | current API-surface audit | | `runAlgebraicPolyOfArray` | **consistent** | -0.080 | current API-surface audit | @@ -566,14 +567,15 @@ existing #9721 finding rather than attributing the former ceiling to its fixture. The **aggregate inversion run** measures the repaired `QAdjoin.inv` at the -same scientific schedule and five outer trials. The export path is retained -from the normalized-chain repair whose timings this run supersedes: +same scientific schedule and five outer trials. The Phase-4 completion rerun +supersedes the normalized-chain repair's earlier timing export: ```sh .lake/build/bin/hexnumberfield_bench run \ Hex.NumberFieldBench.runQAdjoinInvLadder \ --outer-trials 5 \ - --export-file reports/bench-results/hex-number-field-qadjoin-inv-normalized.json + --export-file \ + reports/bench-results/hex-number-field-phase4-final-inversion.json ``` The untimed diagnostic replays the exact `xgcdLeftMonicAux` recurrence on the @@ -618,19 +620,19 @@ the SPEC. | target | ladder | verdict | fitted slope | cMin..cMax | worst spread | |---|---|---|---:|---|---:| -| `runQAdjoinInvLadder` | 4, 8, 16, 32, 48, 64, 96 | **consistent** | **-0.105** | 101.594..136.841 | 0.99% | +| `runQAdjoinInvLadder` | 4, 8, 16, 32, 48, 64, 96 | **consistent** | **-0.106** | 101.713..137.605 | 1.85% | -All seven rungs have five-trial spread at or below 0.99%. Median time is -712.0 µs at `n = 16`, 4.683 ms at `n = 32`, 32.488 ms at `n = 64`, and -96.438 ms at `n = 96`: respectively 2.08×, 4.31×, 14.74×, and 30.96× faster +All seven rungs have five-trial spread at or below 1.85%. Median time is +714.2 µs at `n = 16`, 4.720 ms at `n = 32`, 32.570 ms at `n = 64`, and +96.551 ms at `n = 96`: respectively 2.08×, 4.28×, 14.70×, and 30.92× faster than the shipped-chain single-root medians. At `n = 4`, normalization's extra scale passes cost 23.79 µs versus 20.24 µs, a 17.5% regression; it is already 1.07× faster at `n = 8`. The result hashes match the superseded run at all seven rungs, confirming identical reduced inverses. Against the complexity declaration, the normalized chain is now consistent with the operation-trace- calibrated aggregate finite-word proxy. The slope tolerance remains unchanged. -This does not update the historical PARI ratio curve below, which needs a -paired comparator rerun. +The paired PARI inversion registrations were rerun separately below so the +comparator ratios also describe the normalized implementation. The **exactification audit run** measures the replacement end-to-end family at five outer trials and both newly separated certification phases at three: @@ -963,8 +965,9 @@ check as well as a timing one. **Per-call overhead.** `runPariPolmodOverhead` issues one `polmod`-family request whose PARI-side work is a constant `0`, so it measures the JSON -request/reply round trip alone. Its median is **7.126 us** (min 6.750 us, -max 7.164 us across five repeats). Overhead is at most 22% of the PARI wall +request/reply round trip alone. The multiplication export records **7.126 us**; +the clean-tree inversion rerun records **7.063 us** (min 6.775 us, max 7.173 +us across five repeats). Overhead is at most 22% of the PARI wall time on the smallest rung of either family and under 4% on the largest, so every rung clears the 50% floor `SPEC/benchmarking.md` sets for the eligible range, and every rung is far inside the 10 s hard ceiling and the 1 s soft @@ -982,9 +985,12 @@ and inversion at `n = 4, 6, 8, 10, 12, 16`, each bracketing its crossover. The local single-root fixture removes the former smoke-cost constraint. The registered comparison domains now restore multiplication at `n = 20` and inversion at `n = 16`, giving six rungs in each family. The original five-rung -comparator export supplies the first five rows and the committed +comparator export and the committed [endpoint supplement](bench-results/hex-number-field-single-root-comparators.json) -supplies the restored sixth rows. Before the three exactification registrations +supply the multiplication rows. The clean-tree +[Phase-4 completion rerun](bench-results/hex-number-field-phase4-final-inversion-comparators.json) +supplies all six normalized-inversion rows and the current overhead probe. +Before the three exactification registrations were added, a full `verify` of those 43 registrations, including PARI, completed locally in 0.379 s; the four exactification targets verify together well inside the suite's 360 s hard cap, and the three current mode-3 targets @@ -1008,20 +1014,21 @@ Ratios are quoted as PARI wall time divided by Hex wall time, so a value above | n | Hex | PARI | driver overhead as share of PARI | canonical hash | raw ratio | adjusted ratio | |---:|---:|---:|---:|---|---:|---:| -| 4 | 19.951 us | 33.460 us | 21.3% | `0xb8302e29a4df3f41` | 1.677x | 1.320x | -| 6 | 69.026 us | 54.823 us | 13.0% | `0xc80c3d019e0b9e4c` | 0.794x | 0.691x | -| 8 | 141.853 us | 218.302 us | 3.3% | `0xd16df20a45d683c7` | 1.539x | 1.489x | -| 10 | 251.376 us | 215.512 us | 3.3% | `0x7d0941f1c8c5f9e8` | 0.857x | 0.829x | -| 12 | 505.466 us | 253.295 us | 2.8% | `0x7776688d262fc467` | 0.501x | 0.487x | -| 16 | 1.478 ms | 222.231 us | 3.2% | `0x5820b68b7d69021d` | 0.150x | 0.146x | +| 4 | 23.852 us | 33.126 us | 21.3% | `0xb8302e29a4df3f41` | 1.389x | 1.093x | +| 6 | 65.904 us | 52.177 us | 13.5% | `0xc80c3d019e0b9e4c` | 0.792x | 0.685x | +| 8 | 131.609 us | 214.185 us | 3.3% | `0xd16df20a45d683c7` | 1.627x | 1.574x | +| 10 | 222.623 us | 212.071 us | 3.3% | `0x7d0941f1c8c5f9e8` | 0.953x | 0.921x | +| 12 | 336.255 us | 236.367 us | 3.0% | `0x7776688d262fc467` | 0.703x | 0.682x | +| 16 | 709.281 us | 479.138 us | 1.5% | `0x5820b68b7d69021d` | 0.676x | 0.666x | ### Trend -Both ratios decline in the large: multiplication from 5.279x at `n = 4` to -0.381x at `n = 20`, crossing 1 just past `n = 12` (1.041x raw, 0.936x -adjusted); inversion from 1.677x at `n = 4` to 0.150x at `n = 16`. The two -declines have different causes, and only one of them is a statement about -arithmetic. +Both ratios decline over their full measured ranges: multiplication from +5.279x at `n = 4` to 0.381x at `n = 20`, crossing 1 just past `n = 12` +(1.041x raw, 0.936x adjusted); normalized inversion from 1.389x at `n = 4` +to 0.676x at `n = 16`, with the final raw crossover between `n = 8` and +`n = 10`. The inversion curve remains non-monotone because PARI has a sharp +cost step between `n = 6` and `n = 8`. For **multiplication** the decline is PARI's fixed per-call marshalling being amortised, not an algorithmic-class difference. Fitting each side's growth @@ -1041,27 +1048,25 @@ consistent with the SPEC's declared expectation for this comparator — "the constant-factor gap is structural rather than algorithmic" — and it is why this comparator is `informational` rather than `gating`. -For **inversion**, these comparator numbers describe the former unnormalized -chain. Both sides did substantial work at every rung, and their fitted -exponents differed materially: - -- Hex grows as `n^3.03`. -- PARI's net cost grows as `n^1.73`, with net times 26.3, 47.7, 211.2, 208.4, - 246.2 and 215.1 us. - -The diverging trend and ratio decline by more than a factor of three were what -coefficient swell in the unnormalized rational extended gcd predicted, and -they motivated https://github.com/kim-em/hex-dev/issues/9721. That -implementation has now been replaced by the monic-normalized chain measured -in §Verdicts, so these inversion ratios are retained as defect evidence, not -as a current comparator verdict. A future full comparator rerun must replace -them before drawing a new Hex/PARI trend. The old exponent difference was in -any case only indicative: PARI's net cost jumps discontinuously between -`n = 6` and `n = 8`, so a six-point fit through it is not a clean measurement -of PARI's asymptotics. - -The `n = 6` and `n = 8` inversion rungs are non-monotone (0.794x then 1.539x) -because PARI's own net cost jumps from 45.4 us to 208.4 us between them while +For **inversion**, the current numbers describe the same monic-normalized chain +as the scientific ladder. Both sides do substantial work at every rung. A +descriptive fit over this short crossover range gives: + +- Hex grows as `n^2.43`. +- PARI's net cost grows as `n^2.13`, with net times 26.1, 45.1, 207.1, 205.0, + 229.3 and 472.1 us. + +The Hex exponent is not a replacement complexity claim: these six small +comparator rungs span the lower-order transition that the scientific +`n²(n+7)` registration models explicitly, whereas that ladder continues to +`n = 96`. The comparator fit is orientation only. At `n = 16`, normalized Hex +inversion now takes 709.281 us instead of the former export's 1.478 ms while +preserving the same canonical hash. This removes the obsolete pre-repair trend +from the Phase-4 verdict without changing the SPEC's conservative +`O(n³ log n)` worst-case statement. + +The `n = 6` and `n = 8` inversion rungs are non-monotone (0.792x then 1.627x) +because PARI's own net cost jumps from 45.1 us to 207.1 us between them while Hex's rises smoothly; that is a PARI-side discontinuity and no claim here rests on those two points. @@ -1081,7 +1086,8 @@ does expose. samply 0.13.1 sampled at 999 Hz on the same `chungus2` hardware (Linux x86-64, AMD EPYC 9455 48-Core Processor, 96 logical CPUs), Lean 4.34.0-rc2, LeanBench -0.1.0. The five original profiles use source commit `066f6fc29` (with the +0.1.0. The normalized-inversion profile uses clean source commit `c94811435`. +The five original profiles use source commit `066f6fc29` (with the fixture-corrected algebraic-roots profile noted below); the replacement exactification profile uses `a20d30552`, and the repaired fixed-field-roots profile uses implementation commit `4a827ea546`. Fresh fixed exactification, @@ -1095,6 +1101,9 @@ oracle participates in any profiled route. export LEAN_BENCH_SAMPLY_HOME=/tmp/lean-bench-samply scripts/profile/run_profile.sh .lake/build/bin/hexnumberfield_bench \ Hex.NumberFieldBench.runQAdjoinMulLadder 16 5000000000 +# Current monic-normalized inversion implementation: +scripts/profile/run_profile.sh .lake/build/bin/hexnumberfield_bench \ + Hex.NumberFieldBench.runQAdjoinInvLadder 64 5000000000 # Historical parametric invocations, before the corresponding fixed-mode # replacements (and, for exactification, the family replacement): scripts/profile/run_profile.sh .lake/build/bin/hexnumberfield_bench \ @@ -1142,6 +1151,7 @@ profiles all pass calibration, confidence and the ±5 ms sensitivity check: | family | case | retained / rejected | calibration residual | leaf cost | classified | |---|---|---:|---:|---|---:| | `qadjoin-arithmetic` | `runQAdjoinMulLadder` n=16 | 3,938 / 4,750 | 0.755 ms | allocation 37.79%, GMP 37.51%, Lean runtime 23.72%, own code 0.74% | 99.75% | +| `qadjoin-arithmetic`, normalized inversion | `runQAdjoinInvLadder` n=64 | 4,241 / 23 | 0.411 ms | allocation 19.52%, GMP 59.96%, Lean runtime 20.16%, own code 0.21% | 99.86% | | `lazy-arithmetic` | `runLazyAddLadder` n=8 | 25,651 / 153 | 0.293 ms | allocation 50.31%, GMP 32.79%, Lean runtime 13.61%, own code 0.58% | 97.28% | | `exactification-selection` | former `runExactLadder` n=8 | 5,334 / 488 | 0.574 ms | allocation 43.74%, GMP 29.04%, Lean runtime 18.77%, own code 1.78% | 93.33% | | `exactification-factorization` | `runExactLadder` n=6 | 4,426 / 11,330 | 0.807 ms | allocation 34.86%, GMP 10.85%, Lean runtime 43.20%, own code 9.60% | 98.51% | @@ -1175,7 +1185,7 @@ exactification family; most leaves are still GMP entry points, `malloc`/`free`, or Lean runtime primitives reached from `Hex.*` frames. The inclusive ranking below identifies the hot paths. -### `qadjoin-arithmetic` — attributes cleanly +### `qadjoin-arithmetic` — both registered phases attribute cleanly | share | function | |---:|---| @@ -1188,6 +1198,30 @@ schoolbook multiplication of two degree-`(n-1)` operands, then reduction of the degree-`(2n-2)` product modulo `X^n - 2`. The two phases are 54% and 45% of the call and both are inside the registered target. Nothing here is unattributed. +The fresh normalized-inversion profile records the other changed arithmetic +route: + +| share | function | +|---:|---| +| 93.21% | `Hex.QAdjoin.inv` | +| 93.11% | `Hex.DensePoly.xgcdLeftMonic` / `xgcdLeftMonicAux` | +| 37.18% | `Hex.DensePoly.mulImpl` | +| 25.89% | `Hex.DensePoly.divMod` / `divModArray` | +| 25.61% | `Hex.DensePoly.subtractScaledShiftStep` | +| 21.81% | `Hex.DensePoly.scaleImpl` | + +The monic-normalized extended-gcd chain is the whole registered +`runQAdjoinInvLadder` operation. Its polynomial multiplication, division, +subtraction, and normalization substeps therefore map directly to that target. +GMP accounts for 59.96% of leaves, led by rational-normalization gcds, which is +consistent with the report's explicit warning that the finite-word limb proxy +does not model gcd internals. The profile exposes no dominant phase outside the +registration, so the Attribution rule is satisfied without weakening the +separate worst-case SPEC bound. The raw local profile is +`/tmp/hex-profile-runQAdjoinInvLadder-64.json.gz`; its 4.245 s timed region, +4,241 retained samples, 0.411 ms calibration residual, confidence check, and +±5 ms sensitivity check all pass. + ### `lazy-arithmetic` — attributes to isolation, as declared | share | function | @@ -1336,10 +1370,19 @@ comparison still pays for the rational gcd before the existing two-root exactification fallback; that branch is semantically covered but is not a performance claim of this ladder. -## Artefact traceability +## Reproduction + +The exact scientific, comparator, and profiling commands appear with the +corresponding evidence above. All fixtures are deterministic, so no seed is +required. The table below pins the committed raw timing exports; sampling +profiles remain developer-local as required by `SPEC/profiling.md`. + +### Artefact traceability | artefact | source commit | host state | SHA-256 | |---|---|---|---| +| [`bench-results/hex-number-field-phase4-final-inversion.json`](bench-results/hex-number-field-phase4-final-inversion.json) | `c94811435`, clean tree; final five-trial normalized-inversion ladder | idle | `5365e22a76a261ff3807521823315e1fe0a3cd7a82d112b8cb49462da84629ff` | +| [`bench-results/hex-number-field-phase4-final-inversion-comparators.json`](bench-results/hex-number-field-phase4-final-inversion-comparators.json) | `c94811435`, clean tree; current inversion pairs plus overhead | idle | `64b71bf96b66b0626defd7d7dbb6b89c9ea36c22f78c0c08af8acd562bf71699` | | [`bench-results/hex-number-field-api-surface.json`](bench-results/hex-number-field-api-surface.json) | `5010a63ba`, clean tree; all 13 current parametric registrations | variable scheduler load | `b0d0a48449f71a8b8cd7f924d8a1643c53a48e05936cfff6e440f7e6766f43a2` | | [`bench-results/hex-number-field-root-merge-current.json`](bench-results/hex-number-field-root-merge-current.json) | `2500076f9`, clean tree; authoritative three-trial merge rerun | variable scheduler load | `4c463ec14ed02a80fba3dc726458d3aad1822fb9cf6c6a31955756b2a09ccf0e` | | [`bench-results/hex-number-field-api-surface-fixed.json`](bench-results/hex-number-field-api-surface-fixed.json) | `c7cfc4de4`, clean tree; all 35 newly added fixed registrations | idle | `6d022a22bca113cdd64e9db2d9fe8e2112100bf0bbe270fbf289c87e47d799d0` | @@ -1384,6 +1427,11 @@ only `runQAdjoinRootsLadder` and introduces `runMergeRootListLadder`; its repaired profile comes from `4a827ea546`. The QAdjoin-roots fixed export then supersedes that target's parametric verdict without superseding its repair or profile evidence. +The Phase-4 completion inversion export supersedes the earlier normalized +inversion timing export, while the final inversion-comparator export supersedes +the pre-normalization inversion rows only; multiplication continues to use its +original comparator artefacts. The clean `c94811435` inversion profile at +`n = 64` refreshes attribution for the changed implementation. The three current fixed exactification profiles come from `1e5cb8472` with the instrumentation-only fixed-child sidecar hook described in §Profile. The follow-up at `2df51cf4b` leaves the certified inputs and exactification @@ -1401,14 +1449,3 @@ random seed, so a rung is identified by its parameter and the salt named in the bench source rather than by a seed. ## Concerns - -`libraries.yml` keeps `HexNumberField` at `done_through: 3`. The `QAdjoin.inv` -coefficient-swell concern is resolved by the monic-normalized chain and -aggregate expected-work model recorded in §Verdicts; its conservative -worst-case bit-cost bound remains in the SPEC. The exactification and -QAdjoin-roots model concerns are resolved by their fixed registrations and -profiles above. The exact declaration-to-registration matrix in §Track -assignment re-audit covers every advertised compiled operation, and the -profile-found dominant phases plus both root eliminants have direct targets. -There is no unresolved Phase-4 coverage or Attribution-rule concern in this -report. From 8c035e3742c214913835bb53161a19d76d73bc1d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 07:25:22 +0000 Subject: [PATCH 2/2] docs(number-field): reconcile Phase 4 review --- reports/hex-number-field-performance.md | 26 +++++++++++++++++++------ reports/phase4-ordered-mode-audit.md | 11 ++++++----- 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/reports/hex-number-field-performance.md b/reports/hex-number-field-performance.md index bf7516800..523ed9996 100644 --- a/reports/hex-number-field-performance.md +++ b/reports/hex-number-field-performance.md @@ -624,10 +624,10 @@ the SPEC. All seven rungs have five-trial spread at or below 1.85%. Median time is 714.2 µs at `n = 16`, 4.720 ms at `n = 32`, 32.570 ms at `n = 64`, and -96.551 ms at `n = 96`: respectively 2.08×, 4.28×, 14.70×, and 30.92× faster +96.551 ms at `n = 96`: respectively 2.07×, 4.28×, 14.70×, and 30.93× faster than the shipped-chain single-root medians. At `n = 4`, normalization's extra -scale passes cost 23.79 µs versus 20.24 µs, a 17.5% regression; it is -already 1.07× faster at `n = 8`. The result hashes match the superseded run at +scale passes cost 24.12 µs versus 20.24 µs, a 19.2% regression; it is +already 1.06× faster at `n = 8`. The result hashes match the superseded run at all seven rungs, confirming identical reduced inverses. Against the complexity declaration, the normalized chain is now consistent with the operation-trace- calibrated aggregate finite-word proxy. The slope tolerance remains unchanged. @@ -968,12 +968,15 @@ request whose PARI-side work is a constant `0`, so it measures the JSON request/reply round trip alone. The multiplication export records **7.126 us**; the clean-tree inversion rerun records **7.063 us** (min 6.775 us, max 7.173 us across five repeats). Overhead is at most 22% of the PARI wall -time on the smallest rung of either family and under 4% on the largest, so +time on the smallest rung of either family and under 10% on the largest rung +of either family (9.9% for multiplication and 1.5% for inversion), so every rung clears the 50% floor `SPEC/benchmarking.md` sets for the eligible range, and every rung is far inside the 10 s hard ceiling and the 1 s soft target. Both raw and overhead-adjusted ratios are recorded below; the adjusted figure subtracts only that request/reply floor, leaving serialization and -PARI-side polynomial construction charged to PARI. +PARI-side polynomial construction charged to PARI. Each table uses its +session-matched overhead probe: 7.126 us for the historical multiplication +session and 7.063 us for the current inversion session. **Eligible range and rung density.** `SPEC/benchmarking.md` warns that a doubling-only schedule usually does not give enough eligible rungs to read a @@ -1065,6 +1068,14 @@ preserving the same canonical hash. This removes the obsolete pre-repair trend from the Phase-4 verdict without changing the SPEC's conservative `O(n³ log n)` worst-case statement. +The PARI endpoint also differs between sessions: the former endpoint +supplement recorded 222.231 us at `n = 16`, below its own 253.295 us `n = 12` +row, while the clean current inversion session records 479.138 us. The current +row supersedes that non-monotone endpoint, but the descriptive `n^2.13` PARI +fit and final crossover consequently remain sensitive to this endpoint and are +not used as complexity evidence. Hash agreement fixes the compared value, not +the external runtime's between-session variance. + The `n = 6` and `n = 8` inversion rungs are non-monotone (0.792x then 1.627x) because PARI's own net cost jumps from 45.1 us to 207.1 us between them while Hex's rises smoothly; that is a PARI-side discontinuity and no claim here @@ -1217,7 +1228,10 @@ GMP accounts for 59.96% of leaves, led by rational-normalization gcds, which is consistent with the report's explicit warning that the finite-word limb proxy does not model gcd internals. The profile exposes no dominant phase outside the registration, so the Attribution rule is satisfied without weakening the -separate worst-case SPEC bound. The raw local profile is +separate worst-case SPEC bound. On this controlled bounded-height family the +omitted gcd internals scale within the aggregate proxy's unchanged tolerance; +a slower-than-declared result or a residual slope outside that tolerance would +fail mode 1 and reopen the finding. The raw local profile is `/tmp/hex-profile-runQAdjoinInvLadder-64.json.gz`; its 4.245 s timed region, 4,241 retained samples, 0.411 ms calibration residual, confidence check, and ±5 ms sensitivity check all pass. diff --git a/reports/phase4-ordered-mode-audit.md b/reports/phase4-ordered-mode-audit.md index 3e06d863c..5518c8bd5 100644 --- a/reports/phase4-ordered-mode-audit.md +++ b/reports/phase4-ordered-mode-audit.md @@ -16,8 +16,9 @@ inventory: HexBerlekampZassenhaus ([#9741](https://github.com/kim-em/hex-dev/issues/9741)), and HexRoots ([#9794](https://github.com/kim-em/hex-dev/issues/9794)). HexNumberField was also reconciled and rolled back by #9769, but a later cluster bump restored it -to 7 while its report still states that Phase 4 is blocked. It is included -below because HexNumberFieldTower relies on it. +to 7 before its focused repairs were complete. Its ordered-mode, API-coverage, +and attribution findings are now resolved; it remains included below because +HexNumberFieldTower relies on it. ## Findings and rollbacks @@ -34,7 +35,7 @@ below because HexNumberFieldTower relies on it. | HexConway | Fixed Tier-1/Tier-2 checks lack mode-3 evidence, and the lookup verdict predates the current table. | [#9813](https://github.com/kim-em/hex-dev/issues/9813) | | HexGFq | Fixed constructor/projection verdict surfaces lack mode-3 evidence and expected hashes. | [#9814](https://github.com/kim-em/hex-dev/issues/9814) | | HexMvPolyMathlib | All five proof-track threshold comparisons remain unresolved under `## Concerns`. | [#9810](https://github.com/kim-em/hex-dev/issues/9810) | -| HexNumberField | The report remains blocked on incomplete API coverage and five registrations without passing modes. | [#9722](https://github.com/kim-em/hex-dev/issues/9722), [#9743](https://github.com/kim-em/hex-dev/issues/9743), [#9795](https://github.com/kim-em/hex-dev/issues/9795), [#9796](https://github.com/kim-em/hex-dev/issues/9796) | +| HexNumberField | Resolved: every advertised compiled operation is registered, all current modes pass, dominant profiled phases are attributed, and the report has no unresolved Concern. | [#9722](https://github.com/kim-em/hex-dev/issues/9722), [#9743](https://github.com/kim-em/hex-dev/issues/9743), [#9795](https://github.com/kim-em/hex-dev/issues/9795), [#9796](https://github.com/kim-em/hex-dev/issues/9796) | | HexNumberFieldTower | The Trager envelope fails mode 2's dominant-phase test, and fixed component anchors are used as coverage without mode-3 evidence. | [#9815](https://github.com/kim-em/hex-dev/issues/9815) | | HexRowReduceMathlib | The report-less correspondence-only exemption lacks the required SPEC declaration. | [#9817](https://github.com/kim-em/hex-dev/issues/9817) | | HexDeterminantMathlib | The report-less correspondence-only exemption lacks the required SPEC declaration. | [#9818](https://github.com/kim-em/hex-dev/issues/9818) | @@ -50,8 +51,8 @@ There is no valid manual mode-2 pass in the affected set. HexNumberFieldTower's candidate citation covers the BHKS factorization phase, but the report attributes only 5.26% of the measured call to that phase. HexPolyFp supplies neither a mode-2 citation nor the required inclusive -dominant-phase profile. HexNumberField's report already classifies its -remaining inconclusive registrations as mode 4. +dominant-phase profile. HexNumberField's former inconclusive registrations now +have passing ordered modes and attributed profiles. ## Inspected with no gap