Skip to content

Commit 32552a1

Browse files
andrii-a8candrii-a8c
authored
Merge branch 'main' into 254-add-a-log-file-for-each-spec
2 parents b18e9e6 + 9487f94 commit 32552a1

File tree

13 files changed

+436
-129
lines changed

13 files changed

+436
-129
lines changed

‎.github/workflows/sui-prover.yml‎

Lines changed: 60 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,9 @@ jobs:
110110
- name: Setup
111111
run: |
112112
mkdir -p ~/.local/bin
113+
114+
mkdir -p "$HOME/.asymptotic"
115+
echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"
113116
114117
cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
115118
ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie
@@ -130,13 +133,13 @@ jobs:
130133
git clone https://github.com/asymptotic-code/sui-kit.git sui-kit
131134
132135
cd sui-kit/examples/amm
133-
sui-prover --ci
136+
sui-prover --ci --cloud
134137
135138
cd ../showcase
136-
sui-prover --ci
139+
sui-prover --ci --cloud
137140
138141
cd ../guide
139-
sui-prover --ci
142+
sui-prover --ci --cloud
140143
141144
internal-tests:
142145
# check if prover needed
@@ -211,6 +214,9 @@ jobs:
211214
run: |
212215
mkdir -p ~/.local/bin
213216
217+
mkdir -p "$HOME/.asymptotic"
218+
echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"
219+
214220
cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
215221
ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie
216222
@@ -229,10 +235,10 @@ jobs:
229235
git clone https://github.com/asymptotic-code/integer-library int-lib
230236
231237
cd int-lib/specs
232-
sui-prover --ci
238+
sui-prover --ci --cloud
233239
234240
cd ../specs-bv
235-
sui-prover --no-bv-int-encoding --ci
241+
sui-prover --no-bv-int-encoding --ci --cloud
236242
237243
token-distribution-specs:
238244
needs: build-prover
@@ -253,6 +259,9 @@ jobs:
253259
run: |
254260
mkdir -p ~/.local/bin
255261
262+
mkdir -p "$HOME/.asymptotic"
263+
echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"
264+
256265
cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
257266
ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie
258267
@@ -270,7 +279,7 @@ jobs:
270279
run: |
271280
git clone --depth 1 -b fix/prover_specs https://github.com/asymptotic-code/sui-smart-contracts.git sui-smart-contracts
272281
cd sui-smart-contracts/token-distribution-specs
273-
sui-prover --ci
282+
sui-prover --ci --cloud
274283
275284
scallop-bpl-generation:
276285
needs: build-prover
@@ -361,3 +370,48 @@ jobs:
361370
run: |
362371
cd cetus/cetus_clmm_specs
363372
sui-prover -g --ci
373+
374+
ika-bpl-generation:
375+
needs: build-prover
376+
runs-on: macos-latest
377+
378+
concurrency:
379+
group: ika-bpl-generation-${{ github.head_ref || github.ref_name }}
380+
cancel-in-progress: true
381+
382+
steps:
383+
- name: Download
384+
uses: actions/download-artifact@v4
385+
with:
386+
name: ${{ needs.build-prover.outputs.artifact-name }}
387+
path: ~/prover-bundle
388+
389+
- name: Setup
390+
run: |
391+
mkdir -p ~/.local/bin
392+
393+
cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
394+
ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie
395+
396+
chmod +x ~/.local/bin/boogie
397+
chmod +x ~/.local/bin/sui-prover
398+
chmod +x ~/prover-bundle/z3/bin/z3
399+
400+
echo "$HOME/.local/bin" >> $GITHUB_PATH
401+
echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH
402+
403+
echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
404+
echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV
405+
406+
- name: Clone ika repo
407+
uses: actions/checkout@v4
408+
with:
409+
repository: asymptotic-code/ika-fv
410+
ref: specs
411+
token: ${{ secrets.PAT_TOKEN }}
412+
path: ika
413+
414+
- name: Run
415+
run: |
416+
cd ika/contracts/specs
417+
sui-prover -g --ci

