Skip to content

Commit 660e1c8

Browse files
andrii-a8candrii-a8c
authored
Range quantifiers (#345)
* wip: range quantifiers * fix: natives list * fmt * feat: better temp var handling and more tests * feat: finalized quantifiers * feat: additional restiction for map range
1 parent 271e0a8 commit 660e1c8

25 files changed

+743
-55
lines changed

‎Cargo.lock‎

Lines changed: 21 additions & 21 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

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

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1567,22 +1567,31 @@ impl GlobalEnv {
15671567
const PROVER_BEGIN_EXISTS_LAMBDA: &'static str = "begin_exists_lambda";
15681568
const PROVER_END_EXISTS_LAMBDA: &'static str = "end_exists_lambda";
15691569
const PROVER_BEGIN_MAP_LAMBDA: &'static str = "begin_map_lambda";
1570+
const PROVER_BEGIN_MAP_RANGE_LAMBDA: &'static str = "begin_map_range_lambda";
15701571
const PROVER_END_MAP_LAMBDA: &'static str = "end_map_lambda";
15711572
const PROVER_BEGIN_FILTER_LAMBDA: &'static str = "begin_filter_lambda";
1573+
const PROVER_BEGIN_FILTER_RANGE_LAMBDA: &'static str = "begin_filter_range_lambda";
15721574
const PROVER_END_FILTER_LAMBDA: &'static str = "end_filter_lambda";
15731575
const PROVER_BEGIN_FIND_LAMBDA: &'static str = "begin_find_lambda";
1576+
const PROVER_BEGIN_FIND_RANGE_LAMBDA: &'static str = "begin_find_range_lambda";
15741577
const PROVER_END_FIND_LAMBDA: &'static str = "end_find_lambda";
15751578
const PROVER_BEGIN_FIND_INDEX_LAMBDA: &'static str = "begin_find_index_lambda";
1579+
const PROVER_BEGIN_FIND_INDEX_RANGE_LAMBDA: &'static str = "begin_find_index_range_lambda";
15761580
const PROVER_END_FIND_INDEX_LAMBDA: &'static str = "end_find_index_lambda";
15771581
const PROVER_BEGIN_FIND_INDICES_LAMBDA: &'static str = "begin_find_indices_lambda";
1582+
const PROVER_BEGIN_FIND_INDICES_RANGE_LAMBDA: &'static str = "begin_find_indices_range_lambda";
15781583
const PROVER_END_FIND_INDICES_LAMBDA: &'static str = "end_find_indices_lambda";
15791584
const PROVER_BEGIN_COUNT_LAMBDA: &'static str = "begin_count_lambda";
1585+
const PROVER_BEGIN_COUNT_RANGE_LAMBDA: &'static str = "begin_count_range_lambda";
15801586
const PROVER_END_COUNT_LAMBDA: &'static str = "end_count_lambda";
15811587
const PROVER_BEGIN_ANY_LAMBDA: &'static str = "begin_any_lambda";
1588+
const PROVER_BEGIN_ANY_RANGE_LAMBDA: &'static str = "begin_any_range_lambda";
15821589
const PROVER_END_ANY_LAMBDA: &'static str = "end_any_lambda";
15831590
const PROVER_BEGIN_ALL_LAMBDA: &'static str = "begin_all_lambda";
1591+
const PROVER_BEGIN_ALL_RANGE_LAMBDA: &'static str = "begin_all_range_lambda";
15841592
const PROVER_END_ALL_LAMBDA: &'static str = "end_all_lambda";
15851593
const PROVER_BEGIN_SUM_MAP_LAMBDA: &'static str = "begin_sum_map_lambda";
1594+
const PROVER_BEGIN_SUM_MAP_RANGE_LAMBDA: &'static str = "begin_sum_map_range_lambda";
15861595
const PROVER_END_SUM_MAP_LAMBDA: &'static str = "end_sum_map_lambda";
15871596
const PROVER_VEC_SUM: &'static str = "sum";
15881597
const PROVER_VEC_SLICE: &'static str = "slice";
@@ -1869,6 +1878,13 @@ impl GlobalEnv {
18691878
)
18701879
}
18711880

1881+
pub fn prover_begin_map_range_lambda_qid(&self) -> QualifiedId<FunId> {
1882+
self.get_fun_qid(
1883+
Self::PROVER_VECTOR_MODULE_NAME,
1884+
Self::PROVER_BEGIN_MAP_RANGE_LAMBDA,
1885+
)
1886+
}
1887+
18721888
pub fn prover_end_map_lambda_qid(&self) -> QualifiedId<FunId> {
18731889
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_MAP_LAMBDA)
18741890
}
@@ -1880,6 +1896,13 @@ impl GlobalEnv {
18801896
)
18811897
}
18821898

