From 7ea6e88fe691aed94055d5bc10733f0bd401fe05 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 09:17:28 +0100 Subject: [PATCH 1/8] Reorganize `IndexLogic` --- creusot-contracts/src/lib.rs | 2 +- creusot-contracts/src/logic.rs | 3 +- creusot-contracts/src/logic/ops.rs | 91 +------------------ creusot-contracts/src/logic/ops/index.rs | 91 +++++++++++++++++++ creusot-contracts/src/std/deque.rs | 2 +- creusot-contracts/src/std/iter/filter.rs | 4 +- creusot-contracts/src/std/iter/map.rs | 6 +- .../src/contracts_items/diagnostic_items.rs | 2 +- 8 files changed, 101 insertions(+), 100 deletions(-) create mode 100644 creusot-contracts/src/logic/ops/index.rs diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 704974e24..5b5ec7b4c 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -397,7 +397,7 @@ pub mod well_founded; mod base_prelude { pub use crate::{ ghost::GhostBox, - logic::{IndexLogic as _, Int, OrdLogic, Seq}, + logic::{ops::IndexLogic as _, Int, OrdLogic, Seq}, model::{DeepModel, View}, resolve::*, snapshot::Snapshot, diff --git a/creusot-contracts/src/logic.rs b/creusot-contracts/src/logic.rs index 69552ee36..f923da0be 100644 --- a/creusot-contracts/src/logic.rs +++ b/creusot-contracts/src/logic.rs @@ -8,7 +8,7 @@ mod fmap; mod fset; mod int; mod mapping; -mod ops; +pub mod ops; pub mod ord; mod seq; mod set; @@ -17,7 +17,6 @@ pub use fmap::FMap; pub use fset::FSet; pub use int::Int; pub use mapping::Mapping; -pub use ops::IndexLogic; pub use ord::OrdLogic; pub use seq::Seq; pub use set::Set; diff --git a/creusot-contracts/src/logic/ops.rs b/creusot-contracts/src/logic/ops.rs index 189339cf3..1e58b143f 100644 --- a/creusot-contracts/src/logic/ops.rs +++ b/creusot-contracts/src/logic/ops.rs @@ -1,90 +1,3 @@ -use ::std::alloc::Allocator; +mod index; -use crate::*; - -/// Used for indexing operations (`container[index]`) in pearlite. -pub trait IndexLogic { - type Item; - - /// Performs the indexing (`container[index]`) operation. - #[logic] - #[rustc_diagnostic_item = "index_logic_method"] - fn index_logic(self, idx: I) -> Self::Item; -} - -impl IndexLogic for Vec { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: Int) -> Self::Item { - pearlite! { self@[ix] } - } -} - -impl IndexLogic for Vec { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: usize) -> Self::Item { - pearlite! { self@[ix@] } - } -} - -impl IndexLogic for [T] { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: Int) -> Self::Item { - pearlite! { self@[ix] } - } -} - -impl IndexLogic for [T] { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: usize) -> Self::Item { - pearlite! { self@[ix@] } - } -} - -impl IndexLogic for [T; N] { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: Int) -> Self::Item { - pearlite! { self@[ix] } - } -} - -impl IndexLogic for [T; N] { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: usize) -> Self::Item { - pearlite! { self@[ix@] } - } -} - -impl IndexLogic for Snapshot> { - type Item = T; - - #[logic] - #[open] - #[why3::attr = "inline:trivial"] - fn index_logic(self, ix: Int) -> Self::Item { - pearlite! { (*self)[ix] } - } -} +pub use self::index::IndexLogic; diff --git a/creusot-contracts/src/logic/ops/index.rs b/creusot-contracts/src/logic/ops/index.rs new file mode 100644 index 000000000..6b0f54beb --- /dev/null +++ b/creusot-contracts/src/logic/ops/index.rs @@ -0,0 +1,91 @@ +//! Definition of [`IndexLogic`] + +use crate::*; +use ::std::alloc::Allocator; + +/// Used for indexing operations (`container[index]`) in pearlite. +pub trait IndexLogic { + type Item; + + /// Performs the indexing (`container[index]`) operation. + #[logic] + #[rustc_diagnostic_item = "creusot_index_logic_method"] + fn index_logic(self, idx: I) -> Self::Item; +} + +impl IndexLogic for Vec { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: Int) -> Self::Item { + pearlite! { self@[ix] } + } +} + +impl IndexLogic for Vec { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: usize) -> Self::Item { + pearlite! { self@[ix@] } + } +} + +impl IndexLogic for [T] { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: Int) -> Self::Item { + pearlite! { self@[ix] } + } +} + +impl IndexLogic for [T] { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: usize) -> Self::Item { + pearlite! { self@[ix@] } + } +} + +impl IndexLogic for [T; N] { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: Int) -> Self::Item { + pearlite! { self@[ix] } + } +} + +impl IndexLogic for [T; N] { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: usize) -> Self::Item { + pearlite! { self@[ix@] } + } +} + +impl IndexLogic for Snapshot> { + type Item = T; + + #[logic] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, ix: Int) -> Self::Item { + pearlite! { (*self)[ix] } + } +} diff --git a/creusot-contracts/src/std/deque.rs b/creusot-contracts/src/std/deque.rs index 0daf5535e..2f7336279 100644 --- a/creusot-contracts/src/std/deque.rs +++ b/creusot-contracts/src/std/deque.rs @@ -1,4 +1,4 @@ -use crate::{logic::IndexLogic, resolve::structural_resolve, std::alloc::Allocator, *}; +use crate::{logic::ops::IndexLogic, resolve::structural_resolve, std::alloc::Allocator, *}; pub use ::std::collections::VecDeque; use ::std::{ collections::vec_deque::Iter, diff --git a/creusot-contracts/src/std/iter/filter.rs b/creusot-contracts/src/std/iter/filter.rs index 90a4f9793..bf89598d4 100644 --- a/creusot-contracts/src/std/iter/filter.rs +++ b/creusot-contracts/src/std/iter/filter.rs @@ -1,5 +1,5 @@ -use crate::{inv, logic::*, macros::*, std::ops::*, Invariant, Iterator}; -use std::iter::Filter; +use crate::{logic::Mapping, std::ops::*, *}; +use ::std::iter::Filter; pub trait FilterExt { #[logic] diff --git a/creusot-contracts/src/std/iter/map.rs b/creusot-contracts/src/std/iter/map.rs index d8ec1ed88..fc120b066 100644 --- a/creusot-contracts/src/std/iter/map.rs +++ b/creusot-contracts/src/std/iter/map.rs @@ -1,7 +1,5 @@ -use crate::{ - invariant::*, logic::*, macros::*, resolve, std::ops::*, structural_resolve, Iterator, Resolve, -}; -use std::iter::Map; +use crate::{std::ops::*, structural_resolve, *}; +use ::std::iter::Map; pub trait MapExt { #[logic] diff --git a/creusot/src/contracts_items/diagnostic_items.rs b/creusot/src/contracts_items/diagnostic_items.rs index de40c15a3..94a35f88b 100644 --- a/creusot/src/contracts_items/diagnostic_items.rs +++ b/creusot/src/contracts_items/diagnostic_items.rs @@ -88,7 +88,7 @@ contracts_items! { is_ghost_deref get_ghost_deref fn GhostBox::deref_mut ["ghost_box_deref_mut"] is_ghost_deref_mut get_ghost_deref_mut - fn IndexLogic::index_logic ["index_logic_method"] + fn IndexLogic::index_logic ["creusot_index_logic_method"] is_index_logic get_index_logic fn Deref::deref ["deref_method"] is_deref get_deref From 4c98b56574ac4457abcfd93fe451fc63e5ddc210 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 15:17:56 +0100 Subject: [PATCH 2/8] Add traits for arithmetic in logic --- creusot-contracts-proc/src/pretyping.rs | 56 +++++++-- creusot-contracts/src/logic/int.rs | 64 +++++----- creusot-contracts/src/logic/ops.rs | 6 +- creusot-contracts/src/logic/ops/arithmetic.rs | 118 ++++++++++++++++++ creusot/src/contracts_items/attributes.rs | 4 +- creusot/src/validate.rs | 7 +- 6 files changed, 207 insertions(+), 48 deletions(-) create mode 100644 creusot-contracts/src/logic/ops/arithmetic.rs diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs index 493b1bba0..d9c7a7194 100644 --- a/creusot-contracts-proc/src/pretyping.rs +++ b/creusot-contracts-proc/src/pretyping.rs @@ -1,6 +1,6 @@ use pearlite_syn::Term as RT; use proc_macro2::{Delimiter, Group, Span, TokenStream, TokenTree}; -use syn::{spanned::Spanned, ExprMacro, Pat}; +use syn::{spanned::Spanned, ExprMacro, Pat, UnOp}; use pearlite_syn::term::*; use quote::{quote, quote_spanned, ToTokens}; @@ -50,14 +50,27 @@ pub fn encode_term(term: &RT) -> Result { let mut right = right; use syn::BinOp::*; - if matches!(op, Eq(_) | Ne(_) | Ge(_) | Le(_) | Gt(_) | Lt(_)) { + if matches!( + op, + Eq(_) + | Ne(_) + | Ge(_) + | Le(_) + | Gt(_) + | Lt(_) + | Add(_) + | Sub(_) + | Mul(_) + | Div(_) + | Rem(_) + ) { left = match &**left { - RT::Paren(TermParen { expr, .. }) => &expr, - _ => &*left, + RT::Paren(TermParen { expr, .. }) => expr, + _ => left, }; right = match &**right { - RT::Paren(TermParen { expr, .. }) => &expr, - _ => &*right, + RT::Paren(TermParen { expr, .. }) => expr, + _ => right, }; } @@ -82,6 +95,21 @@ pub fn encode_term(term: &RT) -> Result { Gt(_) => Ok( quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::gt_log(#left, #right) }, ), + Add(_) => Ok( + quote_spanned! {sp=> ::creusot_contracts::logic::ops::AddLogic::add(#left, #right) }, + ), + Sub(_) => Ok( + quote_spanned! {sp=> ::creusot_contracts::logic::ops::SubLogic::sub(#left, #right) }, + ), + Mul(_) => Ok( + quote_spanned! {sp=> ::creusot_contracts::logic::ops::MulLogic::mul(#left, #right) }, + ), + Div(_) => Ok( + quote_spanned! {sp=> ::creusot_contracts::logic::ops::DivLogic::div(#left, #right) }, + ), + Rem(_) => Ok( + quote_spanned! {sp=> ::creusot_contracts::logic::ops::RemLogic::rem(#left, #right) }, + ), _ => Ok(quote_spanned! {sp=> #left #op #right }), } } @@ -209,9 +237,13 @@ pub fn encode_term(term: &RT) -> Result { RT::Type(ty) => Ok(quote_spanned! {sp=> #ty }), RT::Unary(TermUnary { op, expr }) => { let term = encode_term(expr)?; - Ok(quote_spanned! {sp=> - #op #term - }) + if matches!(op, UnOp::Neg(_)) { + Ok(quote_spanned! {sp=> ::creusot_contracts::logic::ops::NegLogic::neg(#term) }) + } else { + Ok(quote_spanned! {sp=> + #op #term + }) + } } RT::Final(TermFinal { term, .. }) => { let term = encode_term(term)?; @@ -253,7 +285,7 @@ pub fn encode_term(term: &RT) -> Result { } RT::Quant(TermQuant { quant_token, args, trigger, term, .. }) => { let mut ts = encode_term(term)?; - ts = encode_trigger(&trigger, ts)?; + ts = encode_trigger(trigger, ts)?; ts = quote_spanned! {sp=> ::creusot_contracts::__stubs::#quant_token( #[creusot::no_translate] @@ -267,7 +299,7 @@ pub fn encode_term(term: &RT) -> Result { RT::Closure(clos) => { let inputs = &clos.inputs; let retty = &clos.output; - let clos = encode_term(&*clos.body)?; + let clos = encode_term(&clos.body)?; Ok( quote_spanned! {sp=> ::creusot_contracts::__stubs::mapping_from_fn(#[creusot::no_translate] |#inputs| #retty #clos)}, @@ -293,7 +325,7 @@ fn encode_trigger( Ok(ts) } -pub fn encode_block(block: &Vec) -> Result { +pub fn encode_block(block: &[TermStmt]) -> Result { let stmts: Vec<_> = block.iter().map(encode_stmt).collect::>()?; Ok(quote! { { #(#stmts)* } }) } diff --git a/creusot-contracts/src/logic/int.rs b/creusot-contracts/src/logic/int.rs index 11a219b90..1457c8432 100644 --- a/creusot-contracts/src/logic/int.rs +++ b/creusot-contracts/src/logic/int.rs @@ -1,4 +1,5 @@ use crate::{ + logic::ops::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic}, std::ops::{Add, Div, Mul, Neg, Rem, Sub}, *, }; @@ -164,68 +165,73 @@ impl Int { } } -#[cfg(creusot)] -impl Add for Int { - type Output = Int; +impl AddLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "add_int"] - fn add(self, _: Int) -> Self { - panic!() + fn add(self, other: Self) -> Self { + let _ = other; + dead } } -#[cfg(creusot)] -impl Sub for Int { - type Output = Int; +impl SubLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "sub_int"] - fn sub(self, _: Int) -> Self { - panic!() + fn sub(self, other: Self) -> Self { + let _ = other; + dead } } -#[cfg(creusot)] -impl Mul for Int { - type Output = Int; +impl MulLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "mul_int"] - fn mul(self, _: Int) -> Self { - panic!() + fn mul(self, other: Self) -> Self { + let _ = other; + dead } } -#[cfg(creusot)] -impl Div for Int { - type Output = Int; +impl DivLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "div_int"] - fn div(self, _: Int) -> Self { - panic!() + fn div(self, other: Self) -> Self { + let _ = other; + dead } } -#[cfg(creusot)] -impl Rem for Int { - type Output = Int; +impl RemLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "rem_int"] - fn rem(self, _: Int) -> Self { - panic!() + fn rem(self, other: Self) -> Self { + let _ = other; + dead } } -#[cfg(creusot)] -impl Neg for Int { - type Output = Int; +impl NegLogic for Int { + type Output = Self; + #[logic] #[trusted] #[creusot::no_translate] #[creusot::builtins = "neg_int"] fn neg(self) -> Self { - panic!() + dead } } diff --git a/creusot-contracts/src/logic/ops.rs b/creusot-contracts/src/logic/ops.rs index 1e58b143f..a290bbcfd 100644 --- a/creusot-contracts/src/logic/ops.rs +++ b/creusot-contracts/src/logic/ops.rs @@ -1,3 +1,7 @@ +mod arithmetic; mod index; -pub use self::index::IndexLogic; +pub use self::{ + arithmetic::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic}, + index::IndexLogic, +}; diff --git a/creusot-contracts/src/logic/ops/arithmetic.rs b/creusot-contracts/src/logic/ops/arithmetic.rs new file mode 100644 index 000000000..26de8149c --- /dev/null +++ b/creusot-contracts/src/logic/ops/arithmetic.rs @@ -0,0 +1,118 @@ +//! Arithmetic operators in logic + +use crate::*; + +/// Trait for addition (`+`) in logic code. +pub trait AddLogic { + type Output; + + #[logic] + fn add(self, other: Rhs) -> Self::Output; +} + +/// Trait for subtraction (`-`) in logic code. +pub trait SubLogic { + type Output; + + #[logic] + fn sub(self, other: Rhs) -> Self::Output; +} + +/// Trait for multiplication (`*`) in logic code. +pub trait MulLogic { + type Output; + + #[logic] + fn mul(self, other: Rhs) -> Self::Output; +} + +/// Trait for division (`/`) in logic code. +pub trait DivLogic { + type Output; + + #[logic] + fn div(self, other: Rhs) -> Self::Output; +} + +/// Trait for remainder (`%`) in logic code. +pub trait RemLogic { + type Output; + + #[logic] + fn rem(self, other: Rhs) -> Self::Output; +} + +/// Trait for negation (unary `-`) in logic code. +pub trait NegLogic { + type Output; + + #[logic] + fn neg(self) -> Self::Output; +} + +macro_rules! logic_traits_impl { + ($($t:ty)*) => { + $( + impl AddLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn add(self, other: Self) -> Int { + pearlite! { self@ + other@ } + } + } + + impl SubLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn sub(self, other: Self) -> Int { + pearlite! { self@ - other@ } + } + } + + impl MulLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn mul(self, other: Self) -> Int { + pearlite! { self@ * other@ } + } + } + + impl DivLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn div(self, other: Self) -> Int { + pearlite! { self@ / other@ } + } + } + + impl RemLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn rem(self, other: Self) -> Int { + pearlite! { self@ % other@ } + } + } + + impl NegLogic for $t { + type Output = Int; + + #[logic] + #[open] + fn neg(self) -> Int { + -self.view() + } + } + )* + }; +} +logic_traits_impl! { i8 i16 i32 i64 u8 u16 u32 u64 isize usize } diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs index b4a9bd8f2..161eb71f8 100644 --- a/creusot/src/contracts_items/attributes.rs +++ b/creusot/src/contracts_items/attributes.rs @@ -148,7 +148,7 @@ fn get_attr<'a>( } let matches = - attr.path.segments.iter().zip(path.iter()).all(|(seg, s)| &*seg.ident.as_str() == *s); + attr.path.segments.iter().zip(path.iter()).all(|(seg, s)| seg.ident.as_str() == *s); if matches { return Some(attr); @@ -172,7 +172,7 @@ fn get_attrs<'a>(attrs: &'a [Attribute], path: &[&str]) -> Vec<&'a Attribute> { } let matches = - item.path.segments.iter().zip(path.iter()).all(|(seg, s)| &*seg.ident.as_str() == *s); + item.path.segments.iter().zip(path.iter()).all(|(seg, s)| seg.ident.as_str() == *s); if matches { matched.push(attr) diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs index e7e7e95c8..c41e2c066 100644 --- a/creusot/src/validate.rs +++ b/creusot/src/validate.rs @@ -51,7 +51,7 @@ pub(crate) fn validate_opacity(ctx: &mut TranslationCtx, item: DefId) -> Option< } } - fn error(&self, id: DefId, span: Span) -> () { + fn error(&self, id: DefId, span: Span) { self.ctx.error( span, &format!( @@ -127,8 +127,7 @@ pub(crate) fn validate_traits(ctx: &mut TranslationCtx) { fn is_overloaded_item(tcx: TyCtxt, def_id: DefId) -> bool { if let Some(name) = tcx.get_diagnostic_name(def_id) { match name.as_str() { - "mul" | "add" | "sub" | "div" | "rem" | "neg" | "box_new" | "deref_method" - | "deref_mut_method" => true, + "box_new" | "deref_method" | "deref_mut_method" => true, _ => { is_snapshot_deref(tcx, def_id) || is_ghost_deref(tcx, def_id) @@ -244,7 +243,7 @@ pub(crate) enum Purity { } impl Purity { - pub(crate) fn of_def_id<'tcx>(ctx: &mut TranslationCtx<'tcx>, def_id: DefId) -> Self { + pub(crate) fn of_def_id(ctx: &mut TranslationCtx, def_id: DefId) -> Self { let is_snapshot = is_snapshot_closure(ctx.tcx, def_id); if is_predicate(ctx.tcx, def_id) && is_prophetic(ctx.tcx, def_id) || is_logic(ctx.tcx, def_id) && is_prophetic(ctx.tcx, def_id) From 0fd51d9010b606e37393e4920e322c1dcde6c2ea Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 15:45:17 +0100 Subject: [PATCH 3/8] Add traits for arithmetic on `Int` in ghost code --- creusot-contracts/src/logic/int.rs | 77 ++++++++++++++++++++++++++ creusot-contracts/src/model.rs | 10 ++++ creusot-contracts/src/std/panicking.rs | 4 ++ 3 files changed, 91 insertions(+) diff --git a/creusot-contracts/src/logic/int.rs b/creusot-contracts/src/logic/int.rs index 1457c8432..ac8fa5a04 100644 --- a/creusot-contracts/src/logic/int.rs +++ b/creusot-contracts/src/logic/int.rs @@ -235,3 +235,80 @@ impl NegLogic for Int { dead } } + +// ========== Ghost operations ============= + +impl PartialEq for Int { + #[trusted] + #[pure] + #[ensures(result == (*self == *other))] + fn eq(&self, other: &Self) -> bool { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Add for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == self + other)] + fn add(self, other: Int) -> Self { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Sub for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == self - other)] + fn sub(self, other: Int) -> Self { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Mul for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == self * other)] + fn mul(self, other: Int) -> Self { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Div for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == self / other)] + fn div(self, other: Int) -> Self { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Rem for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == self % other)] + fn rem(self, other: Int) -> Self { + let _ = other; + unreachable!("BUG: called ghost function in normal code") + } +} + +impl Neg for Int { + type Output = Int; + #[trusted] + #[pure] + #[ensures(result == -self)] + fn neg(self) -> Self { + unreachable!("BUG: called ghost function in normal code") + } +} diff --git a/creusot-contracts/src/model.rs b/creusot-contracts/src/model.rs index f89c176cc..c58299e72 100644 --- a/creusot-contracts/src/model.rs +++ b/creusot-contracts/src/model.rs @@ -117,6 +117,16 @@ impl DeepModel for bool { } } +impl DeepModel for Int { + type DeepModelTy = Int; + + #[logic] + #[open] + fn deep_model(self) -> Self::DeepModelTy { + self + } +} + impl View for String { type ViewTy = Seq; diff --git a/creusot-contracts/src/std/panicking.rs b/creusot-contracts/src/std/panicking.rs index 0a170315b..2db072188 100644 --- a/creusot-contracts/src/std/panicking.rs +++ b/creusot-contracts/src/std/panicking.rs @@ -34,6 +34,10 @@ extern_spec! { #[requires(false)] fn panic_nounwind_nobacktrace(expr: &'static str) -> !; + #[pure] + #[requires(false)] + fn unreachable_display(x: &T) -> !; + #[pure] #[requires(false)] fn assert_failed(kind: AssertKind, left: &T, right: &U, args: Option>) -> ! From ce2f90b9539c05c2390ff2a644cbe2a4c7d4ba69 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 15:45:38 +0100 Subject: [PATCH 4/8] Add a test --- .../tests/should_succeed/ghost/integers.coma | 246 ++++++++++++++++++ .../tests/should_succeed/ghost/integers.rs | 23 ++ .../ghost/integers/why3session.xml | 14 + .../ghost/integers/why3shapes.gz | Bin 0 -> 315 bytes 4 files changed, 283 insertions(+) create mode 100644 creusot/tests/should_succeed/ghost/integers.coma create mode 100644 creusot/tests/should_succeed/ghost/integers.rs create mode 100644 creusot/tests/should_succeed/ghost/integers/why3session.xml create mode 100644 creusot/tests/should_succeed/ghost/integers/why3shapes.gz diff --git a/creusot/tests/should_succeed/ghost/integers.coma b/creusot/tests/should_succeed/ghost/integers.coma new file mode 100644 index 000000000..5fcc060d0 --- /dev/null +++ b/creusot/tests/should_succeed/ghost/integers.coma @@ -0,0 +1,246 @@ +module M_integers__in_ghost_block [#"integers.rs" 4 0 4 23] + let%span sintegers0 = "integers.rs" 5 19 5 23 + let%span sintegers1 = "integers.rs" 7 16 7 20 + let%span sintegers2 = "integers.rs" 9 20 9 24 + let%span sintegers3 = "integers.rs" 10 22 10 28 + let%span sintegers4 = "integers.rs" 14 31 14 35 + let%span sintegers5 = "integers.rs" 14 37 14 42 + let%span sintegers6 = "integers.rs" 14 44 14 48 + let%span sintegers7 = "integers.rs" 15 22 15 28 + let%span sint8 = "../../../../creusot-contracts/src/logic/int.rs" 60 14 60 31 + let%span sghost9 = "../../../../creusot-contracts/src/ghost.rs" 199 22 199 26 + let%span sghost10 = "../../../../creusot-contracts/src/ghost.rs" 199 4 199 32 + let%span sghost11 = "../../../../creusot-contracts/src/ghost.rs" 197 14 197 31 + let%span sghost12 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 + let%span sghost13 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 + let%span sghost14 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 + let%span sghost15 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 + let%span sghost16 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 + let%span sghost17 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 + let%span sint18 = "../../../../creusot-contracts/src/logic/int.rs" 255 14 255 36 + let%span sint19 = "../../../../creusot-contracts/src/logic/int.rs" 277 14 277 36 + let%span sintegers20 = "integers.rs" 20 10 20 29 + let%span sghost21 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 + + use prelude.prelude.Int128 + + use prelude.prelude.Int + + type t_GhostBox'0 = + { t_GhostBox__0'0: int } + + function inner_logic'0 (self : t_GhostBox'0) : int = + [%#sghost21] self.t_GhostBox__0'0 + + use prelude.prelude.Int128 + + let rec new'0 (value:int128) (return' (ret:t_GhostBox'0))= any + [ return' (result:t_GhostBox'0)-> {[%#sint8] inner_logic'0 result = Int128.to_int value} (! return' {result}) ] + + + predicate inv'0 (_1 : t_GhostBox'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'0 [inv'0 x] . inv'0 x = true + + predicate inv'1 (_1 : int) + + axiom inv_axiom'1 [@rewrite] : forall x : int [inv'1 x] . inv'1 x = true + + let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:int))= {[@expl:into_inner 'self' type invariant] [%#sghost9] inv'0 self} + any + [ return' (result:int)-> {[%#sghost10] inv'1 result} + {[%#sghost11] result = self.t_GhostBox__0'0} + (! return' {result}) ] + + + let rec new'1 (x:int) (return' (ret:t_GhostBox'0))= {[@expl:new 'x' type invariant] [%#sghost12] inv'1 x} + any + [ return' (result:t_GhostBox'0)-> {[%#sghost13] inv'0 result} + {[%#sghost14] result.t_GhostBox__0'0 = x} + (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + let rec closure0'0 (_1:()) (return' (ret:t_GhostBox'0))= bb0 + [ bb0 = s0 + [ s0 = new'0 {[%#sintegers0] (1 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_3 <- _ret' ] s1) | s1 = bb1 ] + + | bb1 = s0 [ s0 = into_inner'0 {_3} (fun (_ret':int) -> [ &_2 <- _ret' ] s1) | s1 = bb2 ] + | bb2 = s0 [ s0 = new'1 {_2} (fun (_ret':t_GhostBox'0) -> [ &_0 <- _ret' ] s1) | s1 = bb3 ] + | bb3 = return' {_0} ] + [ & _0 : t_GhostBox'0 = any_l () | & _2 : int = any_l () | & _3 : t_GhostBox'0 = any_l () ] + [ return' (result:t_GhostBox'0)-> return' {result} ] + + + use prelude.prelude.Borrow + + predicate inv'2 (_1 : t_GhostBox'0) + + axiom inv_axiom'2 [@rewrite] : forall x : t_GhostBox'0 [inv'2 x] . inv'2 x = true + + predicate inv'3 (_1 : int) + + axiom inv_axiom'3 [@rewrite] : forall x : int [inv'3 x] . inv'3 x = true + + let rec deref'0 (self:t_GhostBox'0) (return' (ret:int))= {[@expl:deref 'self' type invariant] [%#sghost15] inv'2 self} + any + [ return' (result:int)-> {[%#sghost16] inv'3 result} + {[%#sghost17] self.t_GhostBox__0'0 = result} + (! return' {result}) ] + + + let rec add'0 (self:int) (other:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sint18] result = self + other} (! return' {result}) ] + + + let rec mul'0 (self:int) (other:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sint19] result = self * other} (! return' {result}) ] + + + predicate inv'4 (_1 : ()) + + axiom inv_axiom'4 [@rewrite] : forall x : () [inv'4 x] . inv'4 x = true + + type t_GhostBox'1 = + { t_GhostBox__0'1: () } + + predicate inv'5 (_1 : t_GhostBox'1) + + axiom inv_axiom'5 [@rewrite] : forall x : t_GhostBox'1 [inv'5 x] . inv'5 x = true + + let rec new'2 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost12] inv'4 x} + any + [ return' (result:t_GhostBox'1)-> {[%#sghost13] inv'5 result} + {[%#sghost14] result.t_GhostBox__0'1 = x} + (! return' {result}) ] + + + type closure1'1 = + { field_0'0: t_GhostBox'0 } + + let rec closure1'0 (_1:closure1'1) (return' (ret:t_GhostBox'1))= bb0 + [ bb0 = s0 + [ s0 = new'0 {[%#sintegers1] (2 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_4 <- _ret' ] s1) | s1 = bb1 ] + + | bb1 = s0 [ s0 = into_inner'0 {_4} (fun (_ret':int) -> [ &y <- _ret' ] s1) | s1 = bb2 ] + | bb2 = s0 [ s0 = deref'0 {_1.field_0'0} (fun (_ret':int) -> [ &_7 <- _ret' ] s1) | s1 = bb3 ] + | bb3 = s0 [ s0 = add'0 {_7} {y} (fun (_ret':int) -> [ &z <- _ret' ] s1) | s1 = bb4 ] + | bb4 = s0 + [ s0 = new'0 {[%#sintegers2] (3 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_13 <- _ret' ] s1) | s1 = bb5 ] + + | bb5 = s0 [ s0 = into_inner'0 {_13} (fun (_ret':int) -> [ &_12 <- _ret' ] s1) | s1 = bb6 ] + | bb6 = s0 [ s0 = mul'0 {z} {_12} (fun (_ret':int) -> [ &w <- _ret' ] s1) | s1 = bb7 ] + | bb7 = s0 + [ s0 = {[@expl:assertion] [%#sintegers3] w = 9} s1 + | s1 = new'2 {_2} (fun (_ret':t_GhostBox'1) -> [ &_0 <- _ret' ] s2) + | s2 = bb8 ] + + | bb8 = return' {_0} ] + + [ & _0 : t_GhostBox'1 = any_l () + | & _1 : closure1'1 = _1 + | & _2 : () = any_l () + | & y : int = any_l () + | & _4 : t_GhostBox'0 = any_l () + | & z : int = any_l () + | & _7 : int = any_l () + | & w : int = any_l () + | & _12 : int = any_l () + | & _13 : t_GhostBox'0 = any_l () ] + [ return' (result:t_GhostBox'1)-> return' {result} ] + + let rec ghost_function'0 (x:int) (y:int) (z:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sintegers20] result = x + mod y z} (! return' {result}) ] + + + let rec closure2'0 (_1:()) (return' (ret:t_GhostBox'1))= bb0 + [ bb0 = s0 + [ s0 = new'0 {[%#sintegers4] (4 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_5 <- _ret' ] s1) | s1 = bb1 ] + + | bb1 = s0 [ s0 = into_inner'0 {_5} (fun (_ret':int) -> [ &_4 <- _ret' ] s1) | s1 = bb2 ] + | bb2 = s0 + [ s0 = new'0 {[%#sintegers5] (13 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_7 <- _ret' ] s1) | s1 = bb3 ] + + | bb3 = s0 [ s0 = into_inner'0 {_7} (fun (_ret':int) -> [ &_6 <- _ret' ] s1) | s1 = bb4 ] + | bb4 = s0 + [ s0 = new'0 {[%#sintegers6] (5 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_9 <- _ret' ] s1) | s1 = bb5 ] + + | bb5 = s0 [ s0 = into_inner'0 {_9} (fun (_ret':int) -> [ &_8 <- _ret' ] s1) | s1 = bb6 ] + | bb6 = s0 [ s0 = ghost_function'0 {_4} {_6} {_8} (fun (_ret':int) -> [ &x <- _ret' ] s1) | s1 = bb7 ] + | bb7 = s0 + [ s0 = {[@expl:assertion] [%#sintegers7] x = 7} s1 + | s1 = new'2 {_2} (fun (_ret':t_GhostBox'1) -> [ &_0 <- _ret' ] s2) + | s2 = bb8 ] + + | bb8 = return' {_0} ] + + [ & _0 : t_GhostBox'1 = any_l () + | & _2 : () = any_l () + | & x : int = any_l () + | & _4 : int = any_l () + | & _5 : t_GhostBox'0 = any_l () + | & _6 : int = any_l () + | & _7 : t_GhostBox'0 = any_l () + | & _8 : int = any_l () + | & _9 : t_GhostBox'0 = any_l () ] + [ return' (result:t_GhostBox'1)-> return' {result} ] + + meta "compute_max_steps" 1000000 + + let rec in_ghost_block'0 (_1:()) (return' (ret:()))= (! bb0 + [ bb0 = s0 + [ s0 = [ &_2 <- () ] s1 | s1 = closure0'0 {_2} (fun (_ret':t_GhostBox'0) -> [ &x <- _ret' ] s2) | s2 = bb1 ] + + | bb1 = s0 + [ s0 = [ &_5 <- { field_0'0 = x } ] s1 + | s1 = closure1'0 {_5} (fun (_ret':t_GhostBox'1) -> [ &_4 <- _ret' ] s2) + | s2 = bb2 ] + + | bb2 = bb3 + | bb3 = s0 + [ s0 = [ &_9 <- () ] s1 | s1 = closure2'0 {_9} (fun (_ret':t_GhostBox'1) -> [ &_8 <- _ret' ] s2) | s2 = bb4 ] + + | bb4 = bb5 + | bb5 = bb6 + | bb6 = return' {_0} ] + ) + [ & _0 : () = any_l () + | & x : t_GhostBox'0 = any_l () + | & _2 : () = any_l () + | & _3 : () = any_l () + | & _4 : t_GhostBox'1 = any_l () + | & _5 : closure1'1 = any_l () + | & _7 : () = any_l () + | & _8 : t_GhostBox'1 = any_l () + | & _9 : () = any_l () + | & _10 : () = any_l () ] + [ return' (result:())-> (! return' {result}) ] +end +module M_integers__ghost_function [#"integers.rs" 21 0 21 52] + let%span sintegers0 = "integers.rs" 20 10 20 29 + let%span sint1 = "../../../../creusot-contracts/src/logic/int.rs" 299 14 299 36 + let%span sint2 = "../../../../creusot-contracts/src/logic/int.rs" 255 14 255 36 + + use prelude.prelude.Int + + let rec rem'0 (self:int) (other:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sint1] result = mod self other} (! return' {result}) ] + + + let rec add'0 (self:int) (other:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sint2] result = self + other} (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + meta "compute_max_steps" 1000000 + + let rec ghost_function'0 (x:int) (y:int) (z:int) (return' (ret:int))= (! bb0 + [ bb0 = s0 [ s0 = rem'0 {y} {z} (fun (_ret':int) -> [ &_6 <- _ret' ] s1) | s1 = bb1 ] + | bb1 = s0 [ s0 = add'0 {x} {_6} (fun (_ret':int) -> [ &_0 <- _ret' ] s1) | s1 = bb2 ] + | bb2 = return' {_0} ] + ) [ & _0 : int = any_l () | & x : int = x | & y : int = y | & z : int = z | & _6 : int = any_l () ] + [ return' (result:int)-> {[@expl:ghost_function ensures] [%#sintegers0] result = x + mod y z} (! return' {result}) ] + +end diff --git a/creusot/tests/should_succeed/ghost/integers.rs b/creusot/tests/should_succeed/ghost/integers.rs new file mode 100644 index 000000000..40535d231 --- /dev/null +++ b/creusot/tests/should_succeed/ghost/integers.rs @@ -0,0 +1,23 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +pub fn in_ghost_block() { + let x = ghost!(1int); + ghost! { + let y = 2int; + let z = *x + y; + let w = z * 3int; + proof_assert!(w == 9); + }; + + ghost! { + let x = ghost_function(4int, 13int, 5int); + proof_assert!(x == 7); + }; +} + +#[pure] +#[ensures(result == x + y % z)] +pub fn ghost_function(x: Int, y: Int, z: Int) -> Int { + x + y % z +} diff --git a/creusot/tests/should_succeed/ghost/integers/why3session.xml b/creusot/tests/should_succeed/ghost/integers/why3session.xml new file mode 100644 index 000000000..00bfc5856 --- /dev/null +++ b/creusot/tests/should_succeed/ghost/integers/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/ghost/integers/why3shapes.gz b/creusot/tests/should_succeed/ghost/integers/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..34c688c5f225035076c33d1e103868eb1be54b26 GIT binary patch literal 315 zcmV-B0mS|viwFP!00000|8yMcD1>Ty^24dhZTxvkFbPcntbCIy9F^pzti%0|d{4J&Dq@ zU{9g)EZEbiJqz|?j6I9sen`|@ixa(moKKZVX-!K6pt{{6NCZ{doC~P*UXS|XdEa*Z zQ~Mc-s6Ha7oYn}6`nEVUeHr^HBWE*m$VkqB`VPTt2!;@FNc)`DWA$GG(bgQ`{WH-58D$^0o&pntc2S$;+RF_2~#T zOgD3MbHkbGihWSk=l)s@zc2`#lG_a>!fiJ@t9M2U3#1c4yA4sP Date: Tue, 3 Dec 2024 15:46:23 +0100 Subject: [PATCH 5/8] Fix tests --- creusot/tests/should_fail/bug/436_0.rs | 8 ++++---- creusot/tests/should_succeed/bug/545.rs | 2 +- creusot/tests/should_succeed/bug/682.rs | 2 +- creusot/tests/should_succeed/cell/01.rs | 2 +- creusot/tests/should_succeed/list_reversal_lasso.rs | 2 +- creusot/tests/should_succeed/mc91.rs | 2 +- creusot/tests/should_succeed/mutex.rs | 2 +- 7 files changed, 10 insertions(+), 10 deletions(-) diff --git a/creusot/tests/should_fail/bug/436_0.rs b/creusot/tests/should_fail/bug/436_0.rs index 1fa6e050a..2fe0f54ff 100644 --- a/creusot/tests/should_fail/bug/436_0.rs +++ b/creusot/tests/should_fail/bug/436_0.rs @@ -2,16 +2,16 @@ extern crate creusot_contracts; use creusot_contracts::*; struct S { - g: Snapshot, + g: Snapshot, } #[logic(prophetic)] -fn prophecy(x: &mut S) -> i32 { +fn prophecy(x: &mut S) -> Int { pearlite! { *(^x).g } } pub fn f() { - let b = &mut S { g: snapshot! { 1i32 } }; - b.g = snapshot! { prophecy(b) + 1i32 }; + let b = &mut S { g: snapshot! { 1 } }; + b.g = snapshot! { prophecy(b) + 1 }; proof_assert! { false } } diff --git a/creusot/tests/should_succeed/bug/545.rs b/creusot/tests/should_succeed/bug/545.rs index 170dde32a..5ac86e5ea 100644 --- a/creusot/tests/should_succeed/bug/545.rs +++ b/creusot/tests/should_succeed/bug/545.rs @@ -2,5 +2,5 @@ extern crate creusot_contracts; use creusot_contracts::*; pub fn negative_is_negative() { - proof_assert!(0i32 > -100i32); + proof_assert!(0 > -100); } diff --git a/creusot/tests/should_succeed/bug/682.rs b/creusot/tests/should_succeed/bug/682.rs index e26d997f3..722431d34 100644 --- a/creusot/tests/should_succeed/bug/682.rs +++ b/creusot/tests/should_succeed/bug/682.rs @@ -1,7 +1,7 @@ extern crate creusot_contracts; use creusot_contracts::*; -#[requires(*a <= u64::MAX / 2u64)] +#[requires((*a)@ <= u64::MAX / 2u64)] #[ensures(^a > *a)] fn add_some(a: &mut u64) { *a += 1; diff --git a/creusot/tests/should_succeed/cell/01.rs b/creusot/tests/should_succeed/cell/01.rs index c74245cea..e973635fb 100644 --- a/creusot/tests/should_succeed/cell/01.rs +++ b/creusot/tests/should_succeed/cell/01.rs @@ -33,7 +33,7 @@ impl Inv for Even { #[open] #[predicate] fn inv(x: u32) -> bool { - x % 2u32 == 0u32 + x.view() % 2 == 0 } } diff --git a/creusot/tests/should_succeed/list_reversal_lasso.rs b/creusot/tests/should_succeed/list_reversal_lasso.rs index 52ee499a1..a41990933 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso.rs +++ b/creusot/tests/should_succeed/list_reversal_lasso.rs @@ -2,7 +2,7 @@ extern crate creusot_contracts; -use creusot_contracts::{logic::IndexLogic, *}; +use creusot_contracts::{logic::ops::IndexLogic, *}; use std::ops::{Index, IndexMut}; /* Memory model */ diff --git a/creusot/tests/should_succeed/mc91.rs b/creusot/tests/should_succeed/mc91.rs index 5743ff861..e85f56bc7 100644 --- a/creusot/tests/should_succeed/mc91.rs +++ b/creusot/tests/should_succeed/mc91.rs @@ -3,7 +3,7 @@ extern crate creusot_contracts; use creusot_contracts::*; #[ensures(x <= 100u32 ==> result == 91u32 && - x > 100u32 ==> result == x - 10u32)] + x > 100u32 ==> result@ == x - 10u32)] pub fn mc91(x: u32) -> u32 { if x > 100 { x - 10 diff --git a/creusot/tests/should_succeed/mutex.rs b/creusot/tests/should_succeed/mutex.rs index afea3c389..296264f4a 100644 --- a/creusot/tests/should_succeed/mutex.rs +++ b/creusot/tests/should_succeed/mutex.rs @@ -64,7 +64,7 @@ impl Inv for Even { #[open(self)] #[predicate] fn inv(&self, x: u32) -> bool { - x % 2u32 == 0u32 + x.view() % 2 == 0 } } From cabdb12290191454ff41b5de010ebdd857dc2a80 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 15:52:13 +0100 Subject: [PATCH 6/8] Update tests --- .../creusot-contracts/creusot-contracts.coma | 240 ++++++++++-------- .../creusot-contracts/why3session.xml | 17 +- .../creusot-contracts/why3shapes.gz | Bin 25365 -> 25522 bytes creusot/tests/should_fail/bug/436_0.stderr | 2 +- creusot/tests/should_succeed/100doors.coma | 4 +- creusot/tests/should_succeed/bug/545.coma | 6 +- .../should_succeed/bug/545/why3session.xml | 2 +- .../should_succeed/bug/545/why3shapes.gz | Bin 108 -> 101 bytes creusot/tests/should_succeed/bug/682.coma | 32 ++- .../should_succeed/bug/682/why3session.xml | 8 +- .../should_succeed/bug/682/why3shapes.gz | Bin 249 -> 247 bytes .../should_succeed/bug/final_borrows.coma | 8 +- .../tests/should_succeed/bug/two_phase.coma | 4 +- creusot/tests/should_succeed/cell/01.coma | 6 +- .../should_succeed/cell/01/why3shapes.gz | Bin 202 -> 202 bytes creusot/tests/should_succeed/cell/02.coma | 4 +- .../tests/should_succeed/filter_positive.coma | 4 +- .../tests/should_succeed/ghost/ghost_vec.coma | 2 +- creusot/tests/should_succeed/hashmap.coma | 20 +- .../should_succeed/heapsort_generic.coma | 8 +- creusot/tests/should_succeed/hillel.coma | 36 +-- creusot/tests/should_succeed/index_range.coma | 24 +- .../tests/should_succeed/insertion_sort.coma | 8 +- .../should_succeed/iterators/02_iter_mut.coma | 36 +-- .../iterators/03_std_iterators.coma | 36 +-- .../should_succeed/iterators/04_skip.coma | 4 +- .../iterators/08_collect_extend.coma | 4 +- .../should_succeed/iterators/17_filter.coma | 8 +- creusot/tests/should_succeed/knapsack.coma | 8 +- .../tests/should_succeed/knapsack_full.coma | 10 +- .../should_succeed/list_reversal_lasso.coma | 40 +-- creusot/tests/should_succeed/mc91.coma | 10 +- .../tests/should_succeed/mc91/why3session.xml | 4 +- .../tests/should_succeed/mc91/why3shapes.gz | Bin 209 -> 217 bytes creusot/tests/should_succeed/mutex.coma | 12 +- .../tests/should_succeed/mutex/why3shapes.gz | Bin 418 -> 417 bytes .../selection_sort_generic.coma | 4 +- creusot/tests/should_succeed/slices/01.coma | 8 +- .../tests/should_succeed/slices/02_std.coma | 4 +- .../tests/should_succeed/sparse_array.coma | 28 +- .../should_succeed/syntax/11_array_types.coma | 4 +- .../should_succeed/syntax/13_vec_macro.coma | 4 +- .../syntax/derive_macros/mixed.coma | 8 +- .../should_succeed/syntax/int_suffix.coma | 2 +- .../tests/should_succeed/take_first_mut.coma | 4 +- creusot/tests/should_succeed/trigger2.coma | 8 +- .../type_invariants/vec_inv.coma | 4 +- creusot/tests/should_succeed/vector/01.coma | 4 +- .../tests/should_succeed/vector/02_gnome.coma | 4 +- .../vector/04_binary_search.coma | 4 +- .../vector/05_binary_search_generic.coma | 4 +- .../vector/06_knights_tour.coma | 36 +-- .../should_succeed/vector/08_haystack.coma | 4 +- .../should_succeed/vector/09_capacity.coma | 4 +- 54 files changed, 397 insertions(+), 348 deletions(-) diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index 8de78617c..dda7dcb8a 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -906,7 +906,7 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_r let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice4 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel5 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops6 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex6 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -962,10 +962,10 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops6] Seq.get (view'2 self) ix + [%#sindex6] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -996,7 +996,7 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_t let%span sslice5 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel7 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops8 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex8 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice9 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice10 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -1050,10 +1050,10 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops8] Seq.get (view'2 self) ix + [%#sindex8] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -2621,13 +2621,13 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fu -> ([%#sfuse1] inv'1 next) -> ([%#sfuse0] inv'0 self) -> ([%#sfuse5] steps = (Seq.empty : Seq.seq t_Item'0) /\ self.final = next) end -module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl [#"../../../creusot-contracts/src/std/iter/map.rs" 83 4 83 26] (* as std::iter::Iterator> *) - let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 81 15 81 24 - let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 82 14 82 45 - let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 79 4 79 10 - let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 64 12 75 75 - let%span smap4 = "../../../creusot-contracts/src/std/iter/map.rs" 24 14 24 39 - let%span smap5 = "../../../creusot-contracts/src/std/iter/map.rs" 17 14 17 39 +module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl [#"../../../creusot-contracts/src/std/iter/map.rs" 81 4 81 26] (* as std::iter::Iterator> *) + let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 79 15 79 24 + let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 80 14 80 45 + let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 77 4 77 10 + let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 62 12 73 75 + let%span smap4 = "../../../creusot-contracts/src/std/iter/map.rs" 22 14 22 39 + let%span smap5 = "../../../creusot-contracts/src/std/iter/map.rs" 15 14 15 39 let%span sops6 = "../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 let%span sops7 = "../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 let%span sops8 = "../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 @@ -2671,7 +2671,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 25 4 25 22] (self : t_Map'0) : t_F'0 + function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 23 4 23 22] (self : t_Map'0) : t_F'0 axiom func'0_spec : forall self : t_Map'0 . [%#smap4] inv'0 self -> inv'4 (func'0 self) @@ -2765,7 +2765,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_Item'0 [inv'2 x] . inv'2 x = invariant'1 x - function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 18 4 18 22] (self : t_Map'0) : t_I'0 + function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 16 4 16 22] (self : t_Map'0) : t_I'0 axiom iter'0_spec : forall self : t_Map'0 . [%#smap5] inv'0 self -> inv'3 (iter'0 self) @@ -2798,7 +2798,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 62 4 62 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) + predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 60 4 60 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) = [%#smap3] unnest'0 (func'0 self) (func'0 succ) @@ -2820,21 +2820,21 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc constant self : t_Map'0 - function produces_refl'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 83 4 83 26] (self : t_Map'0) : () + function produces_refl'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 81 4 81 26] (self : t_Map'0) : () goal vc_produces_refl'0 : ([%#smap0] inv'0 self) -> ([%#smap1] produces'0 self (Seq.empty : Seq.seq t_B'0) self) end -module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans [#"../../../creusot-contracts/src/std/iter/map.rs" 93 4 93 90] (* as std::iter::Iterator> *) - let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 87 15 87 21 - let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 88 15 88 21 - let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 89 15 89 21 - let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 90 15 90 32 - let%span smap4 = "../../../creusot-contracts/src/std/iter/map.rs" 91 15 91 32 - let%span smap5 = "../../../creusot-contracts/src/std/iter/map.rs" 92 14 92 42 - let%span smap6 = "../../../creusot-contracts/src/std/iter/map.rs" 85 4 85 10 - let%span smap7 = "../../../creusot-contracts/src/std/iter/map.rs" 64 12 75 75 - let%span smap8 = "../../../creusot-contracts/src/std/iter/map.rs" 24 14 24 39 - let%span smap9 = "../../../creusot-contracts/src/std/iter/map.rs" 17 14 17 39 +module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans [#"../../../creusot-contracts/src/std/iter/map.rs" 91 4 91 90] (* as std::iter::Iterator> *) + let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 85 15 85 21 + let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 86 15 86 21 + let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 87 15 87 21 + let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 88 15 88 32 + let%span smap4 = "../../../creusot-contracts/src/std/iter/map.rs" 89 15 89 32 + let%span smap5 = "../../../creusot-contracts/src/std/iter/map.rs" 90 14 90 42 + let%span smap6 = "../../../creusot-contracts/src/std/iter/map.rs" 83 4 83 10 + let%span smap7 = "../../../creusot-contracts/src/std/iter/map.rs" 62 12 73 75 + let%span smap8 = "../../../creusot-contracts/src/std/iter/map.rs" 22 14 22 39 + let%span smap9 = "../../../creusot-contracts/src/std/iter/map.rs" 15 14 15 39 let%span sops10 = "../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 let%span sops11 = "../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 let%span sops12 = "../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 @@ -2876,7 +2876,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 25 4 25 22] (self : t_Map'0) : t_F'0 + function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 23 4 23 22] (self : t_Map'0) : t_F'0 axiom func'0_spec : forall self : t_Map'0 . [%#smap8] inv'0 self -> inv'4 (func'0 self) @@ -2970,7 +2970,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_Item'0 [inv'2 x] . inv'2 x = invariant'1 x - function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 18 4 18 22] (self : t_Map'0) : t_I'0 + function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 16 4 16 22] (self : t_Map'0) : t_I'0 axiom iter'0_spec : forall self : t_Map'0 . [%#smap9] inv'0 self -> inv'3 (iter'0 self) @@ -3003,7 +3003,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 62 4 62 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) + predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 60 4 60 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) = [%#smap7] unnest'0 (func'0 self) (func'0 succ) @@ -3035,7 +3035,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc constant c : t_Map'0 - function produces_trans'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 93 4 93 90] (a : t_Map'0) (ab : Seq.seq t_B'0) (b : t_Map'0) (bc : Seq.seq t_B'0) (c : t_Map'0) : () + function produces_trans'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 91 4 91 90] (a : t_Map'0) (ab : Seq.seq t_B'0) (b : t_Map'0) (bc : Seq.seq t_B'0) (c : t_Map'0) : () goal vc_produces_trans'0 : ([%#smap4] produces'0 b bc c) @@ -8623,7 +8623,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_r let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice4 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel5 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops6 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex6 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -8676,10 +8676,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops6] Seq.get (view'2 self) ix + [%#sindex6] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -8710,7 +8710,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_t let%span sslice5 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel7 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops8 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex8 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice9 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice10 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -8761,10 +8761,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops8] Seq.get (view'2 self) ix + [%#sindex8] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -8807,7 +8807,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_r let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span smodel9 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops10 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex10 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 use prelude.prelude.Opaque @@ -8868,10 +8868,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops10] Seq.get (view'1 self) ix + [%#sindex10] Seq.get (view'1 self) ix function to_mut_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 90 4 90 43] (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -8911,7 +8911,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_t let%span sslice11 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice12 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span smodel13 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops14 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex14 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 use prelude.prelude.Opaque @@ -8970,10 +8970,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops14] Seq.get (view'1 self) ix + [%#sindex14] Seq.get (view'1 self) ix function to_mut_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 90 4 90 43] (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -21513,11 +21513,11 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2208779330486735413__ goal refines : [%#senumerate0] forall self : t_Enumerate'0 . structural_resolve'0 self /\ inv'0 self -> structural_resolve'0 self /\ (forall result : () . resolve'0 self -> resolve'0 self) end -module M_creusot_contracts__stdqy35z1__iter__map__qyi13484997498660514945__resolve_coherence__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 42 4 42 31] (* as resolve::Resolve> *) - let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 42 4 42 31 - let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 34 8 34 54 - let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 17 14 17 39 - let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 24 14 24 39 +module M_creusot_contracts__stdqy35z1__iter__map__qyi13484997498660514945__resolve_coherence__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 40 4 40 31] (* as resolve::Resolve> *) + let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 40 4 40 31 + let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 32 8 32 54 + let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 15 14 15 39 + let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 22 14 22 39 let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 use prelude.prelude.Borrow @@ -21556,15 +21556,15 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi13484997498660514945__resol axiom inv_axiom'0 [@rewrite] : forall x : t_Map'0 [inv'0 x] . inv'0 x = invariant'0 x - function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 18 4 18 22] (self : t_Map'0) : t_I'0 + function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 16 4 16 22] (self : t_Map'0) : t_I'0 axiom iter'0_spec : forall self : t_Map'0 . [%#smap2] inv'1 self -> inv'2 (iter'0 self) - function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 25 4 25 22] (self : t_Map'0) : t_F'0 + function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 23 4 23 22] (self : t_Map'0) : t_F'0 axiom func'0_spec : forall self : t_Map'0 . [%#smap3] inv'1 self -> inv'3 (func'0 self) - predicate resolve'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 33 4 33 28] (self : t_Map'0) = + predicate resolve'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 31 4 31 28] (self : t_Map'0) = [%#smap1] resolve'2 (iter'0 self) /\ resolve'1 (func'0 self) goal refines : [%#smap0] forall self : t_Map'0 . structural_resolve'0 self /\ inv'0 self @@ -21806,7 +21806,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe let%span svec0 = "../../../creusot-contracts/src/std/vec.rs" 56 4 56 31 let%span svec1 = "../../../creusot-contracts/src/std/vec.rs" 49 20 49 83 let%span svec2 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops3 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex3 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 @@ -21896,10 +21896,10 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 21 4 21 47] (self : t_Vec'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 22 4 22 47] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops3] Seq.get (view'0 self) ix + [%#sindex3] Seq.get (view'0 self) ix predicate resolve'3 [#"../../../creusot-contracts/src/resolve.rs" 19 0 19 40] (_1 : t_T'0) @@ -22226,7 +22226,7 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_r let%span sslice2 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel4 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops5 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex5 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -22286,10 +22286,10 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops5] Seq.get (view'2 self) ix + [%#sindex5] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -22315,7 +22315,7 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_t let%span sslice2 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel4 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops5 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex5 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -22369,10 +22369,10 @@ module M_creusot_contracts__stdqy35z1__deque__qyi3159098507555769709__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops5] Seq.get (view'2 self) ix + [%#sindex5] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -23625,11 +23625,11 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi10730559947553418603__prod /\ (forall result : () . produces'0 self (Seq.empty : Seq.seq t_Item'0) self -> produces'0 self (Seq.empty : Seq.seq t_Item'0) self) end -module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 83 4 83 26] (* as std::iter::Iterator> *) - let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 83 4 83 26 - let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 64 12 75 75 - let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 24 14 24 39 - let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 17 14 17 39 +module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_refl__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 81 4 81 26] (* as std::iter::Iterator> *) + let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 81 4 81 26 + let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 62 12 73 75 + let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 22 14 22 39 + let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 15 14 15 39 let%span sops4 = "../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 let%span sops5 = "../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 let%span sops6 = "../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 @@ -23673,7 +23673,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 25 4 25 22] (self : t_Map'0) : t_F'0 + function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 23 4 23 22] (self : t_Map'0) : t_F'0 axiom func'0_spec : forall self : t_Map'0 . [%#smap2] inv'0 self -> inv'4 (func'0 self) @@ -23767,7 +23767,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_Item'0 [inv'2 x] . inv'2 x = invariant'1 x - function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 18 4 18 22] (self : t_Map'0) : t_I'0 + function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 16 4 16 22] (self : t_Map'0) : t_I'0 axiom iter'0_spec : forall self : t_Map'0 . [%#smap3] inv'0 self -> inv'3 (iter'0 self) @@ -23800,7 +23800,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 62 4 62 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) + predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 60 4 60 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) = [%#smap1] unnest'0 (func'0 self) (func'0 succ) @@ -23825,11 +23825,11 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc /\ (forall result : () . produces'0 self (Seq.empty : Seq.seq t_B'0) self -> produces'0 self (Seq.empty : Seq.seq t_B'0) self) end -module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 93 4 93 90] (* as std::iter::Iterator> *) - let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 93 4 93 90 - let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 64 12 75 75 - let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 24 14 24 39 - let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 17 14 17 39 +module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produces_trans__refines [#"../../../creusot-contracts/src/std/iter/map.rs" 91 4 91 90] (* as std::iter::Iterator> *) + let%span smap0 = "../../../creusot-contracts/src/std/iter/map.rs" 91 4 91 90 + let%span smap1 = "../../../creusot-contracts/src/std/iter/map.rs" 62 12 73 75 + let%span smap2 = "../../../creusot-contracts/src/std/iter/map.rs" 22 14 22 39 + let%span smap3 = "../../../creusot-contracts/src/std/iter/map.rs" 15 14 15 39 let%span sops4 = "../../../creusot-contracts/src/std/ops.rs" 109 15 109 59 let%span sops5 = "../../../creusot-contracts/src/std/ops.rs" 110 14 110 36 let%span sops6 = "../../../creusot-contracts/src/std/ops.rs" 115 14 115 31 @@ -23871,7 +23871,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc | {t_Map__iter'0 = iter ; t_Map__f'0 = f} -> inv'4 iter /\ inv'3 f end - function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 25 4 25 22] (self : t_Map'0) : t_F'0 + function func'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 23 4 23 22] (self : t_Map'0) : t_F'0 axiom func'0_spec : forall self : t_Map'0 . [%#smap2] inv'0 self -> inv'3 (func'0 self) @@ -23965,7 +23965,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_Item'0 [inv'2 x] . inv'2 x = invariant'1 x - function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 18 4 18 22] (self : t_Map'0) : t_I'0 + function iter'0 [#"../../../creusot-contracts/src/std/iter/map.rs" 16 4 16 22] (self : t_Map'0) : t_I'0 axiom iter'0_spec : forall self : t_Map'0 . [%#smap3] inv'0 self -> inv'4 (iter'0 self) @@ -23998,7 +23998,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc use seq.Seq - predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 62 4 62 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) + predicate produces'0 [@inline:trivial] [#"../../../creusot-contracts/src/std/iter/map.rs" 60 4 60 67] (self : t_Map'0) (visited : Seq.seq t_B'0) (succ : t_Map'0) = [%#smap1] unnest'0 (func'0 self) (func'0 succ) @@ -26127,7 +26127,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_t let%span sslice2 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel4 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops5 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex5 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -26178,10 +26178,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops5] Seq.get (view'2 self) ix + [%#sindex5] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -26212,7 +26212,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_r let%span sslice2 = "../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice3 = "../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span smodel4 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 - let%span sops5 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex5 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -26269,10 +26269,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi8256668011736225471__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops5] Seq.get (view'2 self) ix + [%#sindex5] Seq.get (view'2 self) ix function to_ref_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 98 4 98 35] (self : slice t_T'0) : Seq.seq t_T'0 @@ -26301,7 +26301,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_r let%span sslice5 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span smodel7 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops8 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex8 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 use prelude.prelude.Opaque @@ -26362,10 +26362,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_r use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops8] Seq.get (view'1 self) ix + [%#sindex8] Seq.get (view'1 self) ix function to_mut_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 90 4 90 43] (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -26397,7 +26397,7 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_t let%span sslice5 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice6 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span smodel7 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops8 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex8 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 use prelude.prelude.Opaque @@ -26452,10 +26452,10 @@ module M_creusot_contracts__stdqy35z1__slice__qyi7128337469104663169__produces_t use seq.Seq - function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops.rs" 43 4 43 47] (self : slice t_T'0) (ix : int) : t_T'0 + function index_logic'0 [@inline:trivial] [#"../../../creusot-contracts/src/logic/ops/index.rs" 44 4 44 47] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops8] Seq.get (view'1 self) ix + [%#sindex8] Seq.get (view'1 self) ix function to_mut_seq'0 [#"../../../creusot-contracts/src/std/slice.rs" 90 4 90 43] (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -27284,8 +27284,8 @@ module M_creusot_contracts__ghost__qyi17645547594388049322__clone__refines [#".. goal refines : [%#sghost0] forall self : t_GhostBox'0 . inv'0 self -> inv'0 self /\ (forall result : t_GhostBox'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) end -module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [#"../../../creusot-contracts/src/logic/int.rs" 36 4 36 27] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 36 4 36 27 +module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [#"../../../creusot-contracts/src/logic/int.rs" 37 4 37 27] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 37 4 37 27 use prelude.prelude.Borrow @@ -27415,8 +27415,30 @@ module M_creusot_contracts__ghost__qyi17214052996668775070__deref_mut__refines [ = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1) /\ inv'1 result -> inv'1 result) end -module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 173 4 173 32] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 173 4 173 32 +module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#"../../../creusot-contracts/src/logic/int.rs" 245 4 245 38] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 245 4 245 38 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 79 8 79 28 + let%span smodel2 = "../../../creusot-contracts/src/model.rs" 126 8 126 12 + + use prelude.prelude.Borrow + + use prelude.prelude.Int + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : int) + + axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true + + function deep_model'1 [#"../../../creusot-contracts/src/model.rs" 125 4 125 44] (self : int) : int = + [%#smodel2] self + + function deep_model'0 [#"../../../creusot-contracts/src/model.rs" 78 4 78 44] (self : int) : int = + [%#smodel1] deep_model'1 self + + goal refines : [%#sint0] forall self : int . forall other : int . inv'0 other /\ inv'0 self + -> (forall result : bool . result = (self = other) -> result = (deep_model'0 self = deep_model'0 other)) +end +module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 256 4 256 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 256 4 256 36 use prelude.prelude.Int @@ -27425,10 +27447,10 @@ module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#" axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self - -> (forall result : int . inv'0 result) + -> (forall result : int . result = self + rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 184 4 184 32] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 184 4 184 32 +module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 267 4 267 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 267 4 267 36 use prelude.prelude.Int @@ -27437,10 +27459,10 @@ module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [# axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self - -> (forall result : int . inv'0 result) + -> (forall result : int . result = self - rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 195 4 195 32] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 195 4 195 32 +module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 278 4 278 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 278 4 278 36 use prelude.prelude.Int @@ -27449,10 +27471,10 @@ module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#".. axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self - -> (forall result : int . inv'0 result) + -> (forall result : int . result = self * rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 206 4 206 32] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 206 4 206 32 +module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 289 4 289 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 289 4 289 36 use prelude.prelude.Int @@ -27461,10 +27483,10 @@ module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#" axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self - -> (forall result : int . inv'0 result) + -> (forall result : int . result = div self rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 217 4 217 32] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 217 4 217 32 +module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 300 4 300 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 300 4 300 36 use prelude.prelude.Int @@ -27473,10 +27495,10 @@ module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [# axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self - -> (forall result : int . inv'0 result) + -> (forall result : int . result = mod self rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi6972377124305281595__neg__refines [#"../../../creusot-contracts/src/logic/int.rs" 228 4 228 24] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 228 4 228 24 +module M_creusot_contracts__logic__int__qyi6972377124305281595__neg__refines [#"../../../creusot-contracts/src/logic/int.rs" 311 4 311 24] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 311 4 311 24 use prelude.prelude.Int @@ -27484,5 +27506,5 @@ module M_creusot_contracts__logic__int__qyi6972377124305281595__neg__refines [#" axiom inv_axiom'0 [@rewrite] : forall x : int [inv'0 x] . inv'0 x = true - goal refines : [%#sint0] forall self : int . inv'0 self -> (forall result : int . inv'0 result) + goal refines : [%#sint0] forall self : int . inv'0 self -> (forall result : int . result = - self -> inv'0 result) end diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml index 0057aeb48..dbee8e622 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml +++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml @@ -2843,34 +2843,39 @@ + + + + + - + - + - + - + - + - + diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz index c619aeceb2c9af5fcb78f7251c03d5bbe688388b..e11c5b3f114491a58bd8f0820928675e83db43e7 100644 GIT binary patch delta 14942 zcmV-kI-$jt#sRX&0gxII0%#ZB7OBQ)bMwp*P~8LU43R4>CE<6U{uF*KpMLk(^6}Ht zhxh--@67N1!~cE?uR{9EuW#Rd_~Vg%8xVgepFaJd-mG%)OyTFZ|LKvaGJnVCAy-Yg z|MlbN@^Jc>bv-%*_s$NLN~<(vjg{7Q^cl>m&b!{wkhR;8J%ihJ@LgHuUe;4*@Mly9 z^;)jfd-G-09v&V}gfb zCp&1ktTW@_PNISpQSHyz9)Bg?n&qo?WH@`%dRggcPOtD5ta$4-3I6fk8M;;LV3KyL z?T%{z27Z<(7yVdfUbgn{bLQo^;f#1WE=hfOeL37S;yP85_CXw%eb~Xse-9ttTp($a z^fxJW+JYR$zAN5$viHWcyQ*ySwmtsafYtqGS5&*--@OLcc?Uf`7=P$R_I`hNn%z?4 zK4&ae<{@dn^=+vG%Abo#!bZ4^n!tiNej1d4H+Pjf5+JLB_ca=xKfHZ<|9n>MyQd40JCi?D2*=zV zb?Dw|7xLp$>@4a@-cDopRN0E^sZzt?PlF7;Rp5p?`qLnJuYUpA5xOrcezOOcqV|6N zK2-3p&>Vgt&B2Q1c4=pizGr%Sd6gR^u&C4N>}AD|h`Ckyr{k4=UF6n2;h&Dz_(hTX z7Wiuw?&!yjrTzX5%bn{Te8GCRHU``+x7C-(ZTtec4Tn6mN7;Y8TlikBbBkCPm9C22 zE9DOuZh`B6I)4(o+cLNJnE!Mnd{<@elE2q$+|!k-TydT1a7A^u7u7%BD;sasx;^%^_PsH2_#D(hj(?)Rvictz#J8!9JWS2^*T%89!wC+@18xUX{JRh1LJQ02rg zP&x5SL>GR|^6!o)Vv~7EOL(R&4dIzK#s+nUGi~e-dw(_eOI?_Eq*tuY3>SSJQa6nc z9Cv2er1}F8SIS;?1kTrNDC^8ioE+F~mN^$A_v3sVG-L!;!^#fGH)-fT+=xaZ%()BC?ldk^j7 zB-WjG<$wJjpZ^s8`c(c+(BIa)zrOwF*Z*yhS|7`&5AXh3#02*CWG@ot$-Mn?=r4OMhhU`a=R`TRUhJDoYi4a*0{-n&mQ*1{UJ%-%#fcPoLyC(M8;+ngyXlFs^qbw( zhejg0p+sLL<*C$2*7IZ^@F(o^=atEZ>wl9C`|~0)?2dW45OveMjOp8X*%5<_77xVW zqQquiaIt`J69c@Ns~>-CmiOJ{dA8bzZ6AKc&{|k}l`>iHzpDBqA#N^$2Rz=^1ECeX zMF@1A5NKI{g?HZIo%cybpUpiaBgOVeW=!9bj6NG78ME6lJ&}yrNZBSiFXZclX)?(h zKYB`#AuWMVXbB;tL5&JOp6y;ITDerhtMDIXPM^Ylf$;mYKihc)IQ#IEq&)nglYs^- z5Bc-?tVZsHM%f^g{q+8?le`B10>6~Ay$8Yp0b{d(39kWvSHbkZUYYAE(0mxhdWR?oS0O(&Q8v7QVS|U)e zEuf$F?5YE8bnE9+|NUv=cqDh^wT|@&G~-+uk@{HOBi>C^v|-o1H$83EnTLDJqHseGGhKNH=W_cvRn zl3w+Jw@tt--(-7sAmAhfXVF=IrL*FvS{8UX)3BSE_kP=+_6^0@7~`2~Zj9-;F(%oY z(XugyodGX^^O+Z-im!+&7E#43QN@cjmd%;%0+PJ~$qFR9?&j;wn$7Oa3mo$m9JAn< z{kms=!!{N6a6AUvSs9{r5P%}+33hiiSyH3&a6St8G2D>Wj2(&H=9L!BxK!-j(oR& zOUSD4tFPfaUPWvihiiqU_H-ne!ovr?TG%%`{jvIG#gS*SOJnDV*qCI^8C#m6!g?*5 zLBayDZeF-2&~pYZ%B&D8d2d#0ep}+O7dc z95;=x7lTvRvG8^E7oL1NW49-V|N8mYcLmP}u}mHK6v?^gVW0diOBedhxG3m0>TaSw z{rnt$e)}&U-V4aqyPx0wmk)oDF>7|OakKgT>)wtZambr zs4_NjT>R&~Zoa-4Vu$qe#U!-OF373Q+;rLd-pU2n={>Gng|PiReeHAIDpu__*YSqy z#vq`t4g}Oa5Kzxaw*mq6ULfFM$lN7?s||reCvaG%ZM<0*1U`jq)G4dVfK!nbD2U!nook3g%G0e`i z^x-eRzAMiXa5t1$#NN&z#Yy$%TLBuD!41uun=~JGqFUE6`OB%$zfJTsiD*5E=#FF4 zP;458jqu7qzCGyOwhy;|<`tOb{Kj|c2Wp+ja4mUZC($=qKjDD-S5NaBmT70M8abOY z@P?d+qX%G`=XXWvdx?4|Jk$On7^;8ijRROUAMqSZqBbmpJ-8NobnSwSM`!!{^6$?g zXFolcUq3Z!p2JNh;6t&A0LP+lmh?6i-BR4x!U$Oa>?vQ*Z~r-e{MsWa50s`KnoYLF zI>Hc4H|u??Fe`HuDA~RG=BU6!7wuCQ>7a`jA>%(ZW7^`F)T)a&g1-(F*CB>%HLrYz ziFa%d)Uqv5YZjNbF<^_y(k&)y)<9hk^K?DV(``hd>Y`9}QP?M?#Z2|!UWAKK1_?%> z(fz*;kK(<=m8_$G9;vlT+o(rqdqhkxVmI94T9Nfp!A1HUDA8j~(Oqm8_-=BbU2+%+ zrm?+K=*CnEY4g(sGk<6p6aLB z2GOE^miepfCMgH+)Ti+KGrBY%sv1+9xz5ck3>J+sxbNwI0>%tKbw5}d&VH}JriD%D z(h-;D4#$+#zTtG+&mmqe3?IubwG1(L4hP!GVvBtR$fc1hUY1^4GG{ZXU(61yrUz!@ zTc4k0iFJWBc0t@+>SBs615N4_?g2xj$##-po~01yS&Eml1ZiR6dv$5-o4Xz2ebY2V zvK3di?a*C{Hk@IC@nuaDY4 z6K$AbF)q6BG>jqH` zGtE6-fM*=dISVr4Yh<*Ab%TD!;ui>B2L^2jM-cJ?ia8U0EvXDGo=LB1Wazuz1Sw#n zibH3ADeY3l4%Xs1HmJrarh!D_yH6cigXMznONZ;2g;(aD# znftbZ5ib=aLu|u$79p$9h-2Y#ZHseLY;1OaIDZF$5qAZKB;P42)`n`;>}0B$$u^F# zz4PhNj+QSAjxO@iT%_AaPl2sZXEeTa`_|gXXU>!T4%B(F-$8R*b{n5-ra9Lvb8c-Y z^vzD_o0)KR=ot>qyux^*l+JJ%PB0Z&9ex&f(DK0ZAF?@9hdN@{faBS6o z_48E&BFm@p@vmVD0~pL-zpYZ=PIjbj7<(m0e@2hYY~!`f$ctt)>%Ea$qh+t1Z<;+v zx_geg-x*h44SmK5<#Gk*L;u=b8PcuX)Xm(aR)#lfemPoStFTD#CO7I<#I{fGG}O+) z`F;-0w{vi_&y2dEn7W~u);)%Pi3#+7TTFmAMrqxBZ@T;5^u{RNoj%aLK4Q53X6Ngu z+f-?hcJqAQWK&*EBsJb?=ZNiaj(AIXJdnj6<#jvlE1|9}<@ru|Zin*hhVpEuynetM z?UrKXN`~pq)h*F1vKDmHzxt6rTA$e?XxpD+Pz=n;tZ~GE+k+eR4g*9g{ zjtgES4(8ma_wVJFh@Lk=$%EeWNVZMSOQT>6HvJYor# z$1i8M#J+9q>BzJtpmuh=r#q=N4UulU)sGBzmtc>(eYvmSo5g$SXEo@5JJ>2bttmS^ z-A~wZ6m=y=o+g%(qmS1)>g$?)5j%yaH%mfl%yb`qmWK=_PJhwoP1e2Z)~4DJ>6x&UsKV1K>99Hnu^~?3E#ZQU19LFGCaPh zU&C7q7afz-m-TEo%(mx$WYHU=sJ_?9^3D2nKi4l?e{=nan~OuzOQ@PEa-1M=XDq9iB(e#7ijHqgV}I{xtANhvNvDE z1Gf*~{x84-_Lv7Q56G^0zyEo z0O;XusRcm}k4@c2kY+edzjS`->2&RaFYI-X-`BT)H$#k#-MkxM<2BS@#sUMoeoxvT zdUhta^)y~wG&$b4Fp#*{))1Oc&Ym+3x~L+ zC9>g#QB~if{TEPw_N9gMRuq;P>%Wk)zsl5k4`stnVAjq>2;)_EJrwI}DI0H6Hr}A@ zYY|?{ayysbOq313T%Ytybbejf#&;6`VnqJFg8%Sb)zYbWX^Wg>Z+l5YS^GU>yrVEfzwzSO|UI9Axs%_3WGH*-vPH^F0p0-4O@CJr2P1H~_PW z15iB+@BzSU}$#&Fu(qJb=;L{hPF6_*q$R|TJ(%36V_O%H#i@@z6ba?o<##^Hv3?^ zzn%L*Fs6q!ZSEd1-yjIod5IwCQ5!vIV?7x{5-jJz*N!v;gYjV)$G~&!Fid4$Z^-c^Pmb&j9ZS zoY?V5+z@c$*8wLmEa)v><5I*;hwQpEZKBC{$>ayYB!_t4t`{<4`{|uN8$P}Nkglv( zqd0nhz1RB}L%F)1&&%n0qqzdo8yp1St7YA-W-$oHg<#ogJ_2na`^IfY8`vx_`$E|6 zL{L4B#*gmX<$6pLFM(XU_Ar00R}r3Rh-*0&ZZaHTsOgXDTn3e#ETVz?U=EDd7DD_W5~K6L)J?n2~FAPLK4nr-4DR) zegIy>>0iWS+eN9iXRRNWzh57Tc}-{2pR${RooH^)sKqJt>6yHefB4IvHw>rwto@+f z-JtYk!`k(R-|I9!*X}lSKTOf2V~#g!u5|K$ zZ_>;-FZQJs%Afmsl_e%b(9#pZ(^teR{Du3 zRBHPS(1Cse^UYJ=@~#r@QMSBHyLDH836F}^TD2LX^M_*vzio+Ty1u4`S;^fxU9kN4 zV{0mpTG(~PU;(5@6E5oariRBJ_P6Y}V5~HSVNgRy<!V$>>x$ji@9}lpFX%bt`W}CKsfliTeAl*r`0n7e z1D*TzPj0Ov>^<@JbK9R!JA8e|4xhTt&Ru2aOO3rBuE2h};waJ|yBdu-0ZKCxlg+zn!0}w&Uppr z|8f)BK}Yu70c*~=9M@q(JG#|K5xcm%m&&f7@QT-dRdN+PxS*eVLfwXcJ}hh97i9N+ z+dr6_r%lR);urRJZQWlseV>_sr^hR2!?vy6KHqRceEW zo`JZRyd}hDHe2pNKHx%scRv??eeb@U=MITz!*lNcH$3OB@tj}3gR#SN{u}Y!B*(9_ z+S-V{%VF0A>bS!qdq;5LKN#vC4D}C&x|^YP*SO=o+v~mE-_1~#;Q^5)t&8LRep+|K zdm+nc7CSw+yvKl7FOB?0eR&DrjZGfW&xYOnMJSm4dM+EJ#ow2IxrTn9S#1NwYC4~F>%!~BC`W`?;*JhyDW7aP82 zIGM`b7rJra2%Jr;Qn>g2z*}=4ynE*L9-H%BGrNoxxiZInh_^UszsxYIDf(x=PJ57s zcTLmogHHdLroY>NG+jghzUWz+H_zoS>t|`Gd9LYn7(~6tV zil^c@JgD@a2iNsb)HIiyX)ZT&6fU@z+G8VE;e@M_KmI6hbcpx*%~8e-rF}rZGalA= z#*Z)NtdiPIW^cX)kma@Whc9Mbys9GJ#Jv}@xV@Og&8-T5hc9MvdohdW7qey(XfI|_ zdya+Li&=E;Zu|aX)?BZ>m__ZyEE*madUf^}WCQANzU^RqRCu`Q>?sWQJ4hHRxFDwpP|0Qb!+TkOSX`Ab z0!lE}9U}~2Jj8cLZ^L*s%Qwfu3*owbu&zOM4d~^YU_HjQzl$W)^?!%=e=JvD=~zWe zPY&`oyQ%Y?X$N7^2hrAZ@(iJU==Nb(l4OXpSfxyVA=_V7eUeK*y$ZRMU*G=aLoV-R z?RgF#pWnXw@JB(&I;*_TE#r;&LZ3dp9gxvW%cG>@Wl=wd-yhTs9}n9L9}^_?+XdwC zaey3NC3Q7>KmE&^T0?(?Uozn1xk%^sOuLpmQJo%fK=6Vk)0 z@KHK{@b;L_a)(x3g$3-hbLz?e75auy{jsB8Bp63D46|ZpoQ`@#LG`)cF~m{tnJ2 zl5PkV5}tmupFBh8$4*|)V_sGfQL#$l5$sogRbQfKJcRaN{`_?Hb*~#`FIZ_faS)zA zynTBA9RB+DpI`qsSyKLK%1CN+vWA=L%T1BtO<;NJQ#+f{6r*tQEkyzZck3^oE{V1TOSbprAJNw0sJ5KYgCDe&w*d z7TQv)wv8^b7VYkT)6A;o80fq^?QgyjoF%1fUJCqwW=^?62tBCP zw5W5_qR!1)KDDE-{p9Px!B^A5V$Bp5JH5^qhPAB^Ty5y$XbNC~vsL-_hUPTle$V+L zZ4>zmO{;)@*EyKgQ+RP;)ZWLHEX468;$cfPMR(6xsCE+DP2uyqcXQBrk5G4i>o(eB zt;6}gsqjX{Z?}gJmx=GE&x>zo@6B<*{^~cJ`>|G7&nNc7#rf0ajn7soFgruHZKy}c+H*OI(3Ux?Cn`>`~UW21d3GXF^P zNESnZ)mRpTS!LknX}sz70o3c^fTWD$f#ICPPm-{`P8Rk4fWpv$KD^x#g`qEfdx` z?R$gcxmX{Zo}V25<@zOmE4$-%vn)6ox1B}G>xJlAIl^TUeVE=F+P*D13ogGJt6LVh zoZtS`EcP$qk6(6&BJXbAn8GMeH(gBOaNqsPr>~}~@Y}n$N4L-KUX`<&Fq$3J(0#bj z%`WPf({tMetF{Ziyk7$Mu9sM;DeGg?M)Z&Q*Xy4T-me}9ti4{ZYs&Dl znVEmR{<$vhPuatNuWehcSK|@ZUltu~YslP#VSjo6X5O0exL@5M)poBQE&O|HvI8~P zKVO~A!VU58dV$Bf-@g%MZ`Mz~&n*n_rdeE0%4HYz68`3D7T6q|REGzb<*ef$8Y5$4 zWIV$x4ycg{U69FQ(p8^yIQQp&Zch619g{wh_!^y?sc4#i!y@sX`Imj@A3Dn&k^z1N z865V44#zcCTn?(S^;Z)O-$OLQ7Wat>-V+n6v+wKqcS0Hqx82Xe%xWN_YuGXa$1gF} zrTpPMo0TaaF7I)W5{=7!TL;aXHM#O?ZRrL>El6MB(%v!U^3c|rT^7(<8_;KcbkOr% z6KjN;7J%P>%piITO&p&ld%--zt4M?ACMU4T3A~tfvmE-arD4nUdd>9*2x?0wz*SVj zv=l7kTy&S$`*I&H`F=|fuwZ!ZUvSCrdPNi67%>G@ti-^rfzs`P@_KIPfnMC<(4nvN zkcG*Oc6eY%>(INJh*=V;T_R_}zHffMY@kcIJ=%pC?MkLMM(XZaL9td}swubB(VwSs zLb3n(&yx}+>=4WBv7Gyz4!zL+0r%QJ@b8ljC(Hq1v)d;|0RjG#A}LD&_LFWYc?wT| z`ta%b|NQXpv+*fM0Rj7yIV(;ApN5l(D@XyalhP|O11^7ClLjm!9G}WZ$sS<7UJRv8 zPAfv=E^@T}uCNI-mKpN?u#-hBG6CU}cq}*p?US)A90ALd&MX!I^ONN)FaZ>k7A->= zYj`&bF>%#}U!OltBCQ7$4UVegVzYzw50i2&F;d~8J=;T(_AFRKR40x1y@^?3dC|-I zqM$RZf8uXTL3oB`!h9iGKS14%L=Tr%Nx2^fW#Ep2zrVNOf4H|`e){XZMgQ_4-z+*^ zmiPO9qn_wXv&Ai41_IY^vm`XM0|K>-v)VVc1p*H&laW0#0_Yr*#Xa-_F{QJ+KBf$R z{Ez0&G+AyN*~0&86|CfZw` zv9Ol-<~`12jR}8BW8%g{ji0%wjY~FvF44IB+VL~%sf+e5dv!sX#^!|ZXKHA@;xtzK zu;Y&!lhHysH}X@-d)dlP#%jI3HNJRXe$erq-H=TVGxS%Tjam!GUNvf-cikB8>JK_T zZSu+ko%tSxAy?Y9MlI0Ua)1B+@p0$B2>oRB;3JqOt5k)c@x-os%$u5KYRrg#qc*1e zuvm6=ovO3Obgfjm#7axoFdgp%BQyVzSO}fn_@{Jq*ADN)Nt?QvIq$r1G-m(U zm`dS!pq0$cYH02*Hp_-8Y8HEct7hpP*T=?!k9YU%!_lf+%h65(UHi#&uk;rS-(aNt zk$}*xk$aL9b=E0ap@!nZxoOrIf3f5{Ao(K!og<8@Fx&96WfGS3HkS}OSX15sMPubZ z7SuvbOw#tyxn(^`^B4?ugPc|4FBWTzgZ`m_G|P}K&@K3=#l0G&1@_c`g3F4(XG!WG z3o6Gx0rCtqitC(JMszdKG;$(|`FBwM$AW?ms0Q?xr@QYotmTi+ zROwqNm1G7T)L0MHCIJni^rBZ7s__b3YrKq~T5xtqTWC{JSxNL3zi7S&WkGpn5i|s` zI@!r8S^Mh3aUXG7Uj-z8h(5>EJ@@EmnV_(~myvp$s~xfOI)`ZDL$2xpw*;J+vX*$K zEw$b{sS$d+CQ4#lprlU{R1KDwRYn=>tsOLeB>)pift76Lm}`!)d*4tmdX4y+@^Ecz z@+!INwBuoNd?pEg!vns=5>(yqxcah@+-(;zh`*oCk7d+R_Bw!nw0ud;vw35)SFa|W z$j)N!ReMQ7zw96+6V8`-6`}{w+xo55*+wl!m(4L2k#K%LE){|53F4Z5EX1|2&KUdXV9NsvrapL8(|rt4WGRlqYYp%&iVu)~69cu-0`l3rxDQ!LZBnvHi6+IL z^ORyuiZ&_okCciO{2etZMzm{|ADLP%LSnfEz zlsRaa@vzGPBX2_1gtQ6CuZ>UmmtMrlgq9O?9TQLlC%_6vozCNO;P7nu-T0H3yZdG) zo)hwag>$T;jT;rSx849v#J@ZKK{G$)WRlLd=B`gy0pt}PKTr9HfTdWQ;L{58z|n-g z30srrvyYmvG-3Q5J?j<0Z%DNXWfQvVm*0)Knv>!JT>U|iC8f= zDp@+`sw;sQ$_2fA5k0qaK*T;(%xKK&d(mKjG|iytm5bM1Aw@drR|FySxnf>t&atg# z9~N#LqnDvG9lg^x9V)_~D&}5gjg2M(*^{6W5uZ!>X&O9sWj&&wDrPKSwhoOI+|g-K z9_TUFFQSWG`xa%9}ZsEL8USes}z(P*OHM6HQ` zY7>^H~9%A3kgS>6N9M=80o zu0cbqnf$Ng6ZfpP3g8o1B6p}R(K`&i(75R(+xoV=!eD*Yt%{s4aS!#UB*mvRCrO$1Ka{5B&{XT^3Jk&y0+gCq-=e&my z)>EaM0VNawBZ{tdo_g~eoc#Se^pnJ{RI2&$%>jzrMCt+fwTYIfch~F>@6t~aJEiSo z%*E;)rHrhj))8n+W~F>zGxjNCN3)kL_Bxiw_PN}~5Y`StN4XL=sro5nU&kuGh-W{$ z9L176)?Q$fjLh53{8?j9yz=sYpe3>=c{z>_Y0LifkKS)&iO>0r9E-vam}9`MPWD8j z6RFhzfc4(1k)Ja5O1_>Yh*blW{$d&=>Zgod2Q)W4(TlzoqoH>d9k6&< zOt*nYvV6+eS&ke&`wTf9z6qHOz)B}muQx9$DNV4x&d>Rdl864S{lRK~QUxn%>yV5= z0zZm-4%Q?;=`&{pV@-UZf3Llm=~$v5k9w*7{ToD+{G98XUZm`(S$4Hpk{un4S-~I4 z^@WO``Dx?Vx=I;)N1xf}G@8S56dk}B`rC>E`P84t89vK7^hf%TW?IPV)9}K+d*CaD zi@eu5{Hf1D2b~cBCp@ixpsqf>q6^+qjBoQV&Owmh{>10uY5k1YU2KC})B(?rYF@_T zH;Vk82Yvc;0Wi<9t1b?Y)WaK8$E@H6m;F8$`PAo-YHLxqM=$`69dU=z)`T~fzT5w* zeEQ#FfN39n?U`kb3`oxx*s_l1p)0$(=kfWkt2%T5*Hw{w;OU)z1pYsiB##W>i|icr zD*ita%1mB%kDO&p!i;j_xYtZoiY27wZWz9R%c1gSZ4??mc0G1O4^j9DZvYY zn&Q6|09mtXiKfUe{^VS=Skr<(rD@@&1x53UM ziZvB@=}1%Irb11Br8MQ*l(Q*EQ}(88O<9{VEE~8f0~?FjYg5Xm6ivySlD*J@T25C` zyU9j&uRg*_TeLjj7*?BF{?BpHI09mT(vBz< zsBz!AcpH$3mxQSqA09^)2GqWUSK~3oTm=!W`B^8=O! zF=%kEju-8Ojx2z`uJGr3;)wF$aR{$o(jjk($KWG&JqhLkeB-p<`QQ(aBRTOP-y*}F z9yg%jj3#_lgKa=kL8`d;F{vHl|vNH;Qle!hDJqkSuiHLP>>zhV2jgNodki(tMHNeR( z5BfWYFB^b>+I;^``A1>_trBhiJgMX!*~Qqv5Lw1sFO^;s@!Xb?4}aE1Jqr}^ZryAQ zz_biXzwkqG@s5gX_YcK$3~wG|5cQT0Vq*$_d_Ro7DNg?Bc&Y=V>ud5_JqH_Bkw*(i z$J_cl9{ywT_!`?+_NZ$o>?)5>P&;E8Rn0#hPxM*o7lMrJr0jwLcA=XJ%>YE7#)tHvJ5I`%8!Ir@Vi*kI?gM7c=wgU0%tZ*$z5XX-*tpk47p^M(p>ObrU zPwKLv2gmc?b$J~pc%FcFynSsg|9(GYzPxVT2_y8SwFl6^T~uZ1t?&FN4fXe9(e?pI ziL4G^DqCDBfYt~Z<=y6N<=4itoPbgyns3xUBrI32wKI3P;a%pF760j2R;*dkW<{D6 z{D0Uk;@p$#SRa3ke*{>f++&@~rm^j#gi!yjR=)9_ByzO|ObGX}Y zaFF1p2#!8-wW^uJ9;thl`%E;3wKKo`Foqaj70%}?9vDcv6}ZCsS3Cu_lQ3Eqf3xj| z3-6pT;Q_i?rlAxUr_60WFHHRTjj*jNn5v7x$R1Iko*IGHcPTj4FS)-j8gv6Uy!X;i zg}KnEGD-o&8*7JU947ZV7ios;THs`jW7TGy%{ZE|zqpjTJ#qD91tT2}nY&tt15UYh z!sp!o%NX_mh$)21SyA9$u?4o&f3gp(J#QTT&oOY{y^$maL+4!za_9@R_##3*2plsS z$YR}G<}+9SC5{7@C@8K(6Go4x8ZNJnx1rP-zcR+Z{v8B(?hYoU8;lW;RM$;oWPfNH zp7)wiZl=`iIexvzLvC@@X@EyO=&%G+MY~6b3FLX3Fh2ADlYRG@^)XSUe{s&3NVEkm z!vjT+-yQ^0{pY?a&wNADKC7RTv!Xf=zeVR@fq1gczn>pJIW8D>ntMjrHdxdinj8_cO+xjioC|9MO^{F}`zn!WS4b({%1LfqSY>Wr00C0e+E zSNiw7{fjv1U>JulqdS-tOC$|$450q%^Zc~Pe>G-5uzU-)6Sq>wK4Mw?-eJPZd z)GQHSeI4%%G|efnp(I{tNQQa{)LXfD21{#}+AO76GIT}|s2AAH!b+p-8NQR}Ior>8 z+l*ts+AOnKMzi$Se*(30Oz#secoQ1b+NUX#NY3{)R;5|xW|dyLMt{U^SXdueM%3=z zvgQPI^le8S&8j!6)~xEw>&iJ+XYifpDjgUXQkvn;KCcsV!G5(_&1VjVyVfxZ+BDo% z*~4li7zC2N+uets^Kq>2u;!HwA67TCb>RwtR9egl_I~5-f1p~td4XY}Hpluf{RI>k z=ylU90Y8GPvpIT%bZgIRf?9B#Y+mBkE2|vpRUHju#SHX45A87CxOE7JXE|welI8^S za%xWHWpcE@@0=BgCh8B9MFnq3Ik$G?jQ#746VAC5&BM=Q{7=tQ(^rz3^v@G8OA*F_czkB zet)^axDTcItRtj&oZShI9cfiAI?5k2mAk!p;f^Z)e<@|V4?P*^1dfmpxo92duipnR zAiBFB_(D*wO6ZLq8M###3T$_K`?~$ir766IMYVXeCv`ijhP&swylWR~F4(U&XZ!|% z^}XxraNjEMVz4;TagUk#6dGUVUdp0QsV4{QXY)yPo(J=3Z7 z=zI3-&4{y9IUv@xp(f5E_pVitz^5qk1Fov-u1WLWS%BSqq@ zSerHhi^G7HjlbvrpW{Qq$*|G^PKaP@Tc`rlY|Lg~zh_>w<$&f6XSH>TRIM~(ASXej zOh3#&;L;VoR8=P+pe)B=5jUvg*8hI~d#z~1H_krh#!8gZv7VRB!WS3w?fk=Pqwp5O zf9xHn9MOTu?dUVKNk3fwp5%sx^dnox1R4(MMWNkiz28eN`kG;7^do3+b?So7^xmJA zaH{3Je<%BYAMf}E_gE_2E43S_Mr2&1gQ|XO`(HE{F15L2bHV@i*FcJ431E(c(7qoz zK>sjK?sC6l9XbHx=1R>KKEb-q7y#ZB&SiQfd=0FM_sQ3fnObWE^5W?51n5373i+X%tUo7?^7^EXEG zF%KYH8y&~%R5-5>D+=?5(%4ICxUSw)U|sd@eEotrx~cZ^Y=cav{n7JrYqRNm0+i~wT3GMX4+D+3e0Quyrw z@7dg=xqI{X_ptko6<$X`#aZ7TitA^Nl!pzmXT9Hu9@0FxdC-kHFy@UpS1G`Vboha< z6JBAq!UM&{^R9DxyyKFyBjBb zFMkU@qCMpclGI^}ozy(BZ*3mg95(OZ1e4SyGzoBum9k4cgZkX(YR)|6*)|4vfd@)0 z^;x{cI1Bcai_1uUu6M84zBbQnj%zc$d0KNAh;}3p2l|V1%~NI{61CTXv~FAvMz8SB zMh+M*akjHm~x`Njz5QdlnTQ8=mK@fI1GT z(xiK=DAWS$ZOaD*3tf}L!Nl=#iIfdX(Farqvx|W15bt~JDAJ-_bZa@&dhR3mUfDIC zx_Xt37ih=@$$z_jVs&8E(JPt9;2eYRdN|S%n3;F`i+|U(J8iBr@(5sTgRHI&!hhG& z_j)wS8%HfLwayW=^bxgjO{oKhl|+Vv~VojY(wO9gTZUR+t!Pw?Lj3W0e1Lf cjhWlBRz_)czH2=}7i0T>K0+G5BmPx# delta 14799 zcmV;=IWWeu#{reb0gxII251-F7OBQ)bMwp*P~8peG?6PUCFysc{uq8OpMLk3^6}Ht zhxh--@67N1)Bk=7uR{9suW#Rd_`{KX8xX%QpFaJd-mG%)OyTFZ|K*XWGJl8XAy-Yg z|N8NBc{u&^x*nZ@duNAArBxcT#!Blt`V3}O=Us1T$l7hlp22N9_^zySFYBo@_%o`5 zdM#J#z4@|g4-XHg^5y{vRJr&o9jR=jna1pjdF4Be`AFiE@B zcE>dU13ycYi+(IKFI)SMIrDPda7Mfwm!v+tz8vluah)nj`yh_XKI~xRzlRTRE|9cI z`m2;WZ9xuW-xcpW*?VK!T~)Su+aCXQ!0LXpE2`b^?_PuJyn~(|41e?@d%wRs&2Fi2 zpEDLK^N_UP`nJ>o<)h9&v2^&4_VL#x*6_A+gonxzUR93pnsS84$`M{FM|i0m;f`{ISCu3DLgfg*KsmxM zQ2_7-%F%jZI^vLZF@MA}!jYCM*;n*jO<)s%%B|RH@|11 zmGTD+x4`v39)F45ZJFD9%zr!*zN<2K$=~ZW?&-=^uDDKhxT3n-i|QZlm5sM*-JY#Q zwQCacdX1fC)X~m=mG!V?_j^=MyrOdA4V4qGtDJaE<-}c;6L(ck+*djAs>+F9sB+>L zsGRsEq6@!f`FBSYvB|uoB|OuXhVV=qV}m-wnKt%^y?>hfr7p}n(koVHhKs%qshh?J zjyp4KQvCslD`hV`0_STsly&7drg%bbgm`*A)Fn!L!~!^J_f>%9Gu?%K5$IlE&# z=<6o)Xr#McUF98&@d!oR?0qr3wvO!ed}BY^p;7YdVnfn?Z?>fb-1BeY>HS}%y@&R3 z66?;p@_+sh&wmVmc`E-d=x=M@U*7)H>;E=Lt&io?hj)J|Vgh`#{PFNQe0u))IX!>= z7~Z{Il^WsWQGsD>LxXsR@RZN+dfOA+>xsy^XG#88>f2A{w;u-S5T4%W@*jeMr}V=l zLVh|^1Gg?N4J9>+l-&}mZotslUq61xpHuntgMT`67@Rz3ezTkU(8kWoF)A6O+8Lv| zYm9Kl%@{$D{L|dmb@6G8csNGbj1g9244=xoIu2;~oGFJI<bX;zWwPA;m?B4M)(L-Sos*`ps_Y zLn9I0P@=Dr@>FUh>v^&d_!IW|^U7qy^?%8R{do}?cE`M2h`MQB#`NvH?1;fdiw9zG zQDQSMxL82Ai2>fs)sH_m%lmHfJX`Iz&*mPIkz#u!Gp27zMxTw4jM?p&o=C=Qq->L%7xHz&v@+z4 zA3Y_=ke0wFw1g1Sphkrs&vvg9tz0VMRrt>`r%z$OK=_BVKihc)IQ#IEq&)n-lYs^- z5B}5ntVZsHM%f^g{q+7Xle`B10za3ty$8Yp0YkHZ39kWvH^KD3U77$JK1aJE(V6%u z{22aosNo-E1?s(?dnuU`J|Uf76nL20`c}Xefb^Nn0+6`^$Sf6t0nooqH1;hzwM3v` zTR=bU*;NPH=+@7t{`=F!%ijv!tJbF;$&CKn)QN91=%;%)p%dVm8&;kC1nYiD2+pEk z`bxjF^lMRn;6XIir-8Rqol*`wvsoo-we>v6g?$d<5dlr}d;cnNN zmkoEjIEPb_2#=@dzy9uzfBp5t^B>Enr%(S=diUmkWdw9T2T6N-r1EX1{Y-Rg-rsDQ zN_y1?-ZlZVe3R|jfq;_`oJD8-mClNvYFXgnOv7$s-urEP+BXzqV~l5}xiO~W#+YPp zM$5(+b_Tov&SzeTD!wABSVR@CL=`XAST<+23rO|~BrA~Yx|^>zYc{(xFL2CPaLj^Z z_UoR14ck=M!|@ob*8&;T?xt!_@pu8H^Dd4!5N1doX?7BoHQ3grM>O%RB_L4#t2h zV;`~H?Eyp`|Hq<0$MO4Ub-ny()Y(Dnphw(~(Y1vo z++$wZjQB1KOGoH!Bg+>2cd)apka~xyB`oYLX~)PiZ)UE?1>Bkov3lacT+m4SxL(2M z?H7%7jh*1SO%D4k$d-|(mS(8@W}_o7CC*QCIkN^mXXr(lmDy18-fR}_k&tySI`Z9r zE+MPFufB%!cong69Ih3X+S8F>3J)LnYGL2(^vCL#6-S=QE{&ZdVq=muXKZPP3hT9K z1_=wqx_RNAK+hStD6>MW(?+Ts|VwpPdDUx%~!#??4mM-+0aZ%81)ZIjV z`uREh{Pv$eycdwIcR#=VuOI#_W4IFJ0q4Oe{`pgLfA0oey&A(IUbSdIZXYdw#sYfI zGMs$shEzwq7{_ZCCZ&FRi#et;gF#Jcnx;MtA!HQK0%4JZ$^{M-fG^2mxA^AKkCr_TPgd z7HN3lbC{xO?8;^EYPN9=`E!qdL+Hpq&55b!9+X_R>1HJe{F^0^nFPe~y8_fQ+<2&K zQDto6xcJX|-F$s9#184_i%DpmU650qx#_a^y_E~D(|cUE3Ss+s`r7BZRjk@=uHy~Y zjX^+P9SEpkp0G#1UBn!8*^QHI7I)o4{~8QpW8^!|fe4-R4zeEFI)k_jVwjz2 z>BFCYeOI0(;BF|hh`pUbij(Tiw*oXQgBzMRH)%fXM76GC@|RPgf1BuO6481R(H+O8 zq1ZGG8{w6Ke0$KlZ69ub%_}g=`HkCuub$>NEYr?hHF7p* z;0-wsM-RX>&+m%T_Y(C`c&7bDFjW828wapzKH@o+L~U3GdvGoG=-LGtkIwe@zkX`eJcpZ1z=vWJ0ggrAEa`13x}~_Wg%Pp<*i*iq-~Lm7__aq;9w<#eG@ERT zb%Y_9Zr1x&VOHiSP_ldV%~64eF50Iq(m@w5LdJh+#sf!D_KW>JyL6xwo#AJ_K28X#BR97wIb`If{XMyP@>0}qPy5G@ZID`?H1a24{iGqZ`-T|@_LlD>R-4H1ewC()}hutfbQGCS)93oP(LkBJ=IUM z4WdQ;Eb~{{O;QftsZZe_&gjy7sA^1Y<~ldGFjzFk;J&AS3m7x})cs&-IQzW^g zaEY~b(98d;sezBFfiJwdYii&lw+HSJ!Y;dv$|K<~x8VGpKK@Q0_rW<{dtP5IST~4j zm}&0u0zBhr&RLKVUn8R}tQ+(*7QaC7IxuKMID(KDP|TU|Ye{8j@l1M6BSYWyCP)Dr zRUA5hOKF!XcGza33Ob;QeK-fyB|C$IAcN(I&`l2Kaf7kIK+jnag1Slw8(6mpVJN;< zRkwtowuFH0MTCIvs|i6`JQHjPLHfQ{A%|_;NC#^!}%KsjJPW>B>7HJu{KnzW+zk4Otx`^ z?VV4DcC>t1aCDK6<|5rbdJ1fPI-~KW+qc$6K69Szcc9Lb{SKPjvfKDvGtIeXnR9DH zp>K9V-^_%oL(gz<<`u>hrF4eFaDu7G>hQC;gO&%LC*RO2e{}>}jNz+8(8IB+gJY|I zuAi?O5LrHzkADeM7{Flu`fZi^cCsUN!`Lf1`ZIcDW*e_cZANtqk%8+j5rf%jYwKBX>^UKltT7^Y=H@Q)_BDQ^cr=fNZ z&i8Y0zMX@ceP+}R#ncVOwC*wVOH81D-(mv1F-q(1d(++brZ-0E?(~7~^%2AMH#=WP z-KI*5w43MaCY$nVBB}9CJ4bAXbHrQ9DbIJxb32r0H>l_tovbzDiOTO|6Z5OY`0}+6+6e zuhZsm0P~V!ZxCm^G3qec$S;h4;amIPVCdc0C>F+Wx@`=<9Pqwbd9ZBUT6hW0zP^l#GkHA>wv(_hi@Ur4Im0oDz(w=B80XuDPW=F&HW5yIX^3>&t$t*%y99gO?aO`r-YnirKdV81-@#VlX-(PT z>3+hNqo^w}@-(rO9DTgbQD4{Wi`XeVy;%}cW2XD?vpi%dar%osZ?f)Pw>H%_io!B$ zTt(N3H}LwsyZe$AcU^OHnsYuo*Vf^6?&&TI{+f#B1JZYq(p3CDO8DkY?h1pamErM4 z{Tkj{xagRqzN}}%VYWSgCyU+~MfJT-mT%Ut`?-GE`kU)V9ADBiMos2!ecPjd^>>2*JHh|2MDX7$ z06-6KODza;cx>uEf;7Wv`la(rPp4}ad||J9{Jy^ZyBT6^?B?A78?T}MG8P!v^?TC( z(6ckSt*7zgqRH{Tg@Mf7Hz0F!lg!NxGT#wH6PcS|?qCPFOa70i@mG{J#7o^rSvbTk zEs+f`jH>z;?Z1G3vM(*1x1zAbSpS8T{Z*#Udng-r0<(55LKv^Q>!Da*OWAmnvhfCG zUyJZsmfN}fW}NPwl!oS>b>BzWjwYv1p99shW1)A}^-;9qF)P zsN7#5;Qj=E0YkeJfcf>$tK+UrGqlAa#P%E!)1qfQnXtx6y}|kL^*zAH@hloRv)KpR z{q5Wjf-ya;X><38`36Ct&PxPAkJ{)#8|%psl3+OxzJ3(zB4zbPM!)5E_U^CexSf|< zzQeF0*M0)KAHZ&GHiQh#cWr>`hZt2q#JIR_1IOooQT9TC#_Q`PyyP%EX};lp6>a2~ z;Ye=t+YT2I%n7K*Bein^j4urA^a%HE;7|PZ4d|po18_gAv-ryhrUoGoyHH$$oE(FU~^ATtZ**9)G+Q4Rc*%!ig zCxYs6G=6m7F4tq4cnRd%wTJn0y^8R>Z1cQs^LpXtVda+FmgFME^_wlUmk8t4Os#L+ zd$~y4tm533aW=ik=DG>COF1kzCtj=&Y{!g$&D#{ZA4Ast7_wdpNodMO7m{#3>wW-U z_XF@6PX8<(+b&AAJ!}22{Qde!%xgNE{*>Jm>_l^WMlDXEPtW9){KKFBv|%{SXYB{= z?gphV8`iEjEH44J=J9XP&ITJJ909w=%QtC!pRF%7{a&Z>xpudq`(cVE9do=hOD%56ucO4+eG_XP2fn%qp4N3Q zA6rv-)WWVS1`8lPns8CSH#I!=u)k%$1!JWt41*dvDt{Jw;vzDB81w>qyJ`YW4-(e> z{7ZlOt3AX4{X(E2I9_<8b!J5SS|9D2U03YBevhx)enHPE*Z26_OHFj!etQc_dw{V`peU&r{|Kd1?mmu4^TQPdNbbY z@;Zz;^)jiqJFa{S%~4mz^u4p?)}<+u(T+R?2>irB^7y;ODug;%`xtCFkW!3F)?6Y4g9^kG@+z975r z+y24aJZ(}Y6u+>)YwP~9>HEz5J3U@G8@6rj_W6br;`{ganltAbU0(R9FNSvHu>MLm z+Xiyn!R0TLGFN5H>*JAJc)Hi<+Ptl}$h+J3{RIO3y2J3kmH+k2R;AZ_>)MO>(yhF1 z@(jeiwEX*Ja**k&@|IScw-CpnQ{%(e{3=fDbXdQ;`Zfx?1em3mpFG9iW*K^q*E&jHD%r*4;%xW7bX4@lU z^E29Z;-KMCv2Vjc?j8jvVc$_%M{qho)!@Jh7zcb9=8RqW{Gc(Lh;<;t}z1Z+I z!^u?czR-;WN8oH)mBPLE2i}_d;N3H?_t>28n%QNn$dx(nL%hX7`(=hvP0>H|b=re8 zyla|vA9VWrH2uwgrs*OA@I}wkym>BvUO!7i&2vp>>=DBf9rfn@^M^OXn1HlBf4#~! z_67UPzg)b3SasM$`dGqq33A!leA~hJsPJ&p*;5$qcaShta6wKHppwhU|oai8qmu(!Fr5qe-}xp>;De#|4^>J(y@w` zo*d+Fc2nm&(+6HhW}t4e5M@blyWcPe>21 z!bj=HN5qBB|662?rW8+ ze(gPgw@QCl5&iHC-p-=Ec>ifBbbNI{Ke|r7jWJ&qQDI=-P$r^5|FE>SoH-Y7?Pwi|*Q;gbm^NUBr))8&PMWwF2 zAGgTxJ85n+I45mxD1}B6O)uR(3MvXuE3#g+7U`WBfEEfiQ&zE z#88`FP{mNl^ zEwrzY8!YTSaJ+#m>|ycGEV%$#zC5PDFn zX;J5Eu`^ndXgRiEA#hNKBc6yyJ3~O5-xZ2Rg(Goh<780fnIheR#Vg3PWG|_zud* zu?d9L;4dD32)!i03X`v=@%1Z6aCw*1Ttm`Z!qC`o^x`K;-oG3K$4l>j=FF*&7o}Ha z#@=l!EpDb;Ccs=}A2rguZ-NthfRiCcbmX7`8Ao>jp z+xG^?bFn@+JwG}A%k@itR(8kjW?67FZaa&V*9+0La)iqy`Y^pUw0&E27F>QcR<|s0 zIluj>S?piJAHVDlMc&=KF@;f{Zn~Jl;lBHoPhU+};kS2hk8Ypey((ulVKh6cq5E*5 zn_bi|r{}f{R&5u2dA|hiT`#dxQ`X0(jp!fquh%~xyk9*ITAl5G+}!ZW`=YUSlv%bf zix%ve9+uB~cQs*f3M_me`r&5le%ZQg(D$16+oOXWN_hX*x9>Wv+0U`{W^RhM_~gs9 z#URFRZ4Vpvu5XL=+SBw-nvXui@7s3c>OAWu=9;z%P1^)<4Q>wA^I0#>)bDu**OcL9 zGc*5s{c~O1pR$L4U)#1?uf`*+zbrb~){wae!~XOD%)B+_alg7js_kAqTKM#rsnzK3XpE$$N&yeB4BXW!TJ?}RiKZo8j_nbkl<*RW*M}W;yg-OT(7y^_uGs5Y(1VfUBs4 zX(?F7x#%vh_vJoZ^8J<|V8QU*zu=PL^@=9CF=7g+Sc!pK1Et#o<@Mao1HHJzp+jHk zAq$fm?eM^k)}ePb5wj#xyF|`{ec$|i*+7?ad$bD~+m%djjMUw;f?}<{R8wxLqd!mO zgkt~YPm>ZR>=4TAv7Gyz4!zL+0r%QJ@Nbh2C(HqUv)d;|0Rj4xA}LD&`jc)cc?vIo z{P5}d|NQVDv+*fM0Rh{SIV(;AABU5PD@XxvlhP|O11f)AlLjm!93RU^$sS<7UJRv8 zPAfv=E^@T}uCNI-mKpMXzmr8QG6DXRcq}*p{gbgQ90Bu_&MX!I)05>aFaa2o7A->= zOL#X5F>%#}U!OltBCQ7$4UVegVzYzw_mgrhF(Uq=J=;T(_AFRKR40x1y@^?3dC^PL z5IV*7)6fq+cdh{sv-K@q1_C!tvs5&+0|KavvkEx11p;phlfgYQ0^1vt^*!_gVU)A$ zKBf$RfGWkuJO!={G|ETUl*Yu3i5fqBQ5%9YlUH0mNZ5o>s!k?+3 z^@`J2?Zd7=YD`86<=n_mCGTY`I~l9>`qud3d-*}vcXmTIIm}RBbvE`|IQFVh^St+s z@vZ)#>(eH$JW!eMQ5bTiU2D_=oh|qG?;js`|BFyhRu2}zG+Cu81dS(l-DBR=G*e@L zMjW*<<%h+xtLs#qHKuE&$|Y7>x`yd^Cm5OekHkW#?8ZN(qq=r@A6EJq?qy?O+*ss~ z#1a$A2T7?ut6IfI6LV&L%2)0>m)RP#erOzKr5q_)wvn7NAuSjvnae{xZmyfTHs-wj z!qJ%hV`D0X=Ydu-H>;tzyVxuns;F6i?5&!mcU&JE3l{J0*@vT4x0a)w1iJQ<>0aqy zEPR8J@<#$fwMOnqQq)B|~YW$1E8snmWC?L%;qziNlK5B8V25EtRJ$u1r z#b3Q7^^XOWW1j$d1{%e6&MG6i8E6_gk;MEfDF0(YK?hU=`pZ+yP9=+z2Q{}vPe1lA zR%)!}kM>mQTPT%e1|96N9;i(M8bs+uuP{{O6&P#0jGw*W?2xw5rlPWv=q-NHd=1Ki z?U_Z;5X9q)qn~AhjrF~Z)Z<+3h?UnlL=y|Sst4Q> zaAL|@;+?kCdiP0TdF z1uJ};7W($w1r_C@BDqJ8Lo$+rPxsPkj5p!tn{?3Mu8Z7%Mvv|g=*Hjxj0X_7`bACl zZ5rs?b5ZSC!x@DX3sPwbhfvpeLsvBZV;c7-?G=u$5Rstd;mk9CtW0{g(4#=Y@bq)Y zFSlnsqKhsiD_aVyQAdSzcP!@aHU<07<73ap9*x}_yEVo$;nLXgchuN{`LlCeEe^`F z6DqW%K!u=MsdwBnQY63GK0(#hU5B8m!A)ZFz>ZemW6O9;_~^IWN0F;fg6waWV-tk4 zQFGyw0h-EfpMSf5eUx1p$^?-E8@fu$>b(+j15D#Sk7ci*Zk*IOaoyTDvT;P? z@Wx?{Ltp*OO=a$-eVH9ME5L$j-*tjGan&B)xLV_?jjJ@S+_+NXitE+JnT<1Uo9QnI zC6&^Z30wa|x{X0H93q>;Z{b&Mj1`q_i2f>b9-+ z1qu1dVtx`!B}?aAbtMo(xuBOXqUTl)h}fr!8HHJYeJ>h}q8Svua`Cz=q(~?IiXenO zSIq0oIkwg8!@`YY^fGj&qjvhHLq+&g#oVi`u~9@IdlFP4;&UlKMT5t#tVi@y#f<68 z)}gV2J1Q;810ATvOyUid6p>FA^BSppb}U%%?1`12UdP&i#q@I}N5)Nzni%+twTWgE zjV9`UP1KsGHc@G!+(fAf-t9m+NCFkS22DjhEvIj)vpib--e;a$XYhQ>ezSedys7Mz z>txY_eIDjDD z#O;T%FRs5G`?76VEAlDis)=ppv!{7%)_G;iQsYy`z6;MTeQq;sr!Q3A??cGWLoIZF zwSDz-_In6nK2^FIP(lGPqUc)Z*>8S>lfVClev;UgN;N;eIY4onNId|*Hc=AwuA2Sf zTlz_2r?h>HxmcZ}l#zARIs#?Mtd#FDW1lj16noiXuVZ;^pUZ6wVeKGvlq+$Qs-H6U zb*y4VJp0+@D5m7G_5zz^WZr7#&l-Dw;**yLC6PVJ%W+glTlS}Z^sbR5KIc1fEDAqh zjsd$m*%O6Mq*em}*88kRe#+P@^}4g0)!fT^W+8?mRt-@4i)oOkpE7nG(A@AuE&5uF zg5Fhhz~W&s-2xuT@+o6yIdb^yGvsvmCS)=IE1gWe-n^)!G{O8jKj$|}9{RU`_6Ms; z6|AJKLox;l{3z}{Sd;vu@0<~gIq`x1z4l_JV~K)1>ZSJgZxBuLbIxyik+P#^+0|l6 zc2qEC1%D*h7bF(AL&DyX(6jm z!3+EDfmI3@dCztDQ{RIQIwJsoPIyW|U442*6}+Vw-{N1~gCM{CiSNVH`Wdmi*ao+# z1D+q%yo|+f6#2am`tS-}l1`+YC+sqZ1x)}n5YU;rFD;tr#& z32!WYm;Y7y^uNUb(?0szGs_woke)BFWgW#sS9W#p>T@70?Yu+ja*^n#@>sT-EB<4=6fmL=a;?djM#C-Jb8F1)46Ih5vZ2?)L!Wnt*3#6XDb6u}Yiiom+_ln#W~9gprG9>;hDEQ6MX zcMGLXf_-stvUa+E-v0RbIAVhMUUi@bHKFTcTC}xRvVN{!Nz*<&4lrZ$RPLwOtlS5* z^*W2f9f5DTqx#2>527ueYfXi2X>3h#R^#rgdX@WJ`o}*ndu6I=ERaY69N%#2;YZ@Q_3XDp+t`N!jlJ}VugZXi8dtpHn5p+yOQ z?f193-ueE2`&*oav?e6y4vb6;ak1={*u~QS>9xl3-B)?Gp0uNo8P0}di44hkU9q%U z)2dB>t2C`}hoaZfB|C-^lRu@TniG!@#9SEfZuiK zqIb0V59h&?x@_pd@xFImUdIWZC*U1#UrWosKM$ENuUmJ*2z_bo0W@$IRatuXcmAD* z`unzM`v9awR);T@Ev^(mYlMvQE_1f>Yi(I2PCzNmH}*dyELX3!Gk3V*UFMS&|7lxR ztXa`!MVb}-f7mYK-jf(vAAhue1X!ZnW1KvI$u7Y@ap7%p`epQ5`8jsuSK2R7H9uB} z3`a-ZAj|f(UC#vg>S-U&!Bj9m8Dp0tr=WZwa@r|nEvoq#Bz_r-ICczh#ZFNwsAk+X zff++G3*fVhvp3@B*ubN=z#L|Ui&z;>=dd}vUTSb(dyc>lIeT%KIM{%TGI%~Wjy`g=s+q$cse6|DPBezKGr#;WniyUc&gUy07)ZJmxWf8ZJOz#= z-}M~kLw(tq(AyF$gkVf#>srto>vQaee+%!NFyR5ZS*BqtE>4--d|sIN^BdtDN#q-JTddS;0t$L*}m5;eb=_KH+ok|Dg?g0K^nR<*X?1uh;@xYS{-1v&HuT6__q9t4gV4P>!yF7xTD{}9IkOB57Wq6wqNQw_tb<7+5& z#;>&TkADXNp1Xrd=>}uOBh_`&7}+11hUXm<%FUFTJ=d@IddMw~It}oM2OXARs%ZD< zFo8U86UL|ie{$|Vvpy!OG|m|le~GrhFg#H7_^m-O)xV#s^7J<(?X&thIV*PO;kW1< zED%rD`Pcj7C)WkTPIJ!)+Xjo;LvsXW?m3k2TG-5*;kSi-I{edNziVi(J~?C4Y^Kpn zy_p*7-7Kfbszq~lhR>I+;U#nTq_6msf70fLb+4y_?mcQ2CX}$kcQd@4e_P{X{_oo~ z!@t?gqS-rtTgREOBgC`Kr_NZ3RHB6oc%^^!+dqht4w`ZJGP;9Vu|(3~#sKQCKJQP9 z{6}r}1IxEyTd`%Tz=8)7uh~5$*0tCDPP1chXbWi;+$^YBpnqyJ&t@LY+?%;I!?<^8 z=G+X<%KzjyIWqdHR6FFBf4fovlVd7sXK3a7Uj5Iw^6&@`vOhLU)pAQ|c*P;cep87!?? zYO|DP$yYoDe} zB01k%s_t zR9egl_I~5-pjy0ne}Q44Hpl!h{RI>k=ylU90Y8GPvpH&nbZgIRf?9B$Y+mBkE2|vp zRUHLm#SHX45A87Cxcd+e&vMe{B+Uut<>X;)fz2A9zoOWTx4l_ssf0Ak}2Z$IJ*E?W^GYQ;b zhrRL_bkb{)rPt#Hv_s#TR`Ybg9i&*fZrS#DK>pQsE|=2#EGM9KXIajqg`CzLmB0}aA{VXW{B?cs0;0S7fiDE*s)X9;k&#< zu&5S~_M~pduHo*vF7MifnhVaW%^ANzV1DnqI^4GkycjG_bUb5bK841YzL&D7Q|ie9 zJNZ2Wj+t<#wFSHN+dlu$K5UF+m;l5M|Bd3&bsZ~We_r4I!|4A3`?f6|yo^1|9Gqt2 zV-5BFr8fDS{x7z=!0gEBXf-ly|DNeodvv}AdEfTGEIj;bJSitOUuIz1DdwB;!TP@c zhm=!6?m~KuEj7mKbLlvi>)h|}xBb6qScR(v{0VCi^a1rzp&W|!_UV55U;f@drnJ$k z2f@IGe_|Gf`4MXJJDsonzhqeOJ|jiqtXP{i0gJ6p*UX5ovA`L_RIwNZErq4$nce~#!tB<8_wQu?^Y)H!aF32k0Nh$zAR`)}aG1Zm!f^;S;Ruj8R7yWa#A7 ze+f*WBu8g`k6)PLsy0`7747@%HJ}681wbJ%8@3tzedVul2&>Gq*6It6?+3ZtMKZA# z>TAloU4Mb{?++XVgy85j%AC>dz?S9Q`N4A>cG)_0JZA&`4j}odLRB-BZjRG6zQ%dh z*hR)D$3Wa2v+t5F)N6(L@cuHMx9TLzf4w`SY)Fq8F!!J)OgN!`eea(fK1g;Ag7;C) zT#+dtpl`cYtPV7#D+=?5(%;{5iyzJ-7t}6v zI78MW2S&9F6Y|qnsJ}g=-13L>lYn6vf3#7bZ-1=Kz`|tFd0fJa8CRIw0OWjggYNRT zzEs}O?2G_nzA}m!VJia@zEb$@0q@z|qq%$Y_j=g<#tN?^pyI4=55@SIBjsU3>{;&` z(LKzBdF_A|3ycGEo(fAbf95zj ziw=B@?mRKPdDwIOOt9l}dAHq-6TX)Pi)c^zf+TgAVkb3EoLiemHiykSIKd=!2~7f= zVx{a-&!9f{xtcRid5(<%Uf_XJOMMnEG0uWL<>E4upYiS$$JgeW%`rC9o2NC0foMkp zaiG39*F0tRAyIoBNbAP+VDt*_e{AG{;UXt%sUA8Ll)5Rld8usW_q(xX^BT>oH?P*b zYV#^jpTuK@zGqS4vEg~X3aI0dDowiAib5?g-?n^Eu+TL*984UGOQdXAiaww^m|X;1 zhj`y>N0AogqFc+E)^i`hdS%ym_SLIwd_Y4kNdDX7H>M^7?@SoXmY5#7EeJ1cWRmB* pef@uVY=oH3(~I=knc#caX?5$c_F8xS73E^8{||6HCK~IS0RWC=8#n*} diff --git a/creusot/tests/should_fail/bug/436_0.stderr b/creusot/tests/should_fail/bug/436_0.stderr index 7f70e70fa..1ed777cd7 100644 --- a/creusot/tests/should_fail/bug/436_0.stderr +++ b/creusot/tests/should_fail/bug/436_0.stderr @@ -1,7 +1,7 @@ error: called prophetic logic function `prophecy` in logic context --> 436_0.rs:15:23 | -15 | b.g = snapshot! { prophecy(b) + 1i32 }; +15 | b.g = snapshot! { prophecy(b) + 1 }; | ^^^^^^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_succeed/100doors.coma b/creusot/tests/should_succeed/100doors.coma index f61a8065d..b633da86e 100644 --- a/creusot/tests/should_succeed/100doors.coma +++ b/creusot/tests/should_succeed/100doors.coma @@ -26,7 +26,7 @@ module M_100doors__f [#"100doors.rs" 18 0 18 10] let%span svec24 = "../../../creusot-contracts/src/std/vec.rs" 154 26 154 57 let%span svec25 = "../../../creusot-contracts/src/std/vec.rs" 155 26 155 62 let%span svec26 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 - let%span sops27 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex27 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span siter28 = "../../../creusot-contracts/src/std/iter.rs" 86 20 86 24 let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 92 8 92 19 let%span srange30 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24 @@ -90,7 +90,7 @@ module M_100doors__f [#"100doors.rs" 18 0 18 10] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : bool = - [%#sops27] Seq.get (view'0 self) ix + [%#sindex27] Seq.get (view'0 self) ix let rec from_elem'0 (elem:bool) (n:usize) (return' (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'2 elem} any diff --git a/creusot/tests/should_succeed/bug/545.coma b/creusot/tests/should_succeed/bug/545.coma index 4db4c532b..b81b30661 100644 --- a/creusot/tests/should_succeed/bug/545.coma +++ b/creusot/tests/should_succeed/bug/545.coma @@ -1,7 +1,5 @@ module M_545__negative_is_negative [#"545.rs" 4 0 4 29] - let%span s5450 = "545.rs" 5 18 5 32 - - use prelude.prelude.Int32 + let%span s5450 = "545.rs" 5 18 5 26 use prelude.prelude.Int @@ -10,6 +8,6 @@ module M_545__negative_is_negative [#"545.rs" 4 0 4 29] meta "compute_max_steps" 1000000 let rec negative_is_negative'0 (_1:()) (return' (ret:()))= (! bb0 - [ bb0 = s0 [ s0 = {[@expl:assertion] [%#s5450] (0 : int32) > (-100 : int32)} s1 | s1 = return' {_0} ] ] + [ bb0 = s0 [ s0 = {[@expl:assertion] [%#s5450] 0 > - 100} s1 | s1 = return' {_0} ] ] ) [ & _0 : () = any_l () ] [ return' (result:())-> (! return' {result}) ] end diff --git a/creusot/tests/should_succeed/bug/545/why3session.xml b/creusot/tests/should_succeed/bug/545/why3session.xml index 3da0b4cb1..3cd235676 100644 --- a/creusot/tests/should_succeed/bug/545/why3session.xml +++ b/creusot/tests/should_succeed/bug/545/why3session.xml @@ -6,7 +6,7 @@ - + diff --git a/creusot/tests/should_succeed/bug/545/why3shapes.gz b/creusot/tests/should_succeed/bug/545/why3shapes.gz index aa29824d3266e47cb0db818de083d75750815c4c..0188dc9cb08d222d89525e670d83ba18df7d8ab0 100644 GIT binary patch delta 69 zcmV-L0J{HdWsoI6Hb~YrG%(;w%`GUYj0Y>?;xbA#N=dd%GPX1~HZ@5#OEEV|F-kH? bOiHw{G%zzZuv9SgFyI0JpuO5BQ~&?~b50mi delta 76 zcmYeznV{;fbF%;Z8EsFq2E!6wUY;F6#oS(6j}J!e*x}O~>~rR9uurcKkT^5RN2oXG gtj=WJpk7_xGnaTKO%ma;<=MfY!elO)#K6D+0J6v&bpQYW diff --git a/creusot/tests/should_succeed/bug/682.coma b/creusot/tests/should_succeed/bug/682.coma index 628e01159..890d34a4c 100644 --- a/creusot/tests/should_succeed/bug/682.coma +++ b/creusot/tests/should_succeed/bug/682.coma @@ -1,29 +1,35 @@ module M_682__add_some [#"682.rs" 6 0 6 24] let%span s6820 = "682.rs" 7 10 7 11 - let%span s6821 = "682.rs" 4 11 4 32 + let%span s6821 = "682.rs" 4 11 4 35 let%span s6822 = "682.rs" 5 10 5 17 - let%span sresolve3 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sarithmetic3 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42 + let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt64 use prelude.prelude.Borrow predicate resolve'1 (self : borrowed uint64) = - [%#sresolve3] self.final = self.current + [%#sresolve4] self.final = self.current predicate resolve'0 (_1 : borrowed uint64) = resolve'1 _1 use prelude.prelude.Intrinsic + use prelude.prelude.UInt64 + constant v_MAX'0 : uint64 = (18446744073709551615 : uint64) use prelude.prelude.Int + function div'0 (self : uint64) (other : uint64) : int = + [%#sarithmetic3] div (UInt64.to_int self) (UInt64.to_int other) + meta "compute_max_steps" 1000000 - let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6821] a.current - <= div (v_MAX'0 : uint64) (2 : uint64)} + let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6821] UInt64.to_int a.current + <= div'0 (v_MAX'0 : uint64) (2 : uint64)} (! bb0 [ bb0 = s0 [ s0 = UInt64.add {a.current} {[%#s6820] (1 : uint64)} @@ -40,9 +46,10 @@ module M_682__foo [#"682.rs" 12 0 12 23] let%span s6821 = "682.rs" 15 18 15 27 let%span s6822 = "682.rs" 10 11 10 21 let%span s6823 = "682.rs" 11 10 11 17 - let%span s6824 = "682.rs" 4 11 4 32 + let%span s6824 = "682.rs" 4 11 4 35 let%span s6825 = "682.rs" 5 10 5 17 - let%span sresolve6 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sarithmetic6 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42 + let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Borrow @@ -50,16 +57,21 @@ module M_682__foo [#"682.rs" 12 0 12 23] use prelude.prelude.UInt64 + use prelude.prelude.UInt64 + constant v_MAX'0 : uint64 = (18446744073709551615 : uint64) use prelude.prelude.Int - let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6824] a.current - <= div (v_MAX'0 : uint64) (2 : uint64)} + function div'0 (self : uint64) (other : uint64) : int = + [%#sarithmetic6] div (UInt64.to_int self) (UInt64.to_int other) + + let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6824] UInt64.to_int a.current + <= div'0 (v_MAX'0 : uint64) (2 : uint64)} any [ return' (result:())-> {[%#s6825] a.final > a.current} (! return' {result}) ] predicate resolve'1 (self : borrowed uint64) = - [%#sresolve6] self.final = self.current + [%#sresolve7] self.final = self.current predicate resolve'0 (_1 : borrowed uint64) = resolve'1 _1 diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml index f21977ed1..f7e906ff8 100644 --- a/creusot/tests/should_succeed/bug/682/why3session.xml +++ b/creusot/tests/should_succeed/bug/682/why3session.xml @@ -6,13 +6,13 @@ - - + + - - + + diff --git a/creusot/tests/should_succeed/bug/682/why3shapes.gz b/creusot/tests/should_succeed/bug/682/why3shapes.gz index 2821fcbf164e7db4fd3a1574b282d21ac577be23..a2354c5dfccee9ed61b603363f16fbb40cc498c3 100644 GIT binary patch literal 247 zcmVqggbi8{X_uf6M`0#;88u&zM@G(4d#aE9EUvZ4B4OBK1Yet9T_|^V2yQ4}qQyOsteF&5=(E0z3mu9~%-4p-vv>CN|&6rzTi-xEGkV2Od xopQSDwblyrH4qnDV4cRkL+PN;Md_f>g)yXEuD~jr8^gs`vTrP0g*x#80069%b({bI literal 249 zcmV?&M@j^=A;xeeo18vtIXj%aQJcH7mhij?xeF+(5}a?^aPhYPi`&E7X1TR)oW!wt zFF%smpejbE^YGRDwERb{az<)7EuHri!PE8e_RFwemmaNhd*)1HS}|sHm!e29H+d(O z6;|m&XIZK+MJq+Y {[%#s014] inv'1 result} {[%#s015] inv'2 result} (! return' {result}) ] diff --git a/creusot/tests/should_succeed/cell/01/why3shapes.gz b/creusot/tests/should_succeed/cell/01/why3shapes.gz index 99b9bee6604b7aff518737fc4e286a640884996e..6b7e395ebfcb85b7bab3a740d41b17fecc08b3d3 100644 GIT binary patch literal 202 zcmV;*05$&~iwFP!00000|80=D4#F@HM0r1Etw)N#KRgQBjE6|M!@CAgpzr>&4~-w zHx#aK$Tu&J%)1>v1NeJ_FUni+t zU#?tVF27!qm{&Wzv*jOzoJ?5=agQR1O>vA%Km=rh8P1`EV@`R>(l7<`0j&5(Ttfi> E00`z)6951J diff --git a/creusot/tests/should_succeed/cell/02.coma b/creusot/tests/should_succeed/cell/02.coma index 980f8e2b7..c515e97a4 100644 --- a/creusot/tests/should_succeed/cell/02.coma +++ b/creusot/tests/should_succeed/cell/02.coma @@ -88,7 +88,7 @@ module M_02__fib_memo [#"02.rs" 95 0 95 50] let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span s0232 = "02.rs" 72 12 75 13 - let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span svec34 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 use prelude.prelude.Borrow @@ -236,7 +236,7 @@ module M_02__fib_memo [#"02.rs" 95 0 95 50] use prelude.prelude.Snapshot function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_Cell'0 = - [%#sops33] Seq.get (view'1 self) ix + [%#sindex33] Seq.get (view'1 self) ix predicate fib_cell'0 [#"02.rs" 84 0 84 32] (v : t_Vec'0) = [%#s0228] forall i : int . UIntSize.to_int ((index_logic'0 v i).t_Cell__ghost_inv'0).t_Fib__ix'0 = i diff --git a/creusot/tests/should_succeed/filter_positive.coma b/creusot/tests/should_succeed/filter_positive.coma index 807d00bb9..1e0a6ba92 100644 --- a/creusot/tests/should_succeed/filter_positive.coma +++ b/creusot/tests/should_succeed/filter_positive.coma @@ -160,7 +160,7 @@ module M_filter_positive__m [#"filter_positive.rs" 82 0 82 33] let%span smodel39 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice40 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span sops42 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex42 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel43 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span sslice44 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span sresolve45 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 @@ -257,7 +257,7 @@ module M_filter_positive__m [#"filter_positive.rs" 82 0 82 33] axiom inv_axiom'4 [@rewrite] : forall x : t_Vec'0 [inv'4 x] . inv'4 x = true function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops42] Seq.get (view'0 self) ix + [%#sindex42] Seq.get (view'0 self) ix let rec from_elem'0 (elem:int32) (n:usize) (return' (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'3 elem} any diff --git a/creusot/tests/should_succeed/ghost/ghost_vec.coma b/creusot/tests/should_succeed/ghost/ghost_vec.coma index 71ff1072a..d7d4f155e 100644 --- a/creusot/tests/should_succeed/ghost/ghost_vec.coma +++ b/creusot/tests/should_succeed/ghost/ghost_vec.coma @@ -43,7 +43,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18] let%span sghost41 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 let%span sseq42 = "../../../../creusot-contracts/src/logic/seq.rs" 445 22 445 26 let%span sseq43 = "../../../../creusot-contracts/src/logic/seq.rs" 444 14 444 34 - let%span sint44 = "../../../../creusot-contracts/src/logic/int.rs" 59 14 59 31 + let%span sint44 = "../../../../creusot-contracts/src/logic/int.rs" 60 14 60 31 let%span sghost45 = "../../../../creusot-contracts/src/ghost.rs" 199 22 199 26 let%span sghost46 = "../../../../creusot-contracts/src/ghost.rs" 199 4 199 32 let%span sghost47 = "../../../../creusot-contracts/src/ghost.rs" 197 14 197 31 diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma index 8b56ee369..cee42e48a 100644 --- a/creusot/tests/should_succeed/hashmap.coma +++ b/creusot/tests/should_succeed/hashmap.coma @@ -47,7 +47,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 116 4 116 46] (* My let%span svec4 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76 let%span shashmap5 = "hashmap.rs" 80 8 80 33 let%span svec6 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops7 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex7 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span shashmap8 = "hashmap.rs" 86 8 86 53 let%span shashmap9 = "hashmap.rs" 31 12 34 13 let%span shashmap10 = "hashmap.rs" 107 12 108 139 @@ -142,7 +142,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 116 4 116 46] (* My use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 = - [%#sops7] Seq.get (view'1 self) ix + [%#sindex7] Seq.get (view'1 self) ix let rec from_elem'0 (elem:t_List'0) (n:usize) (return' (ret:t_Vec'0))= {[@expl:from_elem 'elem' type invariant] inv'1 elem} any @@ -279,7 +279,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 122 4 122 41] (* My let%span svec37 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant38 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed39 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 - let%span sops40 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex40 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sinvariant41 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span sseq42 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 let%span shashmap43 = "hashmap.rs" 107 12 108 139 @@ -548,7 +548,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 122 4 122 41] (* My resolve'8 _1 function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 = - [%#sops40] Seq.get (view'4 self) ix + [%#sindex40] Seq.get (view'4 self) ix predicate invariant'11 [#"hashmap.rs" 105 4 105 30] (self : t_MyHashMap'0) = [%#shashmap43] 0 < Seq.length (view'4 self.t_MyHashMap__buckets'0) @@ -827,7 +827,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 154 4 154 43] (* My let%span sslice17 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice18 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span shashmap19 = "hashmap.rs" 91 20 91 66 - let%span sops20 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex20 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span shashmap21 = "hashmap.rs" 80 8 80 33 let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -997,7 +997,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 154 4 154 43] (* My [%#shashmap19] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'3 self.t_MyHashMap__buckets'0)) function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 = - [%#sops20] Seq.get (view'3 self) ix + [%#sindex20] Seq.get (view'3 self) ix function bucket'0 [#"hashmap.rs" 85 4 85 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 = [%#shashmap12] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k) @@ -1185,7 +1185,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 173 4 173 24] (* let%span shashmap24 = "hashmap.rs" 116 31 116 46 let%span shashmap25 = "hashmap.rs" 115 14 115 62 let%span svec26 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops27 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex27 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span shashmap28 = "hashmap.rs" 91 20 91 66 let%span shashmap29 = "hashmap.rs" 80 8 80 33 let%span ssnapshot30 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 @@ -1323,7 +1323,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 173 4 173 24] (* use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 = - [%#sops27] Seq.get (view'0 self) ix + [%#sindex27] Seq.get (view'0 self) ix type t_DeepModelTy'0 @@ -1720,7 +1720,7 @@ module M_hashmap__main [#"hashmap.rs" 213 0 213 13] let%span shashmap34 = "hashmap.rs" 31 12 34 13 let%span shashmap35 = "hashmap.rs" 107 12 108 139 let%span shashmap36 = "hashmap.rs" 91 20 91 66 - let%span sops37 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex37 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sinvariant38 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span svec39 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span shashmap40 = "hashmap.rs" 97 12 97 91 @@ -1773,7 +1773,7 @@ module M_hashmap__main [#"hashmap.rs" 213 0 213 13] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 = - [%#sops37] Seq.get (view'3 self) ix + [%#sindex37] Seq.get (view'3 self) ix type t_Option'1 = | C_None'0 diff --git a/creusot/tests/should_succeed/heapsort_generic.coma b/creusot/tests/should_succeed/heapsort_generic.coma index 7cd87cf09..241a95d98 100644 --- a/creusot/tests/should_succeed/heapsort_generic.coma +++ b/creusot/tests/should_succeed/heapsort_generic.coma @@ -136,7 +136,7 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29] let%span sheapsort_generic23 = "heapsort_generic.rs" 11 4 11 19 let%span smodel24 = "../../../creusot-contracts/src/model.rs" 97 8 97 28 let%span smodel25 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops26 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span ssnapshot27 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 let%span svec29 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 @@ -232,7 +232,7 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops26] Seq.get (view'2 self) ix + [%#sindex26] Seq.get (view'2 self) ix function deep_model'3 (self : t_T'0) : t_DeepModelTy'0 @@ -668,7 +668,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29] let%span svec51 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span smodel52 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sheapsort_generic53 = "heapsort_generic.rs" 11 4 11 19 - let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sord55 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord56 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord57 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -785,7 +785,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops54] Seq.get (view'2 self) ix + [%#sindex54] Seq.get (view'2 self) ix function deep_model'2 (self : t_T'0) : t_DeepModelTy'0 diff --git a/creusot/tests/should_succeed/hillel.coma b/creusot/tests/should_succeed/hillel.coma index 64c06a9fb..ad80df120 100644 --- a/creusot/tests/should_succeed/hillel.coma +++ b/creusot/tests/should_succeed/hillel.coma @@ -15,7 +15,7 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59] let%span shillel13 = "hillel.rs" 16 10 16 73 let%span ssnapshot14 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span smodel15 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops16 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span svec17 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -82,7 +82,7 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops16] Seq.get (view'2 self) ix + [%#sindex16] Seq.get (view'2 self) ix use seq.Seq @@ -229,7 +229,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58] let%span shillel13 = "hillel.rs" 31 10 31 62 let%span shillel14 = "hillel.rs" 32 10 32 88 let%span shillel15 = "hillel.rs" 33 10 33 104 - let%span sops16 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel17 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span ssnapshot18 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 @@ -292,7 +292,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops16] Seq.get (view'2 self) ix + [%#sindex16] Seq.get (view'2 self) ix function view'0 (self : borrowed (t_Vec'0)) : Seq.seq t_T'0 = [%#smodel17] view'2 self.current @@ -505,11 +505,11 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] let%span svec23 = "../../../creusot-contracts/src/std/vec.rs" 169 26 169 42 let%span sslice24 = "../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span siter25 = "../../../creusot-contracts/src/std/iter.rs" 101 0 213 1 - let%span sops26 = "../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33 + let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33 let%span smodel27 = "../../../creusot-contracts/src/model.rs" 79 8 79 28 let%span sslice28 = "../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 107 26 110 17 - let%span sops30 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex30 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span scmp31 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 let%span shillel32 = "hillel.rs" 60 8 60 64 let%span shillel33 = "hillel.rs" 53 8 53 105 @@ -533,7 +533,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] let%span smodel51 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span sslice52 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice53 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span svec57 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 @@ -604,7 +604,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] use seq.Seq function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops30] Seq.get (view'3 self) ix + [%#sindex30] Seq.get (view'3 self) ix function deep_model'1 (self : t_T'0) : t_DeepModelTy'0 @@ -724,7 +724,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] use seq.Seq function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq t_T'0)) (ix : int) : t_T'0 = - [%#sops26] Seq.get (Snapshot.inner self) ix + [%#sindex26] Seq.get (Snapshot.inner self) ix function deep_model'2 (self : t_T'0) : t_DeepModelTy'0 = [%#smodel27] deep_model'1 self @@ -736,7 +736,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] use seq.Seq function index_logic'2 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops54] Seq.get (view'5 self) ix + [%#sindex54] Seq.get (view'5 self) ix function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0 @@ -1039,7 +1039,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] let%span siter40 = "../../../creusot-contracts/src/std/iter.rs" 92 8 92 19 let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 40 14 40 44 let%span sslice42 = "../../../creusot-contracts/src/std/slice.rs" 41 14 41 96 - let%span sops43 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex43 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span shillel44 = "hillel.rs" 60 8 60 64 let%span srange45 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24 let%span srange46 = "../../../creusot-contracts/src/std/iter/range.rs" 34 14 34 45 @@ -1055,7 +1055,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] let%span smodel56 = "../../../creusot-contracts/src/model.rs" 97 8 97 28 let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice58 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops59 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex59 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span svec60 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant61 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sinvariant62 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -1201,7 +1201,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] use seq.Seq function index_logic'1 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops59] Seq.get (view'2 self) ix + [%#sindex59] Seq.get (view'2 self) ix function deep_model'3 (self : t_T'0) : t_DeepModelTy'0 @@ -1222,7 +1222,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops43] Seq.get (view'1 self) ix + [%#sindex43] Seq.get (view'1 self) ix function deep_model'1 (self : t_Vec'0) : Seq.seq t_DeepModelTy'0 @@ -1595,7 +1595,7 @@ module M_hillel__score [#"hillel.rs" 147 0 147 38] let%span shillel9 = "hillel.rs" 148 4 148 41 let%span shillel10 = "hillel.rs" 121 0 121 8 let%span shillel11 = "hillel.rs" 138 4 140 5 - let%span sint12 = "../../../creusot-contracts/src/logic/int.rs" 156 4 156 12 + let%span sint12 = "../../../creusot-contracts/src/logic/int.rs" 157 4 157 12 use prelude.prelude.Int @@ -1713,7 +1713,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30] let%span shillel57 = "hillel.rs" 136 10 136 85 let%span shillel58 = "hillel.rs" 134 10 134 18 let%span shillel59 = "hillel.rs" 138 4 140 5 - let%span sint60 = "../../../creusot-contracts/src/logic/int.rs" 156 4 156 12 + let%span sint60 = "../../../creusot-contracts/src/logic/int.rs" 157 4 157 12 let%span srange61 = "../../../creusot-contracts/src/std/iter/range.rs" 33 15 33 24 let%span srange62 = "../../../creusot-contracts/src/std/iter/range.rs" 34 14 34 45 let%span srange63 = "../../../creusot-contracts/src/std/iter/range.rs" 39 15 39 21 @@ -1724,7 +1724,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30] let%span srange68 = "../../../creusot-contracts/src/std/iter/range.rs" 44 14 44 42 let%span snum69 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 let%span srange70 = "../../../creusot-contracts/src/std/iter/range.rs" 15 12 15 78 - let%span sops71 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex71 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span smodel72 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 use prelude.prelude.UInt32 @@ -1815,7 +1815,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30] use seq.Seq function index_logic'0 [@inline:trivial] (self : slice uint32) (ix : int) : uint32 = - [%#sops71] Seq.get (view'1 self) ix + [%#sindex71] Seq.get (view'1 self) ix function to_ref_seq'0 (self : slice uint32) : Seq.seq uint32 diff --git a/creusot/tests/should_succeed/index_range.coma b/creusot/tests/should_succeed/index_range.coma index f70ad1c3f..ce63fe7fa 100644 --- a/creusot/tests/should_succeed/index_range.coma +++ b/creusot/tests/should_succeed/index_range.coma @@ -9,7 +9,7 @@ module M_index_range__create_arr [#"index_range.rs" 14 0 14 27] let%span svec7 = "../../../creusot-contracts/src/std/vec.rs" 74 26 74 44 let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops10 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex10 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel11 = "../../../creusot-contracts/src/model.rs" 106 8 106 22 use prelude.prelude.Opaque @@ -79,7 +79,7 @@ module M_index_range__create_arr [#"index_range.rs" 14 0 14 27] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops10] Seq.get (view'0 self) ix + [%#sindex10] Seq.get (view'0 self) ix use prelude.prelude.Int32 @@ -229,7 +229,7 @@ module M_index_range__test_range [#"index_range.rs" 27 0 27 19] let%span svec84 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec85 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec86 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops87 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex87 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel88 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice89 = "../../../creusot-contracts/src/std/slice.rs" 144 20 144 70 let%span sslice90 = "../../../creusot-contracts/src/std/slice.rs" 150 20 150 67 @@ -279,7 +279,7 @@ module M_index_range__test_range [#"index_range.rs" 27 0 27 19] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops87] Seq.get (view'0 self) ix + [%#sindex87] Seq.get (view'0 self) ix use prelude.prelude.Int32 @@ -861,7 +861,7 @@ module M_index_range__test_range_to [#"index_range.rs" 78 0 78 22] let%span svec57 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec58 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec59 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops60 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex60 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel61 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice62 = "../../../creusot-contracts/src/std/slice.rs" 167 20 167 42 let%span sslice63 = "../../../creusot-contracts/src/std/slice.rs" 173 20 173 57 @@ -911,7 +911,7 @@ module M_index_range__test_range_to [#"index_range.rs" 78 0 78 22] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops60] Seq.get (view'0 self) ix + [%#sindex60] Seq.get (view'0 self) ix use prelude.prelude.Int32 @@ -1349,7 +1349,7 @@ module M_index_range__test_range_from [#"index_range.rs" 115 0 115 24] let%span svec59 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec60 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec61 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops62 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex62 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel63 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice64 = "../../../creusot-contracts/src/std/slice.rs" 187 20 187 44 let%span sslice65 = "../../../creusot-contracts/src/std/slice.rs" 193 20 193 67 @@ -1399,7 +1399,7 @@ module M_index_range__test_range_from [#"index_range.rs" 115 0 115 24] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops62] Seq.get (view'0 self) ix + [%#sindex62] Seq.get (view'0 self) ix use prelude.prelude.Int32 @@ -1842,7 +1842,7 @@ module M_index_range__test_range_full [#"index_range.rs" 154 0 154 24] let%span svec51 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec52 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec53 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops54 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel55 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice56 = "../../../creusot-contracts/src/std/slice.rs" 209 20 209 24 let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 215 20 215 31 @@ -1892,7 +1892,7 @@ module M_index_range__test_range_full [#"index_range.rs" 154 0 154 24] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops54] Seq.get (view'0 self) ix + [%#sindex54] Seq.get (view'0 self) ix use prelude.prelude.Int32 @@ -2300,7 +2300,7 @@ module M_index_range__test_range_to_inclusive [#"index_range.rs" 179 0 179 32] let%span svec54 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec55 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec56 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops57 = "../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex57 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span smodel58 = "../../../creusot-contracts/src/model.rs" 88 8 88 22 let%span sslice59 = "../../../creusot-contracts/src/std/slice.rs" 229 20 229 41 let%span sslice60 = "../../../creusot-contracts/src/std/slice.rs" 235 20 235 61 @@ -2350,7 +2350,7 @@ module M_index_range__test_range_to_inclusive [#"index_range.rs" 179 0 179 32] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : int32 = - [%#sops57] Seq.get (view'0 self) ix + [%#sindex57] Seq.get (view'0 self) ix use prelude.prelude.Int32 diff --git a/creusot/tests/should_succeed/insertion_sort.coma b/creusot/tests/should_succeed/insertion_sort.coma index 6cf0870e1..fd18bc1ad 100644 --- a/creusot/tests/should_succeed/insertion_sort.coma +++ b/creusot/tests/should_succeed/insertion_sort.coma @@ -30,8 +30,8 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40] let%span sinsertion_sort28 = "insertion_sort.rs" 8 8 8 72 let%span srange29 = "../../../creusot-contracts/src/std/iter/range.rs" 23 12 27 70 let%span siter30 = "../../../creusot-contracts/src/std/iter.rs" 107 26 110 17 - let%span sops31 = "../../../creusot-contracts/src/logic/ops.rs" 55 8 55 32 - let%span sops32 = "../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex31 = "../../../creusot-contracts/src/logic/ops/index.rs" 56 8 56 32 + let%span sindex32 = "../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice33 = "../../../creusot-contracts/src/std/slice.rs" 257 19 257 35 let%span sslice34 = "../../../creusot-contracts/src/std/slice.rs" 258 19 258 35 let%span sslice35 = "../../../creusot-contracts/src/std/slice.rs" 259 18 259 50 @@ -222,10 +222,10 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40] function index_logic'0 [@inline:trivial] (self : slice int32) (ix : usize) : int32 = - [%#sops31] Seq.get (view'2 self) (UIntSize.to_int ix) + [%#sindex31] Seq.get (view'2 self) (UIntSize.to_int ix) function index_logic'1 [@inline:trivial] (self : slice int32) (ix : int) : int32 = - [%#sops32] Seq.get (view'2 self) ix + [%#sindex32] Seq.get (view'2 self) ix predicate inv'5 (_1 : borrowed (slice int32)) diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.coma b/creusot/tests/should_succeed/iterators/02_iter_mut.coma index 2b5aadbff..7439a5497 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut.coma +++ b/creusot/tests/should_succeed/iterators/02_iter_mut.coma @@ -9,7 +9,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl [#"02_iter_mut.rs" 5 let%span s02_iter_mut7 = "02_iter_mut.rs" 22 20 22 64 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 @@ -102,7 +102,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl [#"02_iter_mut.rs" 5 use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops10] Seq.get (view'1 self) ix + [%#sindex10] Seq.get (view'1 self) ix function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -147,7 +147,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans [#"02_iter_mut.rs" let%span s02_iter_mut11 = "02_iter_mut.rs" 22 20 22 64 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops14 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex14 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sinvariant15 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 @@ -238,7 +238,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans [#"02_iter_mut.rs" use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops14] Seq.get (view'1 self) ix + [%#sindex14] Seq.get (view'1 self) ix function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -287,7 +287,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 67 4 67 44 let%span sslice3 = "../../../../creusot-contracts/src/std/slice.rs" 291 18 298 9 let%span s02_iter_mut4 = "02_iter_mut.rs" 32 8 32 76 let%span s02_iter_mut5 = "02_iter_mut.rs" 39 12 43 13 - let%span sops6 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex6 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 173 8 173 39 @@ -391,7 +391,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 67 4 67 44 use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops6] Seq.get (view'0 self) ix + [%#sindex6] Seq.get (view'0 self) ix use seq.Seq @@ -869,14 +869,14 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35] let%span s02_iter_mut14 = "02_iter_mut.rs" 74 17 74 21 let%span s02_iter_mut15 = "02_iter_mut.rs" 74 26 74 30 let%span s02_iter_mut16 = "02_iter_mut.rs" 73 14 73 28 - let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33 + let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33 let%span s02_iter_mut18 = "02_iter_mut.rs" 39 12 43 13 let%span s02_iter_mut19 = "02_iter_mut.rs" 67 17 67 21 let%span s02_iter_mut20 = "02_iter_mut.rs" 67 26 67 44 let%span s02_iter_mut21 = "02_iter_mut.rs" 63 14 66 5 let%span svec22 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops24 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sslice25 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span s02_iter_mut27 = "02_iter_mut.rs" 49 15 49 24 @@ -893,7 +893,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35] let%span sslice38 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span s02_iter_mut39 = "02_iter_mut.rs" 32 8 32 76 let%span sresolve40 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sops41 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex41 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span s02_iter_mut42 = "02_iter_mut.rs" 22 20 22 64 let%span sinvariant43 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -1002,7 +1002,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35] function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (borrowed usize))) (ix : int) : borrowed usize = - [%#sops17] Seq.get (Snapshot.inner self) ix + [%#sindex17] Seq.get (Snapshot.inner self) ix use prelude.prelude.Snapshot @@ -1013,7 +1013,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35] use seq.Seq function index_logic'2 [@inline:trivial] (self : slice usize) (ix : int) : usize = - [%#sops41] Seq.get (view'3 self) ix + [%#sindex41] Seq.get (view'3 self) ix function to_mut_seq'0 (self : borrowed (slice usize)) : Seq.seq (borrowed usize) @@ -1113,7 +1113,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 88 0 88 35] use prelude.prelude.Snapshot function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize = - [%#sops24] Seq.get (view'0 self) ix + [%#sindex24] Seq.get (view'0 self) ix meta "compute_max_steps" 1000000 @@ -1191,7 +1191,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans__refines [#"02_iter let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops7 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span s02_iter_mut8 = "02_iter_mut.rs" 22 20 22 64 let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 @@ -1239,7 +1239,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans__refines [#"02_iter use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops7] Seq.get (view'1 self) ix + [%#sindex7] Seq.get (view'1 self) ix function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -1324,7 +1324,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6 let%span sinvariant7 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span s02_iter_mut11 = "02_iter_mut.rs" 22 20 22 64 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 let%span sseq13 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 @@ -1439,7 +1439,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6 use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops10] Seq.get (view'1 self) ix + [%#sindex10] Seq.get (view'1 self) ix function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) @@ -1499,7 +1499,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl__refines [#"02_iter_ let%span s02_iter_mut5 = "02_iter_mut.rs" 22 20 22 64 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops8 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex8 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 @@ -1592,7 +1592,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl__refines [#"02_iter_ use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops8] Seq.get (view'1 self) ix + [%#sindex8] Seq.get (view'1 self) ix function to_mut_seq'0 (self : borrowed (slice t_T'0)) : Seq.seq (borrowed t_T'0) diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.coma b/creusot/tests/should_succeed/iterators/03_std_iterators.coma index ad3506963..110f27a56 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.coma +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.coma @@ -28,7 +28,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42] let%span sresolve26 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice27 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice28 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span sops29 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex29 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sseq30 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span sinvariant32 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -146,7 +146,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42] use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops29] Seq.get (view'2 self) ix + [%#sindex29] Seq.get (view'2 self) ix function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0 @@ -339,7 +339,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41] let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 let%span sresolve25 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec26 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops27 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex27 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span sseq28 = "../../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -471,7 +471,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41] use seq.Seq function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops27] Seq.get (view'5 self) ix + [%#sindex27] Seq.get (view'5 self) ix function to_ref_seq'0 (self : slice t_T'0) : Seq.seq t_T'0 @@ -651,12 +651,12 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 176 26 176 48 let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span siter11 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1 - let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33 + let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 459 12 459 66 let%span siter14 = "../../../../creusot-contracts/src/std/iter.rs" 107 26 110 17 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops17 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sslice18 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 427 14 427 50 @@ -677,7 +677,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice36 = "../../../../creusot-contracts/src/std/slice.rs" 452 20 452 61 let%span sslice37 = "../../../../creusot-contracts/src/std/slice.rs" 437 20 437 36 - let%span sops38 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex38 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 use prelude.prelude.Borrow @@ -798,7 +798,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (borrowed usize))) (ix : int) : borrowed usize = - [%#sops12] Seq.get (Snapshot.inner self) ix + [%#sindex12] Seq.get (Snapshot.inner self) ix use prelude.prelude.Snapshot @@ -809,7 +809,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] use seq.Seq function index_logic'2 [@inline:trivial] (self : slice usize) (ix : int) : usize = - [%#sops38] Seq.get (view'3 self) ix + [%#sindex38] Seq.get (view'3 self) ix function to_mut_seq'0 (self : borrowed (slice usize)) : Seq.seq (borrowed usize) @@ -906,7 +906,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] use prelude.prelude.Snapshot function index_logic'1 [@inline:trivial] (self : t_Vec'0) (ix : int) : usize = - [%#sops17] Seq.get (view'0 self) ix + [%#sindex17] Seq.get (view'0 self) ix meta "compute_max_steps" 1000000 @@ -1373,7 +1373,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] let%span smap_inv51 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 32 15 32 32 let%span smap_inv52 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 33 15 33 32 let%span smap_inv53 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 34 14 34 42 - let%span sops54 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 + let%span sindex54 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 let%span smodel55 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 let%span sinvariant56 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -1553,7 +1553,7 @@ 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 = - [%#sops54] Seq.get (view'4 self) ix + [%#sindex54] Seq.get (view'4 self) ix function to_ref_seq'0 (self : slice uint32) : Seq.seq uint32 @@ -2049,7 +2049,7 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24] let%span siter7 = "../../../../creusot-contracts/src/std/iter.rs" 154 27 154 103 let%span siter8 = "../../../../creusot-contracts/src/std/iter.rs" 155 27 157 54 let%span siter9 = "../../../../creusot-contracts/src/std/iter.rs" 101 0 213 1 - let%span sops10 = "../../../../creusot-contracts/src/logic/ops.rs" 88 8 88 33 + let%span sindex10 = "../../../../creusot-contracts/src/logic/ops/index.rs" 89 8 89 33 let%span senumerate11 = "../../../../creusot-contracts/src/std/iter/enumerate.rs" 74 12 78 113 let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 107 26 110 17 let%span srange13 = "../../../../creusot-contracts/src/std/iter/range.rs" 15 12 15 78 @@ -2206,7 +2206,7 @@ module M_03_std_iterators__enumerate_range [#"03_std_iterators.rs" 72 0 72 24] function index_logic'0 [@inline:trivial] (self : Snapshot.snap_ty (Seq.seq (usize, usize))) (ix : int) : (usize, usize) = - [%#sops10] Seq.get (Snapshot.inner self) ix + [%#sindex10] Seq.get (Snapshot.inner self) ix use prelude.prelude.Snapshot @@ -2406,8 +2406,8 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] let%span sslice29 = "../../../../creusot-contracts/src/std/slice.rs" 257 19 257 35 let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 258 19 258 35 let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 259 18 259 50 - let%span sops32 = "../../../../creusot-contracts/src/logic/ops.rs" 44 8 44 31 - let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 55 8 55 32 + let%span sindex32 = "../../../../creusot-contracts/src/logic/ops/index.rs" 45 8 45 31 + let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 56 8 56 32 let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 88 8 88 22 @@ -2755,10 +2755,10 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] function index_logic'0 [@inline:trivial] (self : slice t_T'0) (ix : int) : t_T'0 = - [%#sops32] Seq.get (view'2 self) ix + [%#sindex32] Seq.get (view'2 self) ix function index_logic'1 [@inline:trivial] (self : slice t_T'0) (ix : usize) : t_T'0 = - [%#sops33] Seq.get (view'2 self) (UIntSize.to_int ix) + [%#sindex33] Seq.get (view'2 self) (UIntSize.to_int ix) predicate resolve'3 (self : borrowed (slice t_T'0)) = [%#sresolve51] self.final = self.current diff --git a/creusot/tests/should_succeed/iterators/04_skip.coma b/creusot/tests/should_succeed/iterators/04_skip.coma index 8217f7144..4b9130608 100644 --- a/creusot/tests/should_succeed/iterators/04_skip.coma +++ b/creusot/tests/should_succeed/iterators/04_skip.coma @@ -234,7 +234,7 @@ module M_04_skip__qyi17349041008065389927__next [#"04_skip.rs" 67 4 67 41] (* {[@expl:mc91 ensures] [%#smc913] x <= (100 : uint32) - -> result = (91 : uint32) /\ x > (100 : uint32) -> result = x - (10 : uint32)} + -> result = (91 : uint32) /\ x > (100 : uint32) -> UInt32.to_int result = sub'0 x (10 : uint32)} (! return' {result}) ] end diff --git a/creusot/tests/should_succeed/mc91/why3session.xml b/creusot/tests/should_succeed/mc91/why3session.xml index 8ee1f7511..08f10d8e5 100644 --- a/creusot/tests/should_succeed/mc91/why3session.xml +++ b/creusot/tests/should_succeed/mc91/why3session.xml @@ -6,8 +6,8 @@ - - + + diff --git a/creusot/tests/should_succeed/mc91/why3shapes.gz b/creusot/tests/should_succeed/mc91/why3shapes.gz index 5ea964a99a1e4c695c482cfda8382445742484aa..03f921796c28e75bf0edb2a96b8721b32e19d3b0 100644 GIT binary patch literal 217 zcmV;~04Dz*iwFP!00000|FzM}3c@fD1<-xIB0FCQlcWzSR_G?!y<}UaO~it>YFfd+ z7krUox^z2pIShBEb7~KGHkRJZ)z)pZq7j|X2&UMzMcs5&!qE2R1Qb*Za@@S<3O)e_ zkmEY_&s}EeiDXzeMcMX^w%&b?sbaXh_9pwsNiRkW88N~LFQdd;;X{Qx=?qgPs)V_k zyO$2faq)XMlWtMIz^f>UM{7nJxqPdXl9Jo)&DgpoiW4B~A literal 209 zcmV;?051O@iwFP!00000|Gknu3&JoEhWGr6j9L+r#22LMYaHWXjv$4hE$U{_oWktOtjJpz);R1T$PF^Ra8M#5fUj(cLd!4 Li4%D$QUU+~*s)|j diff --git a/creusot/tests/should_succeed/mutex.coma b/creusot/tests/should_succeed/mutex.coma index f54c048d0..981f825a4 100644 --- a/creusot/tests/should_succeed/mutex.coma +++ b/creusot/tests/should_succeed/mutex.coma @@ -8,7 +8,7 @@ module M_mutex__qyi5425553346843331945__call [#"mutex.rs" 100 4 100 23] (* {[%#smutex5] inv'1 result} @@ -120,7 +122,7 @@ module M_mutex__concurrent [#"mutex.rs" 163 0 163 19] let%span smutex9 = "mutex.rs" 130 11 130 27 let%span smutex10 = "mutex.rs" 121 21 121 34 let%span smutex11 = "mutex.rs" 117 14 120 5 - let%span smutex12 = "mutex.rs" 67 8 67 24 + let%span smutex12 = "mutex.rs" 67 8 67 25 let%span sresolve13 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span smutex14 = "mutex.rs" 92 8 92 12 let%span smutex15 = "mutex.rs" 149 4 149 16 @@ -138,10 +140,12 @@ module M_mutex__concurrent [#"mutex.rs" 163 0 163 19] use prelude.prelude.Borrow + use prelude.prelude.UInt32 + use prelude.prelude.Int predicate inv'2 [#"mutex.rs" 66 4 66 33] (self : ()) (x : uint32) = - [%#smutex12] mod x (2 : uint32) = (0 : uint32) + [%#smutex12] mod (UInt32.to_int x) 2 = 0 type t_MutexInner'0 diff --git a/creusot/tests/should_succeed/mutex/why3shapes.gz b/creusot/tests/should_succeed/mutex/why3shapes.gz index 1a899d0378865223bd45efc6f170970b13a52909..c015e86748d3285a8986773f19209e8be25f3368 100644 GIT binary patch literal 417 zcmV;S0bc$eiwFP!00000|E*FzlbkRN?fDgSB$r0m#x^(Eg2sU&-HuyEU@>8C4>&NJ z6O-PoTtZBrVnou|AOOm&A@_*AjWc=n+TEs zc!kTn`F@_<=*M}=z%t8C6LMLF%Su17CZXrWe{JvGV`*-giQp*BaGWMu(YGIWPhURl zxVpB@GqA#{Dri-MC-ieWPTnef7hw@V&&*BPcJn^D?N5AzCoA#1?o|D&YY(Ao4@Z{4 z%SH{p|E+2cxAXG7ba3OfiHaupS(y7shvZ=S-}6ireC8%PDJ(Y;#8_d4i6F+LEldP4 zrmQp(B)=>UeOo!Voj=bRWY167@9RpFxB7U3e1-o{g&JIGn=e<&;C4CvU~d257*7XB zL=17OOkC}GUoHf3k9oKU3wuZsJ}~0Y5wO8wS?EFz1LT7!ORfr%L&|Gb=QSj1(28q9 zlFYG==IEfOe>;q^=aD7OrE`De461n>2^ItaYtw8FIb> LVsr|SoC5#==w!;A literal 418 zcmV;T0bTwdiwFP!00000|E*HHlAJIQ%=rp3>~o?AdT`|pNMsQ>+fqsmLMl_YCpZvm z`|n-5NOt*kPOPZaGt;B#(VK^I`vi;I%Bx$qX%3GiFCX3(@dc)Et&l+~gUn%rRR%=@ zw1s8fqMgGy#c2)|GQ?2TrCQR$vbvw5s&LOs{Mz5UXK8AP%HWVDFoob&i2cVsx-TDg zSjWD{6*9FEZORoLoFLBq6rvIEE<=`pCF+*h5AzEy<16R|G&$<%$MBjt$Fzt^cY`Ak)IvNlv@kU3^*l|kmXVJd^n z3By$e#V?D4*tg@joj=bNs-B;~?(6D8H1c=?e {[%#s06_knights_tour37] Seq.length (view'3 result) = 8} @@ -2090,7 +2090,7 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : (usize, t_Point'0) = - [%#sops40] Seq.get (view'0 self) ix + [%#sindex40] Seq.get (view'0 self) ix use prelude.prelude.Snapshot diff --git a/creusot/tests/should_succeed/vector/08_haystack.coma b/creusot/tests/should_succeed/vector/08_haystack.coma index ee95b672b..35eb99cc2 100644 --- a/creusot/tests/should_succeed/vector/08_haystack.coma +++ b/creusot/tests/should_succeed/vector/08_haystack.coma @@ -32,7 +32,7 @@ module M_08_haystack__search [#"08_haystack.rs" 21 0 21 60] let%span siter30 = "../../../../creusot-contracts/src/std/iter.rs" 86 20 86 24 let%span siter31 = "../../../../creusot-contracts/src/std/iter.rs" 92 8 92 19 let%span svec32 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span sops33 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span srange34 = "../../../../creusot-contracts/src/std/iter/range.rs" 81 14 81 45 let%span srange35 = "../../../../creusot-contracts/src/std/iter/range.rs" 79 4 79 10 let%span srange36 = "../../../../creusot-contracts/src/std/iter/range.rs" 86 15 86 32 @@ -166,7 +166,7 @@ module M_08_haystack__search [#"08_haystack.rs" 21 0 21 60] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : uint8 = - [%#sops33] Seq.get (view'1 self) ix + [%#sindex33] Seq.get (view'1 self) ix predicate match_at'0 [#"08_haystack.rs" 7 0 7 77] (needle : t_Vec'0) (haystack : t_Vec'0) (pos : int) (len : int) = [%#s08_haystack22] len <= Seq.length (view'0 needle) diff --git a/creusot/tests/should_succeed/vector/09_capacity.coma b/creusot/tests/should_succeed/vector/09_capacity.coma index 8e64155fb..280ba8d6c 100644 --- a/creusot/tests/should_succeed/vector/09_capacity.coma +++ b/creusot/tests/should_succeed/vector/09_capacity.coma @@ -11,7 +11,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41] let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 130 26 130 43 let%span svec10 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 106 8 106 22 - let%span sops12 = "../../../../creusot-contracts/src/logic/ops.rs" 22 8 22 31 + let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sresolve13 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant15 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -113,7 +113,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41] use seq.Seq function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_T'0 = - [%#sops12] Seq.get (view'0 self) ix + [%#sindex12] Seq.get (view'0 self) ix meta "compute_max_steps" 1000000 From 7a1eebb8b7f79c6e8e25531645c36187ad20dc1d Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 16:21:13 +0100 Subject: [PATCH 7/8] `allow(unused_variables)` instead of `let _ = x` --- creusot-contracts/src/logic/int.rs | 34 +++++++++---------- .../creusot-contracts/creusot-contracts.coma | 24 ++++++------- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/creusot-contracts/src/logic/int.rs b/creusot-contracts/src/logic/int.rs index ac8fa5a04..b15a2ffc1 100644 --- a/creusot-contracts/src/logic/int.rs +++ b/creusot-contracts/src/logic/int.rs @@ -59,8 +59,8 @@ impl Int { #[pure] #[ensures(*result == value@)] #[allow(unreachable_code)] + #[allow(unused_variables)] pub fn new(value: i128) -> GhostBox { - let _ = value; ghost!(panic!()) } @@ -75,8 +75,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.Power.power"] + #[allow(unused_variables)] pub fn pow(self, p: Int) -> Int { - let _ = p; dead } @@ -91,8 +91,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.MinMax.max"] + #[allow(unused_variables)] pub fn max(self, x: Int) -> Int { - let _ = x; dead } @@ -107,8 +107,8 @@ impl Int { #[logic] #[creusot::builtins = "int.MinMax.min"] #[trusted] + #[allow(unused_variables)] pub fn min(self, x: Int) -> Int { - let _ = x; dead } @@ -123,8 +123,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.EuclideanDivision.div"] + #[allow(unused_variables)] pub fn div_euclid(self, d: Int) -> Int { - let _ = d; dead } @@ -139,8 +139,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.EuclideanDivision.mod"] + #[allow(unused_variables)] pub fn rem_euclid(self, d: Int) -> Int { - let _ = d; dead } @@ -171,8 +171,8 @@ impl AddLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "add_int"] + #[allow(unused_variables)] fn add(self, other: Self) -> Self { - let _ = other; dead } } @@ -183,8 +183,8 @@ impl SubLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "sub_int"] + #[allow(unused_variables)] fn sub(self, other: Self) -> Self { - let _ = other; dead } } @@ -195,8 +195,8 @@ impl MulLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "mul_int"] + #[allow(unused_variables)] fn mul(self, other: Self) -> Self { - let _ = other; dead } } @@ -207,8 +207,8 @@ impl DivLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "div_int"] + #[allow(unused_variables)] fn div(self, other: Self) -> Self { - let _ = other; dead } } @@ -219,8 +219,8 @@ impl RemLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "rem_int"] + #[allow(unused_variables)] fn rem(self, other: Self) -> Self { - let _ = other; dead } } @@ -242,8 +242,8 @@ impl PartialEq for Int { #[trusted] #[pure] #[ensures(result == (*self == *other))] + #[allow(unused_variables)] fn eq(&self, other: &Self) -> bool { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -253,8 +253,8 @@ impl Add for Int { #[trusted] #[pure] #[ensures(result == self + other)] + #[allow(unused_variables)] fn add(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -264,8 +264,8 @@ impl Sub for Int { #[trusted] #[pure] #[ensures(result == self - other)] + #[allow(unused_variables)] fn sub(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -275,8 +275,8 @@ impl Mul for Int { #[trusted] #[pure] #[ensures(result == self * other)] + #[allow(unused_variables)] fn mul(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -286,8 +286,8 @@ impl Div for Int { #[trusted] #[pure] #[ensures(result == self / other)] + #[allow(unused_variables)] fn div(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -297,8 +297,8 @@ impl Rem for Int { #[trusted] #[pure] #[ensures(result == self % other)] + #[allow(unused_variables)] fn rem(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index dda7dcb8a..8748b1839 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -27415,8 +27415,8 @@ module M_creusot_contracts__ghost__qyi17214052996668775070__deref_mut__refines [ = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1) /\ inv'1 result -> inv'1 result) end -module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#"../../../creusot-contracts/src/logic/int.rs" 245 4 245 38] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 245 4 245 38 +module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#"../../../creusot-contracts/src/logic/int.rs" 246 4 246 38] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 246 4 246 38 let%span smodel1 = "../../../creusot-contracts/src/model.rs" 79 8 79 28 let%span smodel2 = "../../../creusot-contracts/src/model.rs" 126 8 126 12 @@ -27437,8 +27437,8 @@ module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#". goal refines : [%#sint0] forall self : int . forall other : int . inv'0 other /\ inv'0 self -> (forall result : bool . result = (self = other) -> result = (deep_model'0 self = deep_model'0 other)) end -module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 256 4 256 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 256 4 256 36 +module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 257 4 257 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 257 4 257 36 use prelude.prelude.Int @@ -27449,8 +27449,8 @@ module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#" goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self + rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 267 4 267 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 267 4 267 36 +module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 268 4 268 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 268 4 268 36 use prelude.prelude.Int @@ -27461,8 +27461,8 @@ module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [# goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self - rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 278 4 278 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 278 4 278 36 +module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 279 4 279 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 279 4 279 36 use prelude.prelude.Int @@ -27473,8 +27473,8 @@ module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#".. goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self * rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 289 4 289 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 289 4 289 36 +module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 290 4 290 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 290 4 290 36 use prelude.prelude.Int @@ -27485,8 +27485,8 @@ module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#" goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = div self rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 300 4 300 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 300 4 300 36 +module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 301 4 301 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 301 4 301 36 use prelude.prelude.Int From d944e6ecbc59dea231843e23153afd1dcb379612 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 21:36:07 +0100 Subject: [PATCH 8/8] Remove logic trait impl for machine integers --- creusot-contracts/src/logic/ops/arithmetic.rs | 67 ------------------ creusot/tests/should_succeed/bug/682.coma | 24 +++---- creusot/tests/should_succeed/bug/682.rs | 2 +- .../should_succeed/bug/682/why3session.xml | 4 +- .../should_succeed/bug/682/why3shapes.gz | Bin 247 -> 248 bytes creusot/tests/should_succeed/mc91.coma | 8 +-- creusot/tests/should_succeed/mc91.rs | 4 +- .../tests/should_succeed/mc91/why3session.xml | 2 +- .../tests/should_succeed/mc91/why3shapes.gz | Bin 217 -> 220 bytes 9 files changed, 16 insertions(+), 95 deletions(-) diff --git a/creusot-contracts/src/logic/ops/arithmetic.rs b/creusot-contracts/src/logic/ops/arithmetic.rs index 26de8149c..1b8cb0d0f 100644 --- a/creusot-contracts/src/logic/ops/arithmetic.rs +++ b/creusot-contracts/src/logic/ops/arithmetic.rs @@ -49,70 +49,3 @@ pub trait NegLogic { #[logic] fn neg(self) -> Self::Output; } - -macro_rules! logic_traits_impl { - ($($t:ty)*) => { - $( - impl AddLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn add(self, other: Self) -> Int { - pearlite! { self@ + other@ } - } - } - - impl SubLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn sub(self, other: Self) -> Int { - pearlite! { self@ - other@ } - } - } - - impl MulLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn mul(self, other: Self) -> Int { - pearlite! { self@ * other@ } - } - } - - impl DivLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn div(self, other: Self) -> Int { - pearlite! { self@ / other@ } - } - } - - impl RemLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn rem(self, other: Self) -> Int { - pearlite! { self@ % other@ } - } - } - - impl NegLogic for $t { - type Output = Int; - - #[logic] - #[open] - fn neg(self) -> Int { - -self.view() - } - } - )* - }; -} -logic_traits_impl! { i8 i16 i32 i64 u8 u16 u32 u64 isize usize } diff --git a/creusot/tests/should_succeed/bug/682.coma b/creusot/tests/should_succeed/bug/682.coma index 890d34a4c..af8a0b44a 100644 --- a/creusot/tests/should_succeed/bug/682.coma +++ b/creusot/tests/should_succeed/bug/682.coma @@ -1,16 +1,15 @@ module M_682__add_some [#"682.rs" 6 0 6 24] let%span s6820 = "682.rs" 7 10 7 11 - let%span s6821 = "682.rs" 4 11 4 35 + let%span s6821 = "682.rs" 4 11 4 33 let%span s6822 = "682.rs" 5 10 5 17 - let%span sarithmetic3 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42 - let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sresolve3 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt64 use prelude.prelude.Borrow predicate resolve'1 (self : borrowed uint64) = - [%#sresolve4] self.final = self.current + [%#sresolve3] self.final = self.current predicate resolve'0 (_1 : borrowed uint64) = resolve'1 _1 @@ -23,13 +22,10 @@ module M_682__add_some [#"682.rs" 6 0 6 24] use prelude.prelude.Int - function div'0 (self : uint64) (other : uint64) : int = - [%#sarithmetic3] div (UInt64.to_int self) (UInt64.to_int other) - meta "compute_max_steps" 1000000 let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6821] UInt64.to_int a.current - <= div'0 (v_MAX'0 : uint64) (2 : uint64)} + <= div (UInt64.to_int (v_MAX'0 : uint64)) 2} (! bb0 [ bb0 = s0 [ s0 = UInt64.add {a.current} {[%#s6820] (1 : uint64)} @@ -46,10 +42,9 @@ module M_682__foo [#"682.rs" 12 0 12 23] let%span s6821 = "682.rs" 15 18 15 27 let%span s6822 = "682.rs" 10 11 10 21 let%span s6823 = "682.rs" 11 10 11 17 - let%span s6824 = "682.rs" 4 11 4 35 + let%span s6824 = "682.rs" 4 11 4 33 let%span s6825 = "682.rs" 5 10 5 17 - let%span sarithmetic6 = "../../../../creusot-contracts/src/logic/ops/arithmetic.rs" 92 28 92 42 - let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sresolve6 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Borrow @@ -63,15 +58,12 @@ module M_682__foo [#"682.rs" 12 0 12 23] use prelude.prelude.Int - function div'0 (self : uint64) (other : uint64) : int = - [%#sarithmetic6] div (UInt64.to_int self) (UInt64.to_int other) - let rec add_some'0 (a:borrowed uint64) (return' (ret:()))= {[@expl:add_some requires] [%#s6824] UInt64.to_int a.current - <= div'0 (v_MAX'0 : uint64) (2 : uint64)} + <= div (UInt64.to_int (v_MAX'0 : uint64)) 2} any [ return' (result:())-> {[%#s6825] a.final > a.current} (! return' {result}) ] predicate resolve'1 (self : borrowed uint64) = - [%#sresolve7] self.final = self.current + [%#sresolve6] self.final = self.current predicate resolve'0 (_1 : borrowed uint64) = resolve'1 _1 diff --git a/creusot/tests/should_succeed/bug/682.rs b/creusot/tests/should_succeed/bug/682.rs index 722431d34..8d9cebb99 100644 --- a/creusot/tests/should_succeed/bug/682.rs +++ b/creusot/tests/should_succeed/bug/682.rs @@ -1,7 +1,7 @@ extern crate creusot_contracts; use creusot_contracts::*; -#[requires((*a)@ <= u64::MAX / 2u64)] +#[requires((*a)@ <= u64::MAX@ / 2)] #[ensures(^a > *a)] fn add_some(a: &mut u64) { *a += 1; diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml index f7e906ff8..58ad46e78 100644 --- a/creusot/tests/should_succeed/bug/682/why3session.xml +++ b/creusot/tests/should_succeed/bug/682/why3session.xml @@ -7,12 +7,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/682/why3shapes.gz b/creusot/tests/should_succeed/bug/682/why3shapes.gz index a2354c5dfccee9ed61b603363f16fbb40cc498c3..6f413f037656218a54a9dfc54b07cfb6c57bf265 100644 GIT binary patch literal 248 zcmV0(rH4D*-ZvvgG=ywQjkz(>f^r*a ydF2#Wf=P#tVTmQ>dq#v3%4wsakcCE8X~mUgAd6gRR~SwCJ}2KN{l;SZ0RRA=mvxu` literal 247 zcmVqggbi8{X_uf6M`0#;88u&zM@G(4d#aE9EUvZ4B4OBK1Yet9T_|^V2yQ4}qQyOsteF&5=(E0z3mu9~%-4p-vv>CN|&6rzTi-xEGkV2Od xopQSDwblyrH4qnDV4cRkL+PN;Md_f>g)yXEuD~jr8^gs`vTrP0g*x#80069%b({bI diff --git a/creusot/tests/should_succeed/mc91.coma b/creusot/tests/should_succeed/mc91.coma index 08e2b4715..b89a7f1a1 100644 --- a/creusot/tests/should_succeed/mc91.coma +++ b/creusot/tests/should_succeed/mc91.coma @@ -2,8 +2,7 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26] let%span smc910 = "mc91.rs" 8 11 8 14 let%span smc911 = "mc91.rs" 9 12 9 14 let%span smc912 = "mc91.rs" 11 22 11 24 - let%span smc913 = "mc91.rs" 5 10 6 39 - let%span sarithmetic4 = "../../../creusot-contracts/src/logic/ops/arithmetic.rs" 72 28 72 42 + let%span smc913 = "mc91.rs" 5 10 6 37 use prelude.prelude.UInt32 @@ -13,9 +12,6 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26] use prelude.prelude.UInt32 - function sub'0 (self : uint32) (other : uint32) : int = - [%#sarithmetic4] UInt32.to_int self - UInt32.to_int other - meta "compute_max_steps" 1000000 let rec mc91'0 (x:uint32) (return' (ret:uint32))= (! bb0 @@ -42,7 +38,7 @@ module M_mc91__mc91 [#"mc91.rs" 7 0 7 26] | & _7 : uint32 = any_l () ] [ return' (result:uint32)-> {[@expl:mc91 ensures] [%#smc913] x <= (100 : uint32) - -> result = (91 : uint32) /\ x > (100 : uint32) -> UInt32.to_int result = sub'0 x (10 : uint32)} + -> UInt32.to_int result = 91 /\ x > (100 : uint32) -> UInt32.to_int result = UInt32.to_int x - 10} (! return' {result}) ] end diff --git a/creusot/tests/should_succeed/mc91.rs b/creusot/tests/should_succeed/mc91.rs index e85f56bc7..da9fd7c1f 100644 --- a/creusot/tests/should_succeed/mc91.rs +++ b/creusot/tests/should_succeed/mc91.rs @@ -2,8 +2,8 @@ extern crate creusot_contracts; use creusot_contracts::*; -#[ensures(x <= 100u32 ==> result == 91u32 && - x > 100u32 ==> result@ == x - 10u32)] +#[ensures(x <= 100u32 ==> result@ == 91 && + x > 100u32 ==> result@ == x@ - 10)] pub fn mc91(x: u32) -> u32 { if x > 100 { x - 10 diff --git a/creusot/tests/should_succeed/mc91/why3session.xml b/creusot/tests/should_succeed/mc91/why3session.xml index 08f10d8e5..1d0902705 100644 --- a/creusot/tests/should_succeed/mc91/why3session.xml +++ b/creusot/tests/should_succeed/mc91/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/creusot/tests/should_succeed/mc91/why3shapes.gz b/creusot/tests/should_succeed/mc91/why3shapes.gz index 03f921796c28e75bf0edb2a96b8721b32e19d3b0..c1b9d98977a761b41d8064c30dd65b1acc351ca4 100644 GIT binary patch literal 220 zcmV<203-h&iwFP!00000|CN$m3xY5dhVS<)c3DQSxv3Z#cr)@oyp^L)5=zZ!(7zA* z&{-4e?i_gboO52bu&_EpBNe{NR+V+N!7jFz2mYFfd+ z7krUox^z2pIShBEb7~KGHkRJZ)z)pZq7j|X2&UMzMcs5&!qE2R1Qb*Za@@S<3O)e_ zkmEY_&s}EeiDXzeMcMX^w%&b?sbaXh_9pwsNiRkW88N~LFQdd;;X{Qx=?qgPs)V_k zyO$2faq)XMlWtMIz^f>UM{7nJxqPdXl9Jo)&DgpoiW4B~A