post2exe: recover 15 refused specs and fix 8 direct compilation failures

[ahemtiaz]

Improve post2exe Pipeline: Recover 15 Refused Specs and Fix 8 Compilation Failures

Summary & Impact

Existing code generated executable checkers for 772/1007 problems using the direct backend, 69/1007 using the macro backend (exec_spec_unverified), and failed for 166/1007 problems. By fixing systematic converter refusals, the direct backend now successfully generates executable code for 787/1007 problems, reducing failures from 166/1007 to 151/1007 (+15 problems recovered).

Additionally, among the 772 directly generated executable checkers previously, 12 failed with compilation errors during test case evaluation. After fixing the root causes of these errors, compilation failures have been reduced from 12/772 down to just 4/787 (783/787 now compile cleanly, and all 15 newly generated checkers compile).

Key Metrics

Metric	Before	After	Delta
Specifications accepted via direct backend (of 1,007)	772	787	+15
Emitted checkers that compile cleanly	760 / 772 (98.4%)	783 / 787 (99.5%)	+23

Total code changes across post2exe/gen_post2exe.py and post2exe/gen_test_post.py: +508 / -36 lines.

---

High-Level Fix Overview

Fix ID	Category	Problems Recovered
F1	Refusal	15
F2	Compilation	1
F3	Compilation	1
F4	Compilation	4
F5	Compilation	1
F6	Compilation	1
F7	Runtime / Performance	1
F8	Runtime / Performance	1

---

Detailed Fix Breakdown

1. Converter Refusal Fix (Fix F1)

Fix F1: Structural Recognition of Occurrence Counters & Multiset Lowering

• Fix ID: F1
• Refusal Message:
  • unbounded forall binder v: i32 (14 problems)
  • unbounded forall binder v: int (1 problem)
• Root Cause: All 15 problems express that two sequences contain the same elements via multiset equality (a.len() == b.len() && forall|v| count(a, v) == count(b, v)). Checking an unbounded quantifier over all $2^{32}$ integer values cannot be done by looping, so the converter refused them. The existing recognizer required the helper name to contain "perm"/"multiset" and its body to contain the literal substring "count(". Only 1 problem in the corpus was named count; the other 15 used count_occ, count_int, or count_char.
• Change: Replaced the fragile name/substring heuristic with AST structural pattern matching on the recursive counting shape (_occurrence_count_params, _occurrence_indicator_end, _occurrence_recursion_end). Lowered forall|v| count(a, v) == count(b, v) directly into Rust multiset equality (seq_to_multiset(a) == seq_to_multiset(b)).
• Affected / Recovered Problems (15):
  lc561, lc905, lc912, lc922, lc1122, lc1356, lc1460, lc1465, lc1502, lc1561, lc1589, lc1637, lc1984, lc2032, lc3285
• Line Delta: 133 added, 16 deleted (+133 / -16)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • _occurrence_count_params: lines 1836–1883
  • _occurrence_indicator_end: lines 1711–1730
  • _occurrence_recursion_end: lines 1731–1747
  • _multiset_equality: lines 4539–4581
  • Quantifier lowering call site: lines 4603–4607
  • Deleted legacy name heuristic in _translate_function_impl

---

2. Rust Compilation Fixes (Fixes F2 – F6)

Fix F2: Verus Operator Normalization (=~~= $\to$ =~=)

• Fix ID: F2
• Compiler Error: error: ~ cannot be used as a unary operator
• Root Cause: The Verus deep sequence equality operator =~~= was emitted verbatim into the Rust code. Since ~ is not a valid unary operator in Rust, rustc failed during parsing.
• Change: Normalized =~~= to =~= in _comparison_op. Both lower to Rust's == operator, whose derived PartialEq on owned vectors is already element-wise deep equality.
• Affected / Recovered Problems (1):
  lc566
• Line Delta: 4 added (+4)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • _comparison_op: lines 1396–1399

Fix F3: Support for spec const Declarations

• Fix ID: F3
• Compiler Error: error[E0425]: cannot find value KM_PER_LITER_SPEC
• Root Cause: The regex collecting constant declarations only matched const and pub const, ignoring pub spec const. The constant was referenced in expressions but never emitted in the generated Rust.
• Change: Added optional spec modifier support ((?:spec\s+)?) to constant collection and parsing regexes in both converter and test generator scripts.
• Affected / Recovered Problems (1):
  lc2739
• Line Delta: 4 added (+4 across 2 files)
• Locations & Line Ranges:
  • post2exe/gen_post2exe.py: _translate_direct_const_line, lines 4985–4987 (+3)
  • post2exe/gen_test_post.py: extract_const_lines, line 320 (+1)

Fix F4: Scoped Binder Typing in Quantifier Body Translation

