Skip to content

Add SMT encoding sharing (WIP!) - #4760

Draft
amosr-msft wants to merge 5 commits into
FStarLang:masterfrom
amosr-msft:users/amos/20261022-fstar-smt-sharing
Draft

Add SMT encoding sharing (WIP!)#4760
amosr-msft wants to merge 5 commits into
FStarLang:masterfrom
amosr-msft:users/amos/20261022-fstar-smt-sharing

Conversation

@amosr-msft

@amosr-msft amosr-msft commented Oct 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

experimental :-)
attempt to do structural sharing of SMT encoding - makes .checked files significantly smaller, especially for BV operations.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

@amosr-msft
Add opt-in SMT encoding sharing
f4decbb 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 7081de44-8211-4e82-806b-f466934ac8a6
@amosr-msft amosr-msft changed the title Add opt-in SMT encoding sharing Add SMT encoding sharing (WIP!) Oct 22, 2026
@amosr-msft

amosr-msft commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@amosr-msft
Enable SMT encoding sharing by default
72075d0 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 7081de44-8211-4e82-806b-f466934ac8a6
@amosr-msft
Make SMT encoding sharing unconditional
b3f9782 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 7081de44-8211-4e82-806b-f466934ac8a6
@github-actions

github-actions Bot commented Oct 22, 2026

Copy link
Copy Markdown
Contributor

🔬 F* Performance Comparison

Baseline: Base (master @ 5275509e26b2e4c3df3ade7df1e01b3e38f9553a) | Patched: PR #4760 (users/amos/20261022-fstar-smt-sharing @ f4decbb8c22511b6ab9d056047334f049caffd70) | Matched: 3289 tests

Summary

Metric Median Mean Geo Mean Std Dev P5 → P95 Min → Max
Memory +0.0% +0.0% 1.000× 0.1% +0.0% → +0.1% -0.9% → +0.8%
Time +0.7% +0.7% 1.006× 3.7% -5.5% → +6.9% -14.1% → +21.9%

Totals: Memory: 34.4 MiB | Time: +55.9s

Change Distribution

Metric 🟢 Improved (>5%) ⚪ Unchanged (±5%) 🔴 Regressed (>5%)
Memory 0 (0%) 3289 (100%) 0 (0%)
Time 211 (7%) 2692 (83%) 341 (11%)

Heavy Tests (baseline > 100 MiB, n=743)

