Skip to content

Commit 4559f49

Browse files
andrii-a8candreistefanescuclaude
authored
Range count quantifier (#438)
* quantifier fixes * feat: added range count quantifier * feat: updates * feat: added is valid * refactor: remove dead requires_sum/requires_filter_indices, use range_based() After the unify-quantifier-helpers work, count/sum_map/range_count are direct scalar helpers — none wrap their result with $0_vec_$sum anymore. The `qt.requires_sum()` gates in mono_analysis and verification_analysis were pushing `prover_vec_sum_qid` as a dead dependency. - Remove QuantifierType::requires_sum() and requires_filter_indices() (both had no remaining callers after the refactor). - Drop the now-dead push_todo_fun / mark_inlined calls for the sum helper in mono_analysis.rs and verification_analysis.rs. - Replace `matches!(info.qht, RangeMap | RangeCount)` with the existing `info.qht.range_based()` method in lib.rs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * feat: add range_sum_map quantifier helper Mirrors range_count as the sum-over-integer-range counterpart, and completes the range-based helper family: | Helper | Vector-valued | Scalar-valued | |-----------------|---------------|---------------| | Over a vector | map, filter, | count, sum_map, | | find_indices | find_index | | Over a range | range_map | range_count, | | | range_sum_map (NEW) Move API: `range_sum_map!<U>(start, end, |i| f(i)): Integer` — sums FN(i) for i in [start, end). Typed as Integer for overflow safety. Boogie axioms (scalar helper parallel to sum_map, range-based like range_count): empty, left-step, right-step, split (compound trigger), and bounding gated on `result_is_unsigned` (FN's Move return type). No singleton — derivable from left-step + empty and keeps matching pressure low. Tests: range_sum_map.ok (concrete), range_sum_map.fail, and range_sum_map_split.ok (symbolic n/k forces the split axiom to fire). 404 tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * test: fill coverage gaps for range_count and range_sum_map Targeted tests that exercise axiom shapes previously only covered for the vector-based helpers: - range_count_split.ok — symbolic n/k forcing the split axiom to fire (two-way and three-way partitions). - range_count_loop.ok — loop iterating [0, n) with invariant over the processed prefix, exercising left-step. - range_sum_map_bounding.ok — symbolic a/b nested in [0, n], exercises the unsigned-return bounding axiom gate. - range_sum_map_loop.ok — loop with 0/1-contribution FN (odd_to_int) mirroring sum_map_loop, exercises left-step without overflow concerns. 408 tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io> Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent ee156b0 commit 4559f49

28 files changed

+663
-39
lines changed

‎crates/move-model/src/model.rs‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1633,6 +1633,10 @@ impl GlobalEnv {
16331633
const PROVER_BEGIN_SUM_MAP_RANGE_LAMBDA: &'static str = "begin_sum_map_range_lambda";
16341634
const PROVER_END_SUM_MAP_LAMBDA: &'static str = "end_sum_map_lambda";
16351635
const PROVER_BEGIN_RANGE_MAP_LAMBDA: &'static str = "begin_range_map_lambda";
1636+
const PROVER_BEGIN_RANGE_COUNT_LAMBDA: &'static str = "begin_range_count_lambda";
1637+
const PROVER_END_RANGE_COUNT_LAMBDA: &'static str = "end_range_count_lambda";
1638+
const PROVER_BEGIN_RANGE_SUM_MAP_LAMBDA: &'static str = "begin_range_sum_map_lambda";
1639+
const PROVER_END_RANGE_SUM_MAP_LAMBDA: &'static str = "end_range_sum_map_lambda";
16361640
const PROVER_END_RANGE_MAP_LAMBDA: &'static str = "end_range_map_lambda";
16371641
const PROVER_RANGE: &'static str = "range";
16381642
const PROVER_VEC_SUM: &'static str = "sum";
@@ -2122,6 +2126,34 @@ impl GlobalEnv {
21222126
)
21232127
}
21242128

2129+
pub fn prover_begin_range_count_lambda_qid(&self) -> QualifiedId<FunId> {
2130+
self.get_fun_qid(
2131+
Self::PROVER_VECTOR_MODULE_NAME,
2132+
Self::PROVER_BEGIN_RANGE_COUNT_LAMBDA,
2133+
)
2134+
}
2135+
2136+
pub fn prover_end_range_count_lambda_qid(&self) -> QualifiedId<FunId> {
2137+
self.get_fun_qid(
2138+
Self::PROVER_VECTOR_MODULE_NAME,
2139+
Self::PROVER_END_RANGE_COUNT_LAMBDA,
2140+
)
2141+
}
2142+
2143+
pub fn prover_begin_range_sum_map_lambda_qid(&self) -> QualifiedId<FunId> {
2144+
self.get_fun_qid(
2145+
Self::PROVER_VECTOR_MODULE_NAME,
2146+
Self::PROVER_BEGIN_RANGE_SUM_MAP_LAMBDA,
2147+
)
2148+
}
2149+
2150+
pub fn prover_end_range_sum_map_lambda_qid(&self) -> QualifiedId<FunId> {
2151+
self.get_fun_qid(
2152+
Self::PROVER_VECTOR_MODULE_NAME,
2153+
Self::PROVER_END_RANGE_SUM_MAP_LAMBDA,
2154+
)
2155+
}
2156+
21252157
pub fn prover_range_qid(&self) -> QualifiedId<FunId> {
21262158
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_RANGE)
21272159
}
@@ -3557,6 +3589,10 @@ impl GlobalEnv {
35573589
self.prover_end_sum_map_lambda_qid(),
35583590
self.prover_begin_range_map_lambda_qid(),
35593591
self.prover_end_range_map_lambda_qid(),
3592+
self.prover_begin_range_count_lambda_qid(),
3593+
self.prover_end_range_count_lambda_qid(),
3594+
self.prover_begin_range_sum_map_lambda_qid(),
3595+
self.prover_end_range_sum_map_lambda_qid(),
35603596
self.prover_range_qid(),
35613597
self.prover_vec_sum_qid(),
35623598
self.prover_vec_sum_range_qid(),
@@ -3802,6 +3838,10 @@ impl GlobalEnv {
38023838
self.prover_end_sum_map_lambda_qid(),
38033839
self.prover_begin_range_map_lambda_qid(),
38043840
self.prover_end_range_map_lambda_qid(),
3841+
self.prover_begin_range_count_lambda_qid(),
3842+
self.prover_end_range_count_lambda_qid(),
3843+
self.prover_begin_range_sum_map_lambda_qid(),
3844+
self.prover_end_range_sum_map_lambda_qid(),
38053845
self.prover_range_qid(),
38063846
self.prover_vec_sum_qid(),
38073847
self.prover_vec_sum_range_qid(),

‎crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs‎

Lines changed: 30 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -145,15 +145,18 @@ impl<'env> BoogieTranslator<'env> {
145145
QuantifierHelperType::RangeMap => {
146146
format!("$RangeMapQuantifierHelper_{}", function_name)
147147
}
148-
148+
QuantifierHelperType::RangeCount => {
149+
format!("$RangeCountQuantifierHelper_{}", function_name)
150+
}
151+
QuantifierHelperType::RangeSumMap => {
152+
format!("$RangeSumMapQuantifierHelper_{}", function_name)
153+
}
149154
QuantifierHelperType::FindIndex => {
150155
format!("$FindIndexQuantifierHelper_{}", function_name)
151156
}
152-
153157
QuantifierHelperType::FindIndices => {
154158
format!("$FindIndicesQuantifierHelper_{}", function_name)
155159
}
156-
157160
QuantifierHelperType::Filter => format!("$FilterQuantifierHelper_{}", function_name),
158161
QuantifierHelperType::Count => format!("$CountQuantifierHelper_{}", function_name),
159162
QuantifierHelperType::SumMap => format!("$SumMapQuantifierHelper_{}", function_name),
@@ -3483,6 +3486,30 @@ impl<'env> FunctionTranslator<'env> {
34833486
extra_args,
34843487
)
34853488
}
3489+
QuantifierType::RangeCount => {
3490+
let count_quant_name = self
3491+
.parent
3492+
.get_quantifier_helper_name(QuantifierHelperType::RangeCount, fun_name);
3493+
format!(
3494+
"{}({}, {}{})",
3495+
count_quant_name,
3496+
fmt_temp(srcs[0]),
3497+
fmt_temp(srcs[1]),
3498+
extra_args,
3499+
)
3500+
}
3501+
QuantifierType::RangeSumMap => {
3502+
let sum_map_quant_name = self
3503+
.parent
3504+
.get_quantifier_helper_name(QuantifierHelperType::RangeSumMap, fun_name);
3505+
format!(
3506+
"{}({}, {}{})",
3507+
sum_map_quant_name,
3508+
fmt_temp(srcs[0]),
3509+
fmt_temp(srcs[1]),
3510+
extra_args,
3511+
)
3512+
}
34863513
QuantifierType::Count => {
34873514
let count_quant_name = self
34883515
.parent

‎crates/move-prover-boogie-backend/src/boogie_backend/lib.rs‎

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -560,7 +560,7 @@ impl QuantifierHelperInfo {
560560
let func_env = env.get_function(info.function);
561561
let params_types = Type::instantiate_vec(func_env.get_parameter_types(), &info.inst);
562562

563-
let mut quantifier_params = if matches!(info.qht, QuantifierHelperType::RangeMap) {
563+
let mut quantifier_params = if info.qht.range_based() {
564564
"start: int, end: int".to_string()
565565
} else {
566566
format!(
@@ -569,7 +569,7 @@ impl QuantifierHelperInfo {
569569
)
570570
};
571571

572-
let mut quantifier_args = if matches!(info.qht, QuantifierHelperType::RangeMap) {
572+
let mut quantifier_args = if info.qht.range_based() {
573573
"start, end".to_string()
574574
} else {
575575
"v, start, end".to_string()
@@ -619,17 +619,16 @@ impl QuantifierHelperInfo {
619619
(String::new(), String::new())
620620
};
621621

622-
let (input_vec_is_equal_suffix, input_elem_type) =
623-
if matches!(info.qht, QuantifierHelperType::RangeMap) {
624-
(String::new(), String::new()) // no input vector
625-
} else {
626-
let elem_ty = params_types[info.li].skip_reference();
627-
let vec_type = Type::Vector(Box::new(elem_ty.clone()));
628-
(
629-
boogie_type_suffix(env, &vec_type),
630-
boogie_type(env, &elem_ty),
631-
)
632-
};
622+
let (input_vec_is_equal_suffix, input_elem_type) = if info.qht.range_based() {
623+
(String::new(), String::new()) // no input vector
624+
} else {
625+
let elem_ty = params_types[info.li].skip_reference();
626+
let vec_type = Type::Vector(Box::new(elem_ty.clone()));
627+
(
628+
boogie_type_suffix(env, &vec_type),
629+
boogie_type(env, &elem_ty),
630+
)
631+
};
633632

634633
// True when FN's Move return type is a fixed-width unsigned int
635634
// (U8..U256). Used by helpers (e.g. sum_map bounding) to gate axioms

‎crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1428,6 +1428,69 @@ axiom (forall {{QP}}, a: int, b: int ::
14281428
{%- endif %}
14291429
{%- endif %}
14301430

1431+
{%- if instance.qht == "range_count" %}
1432+
function $RangeCountQuantifierHelper_{{FN}}({{QP}}): int;
1433+
axiom (forall {{QP}} :: {$RangeCountQuantifierHelper_{{FN}}({{QA}})}
1434+
0 <= $RangeCountQuantifierHelper_{{FN}}({{QA}}) &&
1435+
$RangeCountQuantifierHelper_{{FN}}({{QA}}) <= (if start <= end then end - start else 0) &&
1436+
(start >= end ==> $RangeCountQuantifierHelper_{{FN}}({{QA}}) == 0)
1437+
);
1438+
// left step
1439+
axiom (forall {{QP}} :: {$RangeCountQuantifierHelper_{{FN}}({{QA}})}
1440+
start < end ==>
1441+
$RangeCountQuantifierHelper_{{FN}}({{QA}}) ==
1442+
(if {{FN}}({{EAB}}start{{EAA}}) then 1 else 0)
1443+
+ $RangeCountQuantifierHelper_{{FN}}(start + 1, end{{CAT}})
1444+
);
1445+
// right step
1446+
axiom (forall {{QP}} :: {$RangeCountQuantifierHelper_{{FN}}({{QA}})}
1447+
start < end ==>
1448+
$RangeCountQuantifierHelper_{{FN}}({{QA}}) ==
1449+
$RangeCountQuantifierHelper_{{FN}}(start, end - 1{{CAT}})
1450+
+ (if {{FN}}({{EAB}}end - 1{{EAA}}) then 1 else 0)
1451+
);
1452+
// split — compound trigger on the two sub-range counts
1453+
axiom (forall {{QP}}, split_point: int ::
1454+
{$RangeCountQuantifierHelper_{{FN}}(start, split_point{{CAT}}), $RangeCountQuantifierHelper_{{FN}}(split_point, end{{CAT}})}
1455+
start <= split_point && split_point <= end ==>
1456+
$RangeCountQuantifierHelper_{{FN}}(start, split_point{{CAT}}) + $RangeCountQuantifierHelper_{{FN}}(split_point, end{{CAT}})
1457+
== $RangeCountQuantifierHelper_{{FN}}({{QA}}));
1458+
{%- endif %}
1459+
1460+
{%- if instance.qht == "range_sum_map" %}
1461+
function $RangeSumMapQuantifierHelper_{{FN}}({{QP}}): int;
1462+
axiom (forall {{QP}} :: {$RangeSumMapQuantifierHelper_{{FN}}({{QA}})}
1463+
start >= end ==> $RangeSumMapQuantifierHelper_{{FN}}({{QA}}) == 0
1464+
);
1465+
// left step
1466+
axiom (forall {{QP}} :: {$RangeSumMapQuantifierHelper_{{FN}}({{QA}})}
1467+
start < end ==>
1468+
$RangeSumMapQuantifierHelper_{{FN}}({{QA}}) ==
1469+
{{FN}}({{EAB}}start{{EAA}})
1470+
+ $RangeSumMapQuantifierHelper_{{FN}}(start + 1, end{{CAT}})
1471+
);
1472+
// right step
1473+
axiom (forall {{QP}} :: {$RangeSumMapQuantifierHelper_{{FN}}({{QA}})}
1474+
start < end ==>
1475+
$RangeSumMapQuantifierHelper_{{FN}}({{QA}}) ==
1476+
$RangeSumMapQuantifierHelper_{{FN}}(start, end - 1{{CAT}})
1477+
+ {{FN}}({{EAB}}end - 1{{EAA}})
1478+
);
1479+
// split — compound trigger on the two sub-range sums
1480+
axiom (forall {{QP}}, split_point: int ::
1481+
{$RangeSumMapQuantifierHelper_{{FN}}(start, split_point{{CAT}}), $RangeSumMapQuantifierHelper_{{FN}}(split_point, end{{CAT}})}
1482+
start <= split_point && split_point <= end ==>
1483+
$RangeSumMapQuantifierHelper_{{FN}}(start, split_point{{CAT}}) + $RangeSumMapQuantifierHelper_{{FN}}(split_point, end{{CAT}})
1484+
== $RangeSumMapQuantifierHelper_{{FN}}({{QA}}));
1485+
{%- if instance.result_is_unsigned %}
1486+
// bounding — nested range sum <= outer (FN returns unsigned)
1487+
axiom (forall {{QP}}, a: int, b: int ::
1488+
{$RangeSumMapQuantifierHelper_{{FN}}(a, b{{CAT}}), $RangeSumMapQuantifierHelper_{{FN}}({{QA}})}
1489+
start <= a && a <= b && b <= end ==>
1490+
$RangeSumMapQuantifierHelper_{{FN}}(a, b{{CAT}}) <= $RangeSumMapQuantifierHelper_{{FN}}({{QA}}));
1491+
{%- endif %}
1492+
{%- endif %}
1493+
14311494
{% endmacro quantifier_helpers_module %}
14321495

14331496
{% macro dynamic_field_key_module(impl, instance) %}

‎crates/move-stackless-bytecode/src/quantifier_iterator_analysis.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,16 @@ impl QuantifierPattern {
141141
env.prover_end_range_map_lambda_qid(),
142142
QuantifierType::RangeMap,
143143
),
144+
QuantifierPattern::new(
145+
env.prover_begin_range_count_lambda_qid(),
146+
env.prover_end_range_count_lambda_qid(),
147+
QuantifierType::RangeCount,
148+
),
149+
QuantifierPattern::new(
150+
env.prover_begin_range_sum_map_lambda_qid(),
151+
env.prover_end_range_sum_map_lambda_qid(),
152+
QuantifierType::RangeSumMap,
153+
),
144154
]
145155
}
146156

‎crates/move-stackless-bytecode/src/stackless_bytecode.rs‎

Lines changed: 23 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -138,12 +138,16 @@ pub enum QuantifierType {
138138
SumMap,
139139
SumMapRange,
140140
RangeMap,
141+
RangeCount,
142+
RangeSumMap,
141143
}
142144

143145
#[derive(Debug, Clone, Ord, Eq, PartialEq, PartialOrd)]
144146
pub enum QuantifierHelperType {
145147
Map,
146148
RangeMap,
149+
RangeCount,
150+
RangeSumMap,
147151
FindIndex,
148152
FindIndices,
149153
Filter,
@@ -156,13 +160,24 @@ impl QuantifierHelperType {
156160
match self {
157161
QuantifierHelperType::Map => "map",
158162
QuantifierHelperType::RangeMap => "range_map",
163+
QuantifierHelperType::RangeCount => "range_count",
164+
QuantifierHelperType::RangeSumMap => "range_sum_map",
159165
QuantifierHelperType::FindIndex => "find_index",
160166
QuantifierHelperType::FindIndices => "find_indices",
161167
QuantifierHelperType::Filter => "filter",
162168
QuantifierHelperType::Count => "count",
163169
QuantifierHelperType::SumMap => "sum_map",
164170
}
165171
}
172+
173+
pub fn range_based(&self) -> bool {
174+
matches!(
175+
self,
176+
QuantifierHelperType::RangeMap
177+
| QuantifierHelperType::RangeCount
178+
| QuantifierHelperType::RangeSumMap
179+
)
180+
}
166181
}
167182

168183
impl QuantifierType {
@@ -189,6 +204,8 @@ impl QuantifierType {
189204
QuantifierType::SumMap => "sum_map",
190205
QuantifierType::SumMapRange => "sum_map_range",
191206
QuantifierType::RangeMap => "range_map",
207+
QuantifierType::RangeCount => "range_count",
208+
QuantifierType::RangeSumMap => "range_sum_map",
192209
}
193210
}
194211

@@ -200,6 +217,8 @@ impl QuantifierType {
200217
*self != QuantifierType::Forall
201218
&& *self != QuantifierType::Exists
202219
&& *self != QuantifierType::RangeMap
220+
&& *self != QuantifierType::RangeCount
221+
&& *self != QuantifierType::RangeSumMap
203222
}
204223

205224
pub fn range_based(&self) -> bool {
@@ -215,6 +234,8 @@ impl QuantifierType {
215234
| QuantifierType::AllRange
216235
| QuantifierType::SumMapRange
217236
| QuantifierType::RangeMap
237+
| QuantifierType::RangeCount
238+
| QuantifierType::RangeSumMap
218239
)
219240
}
220241

@@ -228,20 +249,6 @@ impl QuantifierType {
228249
)
229250
}
230251

231-
pub fn requires_sum(&self) -> bool {
232-
matches!(
233-
self,
234-
QuantifierType::SumMap
235-
| QuantifierType::SumMapRange
236-
| QuantifierType::Count
237-
| QuantifierType::CountRange
238-
)
239-
}
240-
241-
pub fn requires_filter_indices(&self) -> bool {
242-
matches!(self, QuantifierType::Filter | QuantifierType::FilterRange)
243-
}
244-
245252
pub fn into_quantifier_helper_type(&self) -> Option<QuantifierHelperType> {
246253
match self {
247254
QuantifierType::Map | QuantifierType::MapRange => Some(QuantifierHelperType::Map),
@@ -260,6 +267,8 @@ impl QuantifierType {
260267
Some(QuantifierHelperType::Filter)
261268
}
262269
QuantifierType::RangeMap => Some(QuantifierHelperType::RangeMap),
270+
QuantifierType::RangeCount => Some(QuantifierHelperType::RangeCount),
271+
QuantifierType::RangeSumMap => Some(QuantifierHelperType::RangeSumMap),
263272
_ => None,
264273
}
265274
}

‎crates/move-stackless-bytecode/src/verification_analysis.rs‎

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
//! each function as well as collect information on how these invariants should be handled (i.e.,
88
//! checked after bytecode, checked at function exit, or deferred to caller).
99
10-
use crate::quantifier_iterator_analysis::QuantifierPattern;
1110
use crate::{
1211
function_target::{FunctionData, FunctionTarget},
1312
function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
@@ -583,14 +582,6 @@ impl VerificationAnalysisProcessor {
583582
}
584583
}
585584
Self::mark_inlined(&callee_env, targets);
586-
if let Some(qt) = QuantifierPattern::type_from_qid(callee, env) {
587-
if qt.requires_sum() {
588-
if let Some(qid) = env.prover_vec_sum_qid_opt() {
589-
let sum_fun_env = env.get_function(qid);
590-
Self::mark_inlined(&sum_fun_env, targets);
591-
}
592-
}
593-
}
594585
}
595586
}
596587

0 commit comments

Comments
 (0)