• Fix ID: F4
• Compiler Error: error[E0308]: mismatched types
• Root Cause: Quantifier binders were untyped in the translation scope during body translation. Comparing a vector element (i32) against an untyped binder (int/i64) caused the translator to omit the widening cast (as i64), triggering Rust type mismatches.
• Change: Pushed quantifier binders with their declared direct Rust types into the translator scope during body translation and popped them in a finally block.
• Affected / Recovered Problems (4):
  lc932, lc1389, lc3152, cf1759B
• Line Delta: 10 added (+10)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • translate_quantifier: lines 4611–4620

Fix F5: Function Return Type Cast Alignment

• Fix ID: F5
• Compiler Error: error[E0308]: mismatched types
• Root Cause: Functions whose bodies computed an i32 value (e.g. index element subtraction s[k+1] - s[k]) but declared an i64 return type were emitted without an explicit cast.
• Change: Compared inferred body expression types against declared return types in _translate_function_impl, wrapping the body in an explicit ({body}) as {ret_ty} cast when differing integer types are detected.
• Affected / Recovered Problems (1):
  lc1200
• Line Delta: 5 added (+5)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • _translate_function_impl: lines 2800, 2805–2808

Fix F6: Type Coercion for Bitwise Operators

• Fix ID: F6
• Compiler Error: error[E0308]: mismatched types + no implementation for i32 ^ i64
• Root Cause: Binary bitwise operators (&, |, ^) were missing from numeric pair coercion, emitting mixed integer operations such as i32 ^ i64.
• Change: Added &, |, and ^ to the operator set calling _coerce_numeric_pair in translate_binary.
• Affected / Recovered Problems (1):
  lc2997
• Line Delta: 1 added (+1)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • translate_binary: line 3495

---

3. Complexity & Performance Optimizations (Fixes F7 – F8)

Fix F7: Occurrence Counter Emission as $O(n)$ Histogram Lookup

• Fix ID: F7
• Runtime Bottleneck: Memory exhaustion (>2 GB OOM) and quadratic slowdown.
• Root Cause: Translating an occurrence counter as a recursive Rust function caused seq_drop_last to clone the entire vector at every recursion level, while memoization hashed the full sequence. An $n$-element count cost $O(n^2)$ time and live memory.
• Change: Emitted recognized occurrence counters as a thread-local cached histogram (seq_to_multiset) keyed on the sequence Rc pointer address (_render_occurrence_count_fn), enabling $O(1)$ lookups without copying sequences.
• Affected / Recovered Problems (1):
  lc2404 (peak memory dropped from 2 GB to 9 MB).
• Line Delta: 51 added (+51)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • _render_occurrence_count_fn: lines 1793–1835
  • Emission call site in _translate_function_impl: lines 2781–2788

Fix F8: Index-Pair Quantifier Lowering & Allocation-Keyed Memoization

• Fix ID: F8
• Runtime Bottleneck: Execution timeout (>600 s)
• Root Cause: Quantifiers asserting pairwise distinctness (forall|i, j| 0 <= i < j < n ==> a[i] != a[j]) defaulted to $O(n^2)$ nested loops. Furthermore, recursive memoization hashed entire sequences element-by-element even when sequence parameters were invariant across recursive calls.
• Change:
  1. Lowered distinctness quantifier shapes into linear set insertions ($O(n)$) and transitive ordering comparisons into adjacent-pair scans ($O(n)$).
  2. For recursive functions where sequence parameters remain unchanged across all recursive self-calls, keyed memo tables by Rc pointer allocation identity rather than hashing elements.
• Affected / Recovered Problems (1):
  lc3175 (execution dropped from >600 s timeout to 4 s).
• Line Delta: 162 added (+162)
• Locations & Line Ranges (post2exe/gen_post2exe.py):
  • _index_pair_property: lines 4464–4538
  • Quantifier call site: lines 4608–4610
  • _seq_params_passed_through: lines 1762–1792
  • _self_call_nodes: lines 1748–1761
  • Memo-key generation: lines 2826–2841
  • SEQ_KEY_HELPER: lines 1261–1281
  • Assembly emission: line 6822

---

4. Shared Support Infrastructure

Two shared modules support the fixes above:

1. AST Pattern-Matching Helpers (83 lines):
   • Location: post2exe/gen_post2exe.py, lines 1628–1710
   • Helpers: _block_value_node, _strip_casts, _int_literal_value, _method_call, _seq_end_read, _seq_end_dropped
   • Used by: F1, F7, F8
2. Narrow Integer Literal Saturation (49 lines):
   • Location: post2exe/gen_post2exe.py, lines 4830–4878
   • Helpers: _int_const_value, _cast_narrow_int_literals_to_i64
   • Impact: Clamps constants outside i64 bounds (such as usize::MAX) during comparisons instead of overflowing to negative values, allowing lc566 to evaluate 228/228 test cases.