Metric Median Mean Geo Mean Std Dev P5 → P95
Memory +0.0% +0.0% 1.000× 0.2% -0.5% → +0.6%
Time +0.6% +0.6% 1.006× 2.8% -4.0% → +5.0%
📉 Top 20 Memory Improvements
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
pulse/share/pulse/examples/_cache/AuxPredicate.fst.checked 168.0 MiB 167.0 MiB -0.6% 1.02s 1.03s +1.0%
pulse/share/pulse/examples/_cache/Fibonacci.fst.checked 267.0 MiB 266.0 MiB -0.4% 4.49s 4.53s +0.9%
…re/pulse/examples/_cache/PulseCorePaper.S2.Lock.fst.checked 175.0 MiB 174.0 MiB -0.6% 1.10s 1.09s -1.0%
…pulse/examples/_cache/PulseExample.BinarySearch.fst.checked 214.0 MiB 213.0 MiB -0.5% 2.69s 2.69s -0.0%
…e/pulse/examples/_cache/PulseExample.BubbleSort.fst.checked 274.0 MiB 273.0 MiB -0.4% 4.89s 4.83s -1.2%
…/share/pulse/examples/_cache/Quicksort.Parallel.fst.checked 379.0 MiB 378.0 MiB -0.3% 11.71s 11.63s -0.7%
pulse/share/pulse/examples/_cache/Quicksort.Task.fst.checked 228.0 MiB 227.0 MiB -0.4% 2.58s 2.58s +0.1%
…pulse/examples/by-example/_cache/PulseByExample.fst.checked 247.0 MiB 246.0 MiB -0.4% 3.39s 3.45s +1.8%
…se/examples/by-example/_cache/PulseTutorial.Box.fst.checked 164.0 MiB 163.0 MiB -0.6% 0.91s 0.90s -0.6%
…mple/_cache/PulseTutorial.UserDefinedPredicates.fst.checked 188.0 MiB 187.0 MiB -0.5% 1.56s 1.51s -3.2%
…e/pulse/examples/dice/_cache/CBOR.Pulse.Extern.fsti.checked 242.0 MiB 241.0 MiB -0.4% 2.10s 2.06s -2.0%
…ples/dice/_cache/CDDLExtractionTest.BytesDirect.fst.checked 215.0 MiB 214.0 MiB -0.5% 0.97s 0.98s +1.2%
pulse/share/pulse/examples/dice/_cache/DPE_CBOR.fst.checked 339.0 MiB 338.0 MiB -0.3% 8.24s 8.23s -0.2%
…ulse/examples/parallel/_cache/TaskPool.Examples.fst.checked 172.0 MiB 171.0 MiB -0.6% 1.35s 1.32s -2.4%
pulse/test/_cache/Example.Hashtable.fst.checked 216.0 MiB 215.0 MiB -0.5% 1.20s 1.24s +3.8%
pulse/test/_cache/Example.Unreachable.fst.checked 173.0 MiB 172.0 MiB -0.6% 0.78s 0.76s -2.9%
pulse/test/_cache/Match.fst.checked 135.0 MiB 134.0 MiB -0.7% 0.65s 0.66s +0.2%
pulse/test/_cache/RenameLet.fst.checked 170.0 MiB 169.0 MiB -0.6% 0.88s 0.89s +0.9%
pulse/test/_cache/TestBadDec.fst.checked 164.0 MiB 163.0 MiB -0.6% 0.81s 0.78s -3.0%
pulse/test/bug-reports/_cache/Bug111.fst.checked 133.0 MiB 132.0 MiB -0.8% 0.61s 0.60s -2.1%
📈 Top 20 Memory Regressions
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
…sts/micro-benchmarks/_cache/BvModelAgreesWithZ3.fst.checked 724.0 MiB 727.3 MiB +0.5% 369.42s 364.03s -1.5%
examples/typeclasses/_cache/Deriving.fst.checked 137.1 MiB 138.1 MiB +0.8% 1.45s 1.52s +5.1%
tests/custard/pulse/_output/cherry/PulseBasic.chc 195.0 MiB 196.0 MiB +0.5% 1.33s 1.35s +1.5%
tests/custard/pulse/_output/cherry/MonoAttrI.chc 188.0 MiB 189.0 MiB +0.5% 1.26s 1.32s +4.5%
tests/custard/pulse/_output/UglyAlias.custard.rust.krml 270.0 MiB 271.0 MiB +0.4% 1.65s 1.62s -1.2%
tests/custard/pulse/_output/PulseHashTable.custard.ml 205.0 MiB 206.0 MiB +0.5% 1.68s 1.69s +0.1%
tests/custard/pulse/_output/PulseGlobalArray.custard.ml 189.0 MiB 190.0 MiB +0.5% 1.27s 1.32s +3.9%
tests/custard/pulse/_output/PulseFnPtrRet.custard.ml 188.0 MiB 189.0 MiB +0.5% 1.30s 1.28s -1.5%
tests/custard/pulse/_output/PulseBasic.custard.krml 195.0 MiB 196.0 MiB +0.5% 1.35s 1.35s +0.1%
tests/custard/pulse/_output/MonoAttrI.dc 188.0 MiB 189.0 MiB +0.5% 1.29s 1.30s +0.3%
tests/custard/pulse/_output/EtaName.dc 188.0 MiB 189.0 MiB +0.5% 1.33s 1.34s +1.4%
tests/custard/pulse/_output/DeadRead.dc 189.0 MiB 190.0 MiB +0.5% 1.32s 1.31s -0.5%
tests/custard/pulse/_output/CborBoundarySlice.dc 276.0 MiB 277.0 MiB +0.4% 2.47s 2.42s -2.0%
tests/custard/pulse/_output/CRecType.dc 266.0 MiB 267.0 MiB +0.4% 1.65s 1.65s -0.1%
tests/custard/pulse/_output/CByValue.dc 266.0 MiB 267.0 MiB +0.4% 1.65s 1.60s -2.7%
tests/custard/pulse/_cache/UnitSlice.fst.checked 191.0 MiB 192.0 MiB +0.5% 1.21s 1.22s +0.9%
tests/custard/pulse/_cache/PulseBasic.fst.checked 173.0 MiB 174.0 MiB +0.6% 1.06s 1.09s +2.4%
tests/custard/pulse/_cache/ProjAbbrev.fst.checked 168.0 MiB 169.0 MiB +0.6% 0.82s 0.85s +3.4%
tests/custard/pulse/_cache/MonoAttrI.fsti.checked 133.0 MiB 134.0 MiB +0.8% 0.65s 0.64s -0.8%
tests/custard/pulse/_cache/InlineLetPat.fst.checked 164.0 MiB 165.0 MiB +0.6% 0.84s 0.83s -0.8%
⬇️ Top 20 Time Improvements
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
…sts/micro-benchmarks/_cache/BvModelAgreesWithZ3.fst.checked 724.0 MiB 727.3 MiB +0.5% 369.42s 364.03s -1.5%
tests/extraction/backends/_cache/ExtUIntMask.fst.checked 88.5 MiB 88.5 MiB +0.0% 300.11s 297.00s -1.0%
tests/calc/_cache/Long.fst.checked 1019.3 MiB 1019.4 MiB +0.0% 42.35s 40.22s -5.0%
…re/pulse/examples/dice/_cache/DPE.Messages.Spec.fst.checked 289.0 MiB 289.0 MiB +0.0% 127.79s 125.69s -1.6%
examples/tactics/eci19/_cache/ConstructiveLogic.fst.checked 89.8 MiB 89.8 MiB +0.0% 21.68s 20.96s -3.3%
tests/extraction/backends/_cache/ExtIntDivRem.fst.checked 69.5 MiB 69.5 MiB +0.0% 19.13s 18.47s -3.5%
tests/hacl/_cache/Lib.Vec.Lemmas.fst.checked 296.8 MiB 297.0 MiB +0.1% 22.29s 21.82s -2.1%
…ples/dsls/bool_refinement/_cache/BoolRefinement.fst.checked 436.8 MiB 436.8 MiB +0.0% 113.57s 113.10s -0.4%
tests/extraction/backends/_cache/ExtIntCast.fst.checked 77.2 MiB 77.2 MiB +0.0% 6.82s 6.40s -6.1%
pulse/share/pulse/examples/dice/_cache/DPE.fst.checked 613.0 MiB 613.0 MiB +0.0% 24.61s 24.21s -1.6%
tests/vale/_cache/X64.Poly1305.Math_i.fst.checked 141.6 MiB 141.7 MiB +0.0% 3.36s 3.08s -8.4%
tests/hacl/_cache/Lib.Exponentiation.Definition.fst.checked 138.2 MiB 138.2 MiB +0.0% 4.68s 4.42s -5.5%
…reports/closed/_cache/SquashSubtypingDivergence.fst.checked 63.2 MiB 63.2 MiB +0.0% 11.23s 10.98s -2.2%
tests/semiring/_cache/CanonCommSemiring.fst.checked 349.2 MiB 349.2 MiB +0.0% 14.83s 14.59s -1.6%
tests/extraction/_cache/Division.fst.checked 68.1 MiB 68.1 MiB -0.0% 4.73s 4.53s -4.3%
examples/dsls/stlc/_cache/STLC.Core.fst.checked 217.5 MiB 217.5 MiB +0.0% 7.34s 7.14s -2.7%
tests/bug-reports/closed/.depend 66.4 MiB 66.4 MiB +0.0% 6.16s 5.97s -3.0%
tests/extraction/backends/_cache/ExtInt128.fst.checked 68.8 MiB 68.8 MiB +0.0% 8.82s 8.65s -1.9%
tests/bug-reports/closed/_cache/Bug281.fst.checked 36.2 MiB 36.3 MiB +0.1% 3.81s 3.64s -4.4%
tests/extraction/backends/_cache/ExtIntNe.fst.checked 70.3 MiB 70.3 MiB +0.0% 3.67s 3.50s -4.6%
⬆️ Top 20 Time Regressions
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
tests/custard/_output/NormBudget.rejected 5.4 GiB 5.4 GiB +0.0% 233.10s 284.19s +21.9%
tests/custard/pulse/_cache/CborBoundarySlice.fst.checked 514.0 MiB 514.0 MiB +0.0% 49.22s 52.09s +5.8%
tests/vale/_cache/X64.Vale.Decls.fst.checked 180.1 MiB 180.1 MiB -0.0% 103.20s 105.71s +2.4%
tests/extraction/backends/_cache/ExtUIntUnsigned.fst.checked 107.5 MiB 107.5 MiB +0.0% 132.79s 134.65s +1.4%
tests/extraction/backends/_cache/ExtUInt8Lognot.fst.checked 74.5 MiB 74.5 MiB +0.0% 29.46s 30.56s +3.7%
tests/custard/_cache/ArrowUnfoldLimit.fst.checked 2.9 GiB 2.9 GiB +0.0% 43.39s 44.20s +1.9%
tests/extraction/backends/_cache/ExtUIntRotate.fst.checked 74.7 MiB 74.7 MiB +0.0% 19.87s 20.48s +3.1%
examples/metatheory/_cache/MiniValeSemantics.fst.checked 803.3 MiB 803.3 MiB +0.0% 24.38s 24.99s +2.5%
…ples/by-example/_cache/PulseTutorial.Algorithms.fst.checked 295.0 MiB 295.0 MiB +0.0% 8.30s 8.71s +5.0%
tests/tactics/_cache/Prettify.fst.checked 444.6 MiB 444.6 MiB -0.0% 17.66s 18.05s +2.2%
examples/data_structures/_cache/RBTreeIntrinsic.fst.checked 122.8 MiB 122.8 MiB +0.0% 37.64s 38.01s +1.0%
…lse/share/pulse/examples/dice/_cache/CBOR.Pulse.fst.checked 725.0 MiB 725.0 MiB +0.0% 33.01s 33.31s +0.9%
tests/extraction/backends/_cache/ExtIntSigned.fst.checked 77.0 MiB 77.0 MiB +0.0% 12.04s 12.25s +1.8%
tests/hacl/_cache/Lib.Vec.Lemmas.fsti.checked 138.0 MiB 138.0 MiB +0.0% 3.19s 3.37s +5.6%
pulse/share/pulse/examples/_cache/CustomSyntax.fst.checked 253.0 MiB 253.0 MiB +0.0% 3.97s 4.14s +4.3%
tests/tactics/_cache/Join.fst.checked 195.2 MiB 195.2 MiB +0.0% 7.85s 8.01s +2.1%
examples/data_structures/_cache/BinomialQueue.fst.checked 104.9 MiB 104.9 MiB +0.0% 7.63s 7.79s +2.0%
examples/tactics/_cache/Imp.fst.checked 129.2 MiB 129.2 MiB +0.0% 1.43s 1.57s +10.0%
pulse/test/nolib/_cache/MicroQueries.fst.checked 276.0 MiB 276.0 MiB +0.0% 1.93s 2.07s +6.9%
tests/micro-benchmarks/_cache/BVExtend.fst.checked 56.5 MiB 56.5 MiB +0.0% 15.23s 15.36s +0.9%