1899+
pub fn prover_begin_filter_range_lambda_qid(&self) -> QualifiedId<FunId> {
1900+
self.get_fun_qid(
1901+
Self::PROVER_VECTOR_MODULE_NAME,
1902+
Self::PROVER_BEGIN_FILTER_RANGE_LAMBDA,
1903+
)
1904+
}
1905+
18831906
pub fn prover_end_filter_lambda_qid(&self) -> QualifiedId<FunId> {
18841907
self.get_fun_qid(
18851908
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1894,6 +1917,13 @@ impl GlobalEnv {
18941917
)
18951918
}
18961919

1920+
pub fn prover_begin_find_range_lambda_qid(&self) -> QualifiedId<FunId> {
1921+
self.get_fun_qid(
1922+
Self::PROVER_VECTOR_MODULE_NAME,
1923+
Self::PROVER_BEGIN_FIND_RANGE_LAMBDA,
1924+
)
1925+
}
1926+
18971927
pub fn prover_end_find_lambda_qid(&self) -> QualifiedId<FunId> {
18981928
self.get_fun_qid(
18991929
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1908,6 +1938,13 @@ impl GlobalEnv {
19081938
)
19091939
}
19101940

1941+
pub fn prover_begin_find_index_range_lambda_qid(&self) -> QualifiedId<FunId> {
1942+
self.get_fun_qid(
1943+
Self::PROVER_VECTOR_MODULE_NAME,
1944+
Self::PROVER_BEGIN_FIND_INDEX_RANGE_LAMBDA,
1945+
)
1946+
}
1947+
19111948
pub fn prover_end_find_index_lambda_qid(&self) -> QualifiedId<FunId> {
19121949
self.get_fun_qid(
19131950
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1922,6 +1959,13 @@ impl GlobalEnv {
19221959
)
19231960
}
19241961

1962+
pub fn prover_begin_find_indices_range_lambda_qid(&self) -> QualifiedId<FunId> {
1963+
self.get_fun_qid(
1964+
Self::PROVER_VECTOR_MODULE_NAME,
1965+
Self::PROVER_BEGIN_FIND_INDICES_RANGE_LAMBDA,
1966+
)
1967+
}
1968+
19251969
pub fn prover_end_find_indices_lambda_qid(&self) -> QualifiedId<FunId> {
19261970
self.get_fun_qid(
19271971
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1936,6 +1980,13 @@ impl GlobalEnv {
19361980
)
19371981
}
19381982

1983+
pub fn prover_begin_count_range_lambda_qid(&self) -> QualifiedId<FunId> {
1984+
self.get_fun_qid(
1985+
Self::PROVER_VECTOR_MODULE_NAME,
1986+
Self::PROVER_BEGIN_COUNT_RANGE_LAMBDA,
1987+
)
1988+
}
1989+
19391990
pub fn prover_end_count_lambda_qid(&self) -> QualifiedId<FunId> {
19401991
self.get_fun_qid(
19411992
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1950,6 +2001,13 @@ impl GlobalEnv {
19502001
)
19512002
}
19522003

2004+
pub fn prover_begin_any_range_lambda_qid(&self) -> QualifiedId<FunId> {
2005+
self.get_fun_qid(
2006+
Self::PROVER_VECTOR_MODULE_NAME,
2007+
Self::PROVER_BEGIN_ANY_RANGE_LAMBDA,
2008+
)
2009+
}
2010+
19532011
pub fn prover_end_any_lambda_qid(&self) -> QualifiedId<FunId> {
19542012
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_ANY_LAMBDA)
19552013
}
@@ -1961,6 +2019,13 @@ impl GlobalEnv {
19612019
)
19622020
}
19632021

2022+
pub fn prover_begin_all_range_lambda_qid(&self) -> QualifiedId<FunId> {
2023+
self.get_fun_qid(
2024+
Self::PROVER_VECTOR_MODULE_NAME,
2025+
Self::PROVER_BEGIN_ALL_RANGE_LAMBDA,
2026+
)
2027+
}
2028+
19642029
pub fn prover_end_all_lambda_qid(&self) -> QualifiedId<FunId> {
19652030
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_ALL_LAMBDA)
19662031
}
@@ -1972,6 +2037,13 @@ impl GlobalEnv {
19722037
)
19732038
}
19742039

2040+
pub fn prover_begin_sum_map_range_lambda_qid(&self) -> QualifiedId<FunId> {
2041+
self.get_fun_qid(
2042+
Self::PROVER_VECTOR_MODULE_NAME,
2043+
Self::PROVER_BEGIN_SUM_MAP_RANGE_LAMBDA,
2044+
)
2045+
}
2046+
19752047
pub fn prover_end_sum_map_lambda_qid(&self) -> QualifiedId<FunId> {
19762048
self.get_fun_qid(
19772049
Self::PROVER_VECTOR_MODULE_NAME,
@@ -3314,22 +3386,31 @@ impl GlobalEnv {
33143386
self.prover_begin_exists_lambda_qid(),
33153387
self.prover_end_exists_lambda_qid(),
33163388
self.prover_begin_map_lambda_qid(),
3389+
self.prover_begin_map_range_lambda_qid(),
33173390
self.prover_end_map_lambda_qid(),
33183391
self.prover_begin_filter_lambda_qid(),
3392+
self.prover_begin_filter_range_lambda_qid(),
33193393
self.prover_end_filter_lambda_qid(),
33203394
self.prover_begin_find_lambda_qid(),
3395+
self.prover_begin_find_range_lambda_qid(),
33213396
self.prover_end_find_lambda_qid(),
33223397
self.prover_begin_find_index_lambda_qid(),
3398+
self.prover_begin_find_index_range_lambda_qid(),
33233399
self.prover_end_find_index_lambda_qid(),
33243400
self.prover_begin_find_indices_lambda_qid(),
3401+
self.prover_begin_find_indices_range_lambda_qid(),
33253402
self.prover_end_find_indices_lambda_qid(),
33263403
self.prover_begin_count_lambda_qid(),
3404+
self.prover_begin_count_range_lambda_qid(),
33273405
self.prover_end_count_lambda_qid(),
33283406
self.prover_begin_any_lambda_qid(),
3407+
self.prover_begin_any_range_lambda_qid(),
33293408
self.prover_end_any_lambda_qid(),
33303409
self.prover_begin_all_lambda_qid(),
3410+
self.prover_begin_all_range_lambda_qid(),
33313411
self.prover_end_all_lambda_qid(),
33323412
self.prover_begin_sum_map_lambda_qid(),
3413+
self.prover_begin_sum_map_range_lambda_qid(),
33333414
self.prover_end_sum_map_lambda_qid(),
33343415
self.prover_vec_sum_qid(),
33353416
self.prover_vec_slice_qid(),
@@ -3537,22 +3618,31 @@ impl GlobalEnv {
35373618
self.prover_begin_exists_lambda_qid(),
35383619
self.prover_end_exists_lambda_qid(),
35393620
self.prover_begin_map_lambda_qid(),
3621+
self.prover_begin_map_range_lambda_qid(),
35403622
self.prover_end_map_lambda_qid(),
35413623
self.prover_begin_filter_lambda_qid(),
3624+
self.prover_begin_filter_range_lambda_qid(),
35423625
self.prover_end_filter_lambda_qid(),
35433626
self.prover_begin_find_lambda_qid(),
3627+
self.prover_begin_find_range_lambda_qid(),
35443628
self.prover_end_find_lambda_qid(),
35453629
self.prover_begin_find_index_lambda_qid(),
3630+
self.prover_begin_find_index_range_lambda_qid(),
35463631
self.prover_end_find_index_lambda_qid(),
35473632
self.prover_begin_find_indices_lambda_qid(),
3633+
self.prover_begin_find_indices_range_lambda_qid(),
35483634
self.prover_end_find_indices_lambda_qid(),
35493635
self.prover_begin_count_lambda_qid(),
3636+
self.prover_begin_count_range_lambda_qid(),
35503637
self.prover_end_count_lambda_qid(),
35513638
self.prover_begin_any_lambda_qid(),
3639+
self.prover_begin_any_range_lambda_qid(),
35523640
self.prover_end_any_lambda_qid(),
35533641
self.prover_begin_all_lambda_qid(),
3642+
self.prover_begin_all_range_lambda_qid(),
35543643
self.prover_end_all_lambda_qid(),
35553644
self.prover_begin_sum_map_lambda_qid(),
3645+
self.prover_begin_sum_map_range_lambda_qid(),
35563646
self.prover_end_sum_map_lambda_qid(),
35573647
self.prover_vec_sum_qid(),
35583648
self.prover_vec_slice_qid(),

0 commit comments

Comments
 (0)