SMT query performance optimization: 40% reduction in total SMT time#270
Merged
Conversation
Total SMT time reduced from 117.2 min to 70.4 min (-39.9%). Total wall time reduced from 236.6 min to 164.1 min (-30.6%). Full clean build verified: 690 files, zero errors. ## Root cause: cbor_map_defined_alt quantifier cascade Z3 quantifier profiling (smt.qi.profile=true on isolated .smt2 files) revealed that cbor_map_defined_alt with [SMTPat (cbor_map_defined k f)] caused 64,000+ quantifier instantiations through a chain reaction: 1. cbor_map_equal unfolds to (forall k. cbor_map_get m1 k == cbor_map_get m2 k) 2. Each cbor_map_get produces cbor_map_defined terms 3. cbor_map_defined_alt fires, introducing (exists v. cbor_map_mem (k,v) f) 4. Existential skolemization creates new ground terms 5. New terms trigger more cbor_map_defined matches -> positive feedback loop This cascade caused the single most expensive query (impl_map_group_filter while-loop VC in CDDL.Pulse.MapGroup.fst) to take 1371 seconds. ## Fix: Remove SMTPat, add bring_cbor_map_defined_alt helper Removed [SMTPat] from cbor_map_defined_alt in both: - CBOR.Spec.API.Type.fsti - CBOR.Spec.Raw.DataModel.fsti Added bring_cbor_map_defined_alt() helper that re-introduces the quantifier with its pattern in a controlled scope. Called explicitly in only 8 locations that genuinely need it: - CBOR.Spec.API.Type.fsti: cbor_map_sub, cbor_map_ind_bounded - CBOR.Spec.Raw.DataModel.fsti: cbor_map_sub - CDDL.Spec.MapGroup.fsti: 5 footprint lemmas - CDDL.Spec.MapGroup.Base.fst: cbor_map_singleton_inj - CDDL.Pulse.Parse.ArrayGroup.fst: impl_zero_copy_array - CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux1.fst: disjoint lemma ## Per-file improvements - CDDL.Pulse.MapGroup.fst: 1600s -> 142s (11.3x speedup, -91%) - CDDL.Spec.MapGroup.Base.fst: 543s -> 84s ( 6.5x speedup, -85%) - CBOR.Pulse.Raw.EverParse.Nondet.Gen.fst: 952s -> 715s (-25%) - CBOR.Spec.Raw.EverParse.fst: 1049s -> 955s (-9%) ## Additional settings tightening - CDDL.Pulse.MapGroup.fst: fuel 8->2, ifuel 6->1, rlimit 1024->768 - CBOR.Spec.Raw.EverParse.fst: ifuel 8->2, rlimit 1024->256 (parse_raw_data_item_eq); rlimit 256->64-128 for 4 other functions - CBOR.Pulse.Raw.EverParse.Nondet.Gen.fst: fuel 4->2, ifuel 8->4, rlimit 256->128, context_pruning re-enabled - CDDL.Spec.AST.Elab.Disjoint.Array.fst: z3seed 2->42 (stability) - CDDL.Pulse.Serialize.Gen.ArrayGroup.fst: added --split_queries always (pre-existing flaky proof stabilization) ## Methodology 1. Full clean build with --query_stats to profile all 21,900+ queries 2. Identified top files by aggregated SMT time 3. Used --split_queries always --z3refresh --log_queries to isolate expensive sub-goals into individual .smt2 files 4. Ran Z3 with smt.qi.profile=true on isolated queries to get per-quantifier instantiation counts 5. Identified cbor_map_defined_alt as the dominant quantifier (64K+ instantiations vs <200 for everything else) 6. Removed SMTPat, fixed 8 downstream proofs with explicit calls ## New files - benchmark.sh: Automated benchmarking script for SMT performance (full build + report + CSV generation) - optimizing.md: Detailed optimization plan and investigation notes Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- map_group_footprint_concat: changed 3-way SMTPat to single conclusion pattern. Prevents 65K+ instantiations in recursive map group decomposition (Z3 qi profiling on MGCC Q85). - map_group_footprint_choice: same treatment. - CDDL.Spec.AST.Elab.MGCC: ifuel 8→4. Full clean build: 690 files, zero errors. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The assertion at line 470: remaining_data_items_header h1 + (SZ.v n - 1) <= SZ.v (S.len tl1') was unstable — Z3 needed to derive the nlist length bound through deep subtype checking (743K subtype_of instantiations in qi profiling). Fix: Add explicit call to parse_nlist_kind_low which directly provides the fact that serialized nlist length >= n * parser_kind_low. This reduces Q73 from 68s/194 rlimit to 245ms/1 rlimit. Also bump rlimit back to 256 (from 128) since Q71 uses 181 rlimit on the while-loop invariant — 128 was too tight for CI hardware. Full clean build: 690 files, zero errors, 71.0 min SMT. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Member
|
Thanks a lot Nik! All proofs pass now. |
tahina-pro
added a commit
to tahina-pro/quackyducky
that referenced
this pull request
Mar 27, 2026
….fst/.fsti only) Backport .fst/.fsti changes from project-everest/everparse PR project-everest#270 to master. Removes SMTPat from cbor_map_defined_alt, adds bring_cbor_map_defined_alt helper for controlled scope, and tightens fuel/ifuel/rlimit settings. Two hunks required manual resolution: - CBOR.Pulse.Raw.EverParse.Nondet.Gen.fst: line offset difference - CDDL.Spec.AST.Elab.Disjoint.Array.fst: local lacked --z3seed flag Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
added a commit
to tahina-pro/quackyducky
that referenced
this pull request
Mar 27, 2026
- CDDL.Spec.ArrayGroup.fst: add #push-options "--z3rlimit 16" around array_group_concat_unique_strong'_zero_or_more_left (default rlimit=5 insufficient after cbor_map_defined_alt SMTPat removal) - CDDL.Spec.AST.Elab.Disjoint.Array.fst: revert --z3seed 42 (upstream seed change was for fstar2 branch; master branch passes without seed) Note: CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma12.fst has a pre-existing "Parse error: </labels> not found" failure on master, unrelated to this backport. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
added a commit
that referenced
this pull request
Mar 27, 2026
Backport proof changes from #270 to `master`
tahina-pro
added a commit
to tahina-pro/quackyducky
that referenced
this pull request
Mar 27, 2026
…anges - CDDL.Spec.ArrayGroup.fst: add --split_queries always around array_group_concat_unique_strong'_zero_or_more_left (combined VC unstable after cbor_map_defined_alt SMTPat removal) - CDDL.Spec.AST.Elab.Disjoint.Array.fst: add explicit assert (name_mem n e.e_sem_env.se_bound) in GDef branch (Z3 can no longer derive this automatically with changed SMT context) - CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma12.fst: add --z3refresh to prevent Z3 XML parse errors under parallel builds Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Merged
tahina-pro
added a commit
to tahina-pro/quackyducky
that referenced
this pull request
Mar 28, 2026
…anges - CDDL.Spec.ArrayGroup.fst: add --split_queries always around array_group_concat_unique_strong'_zero_or_more_left (combined VC unstable after cbor_map_defined_alt SMTPat removal) - CDDL.Spec.AST.Elab.Disjoint.Array.fst: add explicit assert (name_mem n e.e_sem_env.se_bound) in GDef branch (Z3 can no longer derive this automatically with changed SMT context) - CDDL.Pulse.Serialize.Gen.MapGroup.ZeroOrMore.Aux2.Lemma12.fst: add --z3refresh to prevent Z3 XML parse errors under parallel builds Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
added a commit
that referenced
this pull request
Mar 28, 2026
This reverts commit 0810f84.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Total SMT time reduced from 117.2 min to 70.4 min (-39.9%). Total wall time reduced from 236.6 min to 164.1 min (-30.6%). Full clean build verified: 690 files, zero errors.
Root cause: cbor_map_defined_alt quantifier cascade
Z3 quantifier profiling (smt.qi.profile=true on isolated .smt2 files) revealed that cbor_map_defined_alt with [SMTPat (cbor_map_defined k f)] caused 64,000+ quantifier instantiations through a chain reaction:
This cascade caused the single most expensive query (impl_map_group_filter while-loop VC in CDDL.Pulse.MapGroup.fst) to take 1371 seconds.
Fix: Remove SMTPat, add bring_cbor_map_defined_alt helper
Removed [SMTPat] from cbor_map_defined_alt in both:
Added bring_cbor_map_defined_alt() helper that re-introduces the quantifier with its pattern in a controlled scope. Called explicitly in only 8 locations that genuinely need it:
Per-file improvements
Additional settings tightening
Methodology
New files