ℹ️ The full comparison table (3289 tests) was omitted to keep this report within GitHub's comment size limit. See the attached HTML report for all tests.

Note: Memory values report the peak OCaml heap of the F* process (excluding Z3 subprocesses). Time measurements are from single runs and may be noisy, especially for fast tests. Tests with baseline time < 0.1s are excluded from time statistics. The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary statistic for performance comparisons (1.0× = no change, <1× = improvement).

📎 Download HTML report and raw .ramon files

@amosr-msft

amosr-msft commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

ran previous benchmark too early
!bench

@github-actions

github-actions Bot commented Oct 22, 2026

Copy link
Copy Markdown
Contributor

🔬 F* Performance Comparison

Baseline: Base (master @ 5275509e26b2e4c3df3ade7df1e01b3e38f9553a) | Patched: PR #4760 (users/amos/20261022-fstar-smt-sharing @ b3f9782a6c3c02f2a91705aa00ee936361b5df27) | Matched: 3289 tests

Summary

Metric Median Mean Geo Mean Std Dev P5 → P95 Min → Max
Memory -4.4% -5.3% 0.946× 4.3% -15.8% → -1.1% -24.5% → +7.9%
Time +2.4% +2.5% 1.022× 7.0% -9.0% → +14.1% -22.3% → +29.4%

