From 06e74329a4c3199361b7233253a1326caf3ec468 Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Sun, 8 Dec 2024 14:42:04 +0100 Subject: [PATCH] works --- creusot/src/backend/program.rs | 13 +- creusot/src/translation/function.rs | 179 +++++-- creusot/src/translation/pearlite.rs | 6 + .../iterators/03_std_iterators.coma | 381 +++++++------- .../iterators/03_std_iterators.rs | 15 +- .../03_std_iterators/why3session.xml | 23 +- .../iterators/03_std_iterators/why3shapes.gz | Bin 6595 -> 6610 bytes .../iterators/06_map_precond.coma | 470 +++++++++--------- .../iterators/06_map_precond.rs | 23 +- .../iterators/06_map_precond/why3session.xml | 25 +- .../iterators/06_map_precond/why3shapes.gz | Bin 5381 -> 5260 bytes 11 files changed, 600 insertions(+), 535 deletions(-) diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index bbfb33b606..42237097ed 100644 --- a/creusot/src/backend/program.rs +++ b/creusot/src/backend/program.rs @@ -185,7 +185,6 @@ pub fn to_why<'tcx, N: Namer<'tcx>>( let inferred_closure_spec = ctx.is_closure_like(body_id.def_id()) && !ctx.sig(body_id.def_id()).contract.has_user_contract; - eprintln!("{body_id:?} {inferred_closure_spec:?}"); // We remove the barrier around the definition in the following edge cases: let open_body = false // a closure with no contract @@ -195,13 +194,11 @@ pub fn to_why<'tcx, N: Namer<'tcx>>( // a ghost closure || is_ghost_closure(ctx.tcx, body_id.def_id()); - if !open_body { - postcond = Expr::BlackBox(Box::new(postcond)); - } let ensures = sig.contract.ensures.into_iter().map(Condition::labelled_exp); - if open_body { - // postcond = ensures.rfold(postcond, |acc, cond| Expr::Assert(Box::new(cond), Box::new(acc))); + if !open_body { + postcond = Expr::BlackBox(Box::new(postcond)); + postcond = ensures.rfold(postcond, |acc, cond| Expr::Assert(Box::new(cond), Box::new(acc))); } if !open_body { @@ -227,8 +224,8 @@ pub fn to_why<'tcx, N: Namer<'tcx>>( ); let requires = sig.contract.requires.into_iter().map(Condition::labelled_exp); - if open_body { - // body = requires.rfold(body, |acc, req| Expr::Assert(Box::new(req), Box::new(acc))); + if !open_body { + body = requires.rfold(body, |acc, req| Expr::Assert(Box::new(req), Box::new(acc))); } let params = sig .args diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs index ac7e22deb9..f519d3711e 100644 --- a/creusot/src/translation/function.rs +++ b/creusot/src/translation/function.rs @@ -25,8 +25,8 @@ use rustc_hir::def_id::DefId; use rustc_index::{bit_set::BitSet, Idx}; use rustc_middle::{ mir::{ - self, traversal::reverse_postorder, BasicBlock, Body, Local, Location, Operand, Place, - PlaceRef, TerminatorKind, START_BLOCK, + self, traversal::reverse_postorder, BasicBlock, Body, Local, Location, Mutability, Operand, + Place, PlaceRef, TerminatorKind, START_BLOCK, }, ty::{ BorrowKind, ClosureKind, GenericArg, GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind, @@ -49,6 +49,8 @@ mod statement; mod terminator; use terminator::discriminator_for_switch; +use self::pearlite::BinOp; + /// Translate a function from rustc's MIR to fMIR. pub(crate) fn fmir<'tcx>(ctx: &mut TranslationCtx<'tcx>, body_id: BodyId) -> fmir::Body<'tcx> { let body = ctx.body(body_id).clone(); @@ -828,37 +830,63 @@ impl<'tcx> TranslationCtx<'tcx> { .collect(), ); - let (mut precondition, mut postcondition) = if contract.is_empty() { - let params: Vec<_> = - args_nms.iter().cloned().zip(args_tys).map(|(nm, ty)| Term::var(nm, ty)).collect(); - let ret_params = params.clone(); - eprintln!("{subst:?}"); - ( - Term::mk_true(self.tcx), - Term { - kind: TermKind::Postcondition { item: def_id, args: subst, params: ret_params }, - ty: self.types.bool, - span, - }, + let env_ty = self.closure_env_ty( + self.type_of(def_id).instantiate_identity(), + kind, + self.lifetimes.re_erased, + ); + let self_ = Term::var(Symbol::intern("self"), env_ty); + let params: Vec<_> = + args_nms.iter().cloned().zip(args_tys).map(|(nm, ty)| Term::var(nm, ty)).collect(); + + let mut precondition = if contract.is_empty() { + self.inferred_precondition_term( + def_id, + subst, + kind, + self_.clone(), + params.clone(), + span, ) } else { - (contract.requires_conj(self.tcx), contract.ensures_conj(self.tcx)) + contract.requires_conj(self.tcx) }; - postcondition = pearlite::Term { - span: postcondition.span, - kind: TermKind::Let { - pattern: arg_pat.clone(), - arg: Box::new(arg_tuple.clone()), - body: Box::new(postcondition), - }, - ty: self.types.bool, + let retty = self.sig(def_id).output; + let postcond = |target_kind| { + let postcondition = if contract.is_empty() { + let mut ret_params = params.clone(); + ret_params.push(Term::var(Symbol::intern("result"), retty)); + + self.inferred_postcondition_term( + target_kind, + def_id, + subst, + kind, + self_.clone(), + ret_params, + span, + ) + } else { + contract.ensures_conj(self.tcx) + }; + + pearlite::Term { + span: postcondition.span, + kind: TermKind::Let { + pattern: arg_pat.clone(), + arg: Box::new(arg_tuple.clone()), + body: Box::new(postcondition), + }, + ty: self.types.bool, + } }; + precondition = pearlite::Term { span: precondition.span, kind: TermKind::Let { - pattern: arg_pat, - arg: Box::new(arg_tuple), + pattern: arg_pat.clone(), + arg: Box::new(arg_tuple.clone()), body: Box::new(precondition), }, ty: self.types.bool, @@ -896,7 +924,7 @@ impl<'tcx> TranslationCtx<'tcx> { let self_ = Term::var(Symbol::intern("self"), env_ty); let mut csubst = closure_capture_subst(self, def_id, subst, false, Some(self_.clone()), self_); - let mut postcondition = postcondition.clone(); + let mut postcondition = postcond(ClosureKind::Fn); csubst.visit_mut_term(&mut postcondition); @@ -915,7 +943,7 @@ impl<'tcx> TranslationCtx<'tcx> { result_state.clone(), ); - let mut postcondition = postcondition.clone(); + let mut postcondition = postcond(ClosureKind::FnMut); csubst.visit_mut_term(&mut postcondition); let args = subst.as_closure().sig().inputs().skip_binder()[0]; @@ -945,12 +973,107 @@ impl<'tcx> TranslationCtx<'tcx> { let mut csubst = closure_capture_subst(self, def_id, subst, true, Some(self_.clone()), self_); - let mut postcondition = postcondition.clone(); + let mut postcondition = postcond(ClosureKind::FnOnce); csubst.visit_mut_term(&mut postcondition); contracts.postcond_once = Some(postcondition); contracts } + + fn inferred_precondition_term( + &self, + def_id: DefId, + args: GenericArgsRef<'tcx>, + kind: ClosureKind, + closure_env: Term<'tcx>, + mut closure_args: Vec>, + span: Span, + ) -> Term<'tcx> { + let env_ty = closure_env.ty; + + let bor_self = Term::var( + Symbol::intern("__bor_self"), + Ty::new_ref(self.tcx, self.tcx.lifetimes.re_erased, env_ty, Mutability::Mut), + ); + // Based on the underlying kind of closure we may need to wrap the call in a quantifier (at least for FnMut ones) + match kind { + ClosureKind::Fn | ClosureKind::FnOnce => { + closure_args.insert(0, closure_env.clone()); + + Term { + kind: TermKind::Precondition { item: def_id, args, params: closure_args }, + ty: self.types.bool, + span, + } + } + ClosureKind::FnMut => { + closure_args.insert(0, bor_self.clone()); + let base = Term { + kind: TermKind::Precondition { item: def_id, args, params: closure_args }, + ty: self.types.bool, + span, + }; + (bor_self.clone().cur().bin_op(self.tcx, BinOp::Eq, closure_env)) + .implies(base) + .forall(self.tcx, (Symbol::intern("__bor_self"), env_ty)) + } + } + } + + /// Infers the `postcond_kind` version of the postcondition predicate for the provided closure. + fn inferred_postcondition_term( + &self, + postcond_kind: ClosureKind, + def_id: DefId, + args: GenericArgsRef<'tcx>, + closure_kind: ClosureKind, + closure_env: Term<'tcx>, + mut closure_args: Vec>, + span: Span, + ) -> Term<'tcx> { + let env_ty = closure_env.ty; + + match closure_kind { + ClosureKind::Fn | ClosureKind::FnOnce => { + closure_args.insert(0, closure_env.clone()); + + let base = Term { + kind: TermKind::Postcondition { item: def_id, args, params: closure_args }, + ty: self.types.bool, + span, + }; + base + } + ClosureKind::FnMut => { + let bor_self = Term::var(Symbol::intern("__bor_self"), env_ty); + closure_args.insert(0, bor_self.clone()); + + let base = Term { + kind: TermKind::Postcondition { item: def_id, args, params: closure_args }, + ty: self.types.bool, + span, + }; + + match postcond_kind { + ClosureKind::FnOnce => base + .conj(bor_self.cur().bin_op(self.tcx, BinOp::Eq, closure_env)) + .exists(self.tcx, (Symbol::intern("__bor_self"), env_ty)), + ClosureKind::FnMut => base + .conj(bor_self.clone().cur().bin_op(self.tcx, BinOp::Eq, closure_env)) + .conj(bor_self.fin().bin_op( + self.tcx, + BinOp::Eq, + Term::var(Symbol::intern("result_state"), env_ty), + )) + .exists(self.tcx, (Symbol::intern("__bor_self"), env_ty)), + ClosureKind::Fn => self.crash_and_error( + span, + "An `FnMut` closure cannot have an `Fn` postcondition", + ), + } + } + } + } } pub(crate) fn closure_resolve<'tcx>( diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index de5a94648d..a672e34d4a 100644 --- a/creusot/src/translation/pearlite.rs +++ b/creusot/src/translation/pearlite.rs @@ -1481,6 +1481,12 @@ impl<'tcx> Term<'tcx> { self.forall_trig(tcx, binder, vec![]) } + pub(crate) fn exists(self, tcx: TyCtxt<'tcx>, binder: (Symbol, Ty<'tcx>)) -> Self { + let ty = Ty::new_tup(tcx, &[binder.1]); + + self.quant(QuantKind::Exists, (vec![Ident::new(binder.0, DUMMY_SP)], ty), vec![]) + } + pub(crate) fn quant( self, quant_kind: QuantKind, diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.coma b/creusot/tests/should_succeed/iterators/03_std_iterators.coma index 7b532d253f..e271f25c48 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.coma +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.coma @@ -243,7 +243,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42] meta "compute_max_steps" 1000000 - let rec slice_iter'0 (slice:slice t_T'0) (return' (ret:usize))= {[@expl:slice_iter 'slice' type invariant] [%#s03_std_iterators7] inv'2 slice} + let rec slice_iter'0[#"03_std_iterators.rs" 6 0 6 42] (slice:slice t_T'0) (return' (ret:usize))= {[@expl:slice_iter 'slice' type invariant] [%#s03_std_iterators7] inv'2 slice} {[@expl:slice_iter requires] [%#s03_std_iterators8] Seq.length (view'0 slice) < 1000} (! bb0 [ bb0 = s0 @@ -572,7 +572,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41] meta "compute_max_steps" 1000000 - let rec vec_iter'0 (vec:t_Vec'0) (return' (ret:usize))= {[@expl:vec_iter 'vec' type invariant] [%#s03_std_iterators7] inv'2 vec} + let rec vec_iter'0[#"03_std_iterators.rs" 17 0 17 41] (vec:t_Vec'0) (return' (ret:usize))= {[@expl:vec_iter 'vec' type invariant] [%#s03_std_iterators7] inv'2 vec} {[@expl:vec_iter requires] [%#s03_std_iterators8] Seq.length (view'0 vec) < 1000} (! bb0 [ bb0 = s0 @@ -902,7 +902,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] meta "compute_max_steps" 1000000 - let rec all_zero'0 (v:borrowed (t_Vec'0)) (return' (ret:()))= (! bb0 + let rec all_zero'0[#"03_std_iterators.rs" 28 0 28 35] (v:borrowed (t_Vec'0)) (return' (ret:()))= (! bb0 [ bb0 = s0 [ s0 = Borrow.borrow_final {v.current} {Borrow.get_id v} (fun (_ret':borrowed (t_Vec'0)) -> [ &_8 <- _ret' ] [ &v <- { v with current = _ret'.final } ] s1) @@ -1226,7 +1226,7 @@ module M_03_std_iterators__skip_take [#"03_std_iterators.rs" 35 0 35 48] meta "compute_max_steps" 1000000 - let rec skip_take'0 (iter:t_I'0) (n:usize) (return' (ret:()))= {[@expl:skip_take 'iter' type invariant] [%#s03_std_iterators1] inv'2 iter} + let rec skip_take'0[#"03_std_iterators.rs" 35 0 35 48] (iter:t_I'0) (n:usize) (return' (ret:()))= {[@expl:skip_take 'iter' type invariant] [%#s03_std_iterators1] inv'2 iter} (! bb0 [ bb0 = s0 [ s0 = take'0 {iter} {n} (fun (_ret':t_Take'0) -> [ &_6 <- _ret' ] s1) | s1 = bb1 ] | bb1 = s0 [ s0 = skip'0 {_6} {n} (fun (_ret':t_Skip'0) -> [ &_5 <- _ret' ] s1) | s1 = bb2 ] @@ -1259,58 +1259,57 @@ module M_03_std_iterators__skip_take [#"03_std_iterators.rs" 35 0 35 48] [ return' (result:())-> (! return' {result}) ] end module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] - let%span s03_std_iterators0 = "03_std_iterators.rs" 42 18 42 19 - let%span s03_std_iterators1 = "03_std_iterators.rs" 56 20 56 40 - let%span s03_std_iterators2 = "03_std_iterators.rs" 57 20 57 33 - let%span s03_std_iterators3 = "03_std_iterators.rs" 58 20 58 36 + let%span s03_std_iterators0 = "03_std_iterators.rs" 42 25 42 26 + let%span s03_std_iterators1 = "03_std_iterators.rs" 53 20 53 40 + let%span s03_std_iterators2 = "03_std_iterators.rs" 54 20 54 33 + let%span s03_std_iterators3 = "03_std_iterators.rs" 55 20 55 36 let%span svec4 = "../../../../creusot-contracts/src/std/vec.rs" 169 26 169 42 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 - let%span s03_std_iterators6 = "03_std_iterators.rs" 50 23 50 24 - let%span s03_std_iterators7 = "03_std_iterators.rs" 47 23 47 65 - let%span s03_std_iterators8 = "03_std_iterators.rs" 48 22 48 89 - let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 55 21 55 25 - let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 55 27 55 31 - let%span siter11 = "../../../../creusot-contracts/src/std/iter.rs" 49 15 51 69 - let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 52 15 52 51 - let%span siter13 = "../../../../creusot-contracts/src/std/iter.rs" 53 15 53 70 - let%span siter14 = "../../../../creusot-contracts/src/std/iter.rs" 55 4 58 61 - let%span siter15 = "../../../../creusot-contracts/src/std/iter.rs" 54 14 54 88 - let%span siter16 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 - let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 - let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 409 4 409 10 - let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 416 15 416 32 - let%span sslice22 = "../../../../creusot-contracts/src/std/slice.rs" 417 15 417 32 - let%span sslice23 = "../../../../creusot-contracts/src/std/slice.rs" 418 14 418 42 - let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 414 4 414 10 - let%span sslice25 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 - let%span smap_inv26 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 153 12 156 47 - let%span smap_inv27 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 140 12 145 71 - let%span smap_inv28 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 15 8 18 9 - let%span smap_inv29 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 37 8 49 9 - let%span svec30 = "../../../../creusot-contracts/src/std/vec.rs" 285 20 285 32 - let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 - let%span sslice32 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sresolve33 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sops34 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 - let%span sops35 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 - let%span sops36 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 - let%span sops37 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 - let%span sops38 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 - let%span sops39 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 - let%span sops40 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 - let%span sslice41 = "../../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 - let%span sslice42 = "../../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 - let%span sslice43 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 - let%span smap_inv44 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 117 12 119 63 - let%span smap_inv45 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 57 8 57 50 - let%span smap_inv46 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 23 14 23 45 - let%span smap_inv47 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 28 15 28 32 - let%span smap_inv48 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 29 15 29 32 - let%span smap_inv49 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 30 14 30 42 - let%span sindex50 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 - let%span smodel51 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 + let%span s03_std_iterators6 = "03_std_iterators.rs" 47 26 47 45 + let%span s03_std_iterators7 = "03_std_iterators.rs" 48 19 48 20 + let%span siter8 = "../../../../creusot-contracts/src/std/iter.rs" 55 21 55 25 + let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 55 27 55 31 + let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 49 15 51 69 + let%span siter11 = "../../../../creusot-contracts/src/std/iter.rs" 52 15 52 51 + let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 53 15 53 70 + let%span siter13 = "../../../../creusot-contracts/src/std/iter.rs" 55 4 58 61 + let%span siter14 = "../../../../creusot-contracts/src/std/iter.rs" 54 14 54 88 + let%span siter15 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 + let%span svec16 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 + let%span smodel17 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22 + let%span sslice18 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 + let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 409 4 409 10 + let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 416 15 416 32 + let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 417 15 417 32 + let%span sslice22 = "../../../../creusot-contracts/src/std/slice.rs" 418 14 418 42 + let%span sslice23 = "../../../../creusot-contracts/src/std/slice.rs" 414 4 414 10 + let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 + let%span smap_inv25 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 153 12 156 47 + let%span smap_inv26 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 140 12 145 71 + let%span smap_inv27 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 15 8 18 9 + let%span smap_inv28 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 37 8 49 9 + let%span svec29 = "../../../../creusot-contracts/src/std/vec.rs" 285 20 285 32 + let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 + let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 + let%span sresolve32 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sops33 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 + let%span sops34 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 + let%span sops35 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 + let%span sops36 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 + let%span sops37 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 + let%span sops38 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 + let%span sops39 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 + let%span sslice40 = "../../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 + let%span sslice41 = "../../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 + let%span sslice42 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 + let%span smap_inv43 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 117 12 119 63 + let%span smap_inv44 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 57 8 57 50 + let%span smap_inv45 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 23 14 23 45 + let%span smap_inv46 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 28 15 28 32 + let%span smap_inv47 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 29 15 29 32 + let%span smap_inv48 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 30 14 30 42 + let%span sindex49 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 + let%span smodel50 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 use prelude.prelude.UIntSize @@ -1359,19 +1358,19 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] function view'4 (self : slice uint32) : Seq.seq uint32 - axiom view'4_spec : forall self : slice uint32 . ([%#sslice31] Seq.length (view'4 self) + axiom view'4_spec : forall self : slice uint32 . ([%#sslice30] Seq.length (view'4 self) <= UIntSize.to_int (v_MAX'0 : usize)) - && ([%#sslice32] view'4 self = Slice.id self) + && ([%#sslice31] view'4 self = Slice.id self) function view'1 (self : slice uint32) : Seq.seq uint32 = - [%#smodel18] view'4 self + [%#smodel17] view'4 self function view'0 (self : t_Vec'0) : Seq.seq uint32 - axiom view'0_spec : forall self : t_Vec'0 . [%#svec17] Seq.length (view'0 self) <= UIntSize.to_int (v_MAX'0 : usize) + axiom view'0_spec : forall self : t_Vec'0 . [%#svec16] Seq.length (view'0 self) <= UIntSize.to_int (v_MAX'0 : usize) function view'2 (self : t_Vec'0) : Seq.seq uint32 = - [%#smodel18] view'0 self + [%#smodel17] view'0 self let rec deref'0 (self:t_Vec'0) (return' (ret:slice uint32))= {[@expl:deref 'self' type invariant] inv'0 self} any [ return' (result:slice uint32)-> {inv'1 result} {[%#svec4] view'1 result = view'2 self} (! return' {result}) ] @@ -1384,34 +1383,27 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] let rec iter'0 (self:slice uint32) (return' (ret:t_Iter'0))= {[@expl:iter 'self' type invariant] inv'1 self} any [ return' (result:t_Iter'0)-> {[%#sslice5] view'3 result = self} (! return' {result}) ] + use prelude.prelude.Snapshot + + use seq.Seq + type closure0'1 = { field_0'0: borrowed usize } predicate resolve'2 (self : borrowed closure0'1) = - [%#sresolve33] self.final = self.current + [%#sresolve32] self.final = self.current predicate resolve'0 (_1 : borrowed closure0'1) = resolve'2 _1 use prelude.prelude.Intrinsic - use prelude.prelude.Snapshot - - use seq.Seq - use seq.Seq use prelude.prelude.Snapshot - predicate postcondition_once'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) - - = - [%#s03_std_iterators8] let (x, _prod) = args in UIntSize.to_int (self.field_0'0).final - = UIntSize.to_int (self.field_0'0).current + 1 - /\ UIntSize.to_int (self.field_0'0).final = Seq.length (Snapshot.inner _prod) + 1 /\ result = x - predicate resolve'8 (self : borrowed usize) = - [%#sresolve33] self.final = self.current + [%#sresolve32] self.final = self.current predicate resolve'7 (_1 : borrowed usize) = resolve'8 _1 @@ -1422,62 +1414,58 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] predicate unnest'0 (self : closure0'1) (_2 : closure0'1) = (_2.field_0'0).final = (self.field_0'0).final + let rec closure0'0[#"03_std_iterators.rs" 46 17 46 27] [@coma:extspec] (_1:borrowed closure0'1) (x:uint32) (_prod:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= bb0 + [ bb0 = s0 + [ s0 = {[@expl:assertion] [%#s03_std_iterators6] UIntSize.to_int ((_1.current).field_0'0).current + = Seq.length (Snapshot.inner _prod)} + s1 + | s1 = UIntSize.add {((_1.current).field_0'0).current} {[%#s03_std_iterators7] (1 : usize)} + (fun (_ret':usize) -> + [ &_1 <- { _1 with current = { field_0'0 = { (_1.current).field_0'0 with current = _ret' } } } ] + s2) + | s2 = -{resolve'0 _1}- s3 + | s3 = [ &_0 <- x ] s4 + | s4 = return' {_0} ] + ] + + [ & _0 : uint32 = any_l () + | & _1 : borrowed closure0'1 = _1 + | & x : uint32 = x + | & _prod : Snapshot.snap_ty (Seq.seq uint32) = _prod ] + [ return' (result:uint32)-> return' {result} ] + + predicate postcondition_once'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) + + = + let (x, _prod) = args in exists __bor_self : borrowed closure0'1 . closure0'0'post'return' __bor_self x _prod result + /\ __bor_self.current = self + predicate postcondition_mut'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result_state : closure0'1) (result : uint32) = - (let (x, _prod) = args in UIntSize.to_int (result_state.field_0'0).current - = UIntSize.to_int (self.field_0'0).current + 1 - /\ UIntSize.to_int (result_state.field_0'0).current = Seq.length (Snapshot.inner _prod) + 1 /\ result = x) + (let (x, _prod) = args in exists __bor_self : borrowed closure0'1 . closure0'0'post'return' __bor_self x _prod result + /\ __bor_self.current = self /\ __bor_self.final = result_state) /\ unnest'0 self result_state function fn_mut_once'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res : uint32) : () - axiom fn_mut_once'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops40] postcondition_once'0 self args res + axiom fn_mut_once'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops39] postcondition_once'0 self args res = (exists res_state : closure0'1 . postcondition_mut'0 self args res_state res /\ resolve'4 res_state) function unnest_trans'0 (self : closure0'1) (b : closure0'1) (c : closure0'1) : () - axiom unnest_trans'0_spec : forall self : closure0'1, b : closure0'1, c : closure0'1 . ([%#sops37] unnest'0 self b) - -> ([%#sops38] unnest'0 b c) -> ([%#sops39] unnest'0 self c) + axiom unnest_trans'0_spec : forall self : closure0'1, b : closure0'1, c : closure0'1 . ([%#sops36] unnest'0 self b) + -> ([%#sops37] unnest'0 b c) -> ([%#sops38] unnest'0 self c) function unnest_refl'0 (self : closure0'1) : () - axiom unnest_refl'0_spec : forall self : closure0'1 . [%#sops36] unnest'0 self self + axiom unnest_refl'0_spec : forall self : closure0'1 . [%#sops35] unnest'0 self self function postcondition_mut_unnest'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res_state : closure0'1) (res : uint32) : () - axiom postcondition_mut_unnest'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : closure0'1, res : uint32 . ([%#sops34] postcondition_mut'0 self args res_state res) - -> ([%#sops35] unnest'0 self res_state) - - let rec closure0'0 (_1:borrowed closure0'1) (x:uint32) (_prod:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= {[@expl:closure requires] [%#s03_std_iterators7] UIntSize.to_int ((_1.current).field_0'0).current - = Seq.length (Snapshot.inner _prod) - /\ ((_1.current).field_0'0).current < (v_MAX'0 : usize)} - (! bb0 - [ bb0 = s0 - [ s0 = UIntSize.add {((_1.current).field_0'0).current} {[%#s03_std_iterators6] (1 : usize)} - (fun (_ret':usize) -> - [ &_1 <- { _1 with current = { field_0'0 = { (_1.current).field_0'0 with current = _ret' } } } ] - s1) - | s1 = -{resolve'0 _1}- s2 - | s2 = [ &res1 <- x ] s3 - | s3 = [ &res <- res1 ] s4 - | s4 = [ &_0 <- res ] s5 - | s5 = return' {_0} ] - ] - ) - [ & _0 : uint32 = any_l () - | & _1 : borrowed closure0'1 = _1 - | & x : uint32 = x - | & res : uint32 = any_l () - | & res1 : uint32 = any_l () ] - - [ return' (result:uint32)-> {[@expl:closure ensures] [%#s03_std_iterators8] UIntSize.to_int ((_1.final).field_0'0).current - = UIntSize.to_int ((_1.current).field_0'0).current + 1 - /\ UIntSize.to_int ((_1.final).field_0'0).current = Seq.length (Snapshot.inner _prod) + 1 /\ result = x} - {[@expl:closure unnest] unnest'0 _1.current _1.final} - (! return' {result}) ] - + axiom postcondition_mut_unnest'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : closure0'1, res : uint32 . ([%#sops33] postcondition_mut'0 self args res_state res) + -> ([%#sops34] unnest'0 self res_state) use seq.Seq @@ -1488,43 +1476,43 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] use seq.Seq function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 = - [%#sindex50] Seq.get (view'4 self) ix + [%#sindex49] Seq.get (view'4 self) ix function to_ref_seq'0 (self : slice uint32) : Seq.seq uint32 - axiom to_ref_seq'0_spec : forall self : slice uint32 . ([%#sslice41] Seq.length (to_ref_seq'0 self) + axiom to_ref_seq'0_spec : forall self : slice uint32 . ([%#sslice40] Seq.length (to_ref_seq'0 self) = Seq.length (view'1 self)) - && ([%#sslice42] forall i : int . 0 <= i /\ i < Seq.length (to_ref_seq'0 self) + && ([%#sslice41] forall i : int . 0 <= i /\ i < Seq.length (to_ref_seq'0 self) -> Seq.get (to_ref_seq'0 self) i = index_logic'0 self i) predicate produces'0 (self : t_Iter'0) (visited : Seq.seq uint32) (tl : t_Iter'0) = - [%#sslice25] to_ref_seq'0 (view'3 self) = Seq.(++) visited (to_ref_seq'0 (view'3 tl)) + [%#sslice24] to_ref_seq'0 (view'3 self) = Seq.(++) visited (to_ref_seq'0 (view'3 tl)) function produces_trans'1 (a : t_Iter'0) (ab : Seq.seq uint32) (b : t_Iter'0) (bc : Seq.seq uint32) (c : t_Iter'0) : () = - [%#sslice24] () + [%#sslice23] () - axiom produces_trans'1_spec : forall a : t_Iter'0, ab : Seq.seq uint32, b : t_Iter'0, bc : Seq.seq uint32, c : t_Iter'0 . ([%#sslice21] produces'0 a ab b) - -> ([%#sslice22] produces'0 b bc c) -> ([%#sslice23] produces'0 a (Seq.(++) ab bc) c) + axiom produces_trans'1_spec : forall a : t_Iter'0, ab : Seq.seq uint32, b : t_Iter'0, bc : Seq.seq uint32, c : t_Iter'0 . ([%#sslice20] produces'0 a ab b) + -> ([%#sslice21] produces'0 b bc c) -> ([%#sslice22] produces'0 a (Seq.(++) ab bc) c) function produces_refl'1 (self : t_Iter'0) : () = - [%#sslice20] () + [%#sslice19] () - axiom produces_refl'1_spec : forall self : t_Iter'0 . [%#sslice19] produces'0 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'1_spec : forall self : t_Iter'0 . [%#sslice18] produces'0 self (Seq.empty : Seq.seq uint32) self function produces_trans'0 (a : t_Iter'0) (ab : Seq.seq uint32) (b : t_Iter'0) (bc : Seq.seq uint32) (c : t_Iter'0) : () = - [%#sslice24] () + [%#sslice23] () - axiom produces_trans'0_spec : forall a : t_Iter'0, ab : Seq.seq uint32, b : t_Iter'0, bc : Seq.seq uint32, c : t_Iter'0 . ([%#sslice21] produces'0 a ab b) - -> ([%#sslice22] produces'0 b bc c) -> ([%#sslice23] produces'0 a (Seq.(++) ab bc) c) + axiom produces_trans'0_spec : forall a : t_Iter'0, ab : Seq.seq uint32, b : t_Iter'0, bc : Seq.seq uint32, c : t_Iter'0 . ([%#sslice20] produces'0 a ab b) + -> ([%#sslice21] produces'0 b bc c) -> ([%#sslice22] produces'0 a (Seq.(++) ab bc) c) function produces_refl'0 (self : t_Iter'0) : () = - [%#sslice20] () + [%#sslice19] () - axiom produces_refl'0_spec : forall self : t_Iter'0 . [%#sslice19] produces'0 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'0_spec : forall self : t_Iter'0 . [%#sslice18] produces'0 self (Seq.empty : Seq.seq uint32) self predicate inv'2 (_1 : t_Iter'0) @@ -1539,36 +1527,35 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] use prelude.prelude.Snapshot predicate precondition'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) = - [%#s03_std_iterators7] let (x, _prod) = args in UIntSize.to_int (self.field_0'0).current - = Seq.length (Snapshot.inner _prod) - /\ (self.field_0'0).current < (v_MAX'0 : usize) + let (x, _prod) = args in forall __bor_self : borrowed closure0'1 . __bor_self.current = self + -> closure0'0'pre __bor_self x _prod predicate resolve'5 (self : borrowed (t_Iter'0)) = - [%#sresolve33] self.final = self.current + [%#sresolve32] self.final = self.current function view'5 (self : borrowed (t_Iter'0)) : slice uint32 = - [%#smodel51] view'3 self.current + [%#smodel50] view'3 self.current use seq.Seq predicate completed'1 (self : borrowed (t_Iter'0)) = - [%#sslice43] resolve'5 self /\ view'4 (view'5 self) = (Seq.empty : Seq.seq uint32) + [%#sslice42] resolve'5 self /\ view'4 (view'5 self) = (Seq.empty : Seq.seq uint32) predicate next_precondition'0 (iter : t_Iter'0) (func : closure0'1) (produced : Seq.seq uint32) = - [%#smap_inv44] forall e : uint32, i : t_Iter'0 . produces'0 iter (Seq.singleton e) i + [%#smap_inv43] forall e : uint32, i : t_Iter'0 . produces'0 iter (Seq.singleton e) i -> precondition'0 func (e, Snapshot.new produced) use seq.Seq predicate preservation'0 (iter : t_Iter'0) (func : closure0'1) = - [%#smap_inv27] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure0'1, b : uint32, i : t_Iter'0 . unnest'0 func f.current + [%#smap_inv26] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure0'1, b : uint32, i : t_Iter'0 . unnest'0 func f.current -> produces'0 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition'0 f.current (e1, Snapshot.new s) -> postcondition_mut'0 f.current (e1, Snapshot.new s) f.final b -> precondition'0 f.final (e2, Snapshot.new (Seq.snoc s e1)) predicate reinitialize'0 (_1 : ()) = - [%#smap_inv26] forall iter : borrowed (t_Iter'0), func : closure0'1 . completed'1 iter + [%#smap_inv25] forall iter : borrowed (t_Iter'0), func : closure0'1 . completed'1 iter -> next_precondition'0 iter.final func (Seq.empty : Seq.seq uint32) /\ preservation'0 iter.final func type t_MapInv'0 = @@ -1586,15 +1573,15 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] | {t_MapInv__iter'0 = iter ; t_MapInv__func'0 = func ; t_MapInv__produced'0 = produced} -> true end) - let rec map_inv'0 (self:t_Iter'0) (func:closure0'1) (return' (ret:t_MapInv'0))= {[@expl:map_inv 'self' type invariant] [%#siter9] inv'2 self} - {[@expl:map_inv 'func' type invariant] [%#siter10] inv'3 func} - {[@expl:map_inv requires #0] [%#siter11] forall e : uint32, i2 : t_Iter'0 . produces'0 self (Seq.singleton e) i2 + let rec map_inv'0 (self:t_Iter'0) (func:closure0'1) (return' (ret:t_MapInv'0))= {[@expl:map_inv 'self' type invariant] [%#siter8] inv'2 self} + {[@expl:map_inv 'func' type invariant] [%#siter9] inv'3 func} + {[@expl:map_inv requires #0] [%#siter10] forall e : uint32, i2 : t_Iter'0 . produces'0 self (Seq.singleton e) i2 -> precondition'0 func (e, Snapshot.new (Seq.empty : Seq.seq uint32))} - {[@expl:map_inv requires #1] [%#siter12] reinitialize'0 ()} - {[@expl:map_inv requires #2] [%#siter13] preservation'0 self func} + {[@expl:map_inv requires #1] [%#siter11] reinitialize'0 ()} + {[@expl:map_inv requires #2] [%#siter12] preservation'0 self func} any - [ return' (result:t_MapInv'0)-> {[%#siter14] inv'4 result} - {[%#siter15] result + [ return' (result:t_MapInv'0)-> {[%#siter13] inv'4 result} + {[%#siter14] result = { t_MapInv__iter'0 = self; t_MapInv__func'0 = func; t_MapInv__produced'0 = Snapshot.new (Seq.empty : Seq.seq uint32) }} @@ -1609,7 +1596,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] true predicate resolve'3 (self : t_MapInv'0) = - [%#smap_inv45] resolve'6 self.t_MapInv__iter'0 /\ resolve'4 self.t_MapInv__func'0 + [%#smap_inv44] resolve'6 self.t_MapInv__iter'0 /\ resolve'4 self.t_MapInv__func'0 predicate resolve'1 (_1 : t_MapInv'0) = resolve'3 _1 @@ -1627,7 +1614,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] use seq.Seq predicate produces'1 [@inline:trivial] (self : t_MapInv'0) (visited : Seq.seq uint32) (succ : t_MapInv'0) = - [%#smap_inv29] unnest'0 self.t_MapInv__func'0 succ.t_MapInv__func'0 + [%#smap_inv28] unnest'0 self.t_MapInv__func'0 succ.t_MapInv__func'0 /\ (exists fs : Seq.seq (borrowed closure0'1) . Seq.length fs = Seq.length visited /\ (exists s : Seq.seq uint32 . Seq.length s = Seq.length visited /\ produces'0 self.t_MapInv__iter'0 s succ.t_MapInv__iter'0 @@ -1647,25 +1634,25 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] function produces_trans'2 (a : t_MapInv'0) (ab : Seq.seq uint32) (b : t_MapInv'0) (bc : Seq.seq uint32) (c : t_MapInv'0) : () - axiom produces_trans'2_spec : forall a : t_MapInv'0, ab : Seq.seq uint32, b : t_MapInv'0, bc : Seq.seq uint32, c : t_MapInv'0 . ([%#smap_inv47] produces'1 a ab b) - -> ([%#smap_inv48] produces'1 b bc c) -> ([%#smap_inv49] produces'1 a (Seq.(++) ab bc) c) + axiom produces_trans'2_spec : forall a : t_MapInv'0, ab : Seq.seq uint32, b : t_MapInv'0, bc : Seq.seq uint32, c : t_MapInv'0 . ([%#smap_inv46] produces'1 a ab b) + -> ([%#smap_inv47] produces'1 b bc c) -> ([%#smap_inv48] produces'1 a (Seq.(++) ab bc) c) function produces_refl'2 (self : t_MapInv'0) : () - axiom produces_refl'2_spec : forall self : t_MapInv'0 . [%#smap_inv46] produces'1 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'2_spec : forall self : t_MapInv'0 . [%#smap_inv45] produces'1 self (Seq.empty : Seq.seq uint32) self predicate completed'0 (self : borrowed (t_MapInv'0)) = - [%#smap_inv28] Snapshot.inner (self.final).t_MapInv__produced'0 = (Seq.empty : Seq.seq uint32) + [%#smap_inv27] Snapshot.inner (self.final).t_MapInv__produced'0 = (Seq.empty : Seq.seq uint32) /\ completed'1 (Borrow.borrow_logic (self.current).t_MapInv__iter'0 (self.final).t_MapInv__iter'0 (Borrow.inherit_id (Borrow.get_id self) 1)) /\ (self.current).t_MapInv__func'0 = (self.final).t_MapInv__func'0 predicate from_iter_post'0 (prod : Seq.seq uint32) (res : t_Vec'0) = - [%#svec30] prod = view'0 res + [%#svec29] prod = view'0 res let rec collect'0 (self:t_MapInv'0) (return' (ret:t_Vec'0))= {[@expl:collect 'self' type invariant] inv'4 self} any [ return' (result:t_Vec'0)-> {inv'5 result} - {[%#siter16] exists done' : borrowed (t_MapInv'0), prod : Seq.seq uint32 . resolve'1 done'.final + {[%#siter15] exists done' : borrowed (t_MapInv'0), prod : Seq.seq uint32 . resolve'1 done'.final /\ completed'0 done' /\ produces'1 self prod done'.current /\ from_iter_post'0 prod result} (! return' {result}) ] @@ -1674,7 +1661,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] meta "compute_max_steps" 1000000 - let rec counter'0 (v:t_Vec'0) (return' (ret:()))= (! bb0 + let rec counter'0[#"03_std_iterators.rs" 41 0 41 27] (v:t_Vec'0) (return' (ret:()))= (! bb0 [ bb0 = s0 [ s0 = [ &cnt <- [%#s03_std_iterators0] (0 : usize) ] s1 | s1 = deref'0 {v} (fun (_ret':slice uint32) -> [ &_7 <- _ret' ] s2) @@ -1711,17 +1698,17 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] | & _10 : borrowed usize = any_l () ] [ return' (result:())-> (! return' {result}) ] end -module M_03_std_iterators__sum_range [#"03_std_iterators.rs" 63 0 63 35] - let%span s03_std_iterators0 = "03_std_iterators.rs" 64 16 64 17 - let%span s03_std_iterators1 = "03_std_iterators.rs" 66 13 66 14 - let%span s03_std_iterators2 = "03_std_iterators.rs" 66 4 66 7 - let%span s03_std_iterators3 = "03_std_iterators.rs" 66 4 66 7 - let%span s03_std_iterators4 = "03_std_iterators.rs" 65 16 65 46 - let%span s03_std_iterators5 = "03_std_iterators.rs" 66 4 66 7 - let%span s03_std_iterators6 = "03_std_iterators.rs" 66 4 66 7 - let%span s03_std_iterators7 = "03_std_iterators.rs" 67 13 67 14 - let%span s03_std_iterators8 = "03_std_iterators.rs" 61 11 61 18 - let%span s03_std_iterators9 = "03_std_iterators.rs" 62 10 62 21 +module M_03_std_iterators__sum_range [#"03_std_iterators.rs" 60 0 60 35] + let%span s03_std_iterators0 = "03_std_iterators.rs" 61 16 61 17 + let%span s03_std_iterators1 = "03_std_iterators.rs" 63 13 63 14 + let%span s03_std_iterators2 = "03_std_iterators.rs" 63 4 63 7 + let%span s03_std_iterators3 = "03_std_iterators.rs" 63 4 63 7 + let%span s03_std_iterators4 = "03_std_iterators.rs" 62 16 62 46 + let%span s03_std_iterators5 = "03_std_iterators.rs" 63 4 63 7 + let%span s03_std_iterators6 = "03_std_iterators.rs" 63 4 63 7 + let%span s03_std_iterators7 = "03_std_iterators.rs" 64 13 64 14 + let%span s03_std_iterators8 = "03_std_iterators.rs" 58 11 58 18 + let%span s03_std_iterators9 = "03_std_iterators.rs" 59 10 59 21 let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span srange11 = "../../../../creusot-contracts/src/std/iter/range.rs" 22 12 26 70 let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 @@ -1852,7 +1839,7 @@ module M_03_std_iterators__sum_range [#"03_std_iterators.rs" 63 0 63 35] meta "compute_max_steps" 1000000 - let rec sum_range'0 (n:isize) (return' (ret:isize))= {[@expl:sum_range requires] [%#s03_std_iterators8] IntSize.to_int n + let rec sum_range'0[#"03_std_iterators.rs" 60 0 60 35] (n:isize) (return' (ret:isize))= {[@expl:sum_range requires] [%#s03_std_iterators8] IntSize.to_int n >= 0} (! bb0 [ bb0 = s0 @@ -1920,14 +1907,14 @@ module M_03_std_iterators__sum_range [#"03_std_iterators.rs" 63 0 63 35] | & _24 : Snapshot.snap_ty (Seq.seq isize) = any_l () ] [ return' (result:isize)-> {[@expl:sum_range ensures] [%#s03_std_iterators9] result = n} (! return' {result}) ] end -module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24] - let%span s03_std_iterators0 = "03_std_iterators.rs" 74 20 74 21 - let%span s03_std_iterators1 = "03_std_iterators.rs" 74 23 74 25 - let%span s03_std_iterators2 = "03_std_iterators.rs" 74 4 74 7 - let%span s03_std_iterators3 = "03_std_iterators.rs" 74 4 74 7 - let%span s03_std_iterators4 = "03_std_iterators.rs" 73 16 73 93 - let%span s03_std_iterators5 = "03_std_iterators.rs" 74 4 74 7 - let%span s03_std_iterators6 = "03_std_iterators.rs" 74 4 74 7 +module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 69 0 69 24] + let%span s03_std_iterators0 = "03_std_iterators.rs" 71 20 71 21 + let%span s03_std_iterators1 = "03_std_iterators.rs" 71 23 71 25 + let%span s03_std_iterators2 = "03_std_iterators.rs" 71 4 71 7 + let%span s03_std_iterators3 = "03_std_iterators.rs" 71 4 71 7 + let%span s03_std_iterators4 = "03_std_iterators.rs" 70 16 70 93 + let%span s03_std_iterators5 = "03_std_iterators.rs" 71 4 71 7 + let%span s03_std_iterators6 = "03_std_iterators.rs" 71 4 71 7 let%span siter7 = "../../../../creusot-contracts/src/std/iter.rs" 150 27 150 93 let%span siter8 = "../../../../creusot-contracts/src/std/iter.rs" 151 27 151 115 let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 @@ -2148,7 +2135,7 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24] meta "compute_max_steps" 1000000 - let rec enumerate_range'0 (_1:()) (return' (ret:()))= (! bb0 + let rec enumerate_range'0[#"03_std_iterators.rs" 69 0 69 24] (_1:()) (return' (ret:()))= (! bb0 [ bb0 = s0 [ s0 = [ &_3 <- { t_Range__start'0 = ([%#s03_std_iterators0] (0 : usize)); @@ -2229,35 +2216,35 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24] | & x : usize = any_l () ] [ return' (result:())-> (! return' {result}) ] end -module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] - let%span s03_std_iterators0 = "03_std_iterators.rs" 96 34 96 54 - let%span s03_std_iterators1 = "03_std_iterators.rs" 101 26 101 27 - let%span s03_std_iterators2 = "03_std_iterators.rs" 101 22 101 27 - let%span s03_std_iterators3 = "03_std_iterators.rs" 101 19 101 20 - let%span s03_std_iterators4 = "03_std_iterators.rs" 101 40 101 41 - let%span s03_std_iterators5 = "03_std_iterators.rs" 101 36 101 41 - let%span s03_std_iterators6 = "03_std_iterators.rs" 101 33 101 34 - let%span s03_std_iterators7 = "03_std_iterators.rs" 101 4 101 7 - let%span s03_std_iterators8 = "03_std_iterators.rs" 101 4 101 7 - let%span s03_std_iterators9 = "03_std_iterators.rs" 100 16 100 80 - let%span s03_std_iterators10 = "03_std_iterators.rs" 99 16 99 76 - let%span s03_std_iterators11 = "03_std_iterators.rs" 98 16 98 78 - let%span s03_std_iterators12 = "03_std_iterators.rs" 97 16 97 34 - let%span s03_std_iterators13 = "03_std_iterators.rs" 101 4 101 7 - let%span s03_std_iterators14 = "03_std_iterators.rs" 101 4 101 7 - let%span s03_std_iterators15 = "03_std_iterators.rs" 102 30 102 31 - let%span s03_std_iterators16 = "03_std_iterators.rs" 103 22 103 28 - let%span s03_std_iterators17 = "03_std_iterators.rs" 104 22 104 54 - let%span s03_std_iterators18 = "03_std_iterators.rs" 105 22 105 54 - let%span s03_std_iterators19 = "03_std_iterators.rs" 94 21 94 26 - let%span s03_std_iterators20 = "03_std_iterators.rs" 93 10 93 44 +module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 91 0 91 37] + let%span s03_std_iterators0 = "03_std_iterators.rs" 93 34 93 54 + let%span s03_std_iterators1 = "03_std_iterators.rs" 98 26 98 27 + let%span s03_std_iterators2 = "03_std_iterators.rs" 98 22 98 27 + let%span s03_std_iterators3 = "03_std_iterators.rs" 98 19 98 20 + let%span s03_std_iterators4 = "03_std_iterators.rs" 98 40 98 41 + let%span s03_std_iterators5 = "03_std_iterators.rs" 98 36 98 41 + let%span s03_std_iterators6 = "03_std_iterators.rs" 98 33 98 34 + let%span s03_std_iterators7 = "03_std_iterators.rs" 98 4 98 7 + let%span s03_std_iterators8 = "03_std_iterators.rs" 98 4 98 7 + let%span s03_std_iterators9 = "03_std_iterators.rs" 97 16 97 80 + let%span s03_std_iterators10 = "03_std_iterators.rs" 96 16 96 76 + let%span s03_std_iterators11 = "03_std_iterators.rs" 95 16 95 78 + let%span s03_std_iterators12 = "03_std_iterators.rs" 94 16 94 34 + let%span s03_std_iterators13 = "03_std_iterators.rs" 98 4 98 7 + let%span s03_std_iterators14 = "03_std_iterators.rs" 98 4 98 7 + let%span s03_std_iterators15 = "03_std_iterators.rs" 99 30 99 31 + let%span s03_std_iterators16 = "03_std_iterators.rs" 100 22 100 28 + let%span s03_std_iterators17 = "03_std_iterators.rs" 101 22 101 54 + let%span s03_std_iterators18 = "03_std_iterators.rs" 102 22 102 54 + let%span s03_std_iterators19 = "03_std_iterators.rs" 91 21 91 26 + let%span s03_std_iterators20 = "03_std_iterators.rs" 90 10 90 44 let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span siter23 = "../../../../creusot-contracts/src/std/iter.rs" 159 27 159 48 let%span siter24 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span siter25 = "../../../../creusot-contracts/src/std/iter.rs" 161 26 161 62 - let%span s03_std_iterators26 = "03_std_iterators.rs" 89 8 89 60 - let%span s03_std_iterators27 = "03_std_iterators.rs" 82 8 82 58 + let%span s03_std_iterators26 = "03_std_iterators.rs" 86 8 86 60 + let%span s03_std_iterators27 = "03_std_iterators.rs" 79 8 79 58 let%span szip28 = "../../../../creusot-contracts/src/std/iter/zip.rs" 46 12 49 95 let%span siter29 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 257 19 257 35 @@ -2427,12 +2414,12 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] use seq.Seq - predicate equiv_reverse_range'0 [#"03_std_iterators.rs" 87 0 87 81] (s1 : Seq.seq t_T'0) (s2 : Seq.seq t_T'0) (l : int) (u : int) (n : int) + predicate equiv_reverse_range'0 [#"03_std_iterators.rs" 84 0 84 81] (s1 : Seq.seq t_T'0) (s2 : Seq.seq t_T'0) (l : int) (u : int) (n : int) = [%#s03_std_iterators26] forall i : int . l <= i /\ i < u -> Seq.get s1 i = Seq.get s2 (n - i) - predicate equiv_range'0 [#"03_std_iterators.rs" 80 0 80 65] (s1 : Seq.seq t_T'0) (s2 : Seq.seq t_T'0) (l : int) (u : int) + predicate equiv_range'0 [#"03_std_iterators.rs" 77 0 77 65] (s1 : Seq.seq t_T'0) (s2 : Seq.seq t_T'0) (l : int) (u : int) = [%#s03_std_iterators27] forall i : int . l <= i /\ i < u -> Seq.get s1 i = Seq.get s2 i @@ -2604,7 +2591,7 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] meta "compute_max_steps" 1000000 - let rec my_reverse'0 (slice:borrowed (slice t_T'0)) (return' (ret:()))= {[@expl:my_reverse 'slice' type invariant] [%#s03_std_iterators19] inv'3 slice} + let rec my_reverse'0[#"03_std_iterators.rs" 91 0 91 37] (slice:borrowed (slice t_T'0)) (return' (ret:()))= {[@expl:my_reverse 'slice' type invariant] [%#s03_std_iterators19] inv'3 slice} (! bb0 [ bb0 = s0 [ s0 = len'0 {slice.current} (fun (_ret':usize) -> [ &n <- _ret' ] s1) | s1 = bb1 ] | bb1 = s0 [ s0 = [ &old_v <- [%#s03_std_iterators0] Snapshot.new (view'0 slice) ] s1 | s1 = bb2 ] diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.rs b/creusot/tests/should_succeed/iterators/03_std_iterators.rs index 4b8892881c..2645742d88 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.rs +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.rs @@ -39,18 +39,15 @@ pub fn skip_take(iter: I, n: usize) { } pub fn counter(v: Vec) { - let mut cnt = 0; + let mut cnt: usize = 0; let x: Vec = v .iter() - .map_inv( - #[requires(cnt@ == (*_prod).len() && cnt < usize::MAX)] - #[ensures(cnt@ == old(cnt)@ + 1 && cnt@ == (*_prod).len() + 1 && result == *x)] - |x, _prod| { - cnt += 1; - *x - }, - ) + .map_inv(|x, _prod| { + proof_assert!(cnt@ == _prod.len()); + cnt += 1; + *x + }) .collect(); proof_assert! { x@.len() == v@.len() }; diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml index bdca7a90ee..1263a909a7 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml +++ b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml @@ -29,43 +29,40 @@ - - - - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz b/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz index 3ecf27ac9653667043d29a7928190d0a1c167c3e..b3b72740e7dcde61833c3eab55278468669a09ad 100644 GIT binary patch literal 6610 zcmV;@87<}?iwFP!00000|Lt2{ZyYz4eeYi(U?04@g8_K?%|*O`VWd$4cJi<@XzZK8 zB3X$rvgAmzlgzK*!>S^?s=B(>vK7a10;p|v6+bR7FV8*qlKt=hd2#=Pf0ynrKBT+* ztJ|CZy3iN@`5znq(to&0KfT~P=C9(8z4G6@^w;U;`-dO)FCK2+T-`kQ4{!eV>i=G_ z?Z#i-eDHTy{^sF@-qDZw>kGG|Z7EDEs2v|F*d5=N!nA_iiJ^ktiESxNE6`3375GkW zOJVacJYzexErmRp@6$sT_bzpB?$eKWs&@wOWBU2c_3igpVR&-szro{in)B*e0fFtz z_LYCRUSp;ne1|^X-QC9bA>HGv^?&)x4mzM6@yqE8Vk-}AuFB>;knrj4yN6#;n5kOq zXjFtkX1^x z1ihN5WM6&9>5R5Ju3n8sQA+1DyPQe-mr~|@ECt%;&fc`Q?{DJ$YK6<0E-32)kMQ6A zDR-8Sc*%3m+o(`Kjc+uZ}0AIe@gMi+kfu3!Q^&aU%vL?_U$`N0?!v! z1Zw3i@#ZQXyvS|$>pihQE~Z-PyVx56x0mD6V`|&&<=RY&axYIWA!=Z(%d${oY5#Jf zroavjr{5#zSjn)NI8~FNLzC$1WC8Mc59#jByW9J`Q+TdkMI6?@R=Mk!lhuCNWkFNQ z4asd^jc}D0^_zo*4#XI{tW~y~UWzw8PH)b_;c+;%QyIL~0eI&ZD~&!kNQw-S6|f6- zu?2RCie0K=ms(&Kuh=CkcIDCn-%Q0fQ}NBL;hUS{o2~d}E56x3@$Gr>t=}bo;@g*m zZzoWV_v^KUF3x7q#aZ3mK&e8}Sa~K2GZdK_zATWyGi31t$jUDcAZt+vrnd%bvu=EM zb>pvxFLEarFT?x0yOf)cucxs1_Wi>I76-E$aB+r_ymWGao_rX4eEvhayXp;eu+ueU zos4({Stm6XUSW@{RFO58%F_i8oTC|cu>S4z``#u;1P%9XP8}s zU_P{6hhV;dU_FIkb2-{8)I5dYHH*wpFXX6Ixj<-9lq$E6Vl{-|6|4CItHt(=eKFv$ zP@^#FD5MWEsk1Ep3E;l&MnQ2#Q?S_-Hm?ic^bc?T;s1&1xz=vS3RtrO)@(CW_1Q0E zyDy$m42XP#XL5nVul#?HF9I<6_1HjTtiS*B>RlO2t;Ozr)nP2!*|HS2j72-QJ{Det zc}^n7+7*X!ne~G zlot!#XQ#}2!Z3NoY2_ig(Sy%=0qq;jM$R(}*p0b+>}m_BpCuwP+d6!x`pRbB3s7-1 z^}+29=20M%%Kpe?0&c74iLdt6iqk~J;)G{abC)}@Mh^kRb~JvJCicD)x@-?|iY^L; z_d8)$Aqo3+0!a=vCzc^bd&~omL7iOf`m)Ngts<$6VA)QEs`Oh_jZoiK)`n_qDEf!P zW)gCxVSWsEQ8%Tm(Pnv=OOv>ZmCeQ`jG@|jWoGgiGm~q~toomw0i1zUhTEHX^>B52 zGp?xIsh!#BZ+~38y}b!(e4R6B?}27LBemG5m;0}7{?+c>v@-Qub@~9CEA#RdL1?xc zSAyVv_b$B4xTC+xZ`R`6>bL25EWF~k7YV;UXPEag^{!{S1KG+$vctw-Z0?dah&Lac+_ijs(!~VG|S9@Z!aN zy6#?FJpA%5T~v`bqYsAlzrTK{TcB@!AN?Ry)%?)Y@`*1yA^`*2DS z#532o_wVl#dqL3f3YX2EzjoBUzX^vOO}I!Ar~;x-{)*=+sqU%_<&O{Q|M4DB4E64b zN|oa-{rLV0LtXqE`-HA{QcOwEsac@vPRbs%u5K`rzrOlc_5yuJY(=i#_ow@G_rZ^H zl|G-M?|py6xd&XwY(qSy(}^0x?e%pE52x%xja_5h?(X*OEb^DKyqwTbdJf5Q*Tu_A z_^XLK?!WJ2je#;q@$E8tFN$6ykFcTqJ(eRc2AaHFR^Hc|ll8Tp_jPu1d88x3GivYn zR!ia_Hp_1p4?xilw5^6tk12X5)hQiA!ksh|4XZtml5U}4x1wS9?d6D{a?f8rMS{y` z=;PI5bDh=v)%xar^#lMJu&Y4*sWXs38#X6HybI7O+pm-~#DR2hB>g_Ux0 zT!1Yz=5u7p6YlF~n_4i2-lJ#oG!t1IJOOvuE!yhQhNg+5nk6@T*KUhvw|mF#ieGoj zL=x+h=9BL|eOxAxLFQI-!z-y8n&z(gv2;1Drg;`^!T5?I=~TLW(QKakt=VvTEL~1V z(&br@AzeN_R_#xTUiR#i)pw^e<79?l^F*kVneJ+4Jio|oS7RWWrpI{S#q@Zjgc?*Z zggOloEcpkW51B9_-9dO`a@4`ww-JF)hVhR|=(OA(o73H0f4 z;Y4Dphl9Kx4(8G%$?j^N$(5VQrgq#z$SU2F>*T8S=|H2neKd(j6?0) z6>;XW(B^PMjzUZ-tZd{>cYAjvaN5@_%z4pv-*wI!4Enq}f<92z>%3?qQTgdu%GqDN z&N<_u+E2UV)i&3+x9<*v*kRal7O^NPtL3b@m4;)BmlI(QWG;0vt=HM99+7!cE$3eN z0-ww4G4;Y(4ccMZlOmN+dg6?FDf^czo~ph?K(o0?Kc5V)YW%dBx?%dL!PdO-@P6u# zhn}iO-bXTrv+Qe*6IlwsN-Ab8uq#VQRYog;{Lc)3eX_8=>8{dse8cAAtP!lesq7OA zW8<@T(HVUWR#!`c()u&ZJ{HfB9f-Jga`4q4^wAuLZG^L70puS11n zUT&z+Tai0<2JD{W4ES|UH$LW&cap!(5&dHx8TGQrawQC&o)k;|F(<|Qr1Y_y-E{h9 zw=6fib6B#irTL9LUM_$0a`~IjPhv$qDX0ep^ZR_VFlbo_wA|n%XFKgQA}WY8ta z**nS{LzJ~M+v%$|pBqijlP7^of8I*t;m|zFp_PYjh|v~@w&l2$7RRmBAGhWsB-`Hr zoxU<_562Va#lcHCZk=4S%E!UmS}IS05`0@r<*CW0TTA7s&HJyG=CKY}B~;{UTT3OX zxxc;&sZgL2l?)GIUB?eQX4jVH4T~ApAR+L;eyl76yZ-Kd+AO~B(=(waT-fHjWvh7g z;VS>$;iCQJ;$P|Rwy#mzh5n91$>5;sT#{NZ2NUUggc7$O(p`6b`_m-DT$s{{*2@Wr z#e~FJ6WX_$4I@vEJZyt`R8^VUzpmb$K0a7&Cx>>o4?iGqdo&t5(ZzaPrplcHzkhUW z0*|Fss)|M&*bgxmlcq2BqUeJGYQ=qxm-RwWLE^!tho{5Fc>Dh0%!pARi5T_4x-X73 z#vM3|@cK+ZR`Q28cY{`DwI@T(9QQpvCmrlH z`*@3^o!fd=bkMCkRd-PKbb;n`>nDY^;+y-Q{82Ce%|g=UdHdP@&vMV-Ea&mbo#s9M zbNC@|?1>HWC-itQ(Yc5NE|0IK3!QI?t&GxlJB4hFQEdNUsKfAY0YQ(LPxxp_&gl9v z=@yeYo4lNvs5>^*{V913!O8sN7=(!dB}6Z^%~>nx$I~Wz?T#TE8%%A zZAxi4Dc%1HyH*kN7=OH*>Pm!;!e%U}%UMlTDlC3)tjm2=U6KG}?9RuSeSa`mDwuhe zz?M{$Em;CPhM+rlIjdRE;l^V)Rj+{O(#Y@Y1#i}0@Sdj;sOEr(A0!f{C(Q?GfE?|s zA-13A672(GeEE3%KLqfL+DC)y zq4p<}tIJjLbDU_29&;{N_)C91`y-M4s&93a)E-dOeAM_+BkhEE;!tSOXJW-i;a*AC zijP&z_><752+aE{-rRhO!2PczP6i^M=!({2;g4`ekH$-%>M@_g`8^tNt)Gi!WGcIC zuGNQ0#YvmkTg#BoK~Mb@aq@7KLV z$AEH8*?*lWtX_dW5eek6N6VghLqNGT(4g|} zLfb~0kMEx`%@Rw7$BtUjIOjH^p@Vha#uzP!q3Dh&E+ScrkOM!FVwnq9+Vtn1%Jffp# z9+Xli6;@7iXMmkfTE$x#v64o)C{sTufBtcUldWt;NWc~wLgFMv$Fxhzk;Crk;n6kD zHqJCoH%>K9=7wz|iK@Yq*3_o9gC}8JYcTvM6!X3R!Fa^rG?>K)E`w=&6h3&z@;i7B zmfaKEm>2|6hH9Uvm0m{e&{n9}ML{85Q1)YRWaoD16n1+joinbLNyN5QLW>lWVK$1; zqC+&wF0%KL=Xcz88vd1pNy2n_wQNY*ImVsyD#?hB(Mk4@aFImnNu76{(;TiZp`sx! zSv1P0l(-Mxb_r_bSq{+=AVSV8=o1ClBO_2TE<;Y7uO~C*~YCrd6njeF&Zd zszl&Q1hPcjJ`|-@Pj;pNET6Bp?2JNbp2i34d>R|9zz!pIj30x6O;8zi#vqC20 zOcab;r-cnBBWovF3V~-c0&m6IdzqkfY|6+lCovQfP+ybJ)nomVcCctzoD>TG%WC?^u4Dj5vIO=gtlx>d0i(e+5kL7EAn6@gz72o@oXBb}pO z^b4v*;93N-MPOS5x<%ky1j0pNTm;HR;9LaKMM`cIM`*6#v!pgjAudc^3&s$nPtgM? zE(p;TnLHqWwn0e%^&*1Y^Sz z3jQT}Fa!kLh=(HH%E$%*5S9FzLPV_`W6nDkJMDe)5kx8(#VkBvt04p;GC0LwU62lj zuUU422z;%K%4lb!7TCxZQHC0|fd-)U2KBoV~&OBB9?kRh~EJH%9oz=gF!gMDPWk;734pM_Ol>;$+nl1U9S7nTc16x)tP z2PfBR1KxrOSO{yr=t;B=qkDuEt@JIN48eA^lAgmMf{TX>P7K1jFMc8_cp;NbAdATe z*LrZXx7g-XbWscxR+cXzUPzW>{{|R`kl>BB=5B8K$=A75=Y$Hde(uU zs%R*=*atyeU{c)ut|v;eb*{s7!48BGBtX2JP~3?mc{FyMX#UXeezH-fWW2K8bFW+M zLx5+bAUmmi$H3ybzyw6Ta3Q{m2?xfam55H6Z#Dd%SFBASBuQYsAv`9Gi3$BxO&T1f z;~co;oq#i;K$3zLh|o+clVg}PCL`=uH*thc$+RS#3oZyHq=;}ih^At63}JpgzvdG2 z%v9kknRALJseIi6Y*a?p=9^1OfyD{%Yo^UGXa3dAn;QdB2>w_5E=uN-&L_$)O4S82 z-7s(QRnEP&fydTM!>pE|_AdD7B3GcmtrnIIIS!()Rsm5&MjZp1wXx;-P&1#E>trOC zU5v3FDt^sMFj10sPFdi4t5Uv2(SflsrKM2Xx$ywge)WogzYCz@)>v?GOSf8$>-gF0A)xrt;kmz1Kgg82r+|iu|Zmg8L-X_IU}k5KnhU+hXk~+tp;Fv1BdB# zGy(ytlI@U(lKKy&6y_PU(RS2nAzLDD1vrv-(zV=D8;9JMWq&H>PsNO!gH)1Q2PZ(T ztYba~?GZ_3-ocdQgJO*P!zo60Oi(_q?kH-KPIMyc2?dvou%pF5fM-z*Ccuq)7Ugh* zcKO1`L_yr-o4Hh##GxP#1#u{d>-;MTj0pvCD2PKr917x45Ql;|6vUw*4h3%{O6~6(V2GZ-pI|mo+|IBl=T`he}NO z_JmXce{Cln?|8l^fXH7PjxgU0IetrjNZex4wM=junb94%Vbls_nJ1rw<83!2YIBP3 QcR08I2N54D=8Ap*0J+~G4gdfE literal 6595 zcmV;!89e46iwFP!00000|LuEOj~q9a?tA`<1m>ac9bo{Th1e!a(H-n`0*@^|MTzL#~=Lr{J8y?A0GGj zcmKIn+kgMR8~@sW+~=RJun~Tr8u7+|_uAj)yYHWVI5a%n-|X+6{KuRBdGr6T#BSsF zcOU)3-rqf4sRn+mKd)>9yP+`cARFvDmN==~c0*y>0UGW)V8gqiuzBk0 zL?d@Yp)Th8{8ZU}$mQlS|9B-D)o8!JOZn%U+xzeLv8%cE-!*zz=Dd3qKopJMz45Qt zd(6Zm8nxT__Ye2!L(Gp?qA~u}tHw3}4dC^(0mMqBsa?gK0+7$|-aq}b0h)=L8t4Tf z8|WobOVd8sfb9Bk1HEKwY1&6Lpt?TLfZC0v&D$sc_U5nmclk;T#EpM@^SAqV`ARem z=x!7>pm$?w^Vh%n*N0vt8Z^7fJvY)D6l8)%9B+@87+@%}+Tk zyHJC=9*LWMI%=q65BojQKcuNtS`r5(Ky%%1J(}HacfGcfLAclFx3EEOkgkV~>Pv^l ziI}1|R-E>XT%sl2VL}*H0*+Op?Nb@3^F8HvR^`v0!KC;;D|JdcB-A*ym71slr zLLCTp_oj!dx~bnCZFB@7#P!%^w`sY!X>odU5f1m$$wpT2mPg=S8&(GW+8{|4BuBs= zuuCkki$?5{BX-FJcHxL!JYrWZE$~f`_@+mE(`)!&C4b`E z*Mx6pPz~GtT0$3!8FZl-Pd7GVFww+NM}uWZ)iQiNKmu0C!XwD44M&i*=p!0hgS8nM zU-ozYw)?>iFB;>AhlgB;_svsSeD~pL0*jqmb+|agNF0b9p(l28_w_&IhkdJ{ot~~C z>tx0g$U5ngz zUP5zJtk(A+2%PSGr|skTqd|uS@C^SzAI8)bOnXv`Ts`wk2!=U~susiKIS9rIvuhBH z-Pm;q#svhcDFo~5USCnqAb3q9E7TMBQso6g(;!sdJ&V=UAdXm#3#_Ky1?Qr}VUj&F z@+72pJjshR{u97`{Tc;3sDi1guz5S!oBrwM@BSb8O4MFWBL=V*16Yeq*VWg1q3Zo` zGg61hcUPj}1rERQ|J64{vFqoeM){|kzx`wXewa(H`R;AkZZ2rduoY&Q3mUsV7c@4` zV-nTZ9>GtH;3w7$K%5$YFajxzKnfGz9IJ2s>Qw{PCE3uLc?b=eUilj`6Mb(;4abAdnTsSF zQVr=0}manX8z7jxfSBWNG)?s999ng+!6;isMdG>x5hhW4mVE3koTm#;7av(q?? z81)g~mnIx>~D%?&IzK^Zw&yL#vl@dH=&5a7N;jQH!lwkAk%Dy)Z9&NdK<3tOYto z!wpUcLsks8MZ~ua8dorf*7le}uvn=C(;@!?-G{g_(xQP|*q0s1&&jK`O74(Qf{JSGXT^pw^jPeeLF*e}A*T`*@BKI*kgwGgD2!kx=Xspc|Iw zWZbZ7SWhG@54RiJg@o;jgzaChd;H{s0sAE!T)zN~H;cn{(eO9xhxg4V07%bA4<8cN z;iGbMKn@9w#KAPbgv&lpEqB+4kSEIuKZ6g$JjoX^4*@+M0>y{ERi_pfLwloF>v_g9 z9o0aC&0?(Tb!Zwn9MdHFaJ8G^W;ch6-46GCsIZvBU42B875njBb()xk7* zfv55%uo~xEjBQ}dm%zDv$zs?%_&=sY;JJJWoXD3{M!I~-G_T&K317GFi5T0?r$#_` z(S|d=Zgq85QzNyZj$L(vVHzLBmc%qaHu#z_U;8dPv*!tF| z8}lr%$g@B_MBhykEh}?=YWf9^BXlrE=-~47i+{TLfBx?KE(RC-CnDoQR`N2(1NvEy z8?I|~Y+P$Rq-f?5zG*ON4O8F^$fX&G%j{RS3jM{AYP`Th$k1IsYWpiJ|{e)KGmc@>NMmsEJ zz9|vJCJ%BsWwlMu^L{GgL$s{pdkC{lNG|N@<;VubbZDE|n;H&te-e(l_m7pOF&X%{ z@Wod-fx(?RcuEH|I*LhPu=kvfWj3CH)0Xc1kn~d>#trPud4bLGf$W)>bXYman{xkf z!f`tE94zO>*aPVrHR$BIKY>0Q|N3p+wBAtp=~T|a@88y>LD%i4=5)8s?fw1xV<)zo zwqHdWgjB_H(b|TA{fO5SW{!9s`Zg%u)=TvS&y#L7_JRw19-8~m3yRTcFZ;Vm5jMxS zRLf=CxN=jCjeegtclqbD&eiBYZKl^SeAZ-Zw{h1#y^lLeLO062J^X7 zcL@*mOv-a-@**O0D|_InORVKv#eJW@$lk_ zcylHZzslBgbB+o1Lpp4dW#?Jt>$eS`y6f63zkS>Asavk=&}xxA^$5Ve#3O*WHQe~z zh1@W{tsebzH*&*RS>_ctc=}X;@pGOE9D>rPp7z7}r~N!U?XPahZY<58Y~t|xABWff zI8VjXm?;<&1@i};JXp{?7|?u(`;X5+*!eNZrQ zT-t;?^x46=mjf%6w)4>zS^FX14vTy{wE6a$LNe_W;AxXytL&c;ED|q6zJ2n}uD%D@ zjisShHHf>hG}P*jy8}@XzhP^22@GV;C3P zM=nDIC+$DZIT`y^XCi-}AGY@&^Fz74|7j9o9xSCZqn8V!#e(Rf1sz7srs1-gaX0S%>4*IAyf=1+#JXQ5hesv;P<3hn&xKS*5%oB5m}1T*OdAfY zsG|wSj)xwv#}{D(5_dY?)piHt-G`?OJw|oHV^l}`zDR5ICvfKBwUK}-jXkPq+c`sb+qSNy{(M9S47iq}S z?|xo8;G8nRMcOb@-zVHW{^U>I^4~2uUFO>_ray~4f45x67Za^#{O9;XJ=hZ+!cU-hw9q+= z9WM7x(~YjL#8zf$$xb2L@6(|BM^hcUe+vkDMt$OEb8-Rc=eS!e=3?XJ!a&`z+Mm&u zb89_uw_Pl%OKqV`*7dCQa8Vrc5_f&{@#|U|SUB)Q2ty3+c`a>*QkN+`e1<=Ep}CLW zKTfuThi;qBU%ax7yq@)xLx;r&=W2M6tcD;!@4I8~vmX+JLkB&N5||+rWriq$>0Qvq zUe9`tdAL3eC&zC9YH4%Gu8yT;7y-r@5a3ZDVVY?^3IkMcUv|FzJeHu=D!I>!FFyh3 zg9-L13{dm4&_=0v{$LZ=D*KnCN1p)n!35ba4Qh05ENzDHfgS@1{pG3K4_}AUW(XbF zF^FL2K?D-x)ATXnOoNrsevLZoJ$*6Sxy#qj`~RH-zvz9^x$b&@v2k_1YW$oww5Y|L z>lOQ@eV_lC$i8n!oiu8XOw^ic{H&Q8qEDQvA!;MB^jWw!glp+@Mbm#1{3#4$`@|dd zmoVIZCUe#i`NFGc%@_WR%jj8u=}T|Sm$>|%b-32^VilQ&Q?`;9Yk_NZWcx6uAo77QM=-2~ z)IljFI2OfQU!fO0I}`;<%&*~SosAr(W)C6}$TPMOcA zUo2}R$u<{;;Jq*8H7BEl@gWwu)#$Wv8tT8FJxio$6blg2u(df;wmx$NYY?*#wAIpS zcACC;A_c%I`5289Qsfk)%*p#m#Z!`YtF_bWW#$6wmBvuC)}D$-&)O)m(xV_Hv)UTr zv~}9N*o;1VmP$jAf=TCGqOjFUV_s%P!6XxBlMLyQl3>p&O>LOT%3fshVFrA!V4IuNkYDH1@=RD6cOo|Cd5EXh<7 zLCjlduR^$(pp}qKVQaMwoGFDMNl{K&3zH~@Er4`TxvbahClC%r6~#b0lP*^0Xku2@ z3bfYC%xMeto(1Ee-m;)RiFheiAu5wWXbs3BY3Xy$=%Y6!`z;_ksCPL+_y2{2lM<$6 zDVlx~`^6J^ zzz8|ivz9`PJ_~D6>mWf;pdhzEMN%24GtPjd z1JVvi^=1C-`4~zF5TXqLMtOi3t$-4PwK8iChxyEl&MS>pib@tNN(wU9NmYpg3Rq?2aiQl zk*H)TF;EdCJs6EWb5i_f43f%57|ark_9Z4SGIJ0hqK~QCwJmx`bRc{5_zjtjg;Vxy zWDY7QWjIP^jM;l;m4xcd1p0M(Ql_A^l(R;T8U+X~6{;Xppk!MlM8gg=I?&)i3kS+N zP{x6(p0jeGqyxnc6gg1nK!F2QWo;eEsvz2dR1T!vNYp|~X$mWyr3Rl%$jV0cIeBgM z7PNGr>xA@TlL8f0QqU?}#R|cvB+){QtWvbeZovo#+B(q2fvzC|^`Z;})+Mrq2r>gD zPZ(6n#c~44oJ7ZffnSt~q@)$XdMi><-e;fC$E>9=GNhm?6Xd|)FV0BeD3z#}ph?Ma zl3H1l6bXZdWxeuSX=n#VIWW>etAM{8L!7;am>?)FDwQMz1xSf0Q%GRUVS9c>rc_cG zJ(%oOB9*N75Tan=buk8+=iBuwGKNAK#fE~)hNwszDTf@rjhql`w9Zy()%cqERT(oz zb2R8nvR+xihEfEJhD5fch2DZi2Nr%4<}_NJSz@+qqD9hH8}v4jCqvP~7A!lk^qVnQ zsDuQPytPRO3M4~Dp+f;tN|EXqu1tPKOe?541z?OCQ&uVG0!Bgh zY#DvQmT9cE*;mH6iBe${Qjzl33Y8d4NV$f4K%&Ae3h7YrSIKFitO_DTOU95= z0;;)D-O(+I%B=co7l2Z;U}Z!ig9O&5P(-pN)!>ZRuti}V3iDMjB3Q7>qY8n207;;8 zRFXYP%t>P0B7j2>U;RR4^u*cZ1R-m(!6#DLO06SimO8Z&6$IlDv_nu1K{~8XRE@0m z&Kd%K6^rp2B}EMsJz1}978qot63A#xIk(XnY_q25u;xusI0XB zA{mFIzo|thTMD8l=`B&t5P=~Y0wf(cTd_qJ4#|FV3lA8x4nWpM8%YvVlA;tFQnCUp z)dV&&I;^I`H?roObe2ZOg2HeTp}u^Q5(Nd^MXjWMDNLH!%Pai%*G2$(R$G+Ch} zhb|7q`VS=(;e`n*6ex-~0HC3itha0f8VIS2Z5jAeFndy&Rw`NoU5phzMdhsu z)$S0Iu@{W^!wE(eK~U4x1(E``RH({{E!nKe^cth>%Lqnmhg!Xea8OH!^})wPK&Z)K zE0|75sOy}cDs(_bC$sjXkpUGk diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.coma b/creusot/tests/should_succeed/iterators/06_map_precond.coma index fc4f164875..72a38ffbac 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.coma +++ b/creusot/tests/should_succeed/iterators/06_map_precond.coma @@ -674,7 +674,7 @@ module M_06_map_precond__qyi16809708214464407778__next [#"06_map_precond.rs" 65 meta "compute_max_steps" 1000000 - let rec next'0 (self:borrowed (t_Map'0)) (return' (ret:t_Option'1))= {[@expl:next 'self' type invariant] [%#s06_map_precond4] inv'2 self} + let rec next'0[#"06_map_precond.rs" 65 4 65 44] (self:borrowed (t_Map'0)) (return' (ret:t_Option'1))= {[@expl:next 'self' type invariant] [%#s06_map_precond4] inv'2 self} (! bb0 [ bb0 = s0 [ s0 = {inv'0 (self.current).t_Map__iter'0} @@ -1346,7 +1346,7 @@ module M_06_map_precond__map [#"06_map_precond.rs" 178 0 181 14] meta "compute_max_steps" 1000000 - let rec map'0 (iter:t_I'0) (func:t_F'0) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond1] inv'0 iter} + let rec map'0[#"06_map_precond.rs" 178 0 181 14] (iter:t_I'0) (func:t_F'0) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond1] inv'0 iter} {[@expl:map 'func' type invariant] [%#s06_map_precond2] inv'1 func} {[@expl:map requires #0] [%#s06_map_precond3] forall e : t_Item'0, i2 : t_I'0 . produces'0 iter (Seq.singleton e) i2 -> precondition'0 func (e, Snapshot.new (Seq.empty : Seq.seq t_Item'0))} @@ -1445,21 +1445,30 @@ module M_06_map_precond__identity [#"06_map_precond.rs" 185 0 185 37] use prelude.prelude.Snapshot - predicate postcondition_once'0 (self : ()) (args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0))) (result : t_Item'0) - - = - let (x, _3) = args in true - predicate resolve'5 (_1 : ()) = true predicate unnest'0 (self : ()) (_2 : ()) = true + let rec closure0'0[#"06_map_precond.rs" 186 14 186 20] [@coma:extspec] (_1:borrowed ()) (x:t_Item'0) (_3:Snapshot.snap_ty (Seq.seq t_Item'0)) (return' (ret:t_Item'0))= bb0 + [ bb0 = s0 [ s0 = -{resolve'1 _1}- s1 | s1 = [ &_0 <- x ] s2 | s2 = bb1 ] | bb1 = return' {_0} ] + [ & _0 : t_Item'0 = any_l () | & _1 : borrowed () = _1 | & x : t_Item'0 = x ] + [ return' (result:t_Item'0)-> return' {result} ] + + + predicate postcondition_once'0 (self : ()) (args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0))) (result : t_Item'0) + + = + let (x, _3) = args in exists __bor_self : borrowed () . closure0'0'post'return' __bor_self x _3 result + /\ __bor_self.current = self + predicate postcondition_mut'0 (self : ()) (args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0))) (result_state : ()) (result : t_Item'0) = - (let (x, _3) = args in true) /\ unnest'0 self result_state + (let (x, _3) = args in exists __bor_self : borrowed () . closure0'0'post'return' __bor_self x _3 result + /\ __bor_self.current = self /\ __bor_self.final = result_state) + /\ unnest'0 self result_state function fn_mut_once'0 (self : ()) (args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0))) (res : t_Item'0) : () @@ -1481,15 +1490,6 @@ module M_06_map_precond__identity [#"06_map_precond.rs" 185 0 185 37] axiom postcondition_mut_unnest'0_spec : forall self : (), args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0)), res_state : (), res : t_Item'0 . ([%#sops18] postcondition_mut'0 self args res_state res) -> ([%#sops19] unnest'0 self res_state) - let rec closure0'0 (_1:borrowed ()) (x:t_Item'0) (_3:Snapshot.snap_ty (Seq.seq t_Item'0)) (return' (ret:t_Item'0))= {[@expl:closure 'x' type invariant] [%#s06_map_precond1] inv'2 x} - (! bb0 [ bb0 = s0 [ s0 = -{resolve'1 _1}- s1 | s1 = [ &_0 <- x ] s2 | s2 = bb1 ] | bb1 = return' {_0} ] ) - [ & _0 : t_Item'0 = any_l () | & _1 : borrowed () = _1 | & x : t_Item'0 = x ] - - [ return' (result:t_Item'0)-> {[@expl:closure result type invariant] [%#s06_map_precond2] inv'2 result} - {[@expl:closure unnest] unnest'0 _1.current _1.final} - (! return' {result}) ] - - predicate inv'1 (_1 : t_I'0) predicate inv'3 (_1 : ()) @@ -1501,7 +1501,7 @@ module M_06_map_precond__identity [#"06_map_precond.rs" 185 0 185 37] use prelude.prelude.Snapshot predicate precondition'0 (self : ()) (args : (t_Item'0, Snapshot.snap_ty (Seq.seq t_Item'0))) = - let (x, _3) = args in true + let (x, _3) = args in forall __bor_self : borrowed () . __bor_self.current = self -> closure0'0'pre __bor_self x _3 predicate completed'0 [#"common.rs" 11 4 11 36] (self : borrowed t_I'0) @@ -1583,7 +1583,7 @@ module M_06_map_precond__identity [#"06_map_precond.rs" 185 0 185 37] meta "compute_max_steps" 1000000 - let rec identity'0 (iter:t_I'0) (return' (ret:()))= {[@expl:identity 'iter' type invariant] [%#s06_map_precond0] inv'1 iter} + let rec identity'0[#"06_map_precond.rs" 185 0 185 37] (iter:t_I'0) (return' (ret:()))= {[@expl:identity 'iter' type invariant] [%#s06_map_precond0] inv'1 iter} (! bb0 [ bb0 = s0 [ s0 = [ &_4 <- () ] s1 @@ -1600,51 +1600,49 @@ module M_06_map_precond__identity [#"06_map_precond.rs" 185 0 185 37] end module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] - let%span s06_map_precond0 = "06_map_precond.rs" 202 8 203 71 + let%span s06_map_precond0 = "06_map_precond.rs" 197 8 198 71 let%span s06_map_precond1 = "06_map_precond.rs" 193 42 193 46 let%span s06_map_precond2 = "06_map_precond.rs" 189 11 189 156 let%span s06_map_precond3 = "06_map_precond.rs" 190 11 191 63 - let%span s06_map_precond4 = "06_map_precond.rs" 198 24 198 25 - let%span s06_map_precond5 = "06_map_precond.rs" 196 19 196 27 - let%span s06_map_precond6 = "06_map_precond.rs" 197 18 197 33 - let%span s06_map_precond7 = "06_map_precond.rs" 179 4 179 8 - let%span s06_map_precond8 = "06_map_precond.rs" 180 4 180 8 - let%span s06_map_precond9 = "06_map_precond.rs" 172 11 174 65 - let%span s06_map_precond10 = "06_map_precond.rs" 175 11 175 38 - let%span s06_map_precond11 = "06_map_precond.rs" 176 11 176 48 - let%span s06_map_precond12 = "06_map_precond.rs" 181 5 181 14 - let%span s06_map_precond13 = "06_map_precond.rs" 177 10 177 75 - let%span s06_map_precond14 = "06_map_precond.rs" 44 8 58 9 - let%span s06_map_precond15 = "06_map_precond.rs" 123 12 126 47 - let%span s06_map_precond16 = "06_map_precond.rs" 111 12 116 71 - let%span s06_map_precond17 = "06_map_precond.rs" 11 4 13 36 - let%span s06_map_precond18 = "06_map_precond.rs" 30 14 30 45 - let%span s06_map_precond19 = "06_map_precond.rs" 28 4 28 10 - let%span s06_map_precond20 = "06_map_precond.rs" 35 15 35 32 - let%span s06_map_precond21 = "06_map_precond.rs" 36 15 36 32 - let%span s06_map_precond22 = "06_map_precond.rs" 37 14 37 42 - let%span s06_map_precond23 = "06_map_precond.rs" 33 4 33 10 - let%span scommon24 = "common.rs" 14 14 14 45 - let%span scommon25 = "common.rs" 18 15 18 32 - let%span scommon26 = "common.rs" 19 15 19 32 - let%span scommon27 = "common.rs" 20 14 20 42 - let%span sresolve28 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sops29 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 - let%span sops30 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 - let%span sops31 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 - let%span sops32 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 - let%span sops33 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 - let%span sops34 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 - let%span sops35 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 - let%span s06_map_precond36 = "06_map_precond.rs" 87 12 90 63 - let%span s06_map_precond37 = "06_map_precond.rs" 165 12 167 73 - let%span s06_map_precond38 = "06_map_precond.rs" 95 14 95 81 - let%span s06_map_precond39 = "06_map_precond.rs" 98 12 104 88 + let%span s06_map_precond4 = "06_map_precond.rs" 194 38 194 39 + let%span s06_map_precond5 = "06_map_precond.rs" 179 4 179 8 + let%span s06_map_precond6 = "06_map_precond.rs" 180 4 180 8 + let%span s06_map_precond7 = "06_map_precond.rs" 172 11 174 65 + let%span s06_map_precond8 = "06_map_precond.rs" 175 11 175 38 + let%span s06_map_precond9 = "06_map_precond.rs" 176 11 176 48 + let%span s06_map_precond10 = "06_map_precond.rs" 181 5 181 14 + let%span s06_map_precond11 = "06_map_precond.rs" 177 10 177 75 + let%span s06_map_precond12 = "06_map_precond.rs" 44 8 58 9 + let%span s06_map_precond13 = "06_map_precond.rs" 123 12 126 47 + let%span s06_map_precond14 = "06_map_precond.rs" 111 12 116 71 + let%span s06_map_precond15 = "06_map_precond.rs" 11 4 13 36 + let%span s06_map_precond16 = "06_map_precond.rs" 30 14 30 45 + let%span s06_map_precond17 = "06_map_precond.rs" 28 4 28 10 + let%span s06_map_precond18 = "06_map_precond.rs" 35 15 35 32 + let%span s06_map_precond19 = "06_map_precond.rs" 36 15 36 32 + let%span s06_map_precond20 = "06_map_precond.rs" 37 14 37 42 + let%span s06_map_precond21 = "06_map_precond.rs" 33 4 33 10 + let%span scommon22 = "common.rs" 14 14 14 45 + let%span scommon23 = "common.rs" 18 15 18 32 + let%span scommon24 = "common.rs" 19 15 19 32 + let%span scommon25 = "common.rs" 20 14 20 42 + let%span sresolve26 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sops27 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 + let%span sops28 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 + let%span sops29 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 + let%span sops30 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 + let%span sops31 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 + let%span sops32 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 + let%span sops33 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 + let%span s06_map_precond34 = "06_map_precond.rs" 87 12 90 63 + let%span s06_map_precond35 = "06_map_precond.rs" 165 12 167 73 + let%span s06_map_precond36 = "06_map_precond.rs" 95 14 95 81 + let%span s06_map_precond37 = "06_map_precond.rs" 98 12 104 88 use prelude.prelude.Borrow predicate resolve'3 (self : borrowed ()) = - [%#sresolve28] self.final = self.current + [%#sresolve26] self.final = self.current predicate resolve'1 (_1 : borrowed ()) = resolve'3 _1 @@ -1653,70 +1651,56 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] use prelude.prelude.Intrinsic - use prelude.prelude.UInt32 - - use prelude.prelude.Int - use seq.Seq use prelude.prelude.Snapshot - predicate postcondition_once'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) = - [%#s06_map_precond6] let (x, _3) = args in UInt32.to_int result = UInt32.to_int x + 1 - predicate resolve'5 (_1 : ()) = true predicate unnest'0 (self : ()) (_2 : ()) = true + let rec closure0'0[#"06_map_precond.rs" 194 22 194 33] [@coma:extspec] (_1:borrowed ()) (x:uint32) (_3:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= bb0 + [ bb0 = s0 + [ s0 = -{resolve'1 _1}- s1 + | s1 = UInt32.add {x} {[%#s06_map_precond4] (1 : uint32)} (fun (_ret':uint32) -> [ &_0 <- _ret' ] s2) + | s2 = return' {_0} ] + ] + [ & _0 : uint32 = any_l () | & _1 : borrowed () = _1 | & x : uint32 = x ] + [ return' (result:uint32)-> return' {result} ] + + + predicate postcondition_once'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) = + let (x, _3) = args in exists __bor_self : borrowed () . closure0'0'post'return' __bor_self x _3 result + /\ __bor_self.current = self + predicate postcondition_mut'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result_state : ()) (result : uint32) = - (let (x, _3) = args in UInt32.to_int result = UInt32.to_int x + 1) /\ unnest'0 self result_state + (let (x, _3) = args in exists __bor_self : borrowed () . closure0'0'post'return' __bor_self x _3 result + /\ __bor_self.current = self /\ __bor_self.final = result_state) + /\ unnest'0 self result_state function fn_mut_once'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res : uint32) : () - axiom fn_mut_once'0_spec : forall self : (), args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops35] postcondition_once'0 self args res + axiom fn_mut_once'0_spec : forall self : (), args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops33] postcondition_once'0 self args res = (exists res_state : () . postcondition_mut'0 self args res_state res /\ resolve'5 res_state) function unnest_trans'0 (self : ()) (b : ()) (c : ()) : () - axiom unnest_trans'0_spec : forall self : (), b : (), c : () . ([%#sops32] unnest'0 self b) - -> ([%#sops33] unnest'0 b c) -> ([%#sops34] unnest'0 self c) + axiom unnest_trans'0_spec : forall self : (), b : (), c : () . ([%#sops30] unnest'0 self b) + -> ([%#sops31] unnest'0 b c) -> ([%#sops32] unnest'0 self c) function unnest_refl'0 (self : ()) : () - axiom unnest_refl'0_spec : forall self : () . [%#sops31] unnest'0 self self + axiom unnest_refl'0_spec : forall self : () . [%#sops29] unnest'0 self self function postcondition_mut_unnest'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res_state : ()) (res : uint32) : () - axiom postcondition_mut_unnest'0_spec : forall self : (), args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : (), res : uint32 . ([%#sops29] postcondition_mut'0 self args res_state res) - -> ([%#sops30] unnest'0 self res_state) - - let rec closure2'0 (_1:borrowed ()) (x:uint32) (_3:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= {[@expl:closure requires] [%#s06_map_precond5] UInt32.to_int x - <= 15} - (! bb0 - [ bb0 = s0 - [ s0 = -{resolve'1 _1}- s1 - | s1 = UInt32.add {x} {[%#s06_map_precond4] (1 : uint32)} (fun (_ret':uint32) -> [ &res1 <- _ret' ] s2) - | s2 = [ &res <- res1 ] s3 - | s3 = [ &_0 <- res ] s4 - | s4 = return' {_0} ] - ] - ) - [ & _0 : uint32 = any_l () - | & _1 : borrowed () = _1 - | & x : uint32 = x - | & res : uint32 = any_l () - | & res1 : uint32 = any_l () ] - - [ return' (result:uint32)-> {[@expl:closure ensures] [%#s06_map_precond6] UInt32.to_int result - = UInt32.to_int x + 1} - {[@expl:closure unnest] unnest'0 _1.current _1.final} - (! return' {result}) ] - + axiom postcondition_mut_unnest'0_spec : forall self : (), args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : (), res : uint32 . ([%#sops27] postcondition_mut'0 self args res_state res) + -> ([%#sops28] unnest'0 self res_state) type t_U'0 @@ -1737,36 +1721,36 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] function produces_trans'1 [#"common.rs" 21 4 21 91] (a : t_U'0) (ab : Seq.seq uint32) (b : t_U'0) (bc : Seq.seq uint32) (c : t_U'0) : () - axiom produces_trans'1_spec : forall a : t_U'0, ab : Seq.seq uint32, b : t_U'0, bc : Seq.seq uint32, c : t_U'0 . ([%#scommon25] produces'1 a ab b) - -> ([%#scommon26] produces'1 b bc c) -> ([%#scommon27] produces'1 a (Seq.(++) ab bc) c) + axiom produces_trans'1_spec : forall a : t_U'0, ab : Seq.seq uint32, b : t_U'0, bc : Seq.seq uint32, c : t_U'0 . ([%#scommon23] produces'1 a ab b) + -> ([%#scommon24] produces'1 b bc c) -> ([%#scommon25] produces'1 a (Seq.(++) ab bc) c) function produces_refl'1 [#"common.rs" 15 4 15 27] (self : t_U'0) : () - axiom produces_refl'1_spec : forall self : t_U'0 . [%#scommon24] produces'1 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'1_spec : forall self : t_U'0 . [%#scommon22] produces'1 self (Seq.empty : Seq.seq uint32) self use prelude.prelude.Snapshot predicate precondition'0 (self : ()) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) = - [%#s06_map_precond5] let (x, _3) = args in UInt32.to_int x <= 15 + let (x, _3) = args in forall __bor_self : borrowed () . __bor_self.current = self -> closure0'0'pre __bor_self x _3 predicate completed'0 [#"common.rs" 11 4 11 36] (self : borrowed t_U'0) predicate next_precondition'0 [#"06_map_precond.rs" 85 4 85 74] (iter : t_U'0) (func : ()) (produced : Seq.seq uint32) = - [%#s06_map_precond36] forall e : uint32, i : t_U'0 [produces'1 iter (Seq.singleton e) i] . produces'1 iter (Seq.singleton e) i + [%#s06_map_precond34] forall e : uint32, i : t_U'0 [produces'1 iter (Seq.singleton e) i] . produces'1 iter (Seq.singleton e) i -> precondition'0 func (e, Snapshot.new produced) use seq.Seq predicate preservation'0 [#"06_map_precond.rs" 109 4 109 45] (iter : t_U'0) (func : ()) = - [%#s06_map_precond16] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed (), b : uint32, i : t_U'0 . unnest'0 func f.current + [%#s06_map_precond14] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed (), b : uint32, i : t_U'0 . unnest'0 func f.current -> produces'1 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition'0 f.current (e1, Snapshot.new s) -> postcondition_mut'0 f.current (e1, Snapshot.new s) f.final b -> precondition'0 f.final (e2, Snapshot.new (Seq.snoc s e1)) predicate reinitialize'0 [#"06_map_precond.rs" 121 4 121 29] (_1 : ()) = - [%#s06_map_precond15] forall iter : borrowed t_U'0, func : () . completed'0 iter + [%#s06_map_precond13] forall iter : borrowed t_U'0, func : () . completed'0 iter -> next_precondition'0 iter.final func (Seq.empty : Seq.seq uint32) /\ preservation'0 iter.final func type t_Map'0 = @@ -1776,17 +1760,17 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] predicate preservation_inv'0 [#"06_map_precond.rs" 96 4 96 73] (iter : t_U'0) (func : ()) (produced : Seq.seq uint32) = - [%#s06_map_precond39] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed (), b : uint32, i : t_U'0 [produces'1 iter (Seq.snoc (Seq.snoc s e1) e2) i, postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b] . unnest'0 func f.current + [%#s06_map_precond37] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed (), b : uint32, i : t_U'0 [produces'1 iter (Seq.snoc (Seq.snoc s e1) e2) i, postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b] . unnest'0 func f.current -> produces'1 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) -> postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b -> precondition'0 f.final (e2, Snapshot.new (Seq.snoc (Seq.(++) produced s) e1)) - axiom preservation_inv'0_spec : forall iter : t_U'0, func : (), produced : Seq.seq uint32 . [%#s06_map_precond38] produced + axiom preservation_inv'0_spec : forall iter : t_U'0, func : (), produced : Seq.seq uint32 . [%#s06_map_precond36] produced = (Seq.empty : Seq.seq uint32) -> preservation_inv'0 iter func produced = preservation'0 iter func predicate invariant'0 [#"06_map_precond.rs" 163 4 163 30] (self : t_Map'0) = - [%#s06_map_precond37] reinitialize'0 () + [%#s06_map_precond35] reinitialize'0 () /\ preservation_inv'0 self.t_Map__iter'0 self.t_Map__func'0 (Snapshot.inner self.t_Map__produced'0) /\ next_precondition'0 self.t_Map__iter'0 self.t_Map__func'0 (Snapshot.inner self.t_Map__produced'0) @@ -1798,15 +1782,15 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] | {t_Map__iter'0 = iter ; t_Map__func'0 = func ; t_Map__produced'0 = produced} -> inv'1 iter end) - let rec map'0 (iter:t_U'0) (func:()) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond7] inv'1 iter} - {[@expl:map 'func' type invariant] [%#s06_map_precond8] inv'2 func} - {[@expl:map requires #0] [%#s06_map_precond9] forall e : uint32, i2 : t_U'0 . produces'1 iter (Seq.singleton e) i2 + let rec map'0 (iter:t_U'0) (func:()) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond5] inv'1 iter} + {[@expl:map 'func' type invariant] [%#s06_map_precond6] inv'2 func} + {[@expl:map requires #0] [%#s06_map_precond7] forall e : uint32, i2 : t_U'0 . produces'1 iter (Seq.singleton e) i2 -> precondition'0 func (e, Snapshot.new (Seq.empty : Seq.seq uint32))} - {[@expl:map requires #1] [%#s06_map_precond10] reinitialize'0 ()} - {[@expl:map requires #2] [%#s06_map_precond11] preservation'0 iter func} + {[@expl:map requires #1] [%#s06_map_precond8] reinitialize'0 ()} + {[@expl:map requires #2] [%#s06_map_precond9] preservation'0 iter func} any - [ return' (result:t_Map'0)-> {[%#s06_map_precond12] inv'0 result} - {[%#s06_map_precond13] result + [ return' (result:t_Map'0)-> {[%#s06_map_precond10] inv'0 result} + {[%#s06_map_precond11] result = { t_Map__iter'0 = iter; t_Map__func'0 = func; t_Map__produced'0 = Snapshot.new (Seq.empty : Seq.seq uint32) }} (! return' {result}) ] @@ -1817,7 +1801,7 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] true predicate resolve'2 [#"06_map_precond.rs" 9 9 9 16] (self : t_Map'0) = - [%#s06_map_precond17] resolve'4 self.t_Map__iter'0 + [%#s06_map_precond15] resolve'4 self.t_Map__iter'0 /\ resolve'5 self.t_Map__func'0 /\ resolve'6 self.t_Map__produced'0 predicate resolve'0 (_1 : t_Map'0) = @@ -1831,6 +1815,8 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] use prelude.prelude.Snapshot + use prelude.prelude.Int + use seq.Seq use seq.Seq @@ -1840,7 +1826,7 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] predicate produces'0 [@inline:trivial] [#"06_map_precond.rs" 43 4 43 67] (self : t_Map'0) (visited : Seq.seq uint32) (succ : t_Map'0) = - [%#s06_map_precond14] unnest'0 self.t_Map__func'0 succ.t_Map__func'0 + [%#s06_map_precond12] unnest'0 self.t_Map__func'0 succ.t_Map__func'0 /\ (exists fs : Seq.seq (borrowed ()) . Seq.length fs = Seq.length visited /\ (exists s : Seq.seq uint32 [produces'1 self.t_Map__iter'0 s succ.t_Map__iter'0] . Seq.length s = Seq.length visited @@ -1860,19 +1846,19 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] function produces_trans'0 [#"06_map_precond.rs" 38 4 38 90] (a : t_Map'0) (ab : Seq.seq uint32) (b : t_Map'0) (bc : Seq.seq uint32) (c : t_Map'0) : () = - [%#s06_map_precond23] () + [%#s06_map_precond21] () - axiom produces_trans'0_spec : forall a : t_Map'0, ab : Seq.seq uint32, b : t_Map'0, bc : Seq.seq uint32, c : t_Map'0 . ([%#s06_map_precond20] produces'0 a ab b) - -> ([%#s06_map_precond21] produces'0 b bc c) -> ([%#s06_map_precond22] produces'0 a (Seq.(++) ab bc) c) + axiom produces_trans'0_spec : forall a : t_Map'0, ab : Seq.seq uint32, b : t_Map'0, bc : Seq.seq uint32, c : t_Map'0 . ([%#s06_map_precond18] produces'0 a ab b) + -> ([%#s06_map_precond19] produces'0 b bc c) -> ([%#s06_map_precond20] produces'0 a (Seq.(++) ab bc) c) function produces_refl'0 [#"06_map_precond.rs" 31 4 31 26] (self : t_Map'0) : () = - [%#s06_map_precond19] () + [%#s06_map_precond17] () - axiom produces_refl'0_spec : forall self : t_Map'0 . [%#s06_map_precond18] produces'0 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'0_spec : forall self : t_Map'0 . [%#s06_map_precond16] produces'0 self (Seq.empty : Seq.seq uint32) self meta "compute_max_steps" 1000000 - let rec increment'0 (iter:t_U'0) (return' (ret:()))= {[@expl:increment 'iter' type invariant] [%#s06_map_precond1] inv'1 iter} + let rec increment'0[#"06_map_precond.rs" 193 0 193 50] (iter:t_U'0) (return' (ret:()))= {[@expl:increment 'iter' type invariant] [%#s06_map_precond1] inv'1 iter} {[@expl:increment requires #0] [%#s06_map_precond2] forall done' : borrowed t_U'0 . completed'0 done' -> (forall next : t_U'0, steps : Seq.seq uint32 . produces'1 done'.final steps next -> steps = (Seq.empty : Seq.seq uint32) /\ done'.final = next)} @@ -1898,152 +1884,139 @@ module M_06_map_precond__increment [#"06_map_precond.rs" 193 0 193 50] [ return' (result:())-> (! return' {result}) ] end -module M_06_map_precond__counter [#"06_map_precond.rs" 209 0 209 48] - let%span s06_map_precond0 = "06_map_precond.rs" 210 18 210 19 - let%span s06_map_precond1 = "06_map_precond.rs" 209 40 209 44 - let%span s06_map_precond2 = "06_map_precond.rs" 207 11 207 156 - let%span s06_map_precond3 = "06_map_precond.rs" 208 11 208 90 - let%span s06_map_precond4 = "06_map_precond.rs" 216 19 216 20 - let%span s06_map_precond5 = "06_map_precond.rs" 213 19 213 61 - let%span s06_map_precond6 = "06_map_precond.rs" 214 18 214 39 - let%span s06_map_precond7 = "06_map_precond.rs" 179 4 179 8 - let%span s06_map_precond8 = "06_map_precond.rs" 180 4 180 8 - let%span s06_map_precond9 = "06_map_precond.rs" 172 11 174 65 - let%span s06_map_precond10 = "06_map_precond.rs" 175 11 175 38 - let%span s06_map_precond11 = "06_map_precond.rs" 176 11 176 48 - let%span s06_map_precond12 = "06_map_precond.rs" 181 5 181 14 - let%span s06_map_precond13 = "06_map_precond.rs" 177 10 177 75 - let%span s06_map_precond14 = "06_map_precond.rs" 123 12 126 47 - let%span s06_map_precond15 = "06_map_precond.rs" 111 12 116 71 - let%span s06_map_precond16 = "06_map_precond.rs" 11 4 13 36 - let%span scommon17 = "common.rs" 14 14 14 45 - let%span scommon18 = "common.rs" 18 15 18 32 - let%span scommon19 = "common.rs" 19 15 19 32 - let%span scommon20 = "common.rs" 20 14 20 42 - let%span sresolve21 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sops22 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 - let%span sops23 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 - let%span sops24 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 - let%span sops25 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 - let%span sops26 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 - let%span sops27 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 - let%span sops28 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 - let%span s06_map_precond29 = "06_map_precond.rs" 87 12 90 63 - let%span s06_map_precond30 = "06_map_precond.rs" 165 12 167 73 - let%span s06_map_precond31 = "06_map_precond.rs" 95 14 95 81 - let%span s06_map_precond32 = "06_map_precond.rs" 98 12 104 88 +module M_06_map_precond__counter [#"06_map_precond.rs" 204 0 204 48] + let%span s06_map_precond0 = "06_map_precond.rs" 205 25 205 26 + let%span s06_map_precond1 = "06_map_precond.rs" 204 40 204 44 + let%span s06_map_precond2 = "06_map_precond.rs" 202 11 202 156 + let%span s06_map_precond3 = "06_map_precond.rs" 203 11 203 90 + let%span s06_map_precond4 = "06_map_precond.rs" 207 22 207 41 + let%span s06_map_precond5 = "06_map_precond.rs" 208 15 208 16 + let%span s06_map_precond6 = "06_map_precond.rs" 179 4 179 8 + let%span s06_map_precond7 = "06_map_precond.rs" 180 4 180 8 + let%span s06_map_precond8 = "06_map_precond.rs" 172 11 174 65 + let%span s06_map_precond9 = "06_map_precond.rs" 175 11 175 38 + let%span s06_map_precond10 = "06_map_precond.rs" 176 11 176 48 + let%span s06_map_precond11 = "06_map_precond.rs" 181 5 181 14 + let%span s06_map_precond12 = "06_map_precond.rs" 177 10 177 75 + let%span s06_map_precond13 = "06_map_precond.rs" 123 12 126 47 + let%span s06_map_precond14 = "06_map_precond.rs" 111 12 116 71 + let%span s06_map_precond15 = "06_map_precond.rs" 11 4 13 36 + let%span scommon16 = "common.rs" 14 14 14 45 + let%span scommon17 = "common.rs" 18 15 18 32 + let%span scommon18 = "common.rs" 19 15 19 32 + let%span scommon19 = "common.rs" 20 14 20 42 + let%span sresolve20 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sops21 = "../../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 + let%span sops22 = "../../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 + let%span sops23 = "../../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 + let%span sops24 = "../../../../creusot-contracts/src/std/ops.rs" 120 15 120 29 + let%span sops25 = "../../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 + let%span sops26 = "../../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 + let%span sops27 = "../../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 + let%span s06_map_precond28 = "06_map_precond.rs" 87 12 90 63 + let%span s06_map_precond29 = "06_map_precond.rs" 165 12 167 73 + let%span s06_map_precond30 = "06_map_precond.rs" 95 14 95 81 + let%span s06_map_precond31 = "06_map_precond.rs" 98 12 104 88 use prelude.prelude.UIntSize use prelude.prelude.Borrow - type closure2'1 = + use prelude.prelude.UIntSize + + use prelude.prelude.Snapshot + + use seq.Seq + + type closure0'1 = { field_0'0: borrowed usize } - predicate resolve'3 (self : borrowed closure2'1) = - [%#sresolve21] self.final = self.current + predicate resolve'3 (self : borrowed closure0'1) = + [%#sresolve20] self.final = self.current - predicate resolve'1 (_1 : borrowed closure2'1) = + predicate resolve'1 (_1 : borrowed closure0'1) = resolve'3 _1 use prelude.prelude.UInt32 use prelude.prelude.Intrinsic - use prelude.prelude.UIntSize - - use prelude.prelude.Snapshot - - use seq.Seq - - constant v_MAX'0 : usize = (18446744073709551615 : usize) - - use prelude.prelude.Int - use seq.Seq use prelude.prelude.Snapshot - predicate postcondition_once'0 (self : closure2'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) - - = - [%#s06_map_precond6] let (x, _prod) = args in UIntSize.to_int (self.field_0'0).final - = UIntSize.to_int (self.field_0'0).current + 1 - predicate resolve'8 (self : borrowed usize) = - [%#sresolve21] self.final = self.current + [%#sresolve20] self.final = self.current predicate resolve'7 (_1 : borrowed usize) = resolve'8 _1 - predicate resolve'5 (_1 : closure2'1) = + predicate resolve'5 (_1 : closure0'1) = resolve'7 _1.field_0'0 - predicate unnest'0 (self : closure2'1) (_2 : closure2'1) = + predicate unnest'0 (self : closure0'1) (_2 : closure0'1) = (_2.field_0'0).final = (self.field_0'0).final - predicate postcondition_mut'0 (self : closure2'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result_state : closure2'1) (result : uint32) + let rec closure0'0[#"06_map_precond.rs" 206 14 206 42] [@coma:extspec] (_1:borrowed closure0'1) (x:uint32) (_prod:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= bb0 + [ bb0 = s0 + [ s0 = {[@expl:assertion] [%#s06_map_precond4] UIntSize.to_int ((_1.current).field_0'0).current + = Seq.length (Snapshot.inner _prod)} + s1 + | s1 = UIntSize.add {((_1.current).field_0'0).current} {[%#s06_map_precond5] (1 : usize)} + (fun (_ret':usize) -> + [ &_1 <- { _1 with current = { field_0'0 = { (_1.current).field_0'0 with current = _ret' } } } ] + s2) + | s2 = -{resolve'1 _1}- s3 + | s3 = [ &_0 <- x ] s4 + | s4 = return' {_0} ] + ] + + [ & _0 : uint32 = any_l () + | & _1 : borrowed closure0'1 = _1 + | & x : uint32 = x + | & _prod : Snapshot.snap_ty (Seq.seq uint32) = _prod ] + [ return' (result:uint32)-> return' {result} ] + + predicate postcondition_once'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result : uint32) + + = + let (x, _prod) = args in exists __bor_self : borrowed closure0'1 . closure0'0'post'return' __bor_self x _prod result + /\ __bor_self.current = self + + predicate postcondition_mut'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (result_state : closure0'1) (result : uint32) = - (let (x, _prod) = args in UIntSize.to_int (result_state.field_0'0).current - = UIntSize.to_int (self.field_0'0).current + 1) + (let (x, _prod) = args in exists __bor_self : borrowed closure0'1 . closure0'0'post'return' __bor_self x _prod result + /\ __bor_self.current = self /\ __bor_self.final = result_state) /\ unnest'0 self result_state - function fn_mut_once'0 (self : closure2'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res : uint32) : () + function fn_mut_once'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res : uint32) : () - axiom fn_mut_once'0_spec : forall self : closure2'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops28] postcondition_once'0 self args res - = (exists res_state : closure2'1 . postcondition_mut'0 self args res_state res /\ resolve'5 res_state) + axiom fn_mut_once'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res : uint32 . [%#sops27] postcondition_once'0 self args res + = (exists res_state : closure0'1 . postcondition_mut'0 self args res_state res /\ resolve'5 res_state) - function unnest_trans'0 (self : closure2'1) (b : closure2'1) (c : closure2'1) : () + function unnest_trans'0 (self : closure0'1) (b : closure0'1) (c : closure0'1) : () - axiom unnest_trans'0_spec : forall self : closure2'1, b : closure2'1, c : closure2'1 . ([%#sops25] unnest'0 self b) - -> ([%#sops26] unnest'0 b c) -> ([%#sops27] unnest'0 self c) + axiom unnest_trans'0_spec : forall self : closure0'1, b : closure0'1, c : closure0'1 . ([%#sops24] unnest'0 self b) + -> ([%#sops25] unnest'0 b c) -> ([%#sops26] unnest'0 self c) - function unnest_refl'0 (self : closure2'1) : () + function unnest_refl'0 (self : closure0'1) : () - axiom unnest_refl'0_spec : forall self : closure2'1 . [%#sops24] unnest'0 self self + axiom unnest_refl'0_spec : forall self : closure0'1 . [%#sops23] unnest'0 self self - function postcondition_mut_unnest'0 (self : closure2'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res_state : closure2'1) (res : uint32) : () + function postcondition_mut_unnest'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) (res_state : closure0'1) (res : uint32) : () - axiom postcondition_mut_unnest'0_spec : forall self : closure2'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : closure2'1, res : uint32 . ([%#sops22] postcondition_mut'0 self args res_state res) - -> ([%#sops23] unnest'0 self res_state) - - let rec closure2'0 (_1:borrowed closure2'1) (x:uint32) (_prod:Snapshot.snap_ty (Seq.seq uint32)) (return' (ret:uint32))= {[@expl:closure requires] [%#s06_map_precond5] UIntSize.to_int ((_1.current).field_0'0).current - = Seq.length (Snapshot.inner _prod) - /\ ((_1.current).field_0'0).current < (v_MAX'0 : usize)} - (! bb0 - [ bb0 = s0 - [ s0 = UIntSize.add {((_1.current).field_0'0).current} {[%#s06_map_precond4] (1 : usize)} - (fun (_ret':usize) -> - [ &_1 <- { _1 with current = { field_0'0 = { (_1.current).field_0'0 with current = _ret' } } } ] - s1) - | s1 = -{resolve'1 _1}- s2 - | s2 = [ &res1 <- x ] s3 - | s3 = [ &res <- res1 ] s4 - | s4 = [ &_0 <- res ] s5 - | s5 = return' {_0} ] - ] - ) - [ & _0 : uint32 = any_l () - | & _1 : borrowed closure2'1 = _1 - | & x : uint32 = x - | & res : uint32 = any_l () - | & res1 : uint32 = any_l () ] - - [ return' (result:uint32)-> {[@expl:closure ensures] [%#s06_map_precond6] UIntSize.to_int ((_1.final).field_0'0).current - = UIntSize.to_int ((_1.current).field_0'0).current + 1} - {[@expl:closure unnest] unnest'0 _1.current _1.final} - (! return' {result}) ] - + axiom postcondition_mut_unnest'0_spec : forall self : closure0'1, args : (uint32, Snapshot.snap_ty (Seq.seq uint32)), res_state : closure0'1, res : uint32 . ([%#sops21] postcondition_mut'0 self args res_state res) + -> ([%#sops22] unnest'0 self res_state) type t_I'0 predicate inv'1 (_1 : t_I'0) - predicate inv'2 (_1 : closure2'1) + predicate inv'2 (_1 : closure0'1) - axiom inv_axiom'1 [@rewrite] : forall x : closure2'1 [inv'2 x] . inv'2 x = true + axiom inv_axiom'1 [@rewrite] : forall x : closure0'1 [inv'2 x] . inv'2 x = true use seq.Seq @@ -2056,58 +2029,57 @@ module M_06_map_precond__counter [#"06_map_precond.rs" 209 0 209 48] function produces_trans'0 [#"common.rs" 21 4 21 91] (a : t_I'0) (ab : Seq.seq uint32) (b : t_I'0) (bc : Seq.seq uint32) (c : t_I'0) : () - axiom produces_trans'0_spec : forall a : t_I'0, ab : Seq.seq uint32, b : t_I'0, bc : Seq.seq uint32, c : t_I'0 . ([%#scommon18] produces'0 a ab b) - -> ([%#scommon19] produces'0 b bc c) -> ([%#scommon20] produces'0 a (Seq.(++) ab bc) c) + axiom produces_trans'0_spec : forall a : t_I'0, ab : Seq.seq uint32, b : t_I'0, bc : Seq.seq uint32, c : t_I'0 . ([%#scommon17] produces'0 a ab b) + -> ([%#scommon18] produces'0 b bc c) -> ([%#scommon19] produces'0 a (Seq.(++) ab bc) c) function produces_refl'0 [#"common.rs" 15 4 15 27] (self : t_I'0) : () - axiom produces_refl'0_spec : forall self : t_I'0 . [%#scommon17] produces'0 self (Seq.empty : Seq.seq uint32) self + axiom produces_refl'0_spec : forall self : t_I'0 . [%#scommon16] produces'0 self (Seq.empty : Seq.seq uint32) self use prelude.prelude.Snapshot - predicate precondition'0 (self : closure2'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) = - [%#s06_map_precond5] let (x, _prod) = args in UIntSize.to_int (self.field_0'0).current - = Seq.length (Snapshot.inner _prod) - /\ (self.field_0'0).current < (v_MAX'0 : usize) + predicate precondition'0 (self : closure0'1) (args : (uint32, Snapshot.snap_ty (Seq.seq uint32))) = + let (x, _prod) = args in forall __bor_self : borrowed closure0'1 . __bor_self.current = self + -> closure0'0'pre __bor_self x _prod predicate completed'0 [#"common.rs" 11 4 11 36] (self : borrowed t_I'0) - predicate next_precondition'0 [#"06_map_precond.rs" 85 4 85 74] (iter : t_I'0) (func : closure2'1) (produced : Seq.seq uint32) + predicate next_precondition'0 [#"06_map_precond.rs" 85 4 85 74] (iter : t_I'0) (func : closure0'1) (produced : Seq.seq uint32) = - [%#s06_map_precond29] forall e : uint32, i : t_I'0 [produces'0 iter (Seq.singleton e) i] . produces'0 iter (Seq.singleton e) i + [%#s06_map_precond28] forall e : uint32, i : t_I'0 [produces'0 iter (Seq.singleton e) i] . produces'0 iter (Seq.singleton e) i -> precondition'0 func (e, Snapshot.new produced) use seq.Seq - predicate preservation'0 [#"06_map_precond.rs" 109 4 109 45] (iter : t_I'0) (func : closure2'1) = - [%#s06_map_precond15] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure2'1, b : uint32, i : t_I'0 . unnest'0 func f.current + predicate preservation'0 [#"06_map_precond.rs" 109 4 109 45] (iter : t_I'0) (func : closure0'1) = + [%#s06_map_precond14] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure0'1, b : uint32, i : t_I'0 . unnest'0 func f.current -> produces'0 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition'0 f.current (e1, Snapshot.new s) -> postcondition_mut'0 f.current (e1, Snapshot.new s) f.final b -> precondition'0 f.final (e2, Snapshot.new (Seq.snoc s e1)) predicate reinitialize'0 [#"06_map_precond.rs" 121 4 121 29] (_1 : ()) = - [%#s06_map_precond14] forall iter : borrowed t_I'0, func : closure2'1 . completed'0 iter + [%#s06_map_precond13] forall iter : borrowed t_I'0, func : closure0'1 . completed'0 iter -> next_precondition'0 iter.final func (Seq.empty : Seq.seq uint32) /\ preservation'0 iter.final func type t_Map'0 = - { t_Map__iter'0: t_I'0; t_Map__func'0: closure2'1; t_Map__produced'0: Snapshot.snap_ty (Seq.seq uint32) } + { t_Map__iter'0: t_I'0; t_Map__func'0: closure0'1; t_Map__produced'0: Snapshot.snap_ty (Seq.seq uint32) } - predicate preservation_inv'0 [#"06_map_precond.rs" 96 4 96 73] (iter : t_I'0) (func : closure2'1) (produced : Seq.seq uint32) + predicate preservation_inv'0 [#"06_map_precond.rs" 96 4 96 73] (iter : t_I'0) (func : closure0'1) (produced : Seq.seq uint32) = - [%#s06_map_precond32] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure2'1, b : uint32, i : t_I'0 [produces'0 iter (Seq.snoc (Seq.snoc s e1) e2) i, postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b] . unnest'0 func f.current + [%#s06_map_precond31] forall s : Seq.seq uint32, e1 : uint32, e2 : uint32, f : borrowed closure0'1, b : uint32, i : t_I'0 [produces'0 iter (Seq.snoc (Seq.snoc s e1) e2) i, postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b] . unnest'0 func f.current -> produces'0 iter (Seq.snoc (Seq.snoc s e1) e2) i -> precondition'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) -> postcondition_mut'0 f.current (e1, Snapshot.new (Seq.(++) produced s)) f.final b -> precondition'0 f.final (e2, Snapshot.new (Seq.snoc (Seq.(++) produced s) e1)) - axiom preservation_inv'0_spec : forall iter : t_I'0, func : closure2'1, produced : Seq.seq uint32 . [%#s06_map_precond31] produced + axiom preservation_inv'0_spec : forall iter : t_I'0, func : closure0'1, produced : Seq.seq uint32 . [%#s06_map_precond30] produced = (Seq.empty : Seq.seq uint32) -> preservation_inv'0 iter func produced = preservation'0 iter func predicate invariant'0 [#"06_map_precond.rs" 163 4 163 30] (self : t_Map'0) = - [%#s06_map_precond30] reinitialize'0 () + [%#s06_map_precond29] reinitialize'0 () /\ preservation_inv'0 self.t_Map__iter'0 self.t_Map__func'0 (Snapshot.inner self.t_Map__produced'0) /\ next_precondition'0 self.t_Map__iter'0 self.t_Map__func'0 (Snapshot.inner self.t_Map__produced'0) @@ -2119,15 +2091,15 @@ module M_06_map_precond__counter [#"06_map_precond.rs" 209 0 209 48] | {t_Map__iter'0 = iter ; t_Map__func'0 = func ; t_Map__produced'0 = produced} -> inv'1 iter end) - let rec map'0 (iter:t_I'0) (func:closure2'1) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond7] inv'1 iter} - {[@expl:map 'func' type invariant] [%#s06_map_precond8] inv'2 func} - {[@expl:map requires #0] [%#s06_map_precond9] forall e : uint32, i2 : t_I'0 . produces'0 iter (Seq.singleton e) i2 + let rec map'0 (iter:t_I'0) (func:closure0'1) (return' (ret:t_Map'0))= {[@expl:map 'iter' type invariant] [%#s06_map_precond6] inv'1 iter} + {[@expl:map 'func' type invariant] [%#s06_map_precond7] inv'2 func} + {[@expl:map requires #0] [%#s06_map_precond8] forall e : uint32, i2 : t_I'0 . produces'0 iter (Seq.singleton e) i2 -> precondition'0 func (e, Snapshot.new (Seq.empty : Seq.seq uint32))} - {[@expl:map requires #1] [%#s06_map_precond10] reinitialize'0 ()} - {[@expl:map requires #2] [%#s06_map_precond11] preservation'0 iter func} + {[@expl:map requires #1] [%#s06_map_precond9] reinitialize'0 ()} + {[@expl:map requires #2] [%#s06_map_precond10] preservation'0 iter func} any - [ return' (result:t_Map'0)-> {[%#s06_map_precond12] inv'0 result} - {[%#s06_map_precond13] result + [ return' (result:t_Map'0)-> {[%#s06_map_precond11] inv'0 result} + {[%#s06_map_precond12] result = { t_Map__iter'0 = iter; t_Map__func'0 = func; t_Map__produced'0 = Snapshot.new (Seq.empty : Seq.seq uint32) }} (! return' {result}) ] @@ -2138,15 +2110,19 @@ module M_06_map_precond__counter [#"06_map_precond.rs" 209 0 209 48] true predicate resolve'2 [#"06_map_precond.rs" 9 9 9 16] (self : t_Map'0) = - [%#s06_map_precond16] resolve'4 self.t_Map__iter'0 + [%#s06_map_precond15] resolve'4 self.t_Map__iter'0 /\ resolve'5 self.t_Map__func'0 /\ resolve'6 self.t_Map__produced'0 predicate resolve'0 (_1 : t_Map'0) = resolve'2 _1 + constant v_MAX'0 : usize = (18446744073709551615 : usize) + + use prelude.prelude.Int + meta "compute_max_steps" 1000000 - let rec counter'0 (iter:t_I'0) (return' (ret:()))= {[@expl:counter 'iter' type invariant] [%#s06_map_precond1] inv'1 iter} + let rec counter'0[#"06_map_precond.rs" 204 0 204 48] (iter:t_I'0) (return' (ret:()))= {[@expl:counter 'iter' type invariant] [%#s06_map_precond1] inv'1 iter} {[@expl:counter requires #0] [%#s06_map_precond2] forall done' : borrowed t_I'0 . completed'0 done' -> (forall next : t_I'0, steps : Seq.seq uint32 . produces'0 done'.final steps next -> steps = (Seq.empty : Seq.seq uint32) /\ done'.final = next)} @@ -2172,7 +2148,7 @@ module M_06_map_precond__counter [#"06_map_precond.rs" 209 0 209 48] | & iter : t_I'0 = iter | & cnt : usize = any_l () | & _5 : t_Map'0 = any_l () - | & _7 : closure2'1 = any_l () + | & _7 : closure0'1 = any_l () | & _8 : borrowed usize = any_l () ] [ return' (result:())-> (! return' {result}) ] end diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.rs b/creusot/tests/should_succeed/iterators/06_map_precond.rs index d6b99fa2ea..7842e78480 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.rs +++ b/creusot/tests/should_succeed/iterators/06_map_precond.rs @@ -191,12 +191,7 @@ pub fn identity(iter: I) { forall 0 <= x && x < prod.len() ==> prod[x] <= 10u32 )] pub fn increment>(iter: U) { - let i = map( - iter, - #[requires(x@ <= 15)] - #[ensures(result@ == x@+1)] - |x: u32, _| x + 1, - ); + let i = map(iter, |x: u32, _| x + 1); proof_assert! { forall> i.produces(prod, fin) ==> @@ -207,14 +202,10 @@ pub fn increment>(iter: U) { #[requires(forall done.completed() ==> forall> (^done).produces(steps, next) ==> steps == Seq::EMPTY && ^done == next)] #[requires(forall iter.produces(prod, fin) ==> prod.len() <= usize::MAX@)] pub fn counter>(iter: I) { - let mut cnt = 0; - map( - iter, - #[requires(cnt@ == (*_prod).len() && cnt < usize::MAX)] - #[ensures(cnt@ == old(cnt)@ + 1)] - |x, _prod: Snapshot>| { - cnt += 1; - x - }, - ); + let mut cnt: usize = 0; + map(iter, |x, _prod: Snapshot>| { + proof_assert!(cnt@ == _prod.len()); + cnt += 1; + x + }); } diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index da3b93c0c0..6da3805e74 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -243,49 +243,40 @@ - - - - + - - - - + - + - + - + - + - + - - - - + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz index 5a21487da5ff83bb9ac6c9bee45ae214d3924d74..8775f384c1c63d194fbe3fe4fbf9d45bf0e3bf6a 100644 GIT binary patch literal 5260 zcmV;76m#nziwFP!00000|Lt5^j~qF2e(zr)zz?!_u>kMG7(FxwQ^*Fq^Rh<4ZvwBJ zDXi2jb+=|`{p|!@kia25A>)G-NQ|OaE~W<{|sW3d@djI)1iO5agXWg z;lpn!ztOwV+u_zdJwJX4&tD$hhxg-t?RdJ{<#1Ex{=Nukz{NeK5B1&RsPbtb0J~OY!cj+kv`6#P=gHTH`;gkt26VpM->0WW zm`BR)2Jdw8-iTn(!13RxK^!S`wltaiN#g5~>Mw=y}M0&hlu`{QiCY2KTeahP20I9y(S&rd$!DMKUmj9-=M?K-w*Op12wStLa}naDaq z-IVGGp|pD(wU3)uG3s*132e7O>bK;PiA_;T0aHe1Foju?ED1&i3u%GM$Q-Ejj8w>M zic~*GDxE>q&7eAy>sfqYvJ0x1Egiw8G+e+<5md;|X}reVkRP4L(*?L*$#@m9Zh=ox z)BsN{WEtHL*`fEu1hYcVz7-9Sy`S_!mxUf1NbbhGme1`e-V|KA6aIFm*(%0}KQHc2 z?lgh@`P*r{)Uvh=xJw8PH$SfpTx2vig7w)>sm{Vd5d)cvq1DVTK#fGO!@R&~1aiFZ z!#FyQ{l}>_EqA(PSy%AfZ&vPfHxy%MRQtq|v2`9fn(gG%t_U_6Gf5DJpPFDgZoDAQ zZ#viAfp|5{}1TZ?;xAK=g2Noio~lown~j?Y}O+MPG30-iu|wXi~_w7iN`P zUofrQePLd?c{nk=Z({G&C$-bMhkQ%uWK(C^1yF2vPG9ejr%BI-*S{QCmcq*I+T4ze zuZ1>zDr@GmIN4=){BV19M85rsJm7XucCjDld;lqEGB;dA6Z&Pf^JR4N3A*`SbYC-- zmt%Ua-w~$y|5{9obxe!0X0eKCaRsJZH?{`n>^@eJyx?1YdKs5~+VuV7T8+M?OXUvGRN?KB5OAuR@a5eLNCeW~%;b4S)F~NS8_scA2STV4fhz71@?1?-uF*#`C|t+|n0hBP(#KyHAla;ClmRn%rEkb&GA zQe#MyO-NtMd?%y}oAJ@(6w+i0X==U(($st#Naxuc8J$2nuWNi#ho%nF^cqMvN9U_B zq;>;_=acSTklv0CE2` zzHVl+yKaW>?w>{%kW9I!)BP_W((}Xpk?A8dpZm}6AMR7>(tN-)pWTn|e=e=<4LB!g z`OCw{-0#Tj=l0s0*+c(y(>`%_`=bjFAED3Ztg0iYXKDkHw#vz$&okp~n%oTP7;<*^ z65`Ez1`Li|ER#Llw$kGLH9OCT`e)&?qx#&cs=e&T!%RT-Xa;ok=T^=7&^-)E@?$GM zb!^3lhZY+4NV{7NV4*7`(0v(!9+eTWBUQ_H?D+~@lxuCdcF*2+k)w-pT`uU(?`HC@ z%Ps1;ft6@6Y@lVcur#M~72R0(VP;7TMxhohseA!4izVr?B|)>KQz5fcOER}(D={r> z^W)+Ccr&s$&OUdTXNUgj2L9;x=l5ebcI3K)6|C$2A*^{Tz#0&|U0U7CNNhUsOrnJj z@V-Q$XLaOA{@x7-j$9|Yj=bL}BxO1SgB4i9-AK-y4?PGiGBihSI}4$(JkvQfZVvs^ zsH8-Y0T+RHHgi~lG#?H(Kj&Ma-T;L@3i!dn`|X-<5d0|HtPRf%l=yj~k_@VJoPT(H zeE1t=`SGtqs0nct%~ko90*5Sx=~=o{>>0Cf$YB{dlN_NR-{A;kw%OPsqDI4#9A<(3 zN(PNw^ox3{xfB;BkOg|W|1~|Hp5LEh&JglntMXr8$kv1=ItYCj6Sj>!vmAP`nAa8M z-N-^rwvg;mg&edh%xV~1hZfNo^Dc8(pK6A1Qz7+2{O=$+4Jj_WE0+g+o{F+z-q#Ow zyR2ed$O$|7b>VNz=bnk2%Vh@Rdsc0|)>0OHiN?qkmqnF{=Kt%{%o23_JUB0UK>e_f z!0WB^UH_?9&BorN?vnqs0N_$o*K90m_c*-guP2z8*4#}tQiV_-QNSy=kJ9Klg|V#M zlS|ZLo~Mg!`XTwEWx(@l3d1C73m5CTR+D$M#?i`kGpaOYjf)A;{}7d>MC!#v{;fgX zs9^GCnrP))4$?L>aqf1wo55{8%~}TR-30^K-sQi@()LxaZWg1CD{A3kn#x(0i*w)g zye6yo61J+GW>T4aE~D2^dh+*uKwUYpxG2Kc@^!zRp0K94T2@p#FNyA40ohBbo;UU6 z7rLj-?wg|BII)>(Zd64znCrMeYq*GcLD}%@X>l#>#FuKz)+G4zMLH`}n4NYucvxS~ zDwkQLR zMdK|k2#Mvd=Y*A~sZP!@T^xpZBDev_loBrc=efG0! zy0M7H_jSW>`!4QY>Yz6+J$6Ll+m}X`7ulE`T^Qu#Y8P7beSbbtT(c;-W>Ip#MO`_y zue6_4a7^q+{-3rVwPio5h)8YNkGk4^THm{2HrdH-S<99a+_*YiC;i>BzFXFJ%la0U zwHV^I_F5Nj;6;|=5ajvpYbVHMD7Uug8Yoqb$PAkQZVgSjuBY380iI@fN(E)%<`-;1Zamo+>rm0D9szot!# zS?B=zKfSs{_v&(53-n!=|A4yeYMZ($L2{`|kn~l8tgjMeU6tV5(b#ifDt9q=i*;D} zmj85*^|%kG|IAnY%~jd-0{a~EvM(OdJYV|AY2D$WD}rFEtGQ#t-;I&i{cg;2S6M{+ z$|7p!g`4?$YPoQ;xeceK+>B1k&AO8Fvm)3;5v(u8WPK?nYZO67ifCm=hJxGE>vpCx z)n8>Us%>VWEyatfo0W_nx^j??@K}*$pEpz_Usfb3KQqME6xsd0P+wCh@((WcZ*ue| zj-vubebmEObEIUs7|{Sq?GFb%ccw%8f7b9uC46_| zGTW?>ACTfbz)YGvjLTfS*fa!M{zU=rGcqpQ43z7`h)bSP849F)bf4b5Ew1>@^WQ(E zH@zKoeyf35)33PPS-%P8@#PSk-ENJLk1prpq0Hkkeg1L+df)sL*&cc1X3=J*lR&>C zx5XqD>~g}BE*CH@_FZr&!`_2+O$Bx?-?}(-R+_NUx%ABtYJVf+_k3IVdzY)`j}!Pb z1Ag!EgVjG_?Rn)hpm6}^+_3CU_st8v z7CiVOt%(Qk`+S`T=V}>^neG6KDjVbN$h0~So(t?JLN~brcVyjy^g=hS&;>b67`BkV z>zz)i(9KRq@KvXi`|w=IJ9avP9?o_DlV4|B^T=e$Ba=msOeP+ADfosD4^Lkn6M0KB z^atgMd2^k8@TKVe0s>2c{o?Swh`BtEE*-GD(t#Y5dNA#nWuG4upmjK+9prv{|L5EP zcsmPoylDOmrnZj$U3LJo84mi$#<)ijj30(s%8iUd)geihlod|Z$@{=4OIEYQsg7@C zB`RLAidN)Cdm|XHX)+F-X>>ABpG2s&azrG8&Z=}YGHS~)yGW?^!dvg1G0dtMXbj&C!9Tis8-Wy&kZu1~99b{6nl+zHDt+{nVhUj>r zGzLR4iY*SZB-M@(<_y!pFo}+uF{xtkQJGrjL2^3C1!;wFS|x!2H3cj0Sb`jwppNIo zOFbRrt>Z>`qZ$4tj(MVeuvS|sA@F4KAT{G8buA6owbPO)r-Tn)TN0UK!E%<@#975@ z#Yx3%#Z1L?#Z<*)#YDxREmkpFF;Y=mQBzS&YsRD|iJO``s*;pE*1|#{k_hW+h_5h_ z@>(WI7;b}0oS0y=GSYj`Wi3Q$X@ zq3~l!=b2%I1foSWN@ONiLs&^TJ5LD@wNR=2Yuf<3)Do*pUS*wdb-kT%I8-4)IMhni z8kx1%@W!V0%*e75TX9oyeJv|W5?m0aMg{^GO(f@uSj%8RH6WIKpP-c>SNoR)?`jDn zBKj;lXow3apWEaB?hG@*D{(c_R1LYAx;Dup1S!S5)WrE<@P{X#^&`Y9@DXstEI3aE z%gBzk6kgXnaE18k8$P-csuEX2E^1;RGlXCpSn`Q73k$VOVx3XCj0Qc^z(+JK(L>FdG*Up<$~=C5s4YlTJ-I05|(;3^`|BAmgys zz=|W#$7+WtOcTtE*us#$4l9Fbim*mtuXW0SMC`xBn?71@~lLdRvJ;38sv^4ii}CcE5#~BD@7`4D`{q4 zPU%$F8ZlE#SdAvwDsv+dK)upIanR7{rz@>0jb~A5UTIcoT4_=#TPag1T`5&5a1$ld z^ezIoL`N%wakYY(M2EoO>SzfJG}E-hiR3}TBDM6)c}su;N<)lTPfQ4i$R%S~9K@1| z-caSEAPhN~G|>Re+;IsMn;g>2bk!wkrtlI-kujEtAh@Aa)mVPStQGR3wQ&dmJZML> zPCEF+0ywH5j5QXSaRHRUf1)zHGORMRGGu`a{4bC2#L025kyXP_*22L7ClXcNOj}n* zT_6)gj7?6Wg?Gdzh1678cs`<{FCsH$7bTCpn;C=yTALh5gJK9lG!PnrVOG+70MXLQ zl9@eISaU?~jlG3IR;*xY7+3R}1Y=8DfxN7;sJFA6oWml{$>$pu!)bwJ!zmP=8S z3=e=h7N=^>UScFLr74LdFE_!Hc{psvT}q&;Ln>3_yTw++G!Rk@>;;>w0PjMuOY=GL zq}U=BYHTmHV1%Ub;U3;WB3v1%M5-C!tFTe@d2ej(USdE3k2!aU(P48euuDlwD5{m> zhBd@?uM>VgZ`NzZovg80aLH?6g+uyWq_P*q&S5V#Y`c|A@C!ENtqnyA6{Yk6Bm;Ay zz=L22p*jEDNt6pM88#OYfl5#)(5#u%+}2Xl=pE!6H5WxuITy;&WYGdSRnFwCP4t0#>ur>g z5vnAR#L6yudpu$%Hhb{Ko^v4><4Gd4(ggSC5-BHSNXjT%3Zc9ff^fJX?TMs0q*Gu) z5+v^MQ=~XemQ%R=cRu|ZoV8KboaJFdn==^LCk@#8If-RkYh%u!JoX&r3=EukKB^OE zS{$@ENFbj?AVFJBl=2L*CPN+71V)~aib_K?0#A}iQ#o@ksW*s+7=(%OOjx(i`xz)k zeT|(r^pjNE7U?Yb_zZ_{r z#;Ii)z9!_Kv?Npn4JII(Pg!M#G>AzMlk9571g;qA9j%Mwq&ZEitq&1>kPJ1^L(wxS SmD$-vQvU_vvlCI)X#fB}C^q!~ literal 5381 zcmV+g75eHQiwFP!00000|Lt5^ZzM-@e(zsFzz<_DAs{0nPeb$25Y#9FUcIbQ@Eeh* z)YutvhU93q{`E#?9bH#f7pFP)+8zOts`7}4jQk=ZDykj-6&!r}NcvhrZ2 zJeVsFhRPeP%Ixi@$LAOS_z;dS$H#~Jk6*HKWUXpb>z_YQdLJKrY`gVgXTLl=#OFqt zHQ?Rg9VYLM3I+{S1C1JZ4f1YLnA|05kTs|=9zeHi0)2O;{V4!P6b-k$Ar_Bqc@#|Qht{u*DhWIxoPJy`$c z=_x+Ew5?^oe#~0!m$0`#zW0zfYPmG}OVI!|hI-m~2j3}iK`XZ)s2_vf)SV^Vg*>uP60cw+*ULBaC2E8ZO|bD9UH&G+twF$dA_52p8abCF8S*wF`X8 zMh)=PLKa~=WQX4K_O@*3$+zC#TIK=6aR5+P0JoHS=JRix0{tc-VN2*8PztmWNe*gj-;J*ZHi!%Ig{HC&Q4!q-OS@mPylW;ul-L0)~fau}kI%l*6JMGwQyZ^TQ7Jb37doPy#Dxqq` z1*vlDE5ypf7v###L&0jqRqVaFP#dj#$hU+}oI1-cfZ}0){Ca;pJ@l-2{mX%6DXi?z z$yOts3vD%0Su@SzWOurw!~W`sy#I=Gz<$f=Vmr=h0I3==H(W$hjhMHcmeEZUbkkOJ zUn9!vF+Jbk5vJ*XEvET-O!Km4eiqaG3QV_d>>Ql4`#6i_1>f@X>u7z){CCX%f5ZHK z)3@jayC|UJBNS3@*nmRHnBk`_X-SPOfv;J@)y%hJ##SYz+R;_HKjl6CPRS@ z^xlvfLz=BZ`da22Azj#vuO6q6W>ZLm{u)Sw{x*=#($okONauBpZ|Z8$9i-tJNHdrs z-D`+9>lrYpi7%5q>|1S7pJu0gsee)~*79?^Rc*4L*K(#HQ|kd;^|{?^TL_OIll;%d@vb#3)g&N`mh6t|#xR zWKmBISfa(S0m{e1l1wEP-B|ZwW=SY&l#7;BdTLa~lGNCepeELBA)2Wr>HXMBbPL=3 zcsM=oM)pSdxx+jj`lp?Jh=07?kKI^Js)LoZ&kv9OoVTipYHGaTbak&IvFgM#i55D< z7b*0tY7%#+V4Ww9TxU%*@_wU`l<5o%me-{2MtUY1dJrf&)HRvTLZGfmcTSD;p??~c zlyElS!lC9kb6A`;9f#d7IV;o~AXhaPhvEDFoNwS%i}uu3^VTWTNl?KCRXWx^K0Q7D zErxd=|2l*k=QVFqtvHM_gZEV~UEJ9Tw~`3-nhq zX!N39HCoQKxFA4Q=<(sV_;h@^KZbll$p1U5|MLr36KJvrz7J#Ew2^0ah8`^DZB=nF8r+^qA_yCWl=@Y{Ga}qS%PkV4$g}nP(N%V z@OJBb-*@#}v-0hcy2F250B|X)Yd$QJeH!NZ(*zUKn!Cw|R3X$y6dQ{oM#tzmg|V*e zvyEUQmVDqkn|?}8vuOYK${H6BK>tHjmJU*{Ch~6$ z>P7{VuiJ@MzvUurWhYL<4tF!Soj+zR1NQEM0jz)Jzsl0KRj;lVqmCOSX@-$Tlu=*kI%=K7|xazmBCA@J5@mTT1xY# zp8Ue_xH^1QwJSF^)14btQ4M4r7ibL^F)t_^_8u44(h9y*TXs%^zg(nqMugdIXM>0H z%Q?$sdMs>qc2QrOaI&Jam2Bf^L zvKB+!+PBul3_Q$!vB;gCSGiE2(bMn^CI{TvQ?mjLaAWt_41KAhvH1o(Fo#!%Pmx*26-;1}qmv?wrDs^r{`ZcXu z%))^9A^rU38r`~=(^{bKd-)HzmtAdBS0%_URSB}bN)Y=hLF}po-;L&;0#nJw+%48& zJ1KA2F>vJak16D7%_F9R6;Mc%$Eq>Gz<| zPDB5LJ~^x3@q?0L@7fQ$m##Dk`qCuO^UBYh-&(HxY|`ma>eXOcuh!M9pLP-_JBfWQ zC-$|R*z6=5?PRNbHq`upIMV$ zwCAZ1HRYntVy+85W5N@btFsozE;zg4=)t~uIBPJh&}Ifk4HNsjSDxMzJaBVZpN7RH=t zjzY$$-qL?~eE#wj@g3y1K~D}&ZB@zwL3<3#?Y&&bP(ssEtXmazJqm7{nt$kI`*{2N z{h#;$@s6$PdoZi@0ObRv`N_dy5!AW3%9i3PTa2r05?7awcW3u4-~Z%Ddg*-l3Ia<< z$BWaq+WloYx&x=#bl}WKi{2${kg`947I)Ek1DIfAdRU=izbBW_{;9|N?8avj4#tSa zMUT!QbQqq4cOr0^d=xTD!>vrwIgfzRD2xOu+=z--RAB`b+bO3xQi7_$|w4AdehLnLfqpd5F`Ijc1q83Lpf?Tx5_D!>Y$0#=zyS86AbJEm;_D}zNX zL0I61C+9RJNhVL?(@8o;0|eenlgL;ue6SP&g4aMv;^HL3VzP{()u_BiK}jk^A%k~8 z>ZI}{F`Z<+Fq~T@BNvnsaN(WB$SoiTOL_4^O(!{HNpq(aTGGs-W6F7Blo29I6Lp>> zXPkseLX%2X2_~)N&O2pTK#ATE<~0#k1QoFgO@+EbRiUgpqzFILh>G%&nvl_NemIZVVpB2 z5Uh3pj4ACQT8984Gr4->(R-Ky`7NZmJ6$dPm(7^+Bzju)XAY1WhJH}U6Hz$6|ktB2hhSZL&OA8WX7OLCIN`- z`#4mbUF~0@)o2(p9$eO)hCrMml8IIzWSDWP_|-_0$#S7n($O&wbv(9U+HAR>A zhx0e!!=;tztpko3*&zw;R3cAOChrjkOai6Q3+cRQS-sK1Y~+?J z8w}SHgVfRJ;91g6J5JU>%kAwnX@fwBLTlj?naEH{#ZiFvQTV_!CM8u8D+!fkl`xgi zGcPAqOi3jON=TU$3pSA!$$KZ2mvkd4r7NW>B`YN=#VbXX!b(AKxMabk*h142ir?%4uNSbJ74ZNtr@qN^(u-=8?AKm1Rmr zB%K4Pmq--BGYC3(EXRB>m4V8znLPuC z6cTVEp`CX!l4KAPCFZp$#|i*d8Ce-o8D1HxOp#=fnzN{rG6p0I+K>t{D3=mTMuSvT zJ_A5*r3PLp&Z5hPD3dqQc_8C4A;=&wyHc}Rvj!0*DSc?2$S+<^8v)> zg*r4kDTZDW2Oy@UqbLP%&6#n$P~%&vDI!5Uct*;nq@^Lj6U*?BDTLxwjowO(d6WuR zV0pPQNbMX4Nj63jT=`f;qs?kdAgq>AyNE^^Pg*eVtjh;a@Up=cZl&fm7hn>&fJy|f zwU9g}M2ph9;PSVzF5pXUZ-|Cf2=1YD-vVEMyEWN z6pSMt%eN>nwv`%pOo|v?GCqIW06Gzba9(-t(fR@ph7~Z#=g*Bqi7SE3_`ogapg1Xk zf-qRYxQ(VE$}3>6*jx-+*+i0j{*eygI=fcIe83cW`P65!0=C&MlF^a0SEvAE;K`;$ z-ja>LV)Qx`it05KdGf$XBqk#$3dxDc6gdlA32urL0A?y+I>+RVLu6crQ80m3wWH zlSK<8kXGkUo8UY-<4h0%8AyRKVEKw(pD&G9!gBye#5p2G;S`7HIM~R_4H-fOxD-NV zG}bvqE>}!5&Ykv}xx_iLz4PRR0!AVr2c^jf9t8`| zQ4B%z!dkKlNL4`cBm(7sc?Co>l3Eao%X| z0j4BK%Yb=L!DSbgPmBsY=pcf-0ZtWgyow3qG2d09R@N$^1q0+MTZ_=7t;QSRvI3s3 zG5OWZg5*wztSFVZS16@+KtiDoTyU0EW-8#Bfx3QWOeh~%HYX;f(;^v47E=f=pPa=F z2&h1?H)F_2sf3!eBx|Jik!e(l=MXEs)A9xcRUokW_iI;WjN^%G$w`_NV!!|@2^L~V zz&zf7FcoB*&9}k%a#!TrWPUYc4Z)BSI;g-jT0!1`G{&ctd`hC6lqAfiImRt$@cDAY jJ0ZvghCcCRebfqNnZ{2NNUA{Mq6Gg1TBV|WA8h~t4$)s<