Skip to content

Commit 27a25ed

Browse files
andrii-a8candrii-a8c
authored
Merge branch 'main' into new-sui-version
2 parents d93b42f + 660e1c8 commit 27a25ed

25 files changed

Lines changed: 734 additions & 46 deletions

‎Cargo.lock‎

Lines changed: 12 additions & 12 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";
@@ -1873,6 +1882,13 @@ impl GlobalEnv {
18731882
)
18741883
}
18751884

1885+
pub fn prover_begin_map_range_lambda_qid(&self) -> QualifiedId<FunId> {
1886+
self.get_fun_qid(
1887+
Self::PROVER_VECTOR_MODULE_NAME,
1888+
Self::PROVER_BEGIN_MAP_RANGE_LAMBDA,
1889+
)
1890+
}
1891+
18761892
pub fn prover_end_map_lambda_qid(&self) -> QualifiedId<FunId> {
18771893
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_MAP_LAMBDA)
18781894
}
@@ -1884,6 +1900,13 @@ impl GlobalEnv {
18841900
)
18851901
}
18861902

1903+
pub fn prover_begin_filter_range_lambda_qid(&self) -> QualifiedId<FunId> {
1904+
self.get_fun_qid(
1905+
Self::PROVER_VECTOR_MODULE_NAME,
1906+
Self::PROVER_BEGIN_FILTER_RANGE_LAMBDA,
1907+
)
1908+
}
1909+
18871910
pub fn prover_end_filter_lambda_qid(&self) -> QualifiedId<FunId> {
18881911
self.get_fun_qid(
18891912
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1898,6 +1921,13 @@ impl GlobalEnv {
18981921
)
18991922
}
19001923

1924+
pub fn prover_begin_find_range_lambda_qid(&self) -> QualifiedId<FunId> {
1925+
self.get_fun_qid(
1926+
Self::PROVER_VECTOR_MODULE_NAME,
1927+
Self::PROVER_BEGIN_FIND_RANGE_LAMBDA,
1928+
)
1929+
}
1930+
19011931
pub fn prover_end_find_lambda_qid(&self) -> QualifiedId<FunId> {
19021932
self.get_fun_qid(
19031933
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1912,6 +1942,13 @@ impl GlobalEnv {
19121942
)
19131943
}
19141944

1945+
pub fn prover_begin_find_index_range_lambda_qid(&self) -> QualifiedId<FunId> {
1946+
self.get_fun_qid(
1947+
Self::PROVER_VECTOR_MODULE_NAME,
1948+
Self::PROVER_BEGIN_FIND_INDEX_RANGE_LAMBDA,
1949+
)
1950+
}
1951+
19151952
pub fn prover_end_find_index_lambda_qid(&self) -> QualifiedId<FunId> {
19161953
self.get_fun_qid(
19171954
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1926,6 +1963,13 @@ impl GlobalEnv {
19261963
)
19271964
}
19281965

1966+
pub fn prover_begin_find_indices_range_lambda_qid(&self) -> QualifiedId<FunId> {
1967+
self.get_fun_qid(
1968+
Self::PROVER_VECTOR_MODULE_NAME,
1969+
Self::PROVER_BEGIN_FIND_INDICES_RANGE_LAMBDA,
1970+
)
1971+
}
1972+
19291973
pub fn prover_end_find_indices_lambda_qid(&self) -> QualifiedId<FunId> {
19301974
self.get_fun_qid(
19311975
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1940,6 +1984,13 @@ impl GlobalEnv {
19401984
)
19411985
}
19421986

1987+
pub fn prover_begin_count_range_lambda_qid(&self) -> QualifiedId<FunId> {
1988+
self.get_fun_qid(
1989+
Self::PROVER_VECTOR_MODULE_NAME,
1990+
Self::PROVER_BEGIN_COUNT_RANGE_LAMBDA,
1991+
)
1992+
}
1993+
19431994
pub fn prover_end_count_lambda_qid(&self) -> QualifiedId<FunId> {
19441995
self.get_fun_qid(
19451996
Self::PROVER_VECTOR_MODULE_NAME,
@@ -1954,6 +2005,13 @@ impl GlobalEnv {
19542005
)
19552006
}
19562007

2008+
pub fn prover_begin_any_range_lambda_qid(&self) -> QualifiedId<FunId> {
2009+
self.get_fun_qid(
2010+
Self::PROVER_VECTOR_MODULE_NAME,
2011+
Self::PROVER_BEGIN_ANY_RANGE_LAMBDA,
2012+
)
2013+
}
2014+
19572015
pub fn prover_end_any_lambda_qid(&self) -> QualifiedId<FunId> {
19582016
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_ANY_LAMBDA)
19592017
}
@@ -1965,6 +2023,13 @@ impl GlobalEnv {
19652023
)
19662024
}
19672025

2026+
pub fn prover_begin_all_range_lambda_qid(&self) -> QualifiedId<FunId> {
2027+
self.get_fun_qid(
2028+
Self::PROVER_VECTOR_MODULE_NAME,
2029+
Self::PROVER_BEGIN_ALL_RANGE_LAMBDA,
2030+
)
2031+
}
2032+
19682033
pub fn prover_end_all_lambda_qid(&self) -> QualifiedId<FunId> {
19692034
self.get_fun_qid(Self::PROVER_VECTOR_MODULE_NAME, Self::PROVER_END_ALL_LAMBDA)
19702035
}
@@ -1976,6 +2041,13 @@ impl GlobalEnv {
19762041
)
19772042
}
19782043

2044+
pub fn prover_begin_sum_map_range_lambda_qid(&self) -> QualifiedId<FunId> {
2045+
self.get_fun_qid(
2046+
Self::PROVER_VECTOR_MODULE_NAME,
2047+
Self::PROVER_BEGIN_SUM_MAP_RANGE_LAMBDA,
2048+
)
2049+
}
2050+
19792051
pub fn prover_end_sum_map_lambda_qid(&self) -> QualifiedId<FunId> {
19802052
self.get_fun_qid(
19812053
Self::PROVER_VECTOR_MODULE_NAME,
@@ -3343,22 +3415,31 @@ impl GlobalEnv {
33433415
self.prover_begin_exists_lambda_qid(),
33443416
self.prover_end_exists_lambda_qid(),
33453417
self.prover_begin_map_lambda_qid(),
3418+
self.prover_begin_map_range_lambda_qid(),
33463419
self.prover_end_map_lambda_qid(),
33473420
self.prover_begin_filter_lambda_qid(),
3421+
self.prover_begin_filter_range_lambda_qid(),
33483422
self.prover_end_filter_lambda_qid(),
33493423
self.prover_begin_find_lambda_qid(),
3424+
self.prover_begin_find_range_lambda_qid(),
33503425
self.prover_end_find_lambda_qid(),
33513426
self.prover_begin_find_index_lambda_qid(),
3427+
self.prover_begin_find_index_range_lambda_qid(),
33523428
self.prover_end_find_index_lambda_qid(),
33533429
self.prover_begin_find_indices_lambda_qid(),
3430+
self.prover_begin_find_indices_range_lambda_qid(),
33543431
self.prover_end_find_indices_lambda_qid(),
33553432
self.prover_begin_count_lambda_qid(),
3433+
self.prover_begin_count_range_lambda_qid(),
33563434
self.prover_end_count_lambda_qid(),
33573435
self.prover_begin_any_lambda_qid(),
3436+
self.prover_begin_any_range_lambda_qid(),
33583437
self.prover_end_any_lambda_qid(),
33593438
self.prover_begin_all_lambda_qid(),
3439+
self.prover_begin_all_range_lambda_qid(),
33603440
self.prover_end_all_lambda_qid(),
33613441
self.prover_begin_sum_map_lambda_qid(),
3442+
self.prover_begin_sum_map_range_lambda_qid(),
33623443
self.prover_end_sum_map_lambda_qid(),
33633444
self.prover_vec_sum_qid(),
33643445
self.prover_vec_slice_qid(),
@@ -3566,22 +3647,31 @@ impl GlobalEnv {
35663647
self.prover_begin_exists_lambda_qid(),
35673648
self.prover_end_exists_lambda_qid(),
35683649
self.prover_begin_map_lambda_qid(),
3650+
self.prover_begin_map_range_lambda_qid(),
35693651
self.prover_end_map_lambda_qid(),
35703652
self.prover_begin_filter_lambda_qid(),
3653+
self.prover_begin_filter_range_lambda_qid(),
35713654
self.prover_end_filter_lambda_qid(),
35723655
self.prover_begin_find_lambda_qid(),
3656+
self.prover_begin_find_range_lambda_qid(),
35733657
self.prover_end_find_lambda_qid(),
35743658
self.prover_begin_find_index_lambda_qid(),
3659+
self.prover_begin_find_index_range_lambda_qid(),
35753660
self.prover_end_find_index_lambda_qid(),
35763661
self.prover_begin_find_indices_lambda_qid(),
3662+
self.prover_begin_find_indices_range_lambda_qid(),
35773663
self.prover_end_find_indices_lambda_qid(),
35783664
self.prover_begin_count_lambda_qid(),
3665+
self.prover_begin_count_range_lambda_qid(),
35793666
self.prover_end_count_lambda_qid(),
35803667
self.prover_begin_any_lambda_qid(),
3668+
self.prover_begin_any_range_lambda_qid(),
35813669
self.prover_end_any_lambda_qid(),
35823670
self.prover_begin_all_lambda_qid(),
3671+
self.prover_begin_all_range_lambda_qid(),
35833672
self.prover_end_all_lambda_qid(),
35843673
self.prover_begin_sum_map_lambda_qid(),
3674+
self.prover_begin_sum_map_range_lambda_qid(),
35853675
self.prover_end_sum_map_lambda_qid(),
35863676
self.prover_vec_sum_qid(),
35873677
self.prover_vec_slice_qid(),

0 commit comments

Comments
 (0)