Totals: Memory: -15.0 GiB | Time: +137.8s

Change Distribution

Metric 🟢 Improved (>5%) ⚪ Unchanged (±5%) 🔴 Regressed (>5%)
Memory 1404 (43%) 1884 (57%) 1 (0%)
Time 427 (14%) 1535 (51%) 1075 (35%)

Heavy Tests (baseline > 100 MiB, n=743)

Metric Median Mean Geo Mean Std Dev P5 → P95
Memory -6.2% -6.9% 0.931× 3.7% -15.0% → -2.6%
Time +3.9% +3.7% 1.035× 6.9% -7.5% → +14.8%
📉 Top 20 Memory Improvements
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
…lse/share/pulse/examples/dice/_cache/CBOR.Pulse.fst.checked 724.0 MiB 638.0 MiB -11.9% 20.65s 24.72s +19.7%
pulse/share/pulse/examples/dice/_cache/DPE.fst.checked 613.0 MiB 540.0 MiB -11.9% 17.49s 17.62s +0.7%
pulse/share/pulse/examples/dice/_cache/DPE_CBOR.fst.checked 339.0 MiB 290.0 MiB -14.5% 5.73s 5.77s +0.8%
…lse/share/pulse/examples/dice/_cache/CDDL.Pulse.fst.checked 440.0 MiB 392.0 MiB -10.9% 7.48s 7.60s +1.6%
tests/custard/pulse/_cache/CborBoundarySlice.fst.checked 514.0 MiB 468.0 MiB -8.9% 30.57s 35.81s +17.1%
…ples/dsls/bool_refinement/_cache/BoolRefinement.fst.checked 436.7 MiB 392.3 MiB -10.2% 83.10s 94.64s +13.9%
…share/pulse/examples/dice/_cache/DPE.TestClient.fst.checked 250.0 MiB 217.0 MiB -13.2% 1.70s 1.63s -4.1%
pulse/share/pulse/examples/dice/_cache/DPE.fsti.checked 287.0 MiB 256.0 MiB -10.8% 1.74s 1.91s +9.6%
pulse/share/pulse/examples/dice/_cache/DPETypes.fsti.checked 295.0 MiB 264.0 MiB -10.5% 1.83s 1.97s +7.5%
pulse/test/_cache/Example.Hashtable.fst.checked 216.0 MiB 185.0 MiB -14.4% 0.92s 0.80s -12.9%
tests/custard/pulse/_cache/PulseHashTable.fst.checked 216.0 MiB 185.0 MiB -14.4% 0.86s 0.81s -5.6%
…share/pulse/examples/_cache/ZetaHashAccumulator.fst.checked 285.0 MiB 255.0 MiB -10.5% 2.90s 2.89s -0.3%
…ples/parallel/_cache/Example.RingBufferTransfer.fst.checked 330.0 MiB 300.0 MiB -9.1% 4.48s 4.77s +6.4%
tests/hacl/_cache/Lib.Sequence.Lemmas.fst.checked 313.4 MiB 283.5 MiB -9.6% 15.47s 16.11s +4.1%
tests/semiring/_cache/CanonCommSemiring.fst.checked 349.4 MiB 320.2 MiB -8.3% 8.98s 9.96s +11.0%
…s/dice/_cache/CDDLExtractionTest.BytesUnwrapped.fst.checked 215.0 MiB 186.0 MiB -13.5% 0.70s 0.68s -3.7%
…e/pulse/examples/dice/_cache/DPE.Messages.Parse.fst.checked 341.0 MiB 312.0 MiB -8.5% 43.52s 44.53s +2.3%
examples/dsls/stlc/_cache/STLC.Infer.fst.checked 174.6 MiB 146.3 MiB -16.2% 1.05s 1.09s +3.7%
…/dice/_cache/CDDLExtractionTest.BytesVeryDirect.fst.checked 214.0 MiB 186.0 MiB -13.1% 0.68s 0.65s -4.4%
tests/micro-benchmarks/_cache/Misc.Norm3.fst.checked 134.3 MiB 107.0 MiB -20.3% 0.65s 0.52s -19.0%
📈 Top 20 Memory Regressions
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
tests/custard/_output/NormBudget.rejected 5.4 GiB 5.8 GiB +7.9% 139.38s 157.39s +12.9%
examples/metatheory/_cache/MiniValeSemantics.fst.checked 802.5 MiB 818.6 MiB +2.0% 14.27s 16.38s +14.8%
tests/tactics/_cache/Prettify.fst.checked 444.6 MiB 450.8 MiB +1.4% 10.76s 11.63s +8.2%
tests/calc/_cache/Long.fst.checked 1019.3 MiB 1.0 GiB +0.5% 25.02s 26.67s +6.6%
bare-tests/_cache/Prims.fst.checked 25.9 MiB 27.0 MiB +4.3% 0.25s 0.26s +4.5%
bare-tests/_cache/FStar.Attributes.fsti.checked 24.5 MiB 25.3 MiB +3.3% 0.13s 0.15s +10.5%
tests/micro-benchmarks/_cache/Test.QuickCode.fst.checked 38.4 MiB 39.1 MiB +1.9% 0.19s 0.22s +19.9%
pulse/share/pulse/examples/c/.depend 53.4 MiB 53.9 MiB +0.9% 0.22s 0.24s +9.0%
bare-tests/_cache/FStar.Attributes-model.fst.checked 28.3 MiB 28.7 MiB +1.3% 0.19s 0.22s +16.0%
pulse/share/pulse/examples/parallel/.depend 56.7 MiB 56.9 MiB +0.4% 0.29s 0.33s +14.0%
pulse/test/nolib/.depend 51.7 MiB 52.0 MiB +0.5% 0.26s 0.28s +8.2%
pulse/share/pulse/examples/dice/.depend 63.2 MiB 63.4 MiB +0.3% 0.43s 0.49s +14.3%
tests/hacl/_cache/Lib.Exponentiation.Definition.fst.checked 138.2 MiB 138.4 MiB +0.1% 2.63s 2.83s +7.6%
pulse/test/bug-reports/.depend 57.6 MiB 57.7 MiB +0.2% 0.42s 0.44s +2.8%
pulse/test/error_messages/.depend 54.1 MiB 54.2 MiB +0.2% 0.31s 0.31s -1.9%
pulse/test/nolib/missing/.depend 52.6 MiB 52.7 MiB +0.1% 0.22s 0.23s +3.6%
tests/typeclasses/.depend 27.0 MiB 27.1 MiB +0.1% 0.19s 0.20s +2.6%
tests/restricted_includes/.depend 24.7 MiB 24.7 MiB +0.1% 0.16s 0.14s -10.1%
tests/overloading/.depend 22.6 MiB 22.7 MiB +0.1% 0.12s 0.13s +9.1%
tests/micro-benchmarks/.depend 42.2 MiB 42.2 MiB +0.1% 1.04s 1.07s +2.3%
⬇️ Top 20 Time Improvements
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
tests/custard/_cache/ArrowUnfoldLimit.fst.checked 2.9 GiB 2.9 GiB -0.1% 28.38s 27.73s -2.3%
doc/book/code/_cache/Part3.DataTypesALaCarte.fst.checked 180.3 MiB 154.4 MiB -14.4% 5.23s 4.83s -7.7%
tests/extraction/backends/_cache/ExtIntCast.fst.checked 77.2 MiB 67.4 MiB -12.7% 3.73s 3.49s -6.4%
tests/extraction/backends/_cache/ExtUInt8Lognot.fst.checked 74.5 MiB 69.2 MiB -7.2% 20.74s 20.52s -1.0%
tests/micro-benchmarks/_cache/BvBinaryOps.fst.checked 74.6 MiB 71.2 MiB -4.5% 5.75s 5.56s -3.3%
doc/book/code/_cache/MerkleTree.fst.checked 70.6 MiB 67.5 MiB -4.4% 0.94s 0.76s -19.3%
tests/extraction/_cache/Division.fst.checked 68.1 MiB 62.9 MiB -7.7% 2.85s 2.68s -5.7%
tests/micro-benchmarks/_cache/Misc.Norm3.fst.checked 134.3 MiB 107.0 MiB -20.3% 0.65s 0.52s -19.0%
pulse/test/_cache/Example.Hashtable.fst.checked 216.0 MiB 185.0 MiB -14.4% 0.92s 0.80s -12.9%
tests/custard/pulse/_output/NestArr.dc 190.0 MiB 178.0 MiB -6.3% 0.95s 0.83s -12.4%
examples/tactics/_cache/Imp.fst.checked 129.2 MiB 122.1 MiB -5.5% 1.03s 0.91s -11.4%
examples/typeclasses/_cache/Deriving.fst.checked 137.1 MiB 121.0 MiB -11.7% 1.04s 0.92s -11.2%
doc/book/code/_cache/Part1.Quicksort.Generic.fst.checked 53.7 MiB 45.2 MiB -15.9% 0.72s 0.61s -15.4%
tests/custard/pulse/_output/cherry/ArrTup.chc 190.0 MiB 178.0 MiB -6.3% 0.95s 0.84s -11.6%
pulse/test/_cache/InlineArrayLen.fst.checked 172.0 MiB 158.0 MiB -8.1% 0.79s 0.68s -13.8%
doc/book/code/_cache/TypeclassesAlt3.fst.checked 89.7 MiB 75.0 MiB -16.3% 1.42s 1.32s -7.4%
pulse/test/_cache/Example.Unreachable.fst.checked 172.0 MiB 153.0 MiB -11.0% 0.56s 0.46s -17.9%
…/typeclasses/_cache/Pulse.Class.BoundedIntegers.fst.checked 105.7 MiB 93.0 MiB -12.0% 1.57s 1.47s -6.3%
doc/book/code/_cache/Part1.Quicksort.fst.checked 59.2 MiB 50.5 MiB -14.7% 0.94s 0.84s -10.3%
tests/custard/pulse/_output/cherry/PulseHashTable.chc 205.0 MiB 194.0 MiB -5.4% 1.16s 1.07s -8.3%
⬆️ Top 20 Time Regressions
File Mem (base) Mem (patch) Mem Δ Time (base) Time (patch) Time Δ
tests/custard/_output/NormBudget.rejected 5.4 GiB 5.8 GiB +7.9% 139.38s 157.39s +12.9%
…re/pulse/examples/dice/_cache/DPE.Messages.Spec.fst.checked 289.0 MiB 273.0 MiB -5.5% 92.33s 104.97s +13.7%
…ples/dsls/bool_refinement/_cache/BoolRefinement.fst.checked 436.7 MiB 392.3 MiB -10.2% 83.10s 94.64s +13.9%
tests/extraction/backends/_cache/ExtUIntMask.fst.checked 88.5 MiB 80.7 MiB -8.8% 226.39s 235.62s +4.1%
…sts/micro-benchmarks/_cache/BvModelAgreesWithZ3.fst.checked 725.1 MiB 720.0 MiB -0.7% 298.58s 305.07s +2.2%
tests/extraction/backends/_cache/ExtUIntUnsigned.fst.checked 107.5 MiB 100.1 MiB -6.9% 98.59s 104.65s +6.1%
tests/custard/pulse/_cache/CborBoundarySlice.fst.checked 514.0 MiB 468.0 MiB -8.9% 30.57s 35.81s +17.1%
examples/data_structures/_cache/RBTreeIntrinsic.fst.checked 123.0 MiB 101.6 MiB -17.3% 24.28s 28.46s +17.2%
…lse/share/pulse/examples/dice/_cache/CBOR.Pulse.fst.checked 724.0 MiB 638.0 MiB -11.9% 20.65s 24.72s +19.7%
…_bool_refinement/_cache/DependentBoolRefinement.fst.checked 274.1 MiB 251.8 MiB -8.1% 14.25s 17.34s +21.7%
examples/metatheory/_cache/MiniValeSemantics.fst.checked 802.5 MiB 818.6 MiB +2.0% 14.27s 16.38s +14.8%
…se/examples/by-example/_cache/ParallelIncrement.fst.checked 501.0 MiB 485.0 MiB -3.2% 12.89s 14.88s +15.5%
…/share/pulse/examples/dice/_cache/CBOR.Spec.Map.fst.checked 482.0 MiB 467.0 MiB -3.1% 7.26s 9.02s +24.3%
tests/vale/_cache/X64.Vale.Decls.fst.checked 180.1 MiB 161.5 MiB -10.3% 80.18s 81.91s +2.2%
tests/calc/_cache/Long.fst.checked 1019.3 MiB 1.0 GiB +0.5% 25.02s 26.67s +6.6%
…-example/_cache/PulseTutorial.ParallelIncrement.fst.checked 416.0 MiB 391.0 MiB -6.0% 11.18s 12.81s +14.6%
…reports/closed/_cache/SquashSubtypingDivergence.fst.checked 63.2 MiB 50.6 MiB -20.0% 7.24s 8.48s +17.2%
…e/pulse/examples/dice/_cache/DPE.Messages.Parse.fst.checked 341.0 MiB 312.0 MiB -8.5% 43.52s 44.53s +2.3%
tests/semiring/_cache/CanonCommSemiring.fst.checked 349.4 MiB 320.2 MiB -8.3% 8.98s 9.96s +11.0%
tests/extraction/backends/_cache/ExtIntDivRem.fst.checked 69.5 MiB 63.7 MiB -8.4% 10.29s 11.23s +9.1%

ℹ️ The full comparison table (3289 tests) was omitted to keep this report within GitHub's comment size limit. See the attached HTML report for all tests.

Note: Memory values report the peak OCaml heap of the F* process (excluding Z3 subprocesses). Time measurements are from single runs and may be noisy, especially for fast tests. Tests with baseline time < 0.1s are excluded from time statistics. The geometric mean (Geo Mean) of the patched/baseline ratio is the most robust summary statistic for performance comparisons (1.0× = no change, <1× = improvement).

📎 Download HTML report and raw .ramon files

@amosr-msft
Optimize SMT sharing traversal
befb3db 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 7081de44-8211-4e82-806b-f466934ac8a6
@amosr-msft
Revert "Optimize SMT sharing traversal"
debed4e 
This reverts commit befb3db.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@amosr-msft