‎Cargo.lock‎

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

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

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -290,8 +290,11 @@ impl<'env> BoogieTranslator<'env> {
290290
parent: self,
291291
struct_env,
292292
type_inst: type_inst.as_slice(),
293-
is_opaque: !mono_info
294-
.is_used_datatype(self.env, &struct_env.get_qualified_id()),
293+
is_opaque: !mono_info.is_used_datatype(
294+
self.env,
295+
self.targets,
296+
&struct_env.get_qualified_id(),
297+
),
295298
}
296299
.translate();
297300
}
@@ -311,8 +314,11 @@ impl<'env> BoogieTranslator<'env> {
311314
parent: self,
312315
enum_env,
313316
type_inst: type_inst.as_slice(),
314-
is_opaque: !mono_info
315-
.is_used_datatype(self.env, &enum_env.get_qualified_id()),
317+
is_opaque: !mono_info.is_used_datatype(
318+
self.env,
319+
self.targets,
320+
&enum_env.get_qualified_id(),
321+
),
316322
}
317323
.translate();
318324
}
@@ -1043,7 +1049,7 @@ impl<'env> StructTranslator<'env> {
10431049
let struct_env = self.struct_env;
10441050
let env = struct_env.module_env.env;
10451051

1046-
if struct_env.is_native() || struct_env.is_intrinsic() {
1052+
if struct_env.is_native() || (struct_env.is_intrinsic() && !self.is_opaque) {
10471053
return;
10481054
}
10491055

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

Lines changed: 30 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ use move_model::{
2020
};
2121
use move_stackless_bytecode::{
2222
dynamic_field_analysis::{self, NameValueInfo},
23-
function_target_pipeline::FunctionVariant,
23+
function_target_pipeline::{FunctionTargetsHolder, FunctionVariant},
2424
mono_analysis::{self, MonoInfo},
2525
};
2626

@@ -129,6 +129,7 @@ fn bv_helper() -> Vec<BvInfo> {
129129
/// Adds the prelude to the generated output.
130130
pub fn add_prelude(
131131
env: &GlobalEnv,
132+
targets: &FunctionTargetsHolder,
132133
options: &BoogieOptions,
133134
writer: &CodeWriter,
134135
) -> anyhow::Result<()> {
@@ -186,21 +187,25 @@ pub fn add_prelude(
186187
.collect_vec();
187188
let mut table_instances = vec![];
188189
if let Some(table_qid) = env.table_qid() {
189-
table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false));
190+
if mono_info.is_used_datatype(env, targets, &table_qid) {
191+
table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false));
192+
}
190193
}
191194
if let Some(object_table_qid) = env.object_table_qid() {
192-
table_instances.push(TableImpl::object_table(
193-
env,
194-
options,
195-
&mono_info,
196-
object_table_qid,
197-
false,
198-
));
195+
if mono_info.is_used_datatype(env, targets, &object_table_qid) {
196+
table_instances.push(TableImpl::object_table(
197+
env,
198+
options,
199+
&mono_info,
200+
object_table_qid,
201+
false,
202+
));
203+
}
199204
}
200205
let mut dynamic_field_instances = vec![];
201206
for info in dynamic_field_analysis::get_env_info(env).dynamic_fields() {
202207
let (struct_qid, type_inst) = info.0.get_datatype().unwrap();
203-
if mono_info.is_used_datatype(env, &struct_qid)
208+
if mono_info.is_used_datatype(env, targets, &struct_qid)
204209
&& mono_info
205210
.structs
206211
.get(&struct_qid)
@@ -249,17 +254,18 @@ pub fn add_prelude(
249254
let option_env = option_module_env
250255
.find_struct(env.symbol_pool().make("Option"))
251256
.unwrap();
252-
let option_instances = if mono_info.is_used_datatype(env, &option_env.get_qualified_id()) {
253-
mono_info
254-
.structs
255-
.get(&option_env.get_qualified_id())
256-
.unwrap_or(&BTreeSet::new())
257-
.iter()
258-
.map(|tys| TypeInfo::new(env, options, &tys[0], false))
259-
.collect_vec()
260-
} else {
261-
vec![]
262-
};
257+
let option_instances =
258+
if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id()) {
259+
mono_info
260+
.structs
261+
.get(&option_env.get_qualified_id())
262+
.unwrap_or(&BTreeSet::new())
263+
.iter()
264+
.map(|tys| TypeInfo::new(env, options, &tys[0], false))
265+
.collect_vec()
266+
} else {
267+
vec![]
268+
};
263269
context.insert("option_instances", &option_instances);
264270
}
265271

@@ -268,7 +274,7 @@ pub fn add_prelude(
268274
.find_struct(env.symbol_pool().make("VecSet"))
269275
.unwrap();
270276
let vec_set_instances =
271-
if mono_info.is_used_datatype(env, &vec_set_struct_env.get_qualified_id()) {
277+
if mono_info.is_used_datatype(env, targets, &vec_set_struct_env.get_qualified_id()) {
272278
mono_info
273279
.structs
274280
.get(&vec_set_struct_env.get_qualified_id())
@@ -287,7 +293,7 @@ pub fn add_prelude(
287293
.find_struct(env.symbol_pool().make("VecMap"))
288294
.unwrap();
289295
let vec_map_instances =
290-
if mono_info.is_used_datatype(env, &vec_map_struct_env.get_qualified_id()) {
296+
if mono_info.is_used_datatype(env, targets, &vec_map_struct_env.get_qualified_id()) {
291297
mono_info
292298
.structs
293299
.get(&vec_map_struct_env.get_qualified_id())
@@ -312,7 +318,7 @@ pub fn add_prelude(
312318
.find_struct(env.symbol_pool().make("TableVec"))
313319
.unwrap();
314320
let table_vec_instances =
315-
if mono_info.is_used_datatype(env, &table_vec_env.get_qualified_id()) {
321+
if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id()) {
316322
mono_info
317323
.structs
318324
.get(&table_vec_env.get_qualified_id())

‎crates/move-prover-boogie-backend/src/generator.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -540,7 +540,7 @@ pub fn generate_boogie(
540540
) -> anyhow::Result<(CodeWriter, BiBTreeMap<Type, String>)> {
541541
let writer = CodeWriter::new(env.internal_loc());
542542
let types = RefCell::new(BiBTreeMap::new());
543-
add_prelude(env, &options.backend, &writer)?;
543+
add_prelude(env, targets, &options.backend, &writer)?;
544544
let mut translator = BoogieTranslator::new(env, &options.backend, targets, &writer, &types);
545545
translator.translate();
546546
Ok((writer, types.into_inner()))

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

Lines changed: 47 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use itertools::Itertools;
1010

1111
use move_binary_format::file_format::CodeOffset;
1212
use move_model::{
13-
model::{FunctionEnv, GlobalEnv, QualifiedInstId, RefType},
13+
model::{DatatypeId, FunctionEnv, GlobalEnv, QualifiedId, QualifiedInstId, RefType},
1414
ty::Type,
1515
well_known::{BORROW_CHILD_OBJECT_MUT, VECTOR_BORROW_MUT},
1616
};
@@ -25,6 +25,7 @@ use crate::{
2525
spec_global_variable_analysis,
2626
stackless_bytecode::{AssignKind, BorrowEdge, BorrowNode, Bytecode, IndexEdgeKind, Operation},
2727
stackless_control_flow_graph::StacklessControlFlowGraph,
28+
verification_analysis::VerificationInfo,
2829
};
2930

3031
#[derive(Debug, Clone, Eq, Ord, PartialEq, PartialOrd, Default)]
@@ -50,6 +51,11 @@ pub struct WriteBackAction {
5051
pub edge: BorrowEdge,
5152
}
5253

54+
#[derive(Debug, Clone, Eq, Ord, PartialEq, PartialOrd)]
55+
pub struct WriteBackDatatypeInfo {
56+
pub datatypes: Vec<QualifiedId<DatatypeId>>,
57+
}
58+
5359
impl BorrowInfo {
5460
/// Gets the children of this node.
5561
fn get_children(&self, node: &BorrowNode) -> Vec<&BorrowNode> {
@@ -453,12 +459,51 @@ impl FunctionTargetProcessor for BorrowAnalysisProcessor {
453459
data
454460
}
455461

456-
fn finalize(&self, _env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
462+
fn finalize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
457463
for (fun_id, variant) in targets.get_funs_and_variants().collect_vec() {
458464
if let Some(data) = targets.get_data_mut(&fun_id, &variant) {
459465
data.annotations.remove::<LiveVarAnnotation>();
460466
}
461467
}
468+
469+
// collect all writeback datatypes from all verified or inlined functions
470+
let writeback_datatype_info = WriteBackDatatypeInfo {
471+
datatypes: targets
472+
.get_funs_and_variants()
473+
.flat_map(|(fun_id, variant)| targets.get_data(&fun_id, &variant))
474+
.filter(|data| {
475+
let verification_info = data.annotations.get::<VerificationInfo>().unwrap();
476+
verification_info.verified || verification_info.inlined
477+
})
478+
.flat_map(|data| {
479+
data.annotations
480+
.get::<BorrowAnnotation>()
481+
.unwrap()
482+
.code_map
483+
.values()
484+
.flat_map(|info| {
485+
info.before
486+
.dying_nodes(&info.after)
487+
.iter()
488+
.flat_map(|(_, actions)| actions)
489+
.flatten()
490+
.flat_map(|action| action.edge.flatten())
491+
.filter_map(|edge| match edge {
492+
BorrowEdge::Field(qualified_inst_id, _)
493+
| BorrowEdge::EnumField(qualified_inst_id, _, _)
494+
| BorrowEdge::DynamicField(qualified_inst_id, _, _) => {
495+
Some(qualified_inst_id.to_qualified_id())
496+
}
497+
BorrowEdge::Direct | BorrowEdge::Index(_) => None,
498+
BorrowEdge::Hyper(borrow_edges) => unreachable!(),
499+
})
500+
.collect_vec()
501+
})
502+
})
503+
.unique()
504+
.collect_vec(),
505+
};
506+
env.set_extension(writeback_datatype_info);
462507
}
463508

464509
fn name(&self) -> String {

0 commit comments

Comments
 (0)