From 7210b30a2bfbe321ca8d4b71b751766e99250886 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Fri, 13 Oct 2023 14:24:43 +0200 Subject: [PATCH 1/8] Forbid use of borrowed variables in ghost code --- creusot/src/resolve.rs | 5 ++ .../src/translation/function/terminator.rs | 12 +++ creusot/src/translation/pearlite.rs | 83 +++++++++++++++++++ .../tests/should_fail/bug/borrowed_ghost.rs | 10 +++ .../should_fail/bug/borrowed_ghost.stderr | 10 +++ 5 files changed, 120 insertions(+) create mode 100644 creusot/tests/should_fail/bug/borrowed_ghost.rs create mode 100644 creusot/tests/should_fail/bug/borrowed_ghost.stderr diff --git a/creusot/src/resolve.rs b/creusot/src/resolve.rs index b73d9ad02f..d55ca34481 100644 --- a/creusot/src/resolve.rs +++ b/creusot/src/resolve.rs @@ -160,6 +160,11 @@ impl<'body, 'tcx> EagerResolver<'body, 'tcx> { self.dead_locals() } + pub fn frozen_locals_before(&mut self, loc: Location) -> BitSet { + ExtendedLocation::Start(loc).seek_to(&mut self.borrows); + self.frozen_locals() + } + pub fn resolved_locals_between_blocks( &mut self, from: BasicBlock, diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs index b712c5d628..e2afb22064 100644 --- a/creusot/src/translation/function/terminator.rs +++ b/creusot/src/translation/function/terminator.rs @@ -77,6 +77,18 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { let TyKind::Closure(def_id, _) = ty.kind() else { panic!() }; let mut assertion = self.assertions.remove(def_id).unwrap(); assertion.subst(&inv_subst(self.body, &self.locals, terminator.source_info)); + + if let Some(resolver) = &mut self.resolver { + let frozen = resolver.frozen_locals_before(location); + let free_vars = assertion.free_vars(); + for f in frozen.iter() { + if free_vars.contains(&self.locals[&f]) { + let msg = format!("Use of borrowed variable {}", self.locals[&f]); + self.ctx.crash_and_error(assertion.span, &msg); + } + } + } + self.emit_ghost_assign(*destination, assertion); self.emit_terminator(Terminator::Goto(target.unwrap())); return; diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index 24465cfe83..1e2c287a81 100644 --- a/creusot/src/translation/pearlite.rs +++ b/creusot/src/translation/pearlite.rs @@ -1355,4 +1355,87 @@ impl<'tcx> Term<'tcx> { TermKind::Assert { cond } => cond.subst_with_inner(bound, inv_subst), } } + + pub(crate) fn free_vars(&self) -> HashSet { + let mut free = HashSet::new(); + self.free(&HashSet::new(), &mut free); + free + } + + fn free(&self, bound: &HashSet, free: &mut HashSet) { + match &self.kind { + TermKind::Var(v) => { + if !bound.contains(v) { + free.insert(*v); + } + } + TermKind::Lit(_) => {} + TermKind::Item(_, _) => {} + TermKind::Binary { lhs, rhs, .. } => { + lhs.free(bound, free); + rhs.free(bound, free) + } + TermKind::Unary { arg, .. } => arg.free(bound, free), + TermKind::Forall { binder, body } => { + let mut bound = bound.clone(); + bound.insert(binder.0); + + body.free(&bound, free); + } + TermKind::Exists { binder, body } => { + let mut bound = bound.clone(); + bound.insert(binder.0); + + body.free(&bound, free); + } + TermKind::Call { fun, args, .. } => { + fun.free(bound, free); + for arg in args { + arg.free(bound, free); + } + } + TermKind::Constructor { fields, .. } => { + for field in fields { + field.free(bound, free); + } + } + TermKind::Tuple { fields } => { + for field in fields { + field.free(bound, free); + } + } + TermKind::Cur { term } => term.free(bound, free), + TermKind::Fin { term } => term.free(bound, free), + TermKind::Impl { lhs, rhs } => { + lhs.free(bound, free); + rhs.free(bound, free) + } + TermKind::Match { scrutinee, arms } => { + scrutinee.free(bound, free); + let mut bound = bound.clone(); + + for (pat, arm) in arms { + pat.binds(&mut bound); + arm.free(&bound, free); + } + } + TermKind::Let { pattern, arg, body } => { + arg.free(bound, free); + let mut bound = bound.clone(); + pattern.binds(&mut bound); + body.free(&bound, free); + } + TermKind::Projection { lhs, .. } => lhs.free(bound, free), + TermKind::Old { term } => term.free(bound, free), + TermKind::Closure { body } => { + body.free(&bound, free); + } + TermKind::Absurd => {} + TermKind::Reborrow { cur, fin } => { + cur.free(bound, free); + fin.free(bound, free) + } + TermKind::Assert { cond } => cond.free(bound, free), + } + } } diff --git a/creusot/tests/should_fail/bug/borrowed_ghost.rs b/creusot/tests/should_fail/bug/borrowed_ghost.rs new file mode 100644 index 0000000000..7dee17a169 --- /dev/null +++ b/creusot/tests/should_fail/bug/borrowed_ghost.rs @@ -0,0 +1,10 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +pub fn use_borrowed() { + let mut x = gh! { true }; + let r = &mut x; // x = ?, r = (gh true, x) + *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x) + // resolve r: x = gh (not (inner x)) + proof_assert! { x.inner() == !x.inner() } // UNSOUND! +} diff --git a/creusot/tests/should_fail/bug/borrowed_ghost.stderr b/creusot/tests/should_fail/bug/borrowed_ghost.stderr new file mode 100644 index 0000000000..bcd2ec41da --- /dev/null +++ b/creusot/tests/should_fail/bug/borrowed_ghost.stderr @@ -0,0 +1,10 @@ +error[creusot]: Use of borrowed variable x + --> borrowed_ghost.rs:7:10 + | +7 | *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x) + | ^^^^^^^^^^^^^^^^^^ + | + = note: this error originates in the macro `gh` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: aborting due to previous error + From 06ee1ccdcc9a1165814a7da4976e2a278583169b Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Fri, 13 Oct 2023 14:35:12 +0200 Subject: [PATCH 2/8] Update tests --- .../iterators/06_map_precond.mlcfg | 46 ++++---- .../iterators/06_map_precond.rs | 2 +- .../iterators/06_map_precond/why3session.xml | 102 +++++++++--------- .../iterators/06_map_precond/why3shapes.gz | Bin 8947 -> 8940 bytes 4 files changed, 72 insertions(+), 78 deletions(-) diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg index cdba4ef8c1..6b98910a19 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg +++ b/creusot/tests/should_succeed/iterators/06_map_precond.mlcfg @@ -3087,9 +3087,8 @@ module C06MapPrecond_Impl0_Next var produced : Ghost.ghost_ty (Seq.seq Item0.item); var r : b; var _12 : borrowed f; - var _15 : Ghost.ghost_ty (Seq.seq Item0.item); - var _18 : Ghost.ghost_ty (); - var _21 : Ghost.ghost_ty (Seq.seq Item0.item); + var _17 : Ghost.ghost_ty (); + var _20 : Ghost.ghost_ty (Seq.seq Item0.item); { goto BB0 } @@ -3110,8 +3109,8 @@ module C06MapPrecond_Impl0_Next BB2 { assert { [@expl:type invariant] Inv1.inv _3 }; assume { Resolve0.resolve _3 }; - _21 <- ([#"../06_map_precond.rs" 77 32 77 50] Ghost.new (Seq.empty )); - goto BB15 + _20 <- ([#"../06_map_precond.rs" 77 32 77 50] Ghost.new (Seq.empty )); + goto BB14 } BB3 { goto BB5 @@ -3139,57 +3138,52 @@ module C06MapPrecond_Impl0_Next _12 <- Borrow.borrow_mut (C06MapPrecond_Map_Type.map_func ( * self)); self <- { self with current = (let C06MapPrecond_Map_Type.C_Map a b c = * self in C06MapPrecond_Map_Type.C_Map a ( ^ _12) c) }; assume { Inv2.inv ( ^ _12) }; - _15 <- ([#"../06_map_precond.rs" 70 39 70 68] Ghost.new (Ghost.inner (C06MapPrecond_Map_Type.map_produced ( * self)))); + r <- ([#"../06_map_precond.rs" 70 24 70 53] CallMut0.call_mut _12 (v, C06MapPrecond_Map_Type.map_produced ( * self))); + _12 <- any borrowed f; + v <- any Item0.item; goto BB8 } BB8 { - r <- ([#"../06_map_precond.rs" 70 24 70 69] CallMut0.call_mut _12 (v, _15)); - _12 <- any borrowed f; - v <- any Item0.item; - _15 <- any Ghost.ghost_ty (Seq.seq Item0.item); goto BB9 } BB9 { - goto BB10 - } - BB10 { assert { [@expl:type invariant] Inv3.inv produced }; assume { Resolve1.resolve produced }; self <- { self with current = (let C06MapPrecond_Map_Type.C_Map a b c = * self in C06MapPrecond_Map_Type.C_Map a b produced) }; - _18 <- ([#"../06_map_precond.rs" 72 16 72 52] Ghost.new ()); - goto BB11 + _17 <- ([#"../06_map_precond.rs" 72 16 72 52] Ghost.new ()); + goto BB10 } - BB11 { - assume { Resolve2.resolve _18 }; + BB10 { + assume { Resolve2.resolve _17 }; assert { [@expl:type invariant] Inv4.inv self }; assume { Resolve3.resolve self }; _0 <- Core_Option_Option_Type.C_Some r; r <- any b; + goto BB11 + } + BB11 { goto BB12 } BB12 { goto BB13 } BB13 { - goto BB14 + goto BB15 } BB14 { - goto BB16 - } - BB15 { - self <- { self with current = (let C06MapPrecond_Map_Type.C_Map a b c = * self in C06MapPrecond_Map_Type.C_Map a b _21) }; - _21 <- any Ghost.ghost_ty (Seq.seq Item0.item); + self <- { self with current = (let C06MapPrecond_Map_Type.C_Map a b c = * self in C06MapPrecond_Map_Type.C_Map a b _20) }; + _20 <- any Ghost.ghost_ty (Seq.seq Item0.item); assert { [@expl:type invariant] Inv3.inv (C06MapPrecond_Map_Type.map_produced ( * self)) }; assume { Resolve1.resolve (C06MapPrecond_Map_Type.map_produced ( * self)) }; assert { [@expl:type invariant] Inv4.inv self }; assume { Resolve3.resolve self }; _0 <- Core_Option_Option_Type.C_None; + goto BB15 + } + BB15 { goto BB16 } BB16 { - goto BB17 - } - BB17 { return _0 } diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.rs b/creusot/tests/should_succeed/iterators/06_map_precond.rs index 195870007b..b4031c22d9 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond.rs +++ b/creusot/tests/should_succeed/iterators/06_map_precond.rs @@ -67,7 +67,7 @@ impl>) -> B> Iterator Some(v) => { proof_assert! { self.func.precondition((v, self.produced)) }; let produced = gh! { self.produced.push(v) }; - let r = (self.func)(v, gh! { self.produced.inner() }); // FIXME: Ghost should be Copy + let r = (self.func)(v, self.produced); self.produced = produced; gh! { Self::produces_one_invariant }; let _ = self; // Make sure self is not resolve until here. diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index aacc82b70b..77ba2b6ed3 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -2,7 +2,7 @@ - + @@ -40,25 +40,25 @@ - + - + - + - + - + @@ -67,25 +67,25 @@ - + - + - + - + - + - + - + @@ -94,7 +94,7 @@ - + @@ -109,7 +109,7 @@ - + @@ -140,25 +140,25 @@ - + - + - + - + - + @@ -167,37 +167,37 @@ - + - + - + - + - + - + - + - + - + @@ -234,7 +234,7 @@ - + @@ -266,28 +266,28 @@ - + - + - + - + - + - + - + @@ -299,39 +299,39 @@ - + - + - + - + - + - + - + - + - + @@ -341,23 +341,23 @@ - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz index 5b0249154f39b53b24caaab123930470ba138add..48584ee07cfa6403f112c80b072addbe0320d4ee 100644 GIT binary patch literal 8940 zcmVp?Iqw1LecK!Qe|#vrR$ zyFxtDjAhSy^Xu~+UaDB#)h*ehk-W(4Y`d#jyd09>IXoAV`Y%7ey8mbRCEdUJEq%Pd zxx4*uugt3-|Leu4U&GDqZ+muq5k98-yAQvm@Y7yhgYXrqiA26NY+WIq3(fh3d$(@k$J3d+ehXFFrGHAZAZIU@=@&ZJRL4^mK&eb#d1%ut z8URF_1!1rA|K5d5v|Glq)+5YS9XWkfGh?3jZ(dDzA7Ax@_Z}}7Tr98<%izleL~5A^ zz08z3oDjQrzlOtBD3!2!2{bRH+I>TrtEAgjF%UGv!DcLX%*^!`HxtUhjH)m+{StK? zxIV$tqLiqETpuX00b4BG$$J(!;02v|p=GrBeOJtOwfLU3dNv0`{M48M6E50>^C}bQ z)dpsPC!SfPgPqJ^RD?&-n6*AwB(@aYQdCQkJ$Q91-&I`LZPl1-eB9&drT&%RU2%!uc>#Xi!EU;5xP*MYS(RLB>=`G{jDt*%VVt;7 ziJI665tV7{MMt>*3ds@f7XcOG3F-7CO`McXrS`RKqQPo{=@>0`LPuh2wi?g=tkoWIXjX$PA6w)=?=Y{NFpnZFska}^c9 z_yvKrhVh(sOcMb#+~7Oh9OYgBzf|zoa5JNRNxfM&mg^=oZcD-8;_s)jA5^@OsoUfn zR>N14gphIEz1sIv(reYPlMF>eu?V*{>JQ$14Fen$EgZK_JjHy^LeW|7TxSKN9yEKv zv+K8~#~Qi%&fw=)EL6x{mcnpzV&Hyf_2-tsaPzLmURwk+u#QRTfY(#hWW?j?swHYe zo1^+iwAE_J{Pl>Y_tI>%O{rhqI2Gz!$M4PA{)5^+je)+wymFaCLDbeS(-~}!7I9Y( z2+dO>cuN3ZZMD9a_E_K}G55tDtr<<_v7Kdidi}XNTC+~r?1tLfnlAe-(`65!Vz&+W zCvNnNDQ~t0bOjE(vgXZWQGu+#9}c;_y>yFB4|-ju*UcuhX*2IuHvI+Yw(XQ`jP*N(dXc(0wI`Ev)5bK8)6lBUi8%^ptN z5zyQUX!h|yvrhpuOF;7r&_J)x^!gc5wgJtrfVROo1!(rGfmRiT4QHX*gx4vQ+p{9g zQK$N;roNt@YH~`g=GxM1`3kGOl(2U3dmC0y)7BBLC|}pYYNBSM8nFBdSgr?F$=Cra z&%lf<*CC6Vyj=b2%Jkr>b@t#wn|s9;a5?-UniZQT(p7LNwgQ(s?o*S2(0DdQev-G!3)JH;S7k> z3Pg%lK_$!3Ydmd2^@&>97!=jFkf&YF!`ncrRuK}lL`crSQ;8Kk)e4?!eqOo#MaQz= zGC@mCs?@Pc6S-=27?#z0vk{inWjDg*-gaSGeXw~!_3>V}M1lP}C@VLEvU1OPj>P7m zEPk;HUM^1rWmzflu7-g{i_W${C}&+bRkd9RvU||&K`mj}b%++lbXSXQfn3=KYl&b- zJ#&?oIXYWIxFyiL(P`TM(CugN-F^o9aIjXj2i=0Tss(Fx3)ZS93D&9-tX{OMGh8B)FtT!PH#2TDAc+FRnis@j6zYH*vD_&F7)TET-baoE9CZ6eA(iC$1*kI z>3#amW~;S{1GoCd*#7;&(nn49+WdmpV|q_k%MZc5IS%I$vN;eNF1%HamFKnt$vOXJ znfBg|yA(Xcy5B z{EdjedJJ2gXWX-Fd$mnpXFspIeqf(<@3t)JM+vv94e9teb9X)YXKc|2C*Plfj}bPa+lBMz~_z2!E<(&*Rx2PW(wc6An5&`)|Xu|6}m% z3D11NGrE;GUn)KW*Ec-#6`s%Waly0yMm$$dYzxN3MkmnwAcyI*0{Ty|{t4Fa4Xh_7 z^}sG&_Gljn`etm^Y)4MM*_xs8IqCd3#O(vc&W++ZS58$}&aYjq#co84d%4WsPi@54 zm|Ul38cXmYi-X6E-l3cK&(S*^J<8QL1VOSjXyDY^dnFFsn{Gp8J)8eT-r!nG>0x!ly2J2>+^dc722$zZ z<>g*?;f;J2GyATaD_t(<-OO^{%`TA+x5PhucPfotS2yno*L00zyvDz0T+^J_)q{)T zn(hL4oFBTTYf5uXbKZ{29UPG}o6#6kLLW66V{*{urkr0p5si_hL_6}SkI%}j<0$h< z)%n4-hvnR3Js{d2m|JS0BWQ}qnKh~(k9H6kX zBl~0ZsZaF~QK`Q?wydH(lnvyP&eY7L7BbtJ)^LwpC{g^f+r63d(mtE6YhBTMFzx!l z)FUg&kC310D?$A2MJYJ; z6P=kkDU(?}+jc1U9#ih!mMmu{MmrCn%X>#mK65d{Tdqzy_gTtdyEew{1gdO7O{rs)ig-ilv^>M|7!~o+Y+wx@u_yK za5dUB0xtWwBRkdg)u5~6Gl6%v>HWM29IS+pb{i{Uy}sabFT0hH&o>%$R~fYP;A&Y3 z^#g|v^B#iN`*ZQv7JjuyOPuM#v3UU2u~$=9%d*AjNi0##_ zUX;)lH{SLfwB^TlYumi9Ky(lNiSd4K!MnbgS|1`et&CaiG_cgI`Dz8PzUqaev#sA=~zi!#fS+dI8On>EId#S9T8cjY&Blww{H0cWZ%KZ!yq4OVNITUqjDJ zWfx5oP`W*sCaHAUg>b}F&~>v)dq!g>o%L9(KdRsf!DV{E)yUi2hO(&t2gXu!ydG=c zn@hr>Z6fL(2tJ2~e+=&z6&1gh^t`madH>(TFX2o0!owFq>6FSty!-g^?q6yA;phKT zv;0K$NO+zkf-uIyqbA4{sSo@ik>2F5Ts=zcPG5Z*=Rh*ywP{LlrIk zEqWJUTWqy%F%xm>^)fMH?hN%4P0{b)!aaVxXMJDGYgK;pmT3SV`d9|YlN^R{)r z>ZZSKQMfw8dqN#*_52q8GMqWZ-q-kux*n`2{Pwt-_DY2_8SpxL)zrf+Hm@N`tIIII zo$sr8h*kibi=*-1K%x#`O!#8YB2g1ppt>*i2#cb;I@)|e+0RXOGbM7_Y?C~Y``FTX zu!(BZAX|IWvB;8iIp?q4b>WMLs9|kP=)uqtb=77nY>SSsLGXPLg{J@xLSwB0K#CH6r0)bZKx z_iezg4kg`H*VDQ&RW3ra>sJ;d9}jva`<}`9rJ_;0IvUlh)3dYJP)zmK?5M*&sHTKX97>Yj$Xt$olBVNuoMm0cR`YKwMW^6a&Ic<|BeUD0XreaP-P%Sv?IjgbExwE&KI_o;A^ERj04SFr|!xpWRxVLM1Z6~RbsSZbeLVa>?$qk-Wc)Mx8ns(rj z=KEj}EuV{%@nCGOb4#onm*4L#J2$GxV9F`HAMwy}CS}hV@;x1UqjDyE@2$rddXaac z*!fJBY2w6|9c0M5yh2a9xEnr`Yl6U}MY)(LhT&GCo6F226Dj{6qP@tw=1zYFuBD28kgyhSl& zi(>E=#gI=D#gOx5WG?$kFUcoU5Se{Ai_m^|^o}mn%Bf<>b=?k>@T=x1T06Fzv-@MZ zxy59M4>$ie&1&M>YrZ%>bWcX-Wa?cSx*a{So!44X7@)EhrmGu>Jm{Kkw5-EgzU!eW zzUC9Y?}yryQcG3!0@yjBjj^wV>j)PIW9942M)Ru1XV>j~+ohnP%?Gcp*Y65<)lLn} zU_Smw8MpWE#&rAX=F`95zxi-?|M?@?Gpn&@d%odSX5?4SH;{H-<^6nOtIp``k?aGl z9d~vNX&2b{Au@EC2A$-D?3}J^aUj}Qbi#!7x6sbFeRkEB812C=xMdDHckgwLpPiBn zCc9@}lN0xhWN1EcUY+2b=Z%|ARusvwc7t=%g3k2>lFiZ1%N*Tg*X<@x_P5Gr*(==J zY-L7#!+|^Ct(^Zcyv65xZ-w0CE#A8e=@6P&$7=<-qOU>cdHl`M;~B6wH4E9^pYDLa zPkSBy(jNJcheHEc^i4tiEMfLp(uB{*BgGGt6E;o%69w~hypMOEZ^!$imkZyK@W1TZ z)2DdpcKDcn2C=O(qT#=Dq`NiS6S`S}Xctn*U~V_T9^Cz$m)K?0c`LkB+HQgFa<#K| z9S?OYpk8^+xye-7w(wPiRU-NmkU616_b9&6RpMIlzT!FLza)xw8K!9QIa>F!R5-ixxRX9On7r)p2;nV9J7CaJK>(#5&^$0zR&iI19CXglHSjUd0@ZCb`@xbO2{FUM7D=hOKgm#7HS}Ujg^I>dxeO-4RnzEsf zjzAyFq#W67+b{&}om;AsMq6r|+z1^chHm}OL z$RSG|7x{6|%IfX0EYi1wBA9O_*z*oLhLX(MI6hl*pLJh-HgCwLd;~$&%x1IpVAKyy z<>-E@P3>WM`L{d-@=+~5A`e|2xHORKR*$N?EA;c#|Nh}>J*)arb@Xd2{f&T4<>#>I ztmStmxLMSo)eeHZfxvgyKb%nMDWUT(9I5kNlFMq)N(X8?2Rcow^9ZO1_PW%IBwmwx zbVk>2cZxt=KhpK}k*=@Ty1woevRQY&EZX#SQz68x>yxf@EF*c-_3fdqZ}ZDX$jI4_ z7Tb0-?>$?hznntPV((Z+9-)iW!%N!t$^CWNl|X+cp@;(R2G(2yJm3B_FF&?Hm=L}G z3nap>m9QcwMcKM_Ir}o!x|?f%nPAo}R=V5#mp9xZCx_CN-@h4|@0&(0m;F0_F_)LW zhT*!u?Ba{}4AA50; z*kPS^BIj(yi!0hrcR=}kO*I5VMv*vK$90QTG#YvNVcrCs0O4}qS9|r%5 zs~wj+E_R&nINSN1+u5Dj>7Cli9a4AfVhp49(L2f5sFTuz_rcp3m1k3k!ab%AiMFFM zY)UK|7biaH(L2u>_tO-ueI?CK>YZde;djFAgxv|V6M84qPM{L86MQGwj{6;VJ8pN} z?6^k72~W+@t5d>=PP#Yf&8?<7^2cgl_ zpmW{g+v>J#kf3jJMmv#=oiIV;pu#kamXAvQp1Osa+z^@YBZQY2TpYMjQKe}T-f1_y zGJ5Axz1vCqwRJ0>1~1qM3r0!C+32jcCTL-#7Y1}w-QwHo)=s%mU`P_^_91#EBJ-0q zgAC5QiRw0LXXMU^o#8vfcG~Z>+iAPgz?6SWDFkekyyuFRr^zcUAx`rYGMO*WLe{4cFn-b*B@&aPh=cG9 z3%2E$|0z%U%Zv9ZLWpxKSyE;Qc%0%0b_zmC&aiA|GR2FNnYqQlS(!OEK9~=L?gsNCKmsH`Q^w+J_K%cO5S0z zLE&fzn_P6`AiXWa>UZ`#U?=GL!nz==GCBn;Pi};sG$oMhjVQv2eGinnX%Lv?XpAsU zC#ZRGuy|G;i$G$T@txc`v2!oa{xPM|aG#8`h8wG3j0q(sD_~w}Zt~LP%y&X8i!eW; zU_t;5gRx^Ap*7>n$P}TJHe%IxLazWqCo^yl&D1j3eo~JBE>JrGA!;66{T-1k)1V+~ zVSu=#9E{?GRUv6_#b8FRzC)5>p<3ofIq@_`*zBW#0XRA61450VXjjgDC&V(v2OWfm zLM;Us44Ty#y~Ii(LNdWOV!xNc9r(bLW^7;(Y7P>3lF0xLlY>3Y6L0i>M|enFIM196 zgSD{!8H|316~cR|^(3wO4oUW2L0zy`jvh8b^n)9N;!whbF>Vn26-PmiCOJbnhJuWq zH9iU-iI2dC+-7X&{m#3chgEKNUhlj*9G@{j)C*%_*eA(&bjjNQ(S-3~Qd@EvarBLo z8;*lo=AWcpIgJx+Gq05j$%zTdT+mRCT^d!KBromaL&HNwsVo)dLisPI9I7&4f^F-bQH#skwTs8Hx~&rcT?Lt;Ov6T=z}$r`=q8tRr7q>7h$)Xz^> zR1*&px>VF&4bo333T=ZH6X;aD(DnTM=oN>V;jAh(?H-Wu2#floSdDDiPL*??tb3DV4oafs3g*gM&jX9_$E%_A1_%uA6c)HE@!u?UPZ0e28;o`fF$ z;|lir3zH|I&|0hwnv?A)u^K>&l;Bqbt{B_s*_R?u2hWEDnZm%J6IT&5Cek4Jqy!k` zg~_wfJveMRYtv-XD5484Sx2IU4})OEz*E)8d*Zey37J2UmtB})bZQh9wylB0V8RRW zN4AYs+Kz)7Czga8luUkLlaC1;M@FQ2g+&VaQ9z?Xjb}~IR2mIxRHxCPMuQp+Y7nN7 zPa&V`Wg3hRc!1vU;t@+?h?Vcte? zIpl+f@*_}CP(e>06b6JjFbs1AA2j08h({wHjd(QT$S;L_4*4ANIplMMc1gJB4p~X8 zIApb+fbUH*lP3i_jgx>LCeTqBLkt|DqIo62RrrCA!bjpG@F5=<`{Sr`VKj0QHhCZ8 z0Fyfnb}-h3FkuQt|4M-O1^8Zo|I4?1UJA_!$uP1g2OF3&gI7TWY2%b2tK3j2#3Tzy zYb-$ckn51YEY(;FjiV?g%((<0x*<-3HIf5sP`Xp48dL$H-yQV9xP_2i-@AFZICfKu*WhFU%f1C_|eaeyKxSR5gT1=QdXS~`Hpjw zMm9KDWduW*lrb@%pxjt2uR7{!GKKp|bvD#P^Pks43Dp78K?^&LmLxK?Sfzy)JXyol zRC);QS13@UK#igvgJS9avwP0KlmdDx(=gvgCX(dnK2oCLW*qD*p(p~U%G&dyC`QH13BqfJdQ73qmOrX#quAkRna<21Qyxkrq&-1r%waDd>v4 zP^1MEX)pmkd|p~DG;pUpQ*5#(=>c2<>1SazLY!+fgQ{TD2t(mpvx-ZMQH)%1ouJ!b zji$}KlQNJeuuRk_UkUU^pc!E)`it_g1q5sXbXdR~5M(}~(*h=xu=EZ1YB9iMjuK|F z4Fj23&ZFCrwgbxu_+q4l;}@gwV~hzcF(<}JVFH{UkjkOzN&^#@(?);PiqRL2BG4cL zqc1S}P|opDGZn%SCDb>f!BgNzCupM(kH!s9m9&zBW5HwUoGJ@|r?@tKqbf|ez=XrJ z#^+m_l#`x2fXm=w_6fFl9M%d;tp;63) zBlSBsB^i67<}}RGF#6<_v~*NuNJ))K4FX1zai;Z5K4Fu|jKO&sy_af$7?e)L0oIsD z`ZU!AToMC6X|py$advDJV^AuNewZefH0(hx0T5MIRS5|z88s_@XLEx#T%t!NvMDMX z0&wF!QknKC#F&+0nVa+F}7ooCBuCGAgl*!j!@XbfYB+nIp-F>O=*Hji?P2 zGaltAC+1+&cq5XL!eN^89!N>2edxFkmT$}gKBy1Nx5V--#Vm<(^%N0o4wk_~e^5{s zBJ_1gRXUBJz?E2^f)k-sEx)B|#k5k4A<4iHk50<~Hn5t*Rvf&oRI6{P`u_o#o0z6< Gpa1|lRItqe literal 8947 zcmVp?Iqw1LecK!QS^#voa& zT_GN6Mv}eW{Q7*nRk6COTe3%%yvXcMyQ^8e9FpHTJQtGsFF&8(|I_^z@6SKSyZh_g zoBwvM&VT-|XAi%->zmI5xjJ)q@&5MX=jeVJ#HIV~_WmK<-i+4|$ot{fPY;6_*uXE{ zh5H$g^fDErgLwD*Ue?>25C@v_zE4@&_rUTOA1GS-baNB$9|k$-n%KTo{g&@r9+lqB z`PEX`45nr_b0SEyAm7%ODJ@M?^1e`u7l-|_c#o`Cbtup`)}HA=d3#260uB9kcRPLx z@qVDv{pBwMRRc8xEiKCSkP=&pZYipzpmR$tx|Q!L&b8{kF-Bbc^|yzA<*HMEQG4o5uj-#jN{ZpMLuoF;~Rh#DBT_o7<3j$JD@) zNVkTqD@1dlIX^S+*Dd^fJagA?CQ7^MpVBPI8Q3!YOy-*Ec=7@$k;y9$ZJJpF0Bf_r z^i}@fdv}3$%UITWn7XVZCogMe%=7T}e7e0m?+5P#UM{#;V8NEb=L?9$G7WN>DYZW# zdN9Ac{Z>+H!s-RkypXDghB8x0*R5h8XoiE%Snima$}MhAC<8N!!qDj#tK&fB5uRqH zL>=V%kP;iP*}|Q)XMsIlkeL@+MxEbx#dKGT?OCg5b1=j&jTtcEtW7wrG9kU%z%1}Y zGmCVv;~9)1;gL0Ftq&TBEk(8z(NcI1UfIfb6&H3}HD($gw>e}S zrNuM0bJ-Bn1_Rl;`tz{zHmsSRHjMo0@*1r1OU>;5y2=%3S7Tk0aDn<4GDRj+)G|oQG-5c!)#Y4OD!J}QmJ6J{OL;cO>&Q4_>@H`-&X~#R-LJl7 zdf2i?>btGcUmnj^09%-ZB3G^`gRmv0Rw`f$kAp2}C#Orc4|j3;SOwt%=cBxZ^(EEz zrt89Ht_BKvz+36vnzw37<1J3gijg_9!4{~eb~a0PdVma z;RukzkRDPjgq2@4kcU|=-EO#&MOIRh#BR|6d`s~) z#fO#>PKvT{AeSHR+|7N3COUJUAd|)UhisL0ps8=WpXk6gY~7sso3T4rQ2~r!5Ljy% z&uND=C4jnXe7oy|+za5B3jXS@XVfpL*Xzb|-3g7`QZStT{aE(BidQmqo1Fb>=t`0# zWE^&{_WhXjTJ`HFL#3fugxebRd+)x60rrX(j$0=lW4;%m=p=Wpvw~6gn%(2s_1oiP zja+?a@bfDcD&#Ipp}RgZaDTA+Q_G;ce&1uSErJnUn7;^}nN61AbtQT-lm zwHh*iJ)!A=tBtl(>Q^_O3iYky_vUPWr?!t{pl>j*Txwqswe?GN2HTTG+~p%e^Oy+U z62O;Rtq)uu3VbByzUYHBqp3W)v+RzqKbHq<))AXsrM9-FOMlCB={>0EZ3F(98$Dsl ztE~ZDfkUsXdG%COAnPB8LvC;2X0ho(ugUb9*@RYY=FQ5c-#~jY>(#qIC;R`S$v)!4 zc~q<2bmVMk&6khr-Syn@OWl9E*G{GRGkcIT+mL&frcMA&?@!zT(98;G z`sqN^&jB=@fMyq>`w_)`>Z5`k$b8Kkqdb0NB;nF({&MAx}G>hqr-LtRf_0iIALtr(i31iWNM?{Je7evyNrIWrCKP zM5$wy#&XqSKP)Q;wGoz;WjDgbpu4cF+}pe$`gpHdqQG_?l;xX2Sw2vjBe6Lsi(jOI zm+~V)SyD>8uVG-;qO&a!N=X+^6>S#+?;d1(5K9<#9il}s+0~+3AeZ;S+C;EPJu{V- zIXYWIxFyiL(do4Rq1(@3yZsFM@nEfJ53&VoMGMx-7OWM|608*^Si7Ky*^Eunf{7J% z^Tro8C()KfS`zEFe9#=+EOqp?m-y7GNpMMxf{D3uv1|iqUR--L;&rG#Z|3TB={(bG ze$FwqmH6!=UTThbsoAG|A3sjj#rpaB9>vD_&8N^}7E|$IPKypyiX|b_C$2$mT$7xbRjvR-W4qB&YnBW!if; z?o#lS%k;Z9yjNKrt|t++HYNLtPurBINouC-0Zm72+83ed(Bj>O&w=%O(2FfI_!|*_ z`4qM~&A2Do_HvuP&VF8Zea}AY-fdabPZDmI8`AM<=I(m(PuQZ5PQE<`$EVrC&q&BA z6mD6_N5Oa0RDL?<)>iYgLG4+L=p!&n*7Tq7`4c{W06s@NeP5yPZ8`o<>)x9p^SDZS zxuMe@!MshQ(tGXFV0{I`@+77r+XxqA8{yB@>}fpP{fR${=Y)d}&-UB!Y`+hlZNf8M z@QiNd&6k4Cz_ks}bcN?rd|dEszY)(>6WfAuVxuGIeU!uGNdf&QSpNj;j|SEwle%Y@ zE_<~11bs8MYPJI>-)zmK@j2@J*vIW7#ZHalDOXNaSWd59t;KFci+j1u-Y;#$*O*+V zW*STIA&Y~jjNZPR_s`MWAH9^TZwP{9YtX={wfBPUxi`&*%6c;Yk;oNf+>w#W!j)~t zu6p8YOZkN$b&Le7VY;3N!9tm zw1?%~V?7|+ADCNeNk`g9JN-ubXbhw2h#c)st6g_z%l8#aK zv5S9|h_UcJ){*?OFZuh$ym6!t*dUj;r zRiFA)4-u96%VW#R+C$ku&eNHinbbmNJJag!kqae?Uv|4UbKbPirt4Z)^d3yRJ}~vf zN^+#L9;RL7T@SDmU@V!-th1{`R6NIQC0A zGjmiXlX|voU+_Jp-1{wAPL7Or9zc`#j;MU*Vum+gopSE8l)*M_jN1uR-h!H3rorA^ zQcjVPV))5HkbNTCWUR7eGDMqdLE8gqWY}_$y8IALgXB%QW%K#Jwh)mm;W{6mYR3v! zqg^B5ypKDQV_jbjx;Q)&czY8+%!|O@N(gDUu@ctn3oZuUt%P*G(V)A^pq&R7%StF8 zIdqu!5WE>q#a~F0a(XgRb7JBdU@O0sFKffle|La<&6!t?KNQAt6RM& zp)GE-?Kx=6kL}jBd0zqR9{LmG{oaE2eKD~KA=aZh@+(c^mA z!V)iM-Ld&)*MaSBQAnYBepOcjtfv+5X?+zX1I-r()Z8rZA(*cQm=z?N*2%ri1!+yS zCG_98zir>(ZTrUlod$fpfM&_Gca4H6I|us4IG+z&&qBSswLq-57|5Qb(td&8UC&Ep z7flmTvOTCKsbtxOaKKd1b+bx)LSs%k>!DbGQo$pFOZ9@Qk+-=GWl{h4jHTvyJ=DH8 zmxO)Wgw;I|bPf&w>^>|iDt;~Ld1-t5;lI1z+!yzSx-TrHr&Q|v?cLq&zvB4Qum7iJ z`6bnpbGhmI#(i9L7@ptNJra26hx6>M3%9?bqsibz1#dt69h18BBvaQ}D5WlB`=7VJ z#=(8yr8_)7UEtqZ!`Z{Xe~agxoUQVQwv4RY{E>mUbeFdNa`y$jk*&jQqr)Xns%YtN z(Yxr{VykttnTTVrmx*C>XHq}WRQmnd-Q&jx()YEz7Uef>3Af9r&{fyzUJ!mZZ(H}P zZu)tP!qpkxBkEAA=d=4uIB|--uki_WJz9_Z{Ir?|A>4@!c%8j!;_()n*Dy(|3pc-= z@2h!?Rsfr_gYn-$qI6%B`=U=GQ6{cHbzk%W7Fl_f0Yc01-J_(jgDo1V(isvcU+s%r zVK!9OFAuGq{R*lXgVfe`#}!Lb8wJ*SXxtYI=|b8t@U3CUndUw%BT;)_HY#Ll$lNMV zFM8JFXVclIo4e@3Kb`*=&wsnUhWvQ@_HC+zRPl1TFjYmvQUSd@$>%liv3ExW>>#ju z=skH;$7dLZHei?g!tJu_Y2Ay;7dhGWD@%^My`J&DXMBDs(x_b?jOyj_*%>5sQMolc zV!sdK@(>c2d#Fh*-MQPkjp24{>+=EhZZDt01mdz|o7N$*)gfB)43a-SBcSEB=(hOY zXZxIGB|>g<621nh@x}3#1e2WA^jls9kSvGukacOWG@w-w&Fc8fj!uTMjneaUr zf-jD*Bv8z}c|$dUV#?+XWL;jNcU=SzZx)Gyw|^^so1E=$+ntv5s1!+ZbRNU4ax;7s zYw$@==o@ROQS{xrMSf(QU8LHI0KxC}c76w1*}EBytmi_Sme~Utk`fmgVv;vIXDiIu zD&sjhx3Fm=;pHIgAW3rzCHt~>j_56v>2%hkOtK!z`UGfhyG2CGTTRRIy@X8q>ndkI z$>K1n-^=}XHou&U^d6P@Ob08`i^UhhvWur(lUJN9?N&aK-)uX7inC?D(NHcfEUK1h z4%JIIhnmM?I5tNk-lY5aPQ-B9Wp#`k#&GPuhl{Q+tE0BXaBSyj>2JV%EOx=$18uPj z-eMQD#V+`>#4h-J1)0en(u?GYDIz6%ZWf{a{@`7@Mk}YXCD&CuMnW%}duZ*>ZZ7V- zczuJ(b|0_*Z=5y7wXb|}cgUWM&b8D#GGse&qB~!;NY4MtR+z4CAo8HgbdO~n*79AC zO3^i+(4ik{RZ1;Y)oWkpgf_;u7Oo>)+=`X2GaJpT8l4@s^BtEg4Q)Pdb+vw1xT|(5 z5QX{pA7$J=ydUGu!}Y_zKfL{Td;jS!nKY}hCj;H^C6nY$&i9UXzT{y(r&VWk_CxmJ z)s8zmhSUq}`@k5woCZC~3EsI{*W!S+vFL;e>F=JM@A&MhEs@#1yKl=JbWYx@8Z|p6 z8B})4zDcgz6Oy5MzG-!Rcm6i2I$2R9!`k^xRSPxOb4NPII4^QclU%j?JIUWFn`K{c zZ?=^gu?+`ikGFFEr|=e?Z@XoDlecK^Buq!o*g8tfk^}k*be_iF95bE)dtI|6^ZVfz z_qWJ%*bArEIirJS%}`kyG6r{jaa{d6E8eJu(74Iva1N}=PYgb^h7L`luUX}{S z*e=KN^McGzupMJ+By0Li=`t|L6Rx`&)fWE~d zTkh9Q+S8jJmU$;$j&B57w2b+x17=ze?A2ayJD1R{HGNf=izS?oM^;BM9z^f^{RR8p zy0?!&df9i-IljN8hCNl`2#H$uW~T(KxnO3uTs}z^b{-lY1wpD!Jky|Iy7+o ztwnRQ*Nb}J_G!SN>$l%s=jW1|FBJQdj@*4|9FkscK(7?~5-8ooWeU0lN>^7kukK}D z9q!es0Bi9|W)c%LA-dc?tuNa{UdPgX)bl!~+B%jQ>R=tK*O{{%vOK&5{weDilQaI< z<~qiDFHgNGzM!uOWKK8Mv4bgmzfgKOu=(76W%&8x%DnTSU0k`=%2WRN2sXdEs{0L9 z*~XU+J|D`Y9M5c^b^7BB->TR(srf&m9FyBQm&<;8(C8@O`e6r>~>rj0*Z<9^=1cIucgv{E5 z59-|`UfC$;#5Jn727rGZ?xcv9V6pF#$WM#wF#q7&i>u#p~J%U-cSm|!_-`g;YoD8Kae|!rv9hyeYmt8w{ zF_)LWfnmD8=VFWPdY$6{zqCEPcup6rv>iN@KL+WtPw7pP11BKe7A2ta0MgiXG)U%663QDB0Pa+3B6y$(`8o9a4AXY;>cv-WpEGD5H?UT4%NQ!jj2(W}Z?9 zN84T~GDYH*@e`foXpNvPz*&Q=Grgu#3nA|b3W2l7f7~L_lqjpEl zj_Ms%J1S9e1XbQdZ`GtGq4g-Wg{Ghx_oL=Co^!tApo4xx-QEyAfYW7Mqlhqc zvfPO&vS}jIG^v=$G_Ovk&_qaLgp=M_$Z7|kCu5Xaj1c`YWHRlmlgTI8=T2$qpe13R zG3gW4lTr?g6(b^%sb3$PB5*TOt*i-TY zqZ7d>ttJ`AM5cNDNe{x)i5fi$$)mMYq~&R{0!xUIG`dXY>$8xy(K(DCH%hQb_{e-< zmSDlw6!SmjNq>FuK6wansyT^51&7DUk62Vf`Y`Ai$fv`{iSEKg>Ho-{>}YZWWPiTntZnkg_$vR8^J zBO}y2A2gnY#Uc<%W_-hUhV9Jjv%imVRMbXgw4zE27-LMZNi&#NlB&Ek8TEq@OFYaE z&j@2cLr{A3BeZ6GDIPtP(nhTKLFi>b=%fO*&`dRf?Z@Q^-~zQ15F+Nml|K;4JO%+# z3j@SNVPF(TtO`+D&4L=K_yI|Vg{p}e`9$OBVY8162H<3%4=^#hqFovNgAhvu4bm|S zg_<+U2sEqFTaJ~2xu~3N#QrFQ8)%?W5)uf6nt=qKcvOJHWMEIzNE^LB5FR3B#uCF_ z&>Gf1fzfZULRibCoVXT0Aj#GWs0&*2(ZWXXHki=~3MGswWdft;6a^`oqy*&%3X=3J z@e%lNd>B5-ZANz1?yT8aSmkPG<<5%z@fjUNJyRNnedL6C6Rma-O&A}-rA{s*ioVh0 zhNGaC*k@^%PvZpJ%t|3#G;D%0=OmP46G!1EPD{J^q~S?LQ`uCQCR$Kiat>zi;PcWo z5~`#h0hj2F;7~512sy{1R})Y_)xl>kPFM((Off=2IGDCX1;xOKHVHR{1tk>15}sa| zFg0=LV34+x3ySyvzM_*JVK4we#OgX?^u-BFHgyn`PrxzQ#yYSM)~)o1Of11NmRO&P zmme?>>EjHT%tWdu6F8nA@u6nv;AG4`G|FBcVGxP1?YV<-1@Q=D#W=6M;n~Xr@E5vX zo+VX~la|yN<;O{SNd$307)wn$uwwI)Ug&sPx+K;@VZn0I3l4&aa{*LRD_KZB@iJcG z#pxnqlvCg#j>Otgg^Bav1v6Sp?OD*TMb{{SaOu4@6Xh^}G<0>Ng(ezm5VP47!i$&Z zM@j;yu#SxwGMK*e{;3JNpDNGrq0J=I}?i5R0MIWpl*p$kQziRqUY zV_eb+;>$yhk)&YB$!kfV<~z=@uot%EXpg--3ygYB=qoq zDqyd_GI<;dt;X6QX|f$TRs(2}9Q>-l6=NGc{aWNnXK9F#DFh5UQQ<*jOd2Ge1OtP- zGI<)h2Zb%Cb(~ZjnK#ZvZIWoAAuv)5JW-9jXKs7qkoi;cvNIJ%BSxlS+bT#5!YpIo zvu&)>dJJNmNMt4m9&I3#^${GGj7V{gMGE;*K%zm3XPKT;X*4KNokW8Y4N5d9L6|^3 zfqbHqJIqWLRYnP&gpNq7hW0 zQHe$+8kHziqEJafoq6Kb>{2{^sb`2#+DTcKQqAcM)I>I>fSR;7e zo`XTaM|@X0Ap4C?`*$?A!cQ8?8B|%IZKR&@u|Qm_7okPzs9@~62vL>HTq~Fsqo9-0 zE`agQ849yh7yza~Fa?AuFbs1AA2edoh(#k7jacL}$uEU`2Kfx~8RRnw?L6V08e~mk z#UQJ;3HVk;HQA&<$8loN!x%aWV~BtwgjeSbT!kO_2z)p`44>o!`;Jr@H!40c9j)~~ zz~qiW2c?a36Q*Fa=M22h!1oONU%vIrQm95qhLLz4v?D@c<{Wce`zb*{}SA zP;Kd$w(v!#LJG|CDTp}o03oQ&G{q_pcyfk=A{ZA83Oq|26O+F@In0yCJh{x1&-_R0 z9Tq?@Ckdm;gMkCM07d|CPn@D`)V}sk{^$0POj;|8Ih!Um3d6Nd@M8iJRR-ubwTJ)V zy@btXr;&_0NN9=A z*fxrmUP2>g(1@7;MFJFw)N}iv-+RpF$e_Ct36pLlEOLrP3MpPuH3rPF0OdlK_2^aS zDU6dcf}4>j{O7GBIsk_dE7I}FCXEsth>!mM#Ap%)mi0h2z@of>f(gAYOpbzGr00bg z`*H+1L(Sx&aWE1ibT>YZ2AG~OeKy2^6$J`5gM!TxTA^UGq+q9cgObglU^6J#3<@@b zg3V+K#v(5iYz76JB?Y@Kw;Ecx5tazZKow<>$b=rklJsVh=M1(EgRR40>#$_&bZYqM z*+>PI5&90+?XMq{uXgzzi_V0F?Hb3TB#Rn`p2p7$hS!RIgGL8tRi2JQ(6Erp}167+}(wP4VvZ zjA}6H43iF%`x~0%lboE;%oz@yhs4Rke4%dSae|T-$_mR#I>=!EU{jD{X~!d$I>`fZ zBkXk_(I{rZB$d22MW3lT2~*XLHiFT0I=&KOgsCP1gW;r%s=5Q3c)lj18lAD+Tgyd& z803ce01M3`eVQg$d&r)-S?!@r8#1!d3E@W@rinxe8`>ZH)7#}=0YwzrdL Date: Fri, 13 Oct 2023 17:04:24 +0200 Subject: [PATCH 3/8] Cleanup --- .../src/translation/function/terminator.rs | 26 +++++----- creusot/src/translation/pearlite.rs | 50 +++++++++---------- 2 files changed, 39 insertions(+), 37 deletions(-) diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs index e2afb22064..763d498c85 100644 --- a/creusot/src/translation/function/terminator.rs +++ b/creusot/src/translation/function/terminator.rs @@ -77,18 +77,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { let TyKind::Closure(def_id, _) = ty.kind() else { panic!() }; let mut assertion = self.assertions.remove(def_id).unwrap(); assertion.subst(&inv_subst(self.body, &self.locals, terminator.source_info)); - - if let Some(resolver) = &mut self.resolver { - let frozen = resolver.frozen_locals_before(location); - let free_vars = assertion.free_vars(); - for f in frozen.iter() { - if free_vars.contains(&self.locals[&f]) { - let msg = format!("Use of borrowed variable {}", self.locals[&f]); - self.ctx.crash_and_error(assertion.span, &msg); - } - } - } - + self.check_ghost_term(&assertion, location); self.emit_ghost_assign(*destination, assertion); self.emit_terminator(Terminator::Goto(target.unwrap())); return; @@ -191,6 +180,19 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { _ => unreachable!("Resume assertions"), } } + + fn check_ghost_term(&mut self, term: &Term<'tcx>, location: Location) { + if let Some(resolver) = &mut self.resolver { + let frozen = resolver.frozen_locals_before(location); + let free_vars = term.free_vars(); + for f in frozen.iter() { + if free_vars.contains(&self.locals[&f]) { + let msg = format!("Use of borrowed variable {}", self.locals[&f]); + self.ctx.crash_and_error(term.span, &msg); + } + } + } + } } pub(crate) fn resolve_function<'tcx>( diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index 1e2c287a81..e6275cc4ef 100644 --- a/creusot/src/translation/pearlite.rs +++ b/creusot/src/translation/pearlite.rs @@ -1358,11 +1358,11 @@ impl<'tcx> Term<'tcx> { pub(crate) fn free_vars(&self) -> HashSet { let mut free = HashSet::new(); - self.free(&HashSet::new(), &mut free); + self.free_vars_inner(&HashSet::new(), &mut free); free } - fn free(&self, bound: &HashSet, free: &mut HashSet) { + fn free_vars_inner(&self, bound: &HashSet, free: &mut HashSet) { match &self.kind { TermKind::Var(v) => { if !bound.contains(v) { @@ -1372,70 +1372,70 @@ impl<'tcx> Term<'tcx> { TermKind::Lit(_) => {} TermKind::Item(_, _) => {} TermKind::Binary { lhs, rhs, .. } => { - lhs.free(bound, free); - rhs.free(bound, free) + lhs.free_vars_inner(bound, free); + rhs.free_vars_inner(bound, free) } - TermKind::Unary { arg, .. } => arg.free(bound, free), + TermKind::Unary { arg, .. } => arg.free_vars_inner(bound, free), TermKind::Forall { binder, body } => { let mut bound = bound.clone(); bound.insert(binder.0); - body.free(&bound, free); + body.free_vars_inner(&bound, free); } TermKind::Exists { binder, body } => { let mut bound = bound.clone(); bound.insert(binder.0); - body.free(&bound, free); + body.free_vars_inner(&bound, free); } TermKind::Call { fun, args, .. } => { - fun.free(bound, free); + fun.free_vars_inner(bound, free); for arg in args { - arg.free(bound, free); + arg.free_vars_inner(bound, free); } } TermKind::Constructor { fields, .. } => { for field in fields { - field.free(bound, free); + field.free_vars_inner(bound, free); } } TermKind::Tuple { fields } => { for field in fields { - field.free(bound, free); + field.free_vars_inner(bound, free); } } - TermKind::Cur { term } => term.free(bound, free), - TermKind::Fin { term } => term.free(bound, free), + TermKind::Cur { term } => term.free_vars_inner(bound, free), + TermKind::Fin { term } => term.free_vars_inner(bound, free), TermKind::Impl { lhs, rhs } => { - lhs.free(bound, free); - rhs.free(bound, free) + lhs.free_vars_inner(bound, free); + rhs.free_vars_inner(bound, free) } TermKind::Match { scrutinee, arms } => { - scrutinee.free(bound, free); + scrutinee.free_vars_inner(bound, free); let mut bound = bound.clone(); for (pat, arm) in arms { pat.binds(&mut bound); - arm.free(&bound, free); + arm.free_vars_inner(&bound, free); } } TermKind::Let { pattern, arg, body } => { - arg.free(bound, free); + arg.free_vars_inner(bound, free); let mut bound = bound.clone(); pattern.binds(&mut bound); - body.free(&bound, free); + body.free_vars_inner(&bound, free); } - TermKind::Projection { lhs, .. } => lhs.free(bound, free), - TermKind::Old { term } => term.free(bound, free), + TermKind::Projection { lhs, .. } => lhs.free_vars_inner(bound, free), + TermKind::Old { term } => term.free_vars_inner(bound, free), TermKind::Closure { body } => { - body.free(&bound, free); + body.free_vars_inner(&bound, free); } TermKind::Absurd => {} TermKind::Reborrow { cur, fin } => { - cur.free(bound, free); - fin.free(bound, free) + cur.free_vars_inner(bound, free); + fin.free_vars_inner(bound, free) } - TermKind::Assert { cond } => cond.free(bound, free), + TermKind::Assert { cond } => cond.free_vars_inner(bound, free), } } } From 6c7f62b54ba89ae28b660f7952dc83a64df896b9 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Fri, 13 Oct 2023 17:09:44 +0200 Subject: [PATCH 4/8] Fix prover version --- .../should_succeed/iterators/06_map_precond/why3session.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index 77ba2b6ed3..ff670a8aba 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -2,7 +2,7 @@ - + From fc06797d1a7f68eef82329f2f034e9ac157fb711 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Mon, 16 Oct 2023 16:42:14 +0200 Subject: [PATCH 5/8] Also deny borrowed variables in proof_assert --- creusot/src/translation/function.rs | 15 +- creusot/src/translation/function/statement.rs | 1 + .../src/translation/function/terminator.rs | 13 - creusot/tests/should_succeed/hillel.mlcfg | 629 +++++++++--------- creusot/tests/should_succeed/hillel.rs | 3 +- .../should_succeed/hillel/why3session.xml | 113 ++-- .../tests/should_succeed/hillel/why3shapes.gz | Bin 7117 -> 7185 bytes 7 files changed, 398 insertions(+), 376 deletions(-) diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs index ce4684d309..ee1f5149aa 100644 --- a/creusot/src/translation/function.rs +++ b/creusot/src/translation/function.rs @@ -24,7 +24,7 @@ use rustc_hir::def_id::DefId; use rustc_index::bit_set::BitSet; use rustc_middle::{ - mir::{self, traversal::reverse_postorder, BasicBlock, Body, Local, Operand, Place}, + mir::{self, traversal::reverse_postorder, BasicBlock, Body, Local, Location, Operand, Place}, ty::{ subst::{GenericArg, SubstsRef}, ClosureKind::*, @@ -334,6 +334,19 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> { .collect(); fmir::Place { local: self.locals[&_pl.local], projection } } + + fn check_ghost_term(&mut self, term: &Term<'tcx>, location: Location) { + if let Some(resolver) = &mut self.resolver { + let frozen = resolver.frozen_locals_before(location); + let free_vars = term.free_vars(); + for f in frozen.iter() { + if free_vars.contains(&self.locals[&f]) { + let msg = format!("Use of borrowed variable {}", self.locals[&f]); + self.ctx.crash_and_error(term.span, &msg); + } + } + } + } } fn translate_vars<'tcx>( diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs index 7805a06702..849054a5f1 100644 --- a/creusot/src/translation/function/statement.rs +++ b/creusot/src/translation/function/statement.rs @@ -130,6 +130,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { .remove(def_id) .expect("Could not find body of assertion"); assertion.subst(&inv_subst(&self.body, &self.locals, si)); + self.check_ghost_term(&assertion, loc); self.emit_statement(fmir::Statement::Assertion { cond: assertion, msg: "assertion".to_owned(), diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs index 763d498c85..bc6694bfc7 100644 --- a/creusot/src/translation/function/terminator.rs +++ b/creusot/src/translation/function/terminator.rs @@ -180,19 +180,6 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { _ => unreachable!("Resume assertions"), } } - - fn check_ghost_term(&mut self, term: &Term<'tcx>, location: Location) { - if let Some(resolver) = &mut self.resolver { - let frozen = resolver.frozen_locals_before(location); - let free_vars = term.free_vars(); - for f in frozen.iter() { - if free_vars.contains(&self.locals[&f]) { - let msg = format!("Use of borrowed variable {}", self.locals[&f]); - self.ctx.crash_and_error(term.span, &msg); - } - } - } - } } pub(crate) fn resolve_function<'tcx>( diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg index 1a9fe3fd08..ac163b64e3 100644 --- a/creusot/tests/should_succeed/hillel.mlcfg +++ b/creusot/tests/should_succeed/hillel.mlcfg @@ -1927,27 +1927,27 @@ module Hillel_InsertUnique type t use prelude.Ghost use seq.Seq - use prelude.Int use prelude.Borrow + use prelude.Int use prelude.Slice - clone CreusotContracts_Invariant_Inv_Interface as Inv14 with + clone CreusotContracts_Invariant_Inv_Interface as Inv15 with type t = slice t - clone TyInv_Trivial as TyInv_Trivial14 with + clone TyInv_Trivial as TyInv_Trivial15 with type t = slice t, - predicate Inv0.inv = Inv14.inv, + predicate Inv0.inv = Inv15.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv13 with + clone CreusotContracts_Invariant_Inv_Interface as Inv14 with type t = t - clone TyInv_Trivial as TyInv_Trivial13 with + clone TyInv_Trivial as TyInv_Trivial14 with type t = t, - predicate Inv0.inv = Inv13.inv, + predicate Inv0.inv = Inv14.inv, axiom . use seq.Seq - clone CreusotContracts_Invariant_Inv_Interface as Inv12 with + clone CreusotContracts_Invariant_Inv_Interface as Inv13 with type t = Seq.seq t - clone TyInv_Trivial as TyInv_Trivial12 with + clone TyInv_Trivial as TyInv_Trivial13 with type t = Seq.seq t, - predicate Inv0.inv = Inv12.inv, + predicate Inv0.inv = Inv13.inv, axiom . use Core_Slice_Iter_Iter_Type as Core_Slice_Iter_Iter_Type clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Interface as ShallowModel2 with @@ -1956,69 +1956,69 @@ module Hillel_InsertUnique type t = Core_Slice_Iter_Iter_Type.t_iter t, type ShallowModelTy0.shallowModelTy = slice t, function ShallowModel0.shallow_model = ShallowModel2.shallow_model - clone CreusotContracts_Invariant_Inv_Interface as Inv11 with + clone CreusotContracts_Invariant_Inv_Interface as Inv12 with type t = Seq.seq t - clone TyInv_Trivial as TyInv_Trivial11 with + clone TyInv_Trivial as TyInv_Trivial12 with type t = Seq.seq t, - predicate Inv0.inv = Inv11.inv, + predicate Inv0.inv = Inv12.inv, axiom . clone Core_Num_Impl11_Max as Max0 clone CreusotContracts_Std1_Slice_Impl0_ShallowModel_Interface as ShallowModel5 with type t = t, - predicate Inv0.inv = Inv14.inv, + predicate Inv0.inv = Inv15.inv, val Max0.mAX' = Max0.mAX', - predicate Inv1.inv = Inv12.inv, + predicate Inv1.inv = Inv13.inv, axiom . use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type - clone CreusotContracts_Invariant_Inv_Interface as Inv10 with + clone CreusotContracts_Invariant_Inv_Interface as Inv11 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) - clone TyInv_Trivial as TyInv_Trivial10 with + clone TyInv_Trivial as TyInv_Trivial11 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global), - predicate Inv0.inv = Inv10.inv, + predicate Inv0.inv = Inv11.inv, axiom . clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with type self = t - clone CreusotContracts_Invariant_Inv_Interface as Inv9 with + clone CreusotContracts_Invariant_Inv_Interface as Inv10 with type t = DeepModelTy0.deepModelTy - clone TyInv_Trivial as TyInv_Trivial9 with + clone TyInv_Trivial as TyInv_Trivial10 with type t = DeepModelTy0.deepModelTy, - predicate Inv0.inv = Inv9.inv, + predicate Inv0.inv = Inv10.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv8 with + clone CreusotContracts_Invariant_Inv_Interface as Inv9 with type t = Seq.seq DeepModelTy0.deepModelTy - clone TyInv_Trivial as TyInv_Trivial8 with + clone TyInv_Trivial as TyInv_Trivial9 with type t = Seq.seq DeepModelTy0.deepModelTy, - predicate Inv0.inv = Inv8.inv, + predicate Inv0.inv = Inv9.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv7 with + clone CreusotContracts_Invariant_Inv_Interface as Inv8 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface as ShallowModel3 with type t = t, type a = Alloc_Alloc_Global_Type.t_global, - predicate Inv0.inv = Inv7.inv, + predicate Inv0.inv = Inv8.inv, val Max0.mAX' = Max0.mAX', - predicate Inv1.inv = Inv12.inv, + predicate Inv1.inv = Inv13.inv, axiom . clone CreusotContracts_Model_Impl7_ShallowModel as ShallowModel4 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global), type ShallowModelTy0.shallowModelTy = Seq.seq t, function ShallowModel0.shallow_model = ShallowModel3.shallow_model - clone TyInv_Trivial as TyInv_Trivial7 with + clone TyInv_Trivial as TyInv_Trivial8 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global), - predicate Inv0.inv = Inv7.inv, + predicate Inv0.inv = Inv8.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv6 with + clone CreusotContracts_Invariant_Inv_Interface as Inv7 with type t = borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) - clone TyInv_Trivial as TyInv_Trivial6 with + clone TyInv_Trivial as TyInv_Trivial7 with type t = borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)), - predicate Inv0.inv = Inv6.inv, + predicate Inv0.inv = Inv7.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv5 with + clone CreusotContracts_Invariant_Inv_Interface as Inv6 with type t = t - clone TyInv_Trivial as TyInv_Trivial5 with + clone TyInv_Trivial as TyInv_Trivial6 with type t = t, - predicate Inv0.inv = Inv5.inv, + predicate Inv0.inv = Inv6.inv, axiom . clone CreusotContracts_Model_DeepModel_DeepModel_Interface as DeepModel1 with type self = t, @@ -2031,171 +2031,179 @@ module Hillel_InsertUnique type t = t, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, function DeepModel0.deep_model = DeepModel2.deep_model - clone CreusotContracts_Invariant_Inv_Interface as Inv4 with + clone CreusotContracts_Invariant_Inv_Interface as Inv5 with type t = t - clone TyInv_Trivial as TyInv_Trivial4 with + clone TyInv_Trivial as TyInv_Trivial5 with type t = t, - predicate Inv0.inv = Inv4.inv, + predicate Inv0.inv = Inv5.inv, axiom . use Core_Option_Option_Type as Core_Option_Option_Type - clone CreusotContracts_Invariant_Inv_Interface as Inv3 with + clone CreusotContracts_Invariant_Inv_Interface as Inv4 with type t = Core_Option_Option_Type.t_option t - clone TyInv_Trivial as TyInv_Trivial3 with + clone TyInv_Trivial as TyInv_Trivial4 with type t = Core_Option_Option_Type.t_option t, - predicate Inv0.inv = Inv3.inv, + predicate Inv0.inv = Inv4.inv, axiom . - clone CreusotContracts_Resolve_Impl1_Resolve as Resolve4 with + clone CreusotContracts_Resolve_Impl1_Resolve as Resolve5 with type t = Core_Slice_Iter_Iter_Type.t_iter t clone CreusotContracts_Std1_Slice_Impl14_Completed as Completed0 with type t = t, - predicate Resolve0.resolve = Resolve4.resolve, + predicate Resolve0.resolve = Resolve5.resolve, function ShallowModel0.shallow_model = ShallowModel6.shallow_model, function ShallowModel1.shallow_model = ShallowModel5.shallow_model, - predicate Inv0.inv = Inv14.inv, + predicate Inv0.inv = Inv15.inv, val Max0.mAX' = Max0.mAX', - predicate Inv1.inv = Inv12.inv + predicate Inv1.inv = Inv13.inv clone CreusotContracts_Logic_Ops_Impl2_IndexLogic as IndexLogic2 with type t = t, function ShallowModel0.shallow_model = ShallowModel5.shallow_model, - predicate Inv0.inv = Inv14.inv, + predicate Inv0.inv = Inv15.inv, val Max0.mAX' = Max0.mAX', - predicate Inv1.inv = Inv12.inv + predicate Inv1.inv = Inv13.inv clone CreusotContracts_Model_Impl5_ShallowModel as ShallowModel0 with type t = slice t, type ShallowModelTy0.shallowModelTy = Seq.seq t, function ShallowModel0.shallow_model = ShallowModel5.shallow_model - clone CreusotContracts_Invariant_Inv_Interface as Inv0 with + clone CreusotContracts_Invariant_Inv_Interface as Inv1 with type t = slice t clone CreusotContracts_Std1_Slice_Impl4_ToRefSeq_Interface as ToRefSeq0 with type t = t, - predicate Inv0.inv = Inv0.inv, + predicate Inv0.inv = Inv1.inv, function ShallowModel0.shallow_model = ShallowModel0.shallow_model, function IndexLogic0.index_logic = IndexLogic2.index_logic, - predicate Inv1.inv = Inv11.inv, + predicate Inv1.inv = Inv12.inv, axiom . clone CreusotContracts_Std1_Slice_Impl14_Produces as Produces0 with type t = t, function ShallowModel0.shallow_model = ShallowModel2.shallow_model, function ToRefSeq0.to_ref_seq = ToRefSeq0.to_ref_seq, - predicate Inv0.inv = Inv0.inv, + predicate Inv0.inv = Inv1.inv, function ShallowModel1.shallow_model = ShallowModel0.shallow_model, function IndexLogic0.index_logic = IndexLogic2.index_logic, - predicate Inv1.inv = Inv11.inv + predicate Inv1.inv = Inv12.inv clone CreusotContracts_Std1_Slice_Impl14_ProducesTrans as ProducesTrans0 with type t = t, predicate Produces0.produces = Produces0.produces, - predicate Inv0.inv = Inv11.inv, + predicate Inv0.inv = Inv12.inv, axiom . clone CreusotContracts_Std1_Slice_Impl14_ProducesRefl as ProducesRefl0 with type t = t, predicate Produces0.produces = Produces0.produces, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv2 with + clone CreusotContracts_Invariant_Inv_Interface as Inv3 with type t = Core_Slice_Iter_Iter_Type.t_iter t - clone TyInv_Trivial as TyInv_Trivial2 with + clone TyInv_Trivial as TyInv_Trivial3 with type t = Core_Slice_Iter_Iter_Type.t_iter t, - predicate Inv0.inv = Inv2.inv, + predicate Inv0.inv = Inv3.inv, axiom . use prelude.Ghost - clone CreusotContracts_Invariant_Inv_Interface as Inv1 with + clone CreusotContracts_Invariant_Inv_Interface as Inv2 with type t = Ghost.ghost_ty (Seq.seq t) - clone TyInv_Trivial as TyInv_Trivial1 with + clone TyInv_Trivial as TyInv_Trivial2 with type t = Ghost.ghost_ty (Seq.seq t), - predicate Inv0.inv = Inv1.inv, + predicate Inv0.inv = Inv2.inv, axiom . clone CreusotContracts_Std1_Iter_Impl0_IntoIterPost as IntoIterPost0 with type i = Core_Slice_Iter_Iter_Type.t_iter t clone CreusotContracts_Std1_Iter_Impl0_IntoIterPre as IntoIterPre0 with type i = Core_Slice_Iter_Iter_Type.t_iter t - clone TyInv_Trivial as TyInv_Trivial0 with + clone TyInv_Trivial as TyInv_Trivial1 with type t = slice t, - predicate Inv0.inv = Inv0.inv, + predicate Inv0.inv = Inv1.inv, axiom . clone CreusotContracts_Model_Impl5_ShallowModel as ShallowModel1 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global), type ShallowModelTy0.shallowModelTy = Seq.seq t, function ShallowModel0.shallow_model = ShallowModel3.shallow_model + clone CreusotContracts_Invariant_Inv_Interface as Inv0 with + type t = Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) + clone TyInv_Trivial as TyInv_Trivial0 with + type t = Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)), + predicate Inv0.inv = Inv0.inv, + axiom . clone CreusotContracts_Logic_Ops_Impl0_IndexLogic as IndexLogic1 with type t = t, type a = Alloc_Alloc_Global_Type.t_global, function ShallowModel0.shallow_model = ShallowModel3.shallow_model, - predicate Inv0.inv = Inv7.inv, + predicate Inv0.inv = Inv8.inv, val Max0.mAX' = Max0.mAX', - predicate Inv1.inv = Inv12.inv + predicate Inv1.inv = Inv13.inv clone CreusotContracts_Std1_Vec_Impl1_DeepModel_Interface as DeepModel3 with type t = t, type a = Alloc_Alloc_Global_Type.t_global, - predicate Inv0.inv = Inv7.inv, + predicate Inv0.inv = Inv8.inv, function ShallowModel0.shallow_model = ShallowModel3.shallow_model, function IndexLogic0.index_logic = IndexLogic1.index_logic, function DeepModel0.deep_model = DeepModel1.deep_model, - predicate Inv1.inv = Inv8.inv, + predicate Inv1.inv = Inv9.inv, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy, val Max0.mAX' = Max0.mAX', - predicate Inv2.inv = Inv12.inv, + predicate Inv2.inv = Inv13.inv, axiom . clone Alloc_Vec_Impl1_Push_Interface as Push0 with type t = t, type a = Alloc_Alloc_Global_Type.t_global, - predicate Inv0.inv = Inv6.inv, - predicate Inv1.inv = Inv5.inv, + predicate Inv0.inv = Inv7.inv, + predicate Inv1.inv = Inv6.inv, function ShallowModel0.shallow_model = ShallowModel3.shallow_model, function ShallowModel1.shallow_model = ShallowModel4.shallow_model, - predicate Inv2.inv = Inv7.inv, + predicate Inv2.inv = Inv8.inv, val Max0.mAX' = Max0.mAX', - predicate Inv3.inv = Inv12.inv + predicate Inv3.inv = Inv13.inv clone Hillel_IsUnique as IsUnique0 with type t = DeepModelTy0.deepModelTy clone Hillel_Contains as Contains0 with type t = DeepModelTy0.deepModelTy - clone CreusotContracts_Resolve_Impl1_Resolve as Resolve9 with + clone CreusotContracts_Resolve_Impl1_Resolve as Resolve10 with type t = Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve8 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve9 with type self = t - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve7 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve8 with type self = Core_Slice_Iter_Iter_Type.t_iter t clone Core_Cmp_Impls_Impl9_Eq_Interface as Eq0 with type a = t, type b = t, - predicate Inv0.inv = Inv13.inv, - predicate Inv1.inv = Inv13.inv, + predicate Inv0.inv = Inv14.inv, + predicate Inv1.inv = Inv14.inv, function DeepModel0.deep_model = DeepModel4.deep_model, function DeepModel1.deep_model = DeepModel4.deep_model, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve6 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve7 with type self = t - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve5 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve6 with type self = Core_Option_Option_Type.t_option t clone Core_Slice_Iter_Impl181_Next_Interface as Next0 with type t = t, type Item0.item = t, predicate Completed0.completed = Completed0.completed, predicate Produces0.produces = Produces0.produces, - predicate Inv0.inv = Inv3.inv + predicate Inv0.inv = Inv4.inv clone CreusotContracts_Logic_Ops_Impl6_IndexLogic as IndexLogic0 with type t = t - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve3 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve4 with type self = Ghost.ghost_ty (Seq.seq t) - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve3 with type self = Ghost.ghost_ty (Core_Slice_Iter_Iter_Type.t_iter t) clone Core_Iter_Traits_Collect_Impl0_IntoIter_Interface as IntoIter0 with type i = Core_Slice_Iter_Iter_Type.t_iter t, predicate IntoIterPre0.into_iter_pre = IntoIterPre0.into_iter_pre, - predicate Inv0.inv = Inv2.inv, + predicate Inv0.inv = Inv3.inv, predicate IntoIterPost0.into_iter_post = IntoIterPost0.into_iter_post clone Core_Slice_Impl0_Iter_Interface as Iter0 with type t = t, - predicate Inv0.inv = Inv0.inv, + predicate Inv0.inv = Inv1.inv, function ShallowModel0.shallow_model = ShallowModel2.shallow_model - clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve2 with type self = slice t clone Alloc_Vec_Impl8_Deref_Interface as Deref0 with type t = t, type a = Alloc_Alloc_Global_Type.t_global, - predicate Inv0.inv = Inv10.inv, + predicate Inv0.inv = Inv11.inv, function ShallowModel0.shallow_model = ShallowModel0.shallow_model, function ShallowModel1.shallow_model = ShallowModel1.shallow_model, - predicate Inv1.inv = Inv0.inv + predicate Inv1.inv = Inv1.inv + clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve1 with + type self = Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) clone Hillel_IsSubset as IsSubset0 with type t = DeepModelTy0.deepModelTy, predicate Contains0.contains = Contains0.contains @@ -2207,14 +2215,14 @@ module Hillel_InsertUnique type self = Ghost.ghost_ty () clone Hillel_SubsetPush as SubsetPush0 with type t = DeepModelTy0.deepModelTy, - predicate Inv0.inv = Inv8.inv, - predicate Inv1.inv = Inv9.inv, + predicate Inv0.inv = Inv9.inv, + predicate Inv1.inv = Inv10.inv, predicate IsSubset0.is_subset = IsSubset0.is_subset, axiom . let rec cfg insert_unique [#"../hillel.rs" 79 0 79 62] [@cfg:stackify] [@cfg:subregion_analysis] (vec : borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global))) (elem : t) : () requires {[#"../hillel.rs" 74 11 74 38] IsUnique0.is_unique (DeepModel0.deep_model vec)} - requires {[#"../hillel.rs" 79 36 79 39] Inv6.inv vec} - requires {[#"../hillel.rs" 79 54 79 58] Inv5.inv elem} + requires {[#"../hillel.rs" 79 36 79 39] Inv7.inv vec} + requires {[#"../hillel.rs" 79 54 79 58] Inv6.inv elem} ensures { [#"../hillel.rs" 75 10 75 40] IsUnique0.is_unique (DeepModel3.deep_model ( ^ vec)) } ensures { [#"../hillel.rs" 76 10 76 58] IsSubset0.is_subset (DeepModel0.deep_model vec) (DeepModel3.deep_model ( ^ vec)) } ensures { [#"../hillel.rs" 77 10 77 82] IsSubset0.is_subset (DeepModel3.deep_model ( ^ vec)) (Seq.snoc (DeepModel0.deep_model vec) (DeepModel1.deep_model elem)) } @@ -2225,21 +2233,22 @@ module Hillel_InsertUnique var vec : borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)) = vec; var elem : t = elem; var _8 : Ghost.ghost_ty (); + var ghost_vec : Ghost.ghost_ty (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); var iter : Core_Slice_Iter_Iter_Type.t_iter t; - var _14 : Core_Slice_Iter_Iter_Type.t_iter t; - var _16 : slice t; + var _16 : Core_Slice_Iter_Iter_Type.t_iter t; + var _18 : slice t; var iter_old : Ghost.ghost_ty (Core_Slice_Iter_Iter_Type.t_iter t); var produced : Ghost.ghost_ty (Seq.seq t); - var _26 : Core_Option_Option_Type.t_option t; - var _27 : borrowed (Core_Slice_Iter_Iter_Type.t_iter t); - var _28 : borrowed (Core_Slice_Iter_Iter_Type.t_iter t); + var _28 : Core_Option_Option_Type.t_option t; + var _29 : borrowed (Core_Slice_Iter_Iter_Type.t_iter t); + var _30 : borrowed (Core_Slice_Iter_Iter_Type.t_iter t); var __creusot_proc_iter_elem : t; - var _31 : Ghost.ghost_ty (Seq.seq t); + var _33 : Ghost.ghost_ty (Seq.seq t); var e : t; - var _36 : bool; - var _39 : t; - var _46 : (); - var _47 : borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); + var _38 : bool; + var _41 : t; + var _48 : (); + var _49 : borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); { goto BB0 } @@ -2259,141 +2268,147 @@ module Hillel_InsertUnique goto BB4 } BB4 { - _16 <- ([#"../hillel.rs" 84 13 84 23] Deref0.deref ( * vec)); + ghost_vec <- ([#"../hillel.rs" 82 20 82 32] Ghost.new ( * vec)); goto BB5 } BB5 { - assert { [@expl:type invariant] Inv0.inv _16 }; - assume { Resolve1.resolve _16 }; - _14 <- ([#"../hillel.rs" 84 13 84 23] Iter0.iter _16); + assert { [@expl:type invariant] Inv0.inv ghost_vec }; + assume { Resolve1.resolve ghost_vec }; + _18 <- ([#"../hillel.rs" 85 13 85 23] Deref0.deref ( * vec)); goto BB6 } BB6 { - iter <- ([#"../hillel.rs" 83 4 83 111] IntoIter0.into_iter _14); - _14 <- any Core_Slice_Iter_Iter_Type.t_iter t; + assert { [@expl:type invariant] Inv1.inv _18 }; + assume { Resolve2.resolve _18 }; + _16 <- ([#"../hillel.rs" 85 13 85 23] Iter0.iter _18); goto BB7 } BB7 { - iter_old <- ([#"../hillel.rs" 83 4 83 111] Ghost.new iter); + iter <- ([#"../hillel.rs" 84 4 84 111] IntoIter0.into_iter _16); + _16 <- any Core_Slice_Iter_Iter_Type.t_iter t; goto BB8 } BB8 { - assume { Resolve2.resolve iter_old }; - produced <- ([#"../hillel.rs" 83 4 83 111] Ghost.new (Seq.empty )); + iter_old <- ([#"../hillel.rs" 84 4 84 111] Ghost.new iter); goto BB9 } BB9 { - assert { [@expl:type invariant] Inv1.inv produced }; - assume { Resolve3.resolve produced }; + assume { Resolve3.resolve iter_old }; + produced <- ([#"../hillel.rs" 84 4 84 111] Ghost.new (Seq.empty )); goto BB10 } BB10 { + assert { [@expl:type invariant] Inv2.inv produced }; + assume { Resolve4.resolve produced }; goto BB11 } BB11 { - invariant { [#"../hillel.rs" 83 4 83 111] Inv2.inv iter }; - invariant { [#"../hillel.rs" 83 4 83 111] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; - invariant { [#"../hillel.rs" 83 4 83 111] forall j : int . 0 <= j /\ j < Seq.length (Ghost.inner produced) -> DeepModel2.deep_model (IndexLogic0.index_logic produced j) <> DeepModel1.deep_model elem }; goto BB12 } BB12 { - _28 <- Borrow.borrow_mut iter; - iter <- ^ _28; - _27 <- Borrow.borrow_mut ( * _28); - _28 <- { _28 with current = ( ^ _27) }; - _26 <- ([#"../hillel.rs" 83 4 83 111] Next0.next _27); - _27 <- any borrowed (Core_Slice_Iter_Iter_Type.t_iter t); + invariant { [#"../hillel.rs" 84 4 84 111] Inv3.inv iter }; + invariant { [#"../hillel.rs" 84 4 84 111] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; + invariant { [#"../hillel.rs" 84 4 84 111] forall j : int . 0 <= j /\ j < Seq.length (Ghost.inner produced) -> DeepModel2.deep_model (IndexLogic0.index_logic produced j) <> DeepModel1.deep_model elem }; goto BB13 } BB13 { - assume { Resolve4.resolve _28 }; - switch (_26) - | Core_Option_Option_Type.C_None -> goto BB14 - | Core_Option_Option_Type.C_Some _ -> goto BB15 - end + _30 <- Borrow.borrow_mut iter; + iter <- ^ _30; + _29 <- Borrow.borrow_mut ( * _30); + _30 <- { _30 with current = ( ^ _29) }; + _28 <- ([#"../hillel.rs" 84 4 84 111] Next0.next _29); + _29 <- any borrowed (Core_Slice_Iter_Iter_Type.t_iter t); + goto BB14 } BB14 { - assert { [@expl:type invariant] Inv3.inv _26 }; - assume { Resolve5.resolve _26 }; - assume { Resolve7.resolve iter }; - assert { [@expl:assertion] [#"../hillel.rs" 92 20 92 71] IsUnique0.is_unique (Seq.snoc (DeepModel0.deep_model vec) (DeepModel1.deep_model elem)) }; - goto BB23 + assume { Resolve5.resolve _30 }; + switch (_28) + | Core_Option_Option_Type.C_None -> goto BB15 + | Core_Option_Option_Type.C_Some _ -> goto BB16 + end } BB15 { - goto BB17 + assert { [@expl:type invariant] Inv4.inv _28 }; + assume { Resolve6.resolve _28 }; + assume { Resolve8.resolve iter }; + assert { [@expl:assertion] [#"../hillel.rs" 93 20 93 71] IsUnique0.is_unique (Seq.snoc (DeepModel0.deep_model vec) (DeepModel1.deep_model elem)) }; + goto BB24 } BB16 { - assert { [@expl:type invariant] Inv3.inv _26 }; - assume { Resolve5.resolve _26 }; - assume { Resolve7.resolve iter }; - assert { [@expl:type invariant] Inv5.inv elem }; - assume { Resolve8.resolve elem }; - assert { [@expl:type invariant] Inv6.inv vec }; - assume { Resolve9.resolve vec }; - absurd + goto BB18 } BB17 { - __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _26; - assert { [@expl:type invariant] Inv3.inv _26 }; - assume { Resolve5.resolve _26 }; - _31 <- ([#"../hillel.rs" 83 4 83 111] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); - goto BB18 + assert { [@expl:type invariant] Inv4.inv _28 }; + assume { Resolve6.resolve _28 }; + assume { Resolve8.resolve iter }; + assert { [@expl:type invariant] Inv6.inv elem }; + assume { Resolve9.resolve elem }; + assert { [@expl:type invariant] Inv7.inv vec }; + assume { Resolve10.resolve vec }; + absurd } BB18 { - produced <- _31; - _31 <- any Ghost.ghost_ty (Seq.seq t); - assert { [@expl:type invariant] Inv1.inv produced }; - assume { Resolve3.resolve produced }; - e <- __creusot_proc_iter_elem; - assert { [@expl:type invariant] Inv4.inv __creusot_proc_iter_elem }; - assume { Resolve6.resolve __creusot_proc_iter_elem }; - assert { [@expl:assertion] [#"../hillel.rs" 85 24 85 54] e = IndexLogic1.index_logic ( * vec) (Seq.length (Ghost.inner produced) - 1) }; - _39 <- elem; - _36 <- ([#"../hillel.rs" 86 11 86 21] Eq0.eq e _39); + __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _28; + assert { [@expl:type invariant] Inv4.inv _28 }; + assume { Resolve6.resolve _28 }; + _33 <- ([#"../hillel.rs" 84 4 84 111] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB19 } BB19 { - assert { [@expl:type invariant] Inv4.inv _39 }; - assume { Resolve6.resolve _39 }; - assert { [@expl:type invariant] Inv4.inv e }; - assume { Resolve6.resolve e }; - switch (_36) - | False -> goto BB22 - | True -> goto BB20 - end + produced <- _33; + _33 <- any Ghost.ghost_ty (Seq.seq t); + assert { [@expl:type invariant] Inv2.inv produced }; + assume { Resolve4.resolve produced }; + e <- __creusot_proc_iter_elem; + assert { [@expl:type invariant] Inv5.inv __creusot_proc_iter_elem }; + assume { Resolve7.resolve __creusot_proc_iter_elem }; + assert { [@expl:assertion] [#"../hillel.rs" 86 24 86 57] e = IndexLogic1.index_logic (Ghost.inner ghost_vec) (Seq.length (Ghost.inner produced) - 1) }; + _41 <- elem; + _38 <- ([#"../hillel.rs" 87 11 87 21] Eq0.eq e _41); + goto BB20 } BB20 { - assume { Resolve7.resolve iter }; - assert { [@expl:type invariant] Inv5.inv elem }; - assume { Resolve8.resolve elem }; - assert { [@expl:type invariant] Inv6.inv vec }; - assume { Resolve9.resolve vec }; - assert { [@expl:assertion] [#"../hillel.rs" 87 28 87 73] Contains0.contains (DeepModel0.deep_model vec) (DeepModel1.deep_model elem) }; - goto BB21 + assert { [@expl:type invariant] Inv5.inv _41 }; + assume { Resolve7.resolve _41 }; + assert { [@expl:type invariant] Inv5.inv e }; + assume { Resolve7.resolve e }; + switch (_38) + | False -> goto BB23 + | True -> goto BB21 + end } BB21 { - _0 <- (); - goto BB25 + assume { Resolve8.resolve iter }; + assert { [@expl:type invariant] Inv6.inv elem }; + assume { Resolve9.resolve elem }; + assert { [@expl:type invariant] Inv7.inv vec }; + assume { Resolve10.resolve vec }; + assert { [@expl:assertion] [#"../hillel.rs" 88 28 88 73] Contains0.contains (DeepModel0.deep_model vec) (DeepModel1.deep_model elem) }; + goto BB22 } BB22 { - goto BB11 + _0 <- (); + goto BB26 } BB23 { - _47 <- Borrow.borrow_mut ( * vec); - vec <- { vec with current = ( ^ _47) }; - assume { Inv7.inv ( ^ _47) }; - _46 <- ([#"../hillel.rs" 93 4 93 18] Push0.push _47 elem); - _47 <- any borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); - elem <- any t; - goto BB24 + goto BB12 } BB24 { - assert { [@expl:type invariant] Inv6.inv vec }; - assume { Resolve9.resolve vec }; - _0 <- (); + _49 <- Borrow.borrow_mut ( * vec); + vec <- { vec with current = ( ^ _49) }; + assume { Inv8.inv ( ^ _49) }; + _48 <- ([#"../hillel.rs" 94 4 94 18] Push0.push _49 elem); + _49 <- any borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); + elem <- any t; goto BB25 } BB25 { + assert { [@expl:type invariant] Inv7.inv vec }; + assume { Resolve10.resolve vec }; + _0 <- (); + goto BB26 + } + BB26 { return _0 } @@ -2921,12 +2936,12 @@ module Hillel_Unique_Interface axiom . clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = slice t - val unique [#"../hillel.rs" 99 0 99 56] (str : slice t) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) - requires {[#"../hillel.rs" 99 36 99 39] Inv0.inv str} - ensures { [#"../hillel.rs" 96 10 96 40] IsUnique0.is_unique (DeepModel0.deep_model result) } - ensures { [#"../hillel.rs" 97 10 97 58] IsSubset0.is_subset (DeepModel0.deep_model result) (DeepModel1.deep_model str) } - ensures { [#"../hillel.rs" 98 10 98 58] IsSubset0.is_subset (DeepModel1.deep_model str) (DeepModel0.deep_model result) } - ensures { [#"../hillel.rs" 99 50 99 56] Inv1.inv result } + val unique [#"../hillel.rs" 100 0 100 56] (str : slice t) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) + requires {[#"../hillel.rs" 100 36 100 39] Inv0.inv str} + ensures { [#"../hillel.rs" 97 10 97 40] IsUnique0.is_unique (DeepModel0.deep_model result) } + ensures { [#"../hillel.rs" 98 10 98 58] IsSubset0.is_subset (DeepModel0.deep_model result) (DeepModel1.deep_model str) } + ensures { [#"../hillel.rs" 99 10 99 58] IsSubset0.is_subset (DeepModel1.deep_model str) (DeepModel0.deep_model result) } + ensures { [#"../hillel.rs" 100 50 100 56] Inv1.inv result } end module Hillel_Unique @@ -3171,12 +3186,12 @@ module Hillel_Unique predicate Inv0.inv = Inv2.inv, val Max0.mAX' = Max0.mAX', predicate Inv1.inv = Inv6.inv - let rec cfg unique [#"../hillel.rs" 99 0 99 56] [@cfg:stackify] [@cfg:subregion_analysis] (str : slice t) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) - requires {[#"../hillel.rs" 99 36 99 39] Inv5.inv str} - ensures { [#"../hillel.rs" 96 10 96 40] IsUnique0.is_unique (DeepModel0.deep_model result) } - ensures { [#"../hillel.rs" 97 10 97 58] IsSubset0.is_subset (DeepModel0.deep_model result) (DeepModel1.deep_model str) } - ensures { [#"../hillel.rs" 98 10 98 58] IsSubset0.is_subset (DeepModel1.deep_model str) (DeepModel0.deep_model result) } - ensures { [#"../hillel.rs" 99 50 99 56] Inv2.inv result } + let rec cfg unique [#"../hillel.rs" 100 0 100 56] [@cfg:stackify] [@cfg:subregion_analysis] (str : slice t) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global) + requires {[#"../hillel.rs" 100 36 100 39] Inv5.inv str} + ensures { [#"../hillel.rs" 97 10 97 40] IsUnique0.is_unique (DeepModel0.deep_model result) } + ensures { [#"../hillel.rs" 98 10 98 58] IsSubset0.is_subset (DeepModel0.deep_model result) (DeepModel1.deep_model str) } + ensures { [#"../hillel.rs" 99 10 99 58] IsSubset0.is_subset (DeepModel1.deep_model str) (DeepModel0.deep_model result) } + ensures { [#"../hillel.rs" 100 50 100 56] Inv2.inv result } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global); @@ -3204,30 +3219,30 @@ module Hillel_Unique goto BB0 } BB0 { - unique <- ([#"../hillel.rs" 100 21 100 31] New0.new ()); + unique <- ([#"../hillel.rs" 101 21 101 31] New0.new ()); goto BB1 } BB1 { - sub_str <- ([#"../hillel.rs" 101 37 101 55] Ghost.new (Seq.empty )); + sub_str <- ([#"../hillel.rs" 102 37 102 55] Ghost.new (Seq.empty )); goto BB2 } BB2 { assert { [@expl:type invariant] Inv0.inv sub_str }; assume { Resolve0.resolve sub_str }; - _11 <- ([#"../hillel.rs" 106 16 106 25] Len0.len str); + _11 <- ([#"../hillel.rs" 107 16 107 25] Len0.len str); goto BB3 } BB3 { - iter <- ([#"../hillel.rs" 103 4 103 48] IntoIter0.into_iter (Core_Ops_Range_Range_Type.C_Range ([#"../hillel.rs" 106 13 106 14] (0 : usize)) _11)); + iter <- ([#"../hillel.rs" 104 4 104 48] IntoIter0.into_iter (Core_Ops_Range_Range_Type.C_Range ([#"../hillel.rs" 107 13 107 14] (0 : usize)) _11)); _11 <- any usize; goto BB4 } BB4 { - iter_old <- ([#"../hillel.rs" 103 4 103 48] Ghost.new iter); + iter_old <- ([#"../hillel.rs" 104 4 104 48] Ghost.new iter); goto BB5 } BB5 { - produced <- ([#"../hillel.rs" 103 4 103 48] Ghost.new (Seq.empty )); + produced <- ([#"../hillel.rs" 104 4 104 48] Ghost.new (Seq.empty )); goto BB6 } BB6 { @@ -3243,11 +3258,11 @@ module Hillel_Unique goto BB10 } BB10 { - invariant { [#"../hillel.rs" 103 4 103 48] Inv1.inv iter }; - invariant { [#"../hillel.rs" 103 4 103 48] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; - invariant { [#"../hillel.rs" 103 16 103 46] IsUnique0.is_unique (DeepModel0.deep_model unique) }; - invariant { [#"../hillel.rs" 104 16 104 64] IsSubset0.is_subset (DeepModel0.deep_model unique) (DeepModel1.deep_model str) }; - invariant { [#"../hillel.rs" 105 16 105 95] IsSubset0.is_subset (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (Ghost.inner produced))) (DeepModel0.deep_model unique) }; + invariant { [#"../hillel.rs" 104 4 104 48] Inv1.inv iter }; + invariant { [#"../hillel.rs" 104 4 104 48] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; + invariant { [#"../hillel.rs" 104 16 104 46] IsUnique0.is_unique (DeepModel0.deep_model unique) }; + invariant { [#"../hillel.rs" 105 16 105 64] IsSubset0.is_subset (DeepModel0.deep_model unique) (DeepModel1.deep_model str) }; + invariant { [#"../hillel.rs" 106 16 106 95] IsSubset0.is_subset (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (Ghost.inner produced))) (DeepModel0.deep_model unique) }; goto BB11 } BB11 { @@ -3255,7 +3270,7 @@ module Hillel_Unique iter <- ^ _25; _24 <- Borrow.borrow_mut ( * _25); _25 <- { _25 with current = ( ^ _24) }; - _23 <- ([#"../hillel.rs" 103 4 103 48] Next0.next _24); + _23 <- ([#"../hillel.rs" 104 4 104 48] Next0.next _24); _24 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize); goto BB12 } @@ -3269,7 +3284,7 @@ module Hillel_Unique BB13 { assert { [@expl:type invariant] Inv5.inv str }; assume { Resolve4.resolve str }; - assert { [@expl:assertion] [#"../hillel.rs" 112 20 112 95] IsSubset0.is_subset (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (ShallowModel0.shallow_model str))) (DeepModel0.deep_model unique) }; + assert { [@expl:assertion] [#"../hillel.rs" 113 20 113 95] IsSubset0.is_subset (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (ShallowModel0.shallow_model str))) (DeepModel0.deep_model unique) }; goto BB21 } BB14 { @@ -3284,7 +3299,7 @@ module Hillel_Unique } BB16 { __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _23; - _28 <- ([#"../hillel.rs" 103 4 103 48] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); + _28 <- ([#"../hillel.rs" 104 4 104 48] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB17 } BB17 { @@ -3292,8 +3307,8 @@ module Hillel_Unique _28 <- any Ghost.ghost_ty (Seq.seq usize); i <- __creusot_proc_iter_elem; _32 <- i; - _34 <- ([#"../hillel.rs" 107 22 107 28] _32 < Slice.length str); - assert { [@expl:index in bounds] [#"../hillel.rs" 107 22 107 28] _34 }; + _34 <- ([#"../hillel.rs" 108 22 108 28] _32 < Slice.length str); + assert { [@expl:index in bounds] [#"../hillel.rs" 108 22 108 28] _34 }; goto BB18 } BB18 { @@ -3306,14 +3321,14 @@ module Hillel_Unique assume { Inv2.inv ( ^ _36) }; assert { [@expl:type invariant] Inv3.inv elem }; assume { Resolve2.resolve elem }; - _35 <- ([#"../hillel.rs" 108 8 108 40] InsertUnique0.insert_unique _36 elem); + _35 <- ([#"../hillel.rs" 109 8 109 40] InsertUnique0.insert_unique _36 elem); _36 <- any borrowed (Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)); goto BB19 } BB19 { assert { [@expl:type invariant] Inv4.inv _37 }; assume { Resolve3.resolve _37 }; - _39 <- ([#"../hillel.rs" 109 18 109 44] Ghost.new (Seq.snoc (Ghost.inner sub_str) elem)); + _39 <- ([#"../hillel.rs" 110 18 110 44] Ghost.new (Seq.snoc (Ghost.inner sub_str) elem)); goto BB20 } BB20 { @@ -3324,7 +3339,7 @@ module Hillel_Unique goto BB10 } BB21 { - assert { [@expl:assertion] [#"../hillel.rs" 113 20 113 88] Seq.(==) (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (ShallowModel0.shallow_model str))) (DeepModel1.deep_model str) }; + assert { [@expl:assertion] [#"../hillel.rs" 114 20 114 88] Seq.(==) (SeqExt.subsequence (DeepModel1.deep_model str) 0 (Seq.length (ShallowModel0.shallow_model str))) (DeepModel1.deep_model str) }; _0 <- unique; unique <- any Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global); goto BB22 @@ -3338,48 +3353,48 @@ module Hillel_SumRange_Stub use prelude.Int use seq.Seq use prelude.UInt32 - function sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + function sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int end module Hillel_SumRange_Interface use prelude.Int use seq.Seq use prelude.UInt32 - function sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int - val sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int - requires {[#"../hillel.rs" 119 11 119 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 120 10 120 21] result >= 0 } + function sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + val sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + requires {[#"../hillel.rs" 120 11 120 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 121 10 121 21] result >= 0 } ensures { result = sum_range seq from to' } - axiom sum_range_spec : forall seq : Seq.seq uint32, from : int, to' : int . ([#"../hillel.rs" 119 11 119 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 120 10 120 21] sum_range seq from to' >= 0) + axiom sum_range_spec : forall seq : Seq.seq uint32, from : int, to' : int . ([#"../hillel.rs" 120 11 120 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 121 10 121 21] sum_range seq from to' >= 0) end module Hillel_SumRange use prelude.Int use seq.Seq use prelude.UInt32 - function sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int - val sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int - requires {[#"../hillel.rs" 119 11 119 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 120 10 120 21] result >= 0 } + function sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + val sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + requires {[#"../hillel.rs" 120 11 120 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 121 10 121 21] result >= 0 } ensures { result = sum_range seq from to' } - axiom def : forall seq : Seq.seq uint32, from : int, to' : int . sum_range seq from to' = ([#"../hillel.rs" 117 0 117 8] if to' - from > 0 then + axiom def : forall seq : Seq.seq uint32, from : int, to' : int . sum_range seq from to' = ([#"../hillel.rs" 118 0 118 8] if to' - from > 0 then UInt32.to_int (Seq.get seq from) + sum_range seq (from + 1) to' else 0 ) - axiom sum_range_spec : forall seq : Seq.seq uint32, from : int, to' : int . ([#"../hillel.rs" 119 11 119 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 120 10 120 21] sum_range seq from to' >= 0) + axiom sum_range_spec : forall seq : Seq.seq uint32, from : int, to' : int . ([#"../hillel.rs" 120 11 120 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 121 10 121 21] sum_range seq from to' >= 0) end module Hillel_SumRange_Impl use prelude.Int use seq.Seq use prelude.UInt32 - let rec ghost function sum_range [#"../hillel.rs" 121 0 121 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int - requires {[#"../hillel.rs" 119 11 119 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 120 10 120 21] result >= 0 } - variant {[#"../hillel.rs" 118 10 118 19] to' - from} + let rec ghost function sum_range [#"../hillel.rs" 122 0 122 54] (seq : Seq.seq uint32) (from : int) (to' : int) : int + requires {[#"../hillel.rs" 120 11 120 53] 0 <= from /\ from <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 121 10 121 21] result >= 0 } + variant {[#"../hillel.rs" 119 10 119 19] to' - from} = [@vc:do_not_keep_trace] [@vc:sp] - [#"../hillel.rs" 117 0 117 8] if pure {to' - from > 0} then + [#"../hillel.rs" 118 0 118 8] if pure {to' - from > 0} then UInt32.to_int (Seq.get seq from) + sum_range seq (from + 1) to' else 0 @@ -3391,7 +3406,7 @@ module Hillel_SumRangeSplit_Stub use prelude.UInt32 clone Hillel_SumRange_Stub as SumRange0 with axiom . - function sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + function sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () end module Hillel_SumRangeSplit_Interface use prelude.Int @@ -3399,13 +3414,13 @@ module Hillel_SumRangeSplit_Interface use prelude.UInt32 clone Hillel_SumRange_Stub as SumRange0 with axiom . - function sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () - val sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () - requires {[#"../hillel.rs" 131 11 131 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 132 10 132 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } + function sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + val sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + requires {[#"../hillel.rs" 132 11 132 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 133 10 133 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } ensures { result = sum_range_split seq from to' i } - axiom sum_range_split_spec : forall seq : Seq.seq uint32, from : int, to' : int, i : int . ([#"../hillel.rs" 131 11 131 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 132 10 132 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to') + axiom sum_range_split_spec : forall seq : Seq.seq uint32, from : int, to' : int, i : int . ([#"../hillel.rs" 132 11 132 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 133 10 133 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to') end module Hillel_SumRangeSplit use prelude.Int @@ -3413,18 +3428,18 @@ module Hillel_SumRangeSplit use prelude.UInt32 clone Hillel_SumRange_Stub as SumRange0 with axiom . - function sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () - val sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () - requires {[#"../hillel.rs" 131 11 131 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 132 10 132 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } + function sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + val sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + requires {[#"../hillel.rs" 132 11 132 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 133 10 133 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } ensures { result = sum_range_split seq from to' i } - axiom def : forall seq : Seq.seq uint32, from : int, to' : int, i : int . sum_range_split seq from to' i = ([#"../hillel.rs" 134 4 136 5] if i > from then + axiom def : forall seq : Seq.seq uint32, from : int, to' : int, i : int . sum_range_split seq from to' i = ([#"../hillel.rs" 135 4 137 5] if i > from then let _ = sum_range_split seq (from + 1) to' i in () else () ) - axiom sum_range_split_spec : forall seq : Seq.seq uint32, from : int, to' : int, i : int . ([#"../hillel.rs" 131 11 131 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 132 10 132 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to') + axiom sum_range_split_spec : forall seq : Seq.seq uint32, from : int, to' : int, i : int . ([#"../hillel.rs" 132 11 132 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq) -> ([#"../hillel.rs" 133 10 133 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to') end module Hillel_SumRangeSplit_Impl use prelude.Int @@ -3432,13 +3447,13 @@ module Hillel_SumRangeSplit_Impl use prelude.UInt32 clone Hillel_SumRange as SumRange0 with axiom . - let rec ghost function sum_range_split [#"../hillel.rs" 133 0 133 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () - requires {[#"../hillel.rs" 131 11 131 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} - ensures { [#"../hillel.rs" 132 10 132 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } - variant {[#"../hillel.rs" 130 10 130 18] i - from} + let rec ghost function sum_range_split [#"../hillel.rs" 134 0 134 61] (seq : Seq.seq uint32) (from : int) (to' : int) (i : int) : () + requires {[#"../hillel.rs" 132 11 132 63] 0 <= from /\ from <= i /\ i <= to' /\ to' <= Seq.length seq} + ensures { [#"../hillel.rs" 133 10 133 85] SumRange0.sum_range seq from to' = SumRange0.sum_range seq from i + SumRange0.sum_range seq i to' } + variant {[#"../hillel.rs" 131 10 131 18] i - from} = [@vc:do_not_keep_trace] [@vc:sp] - [#"../hillel.rs" 134 4 136 5] if pure {i > from} then let _ = sum_range_split seq (from + 1) to' i in () else () + [#"../hillel.rs" 135 4 137 5] if pure {i > from} then let _ = sum_range_split seq (from + 1) to' i in () else () end module CreusotContracts_Logic_Int_Impl0_AbsDiff_Stub use prelude.Int @@ -3465,7 +3480,7 @@ module Hillel_Score_Stub use prelude.UInt32 clone Hillel_SumRange_Stub as SumRange0 with axiom . - function score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int + function score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int end module Hillel_Score_Interface use prelude.Int @@ -3473,14 +3488,14 @@ module Hillel_Score_Interface use prelude.UInt32 clone Hillel_SumRange_Stub as SumRange0 with axiom . - function score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int - val score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int - requires {[#"../hillel.rs" 140 11 140 35] 0 <= i /\ i <= Seq.length seq} - ensures { [#"../hillel.rs" 141 10 141 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } - ensures { [#"../hillel.rs" 142 0 142 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } + function score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int + val score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int + requires {[#"../hillel.rs" 141 11 141 35] 0 <= i /\ i <= Seq.length seq} + ensures { [#"../hillel.rs" 142 10 142 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } + ensures { [#"../hillel.rs" 143 0 143 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } ensures { result = score seq i } - axiom score_spec : forall seq : Seq.seq uint32, i : int . ([#"../hillel.rs" 140 11 140 35] 0 <= i /\ i <= Seq.length seq) -> ([#"../hillel.rs" 142 0 142 79] 0 = i \/ i = Seq.length seq -> score seq i = SumRange0.sum_range seq 0 (Seq.length seq)) && ([#"../hillel.rs" 141 10 141 64] 0 <= score seq i /\ score seq i <= SumRange0.sum_range seq 0 (Seq.length seq)) + axiom score_spec : forall seq : Seq.seq uint32, i : int . ([#"../hillel.rs" 141 11 141 35] 0 <= i /\ i <= Seq.length seq) -> ([#"../hillel.rs" 143 0 143 79] 0 = i \/ i = Seq.length seq -> score seq i = SumRange0.sum_range seq 0 (Seq.length seq)) && ([#"../hillel.rs" 142 10 142 64] 0 <= score seq i /\ score seq i <= SumRange0.sum_range seq 0 (Seq.length seq)) end module Hillel_Score use prelude.Int @@ -3492,15 +3507,15 @@ module Hillel_Score clone Hillel_SumRangeSplit_Stub as SumRangeSplit0 with function SumRange0.sum_range = SumRange0.sum_range, axiom . - function score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int = - [#"../hillel.rs" 144 4 144 41] let _ = SumRangeSplit0.sum_range_split seq 0 (Seq.length seq) i in AbsDiff0.abs_diff (SumRange0.sum_range seq 0 i) (SumRange0.sum_range seq i (Seq.length seq)) - val score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int - requires {[#"../hillel.rs" 140 11 140 35] 0 <= i /\ i <= Seq.length seq} - ensures { [#"../hillel.rs" 141 10 141 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } - ensures { [#"../hillel.rs" 142 0 142 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } + function score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int = + [#"../hillel.rs" 145 4 145 41] let _ = SumRangeSplit0.sum_range_split seq 0 (Seq.length seq) i in AbsDiff0.abs_diff (SumRange0.sum_range seq 0 i) (SumRange0.sum_range seq i (Seq.length seq)) + val score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int + requires {[#"../hillel.rs" 141 11 141 35] 0 <= i /\ i <= Seq.length seq} + ensures { [#"../hillel.rs" 142 10 142 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } + ensures { [#"../hillel.rs" 143 0 143 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } ensures { result = score seq i } - axiom score_spec : forall seq : Seq.seq uint32, i : int . ([#"../hillel.rs" 140 11 140 35] 0 <= i /\ i <= Seq.length seq) -> ([#"../hillel.rs" 142 0 142 79] 0 = i \/ i = Seq.length seq -> score seq i = SumRange0.sum_range seq 0 (Seq.length seq)) && ([#"../hillel.rs" 141 10 141 64] 0 <= score seq i /\ score seq i <= SumRange0.sum_range seq 0 (Seq.length seq)) + axiom score_spec : forall seq : Seq.seq uint32, i : int . ([#"../hillel.rs" 141 11 141 35] 0 <= i /\ i <= Seq.length seq) -> ([#"../hillel.rs" 143 0 143 79] 0 = i \/ i = Seq.length seq -> score seq i = SumRange0.sum_range seq 0 (Seq.length seq)) && ([#"../hillel.rs" 142 10 142 64] 0 <= score seq i /\ score seq i <= SumRange0.sum_range seq 0 (Seq.length seq)) end module Hillel_Score_Impl use prelude.Int @@ -3512,13 +3527,13 @@ module Hillel_Score_Impl clone Hillel_SumRangeSplit as SumRangeSplit0 with function SumRange0.sum_range = SumRange0.sum_range, axiom . - let rec ghost function score [#"../hillel.rs" 143 0 143 38] (seq : Seq.seq uint32) (i : int) : int - requires {[#"../hillel.rs" 140 11 140 35] 0 <= i /\ i <= Seq.length seq} - ensures { [#"../hillel.rs" 141 10 141 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } - ensures { [#"../hillel.rs" 142 0 142 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } + let rec ghost function score [#"../hillel.rs" 144 0 144 38] (seq : Seq.seq uint32) (i : int) : int + requires {[#"../hillel.rs" 141 11 141 35] 0 <= i /\ i <= Seq.length seq} + ensures { [#"../hillel.rs" 142 10 142 64] 0 <= result /\ result <= SumRange0.sum_range seq 0 (Seq.length seq) } + ensures { [#"../hillel.rs" 143 0 143 79] 0 = i \/ i = Seq.length seq -> result = SumRange0.sum_range seq 0 (Seq.length seq) } = [@vc:do_not_keep_trace] [@vc:sp] - [#"../hillel.rs" 144 4 144 41] let _ = SumRangeSplit0.sum_range_split seq 0 (Seq.length seq) i in let a' = SumRange0.sum_range seq 0 i in let b' = SumRange0.sum_range seq i (Seq.length seq) in AbsDiff0.abs_diff a' b' + [#"../hillel.rs" 145 4 145 41] let _ = SumRangeSplit0.sum_range_split seq 0 (Seq.length seq) i in let a' = SumRange0.sum_range seq 0 i in let b' = SumRange0.sum_range seq i (Seq.length seq) in AbsDiff0.abs_diff a' b' end module CreusotContracts_Std1_Slice_Impl11_IntoIterPre_Stub type t @@ -3616,11 +3631,11 @@ module Hillel_Fulcrum_Interface clone CreusotContracts_Model_Impl5_ShallowModel_Stub as ShallowModel0 with type t = slice uint32, type ShallowModelTy0.shallowModelTy = Seq.seq uint32 - val fulcrum [#"../hillel.rs" 155 0 155 30] (s : slice uint32) : usize - requires {[#"../hillel.rs" 151 11 151 45] SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) <= 1000} - requires {[#"../hillel.rs" 152 11 152 23] Seq.length (ShallowModel0.shallow_model s) > 0} - ensures { [#"../hillel.rs" 153 10 153 44] 0 <= UIntSize.to_int result /\ UIntSize.to_int result < Seq.length (ShallowModel0.shallow_model s) } - ensures { [#"../hillel.rs" 154 0 154 88] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model s) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int result) <= Score0.score (ShallowModel0.shallow_model s) i } + val fulcrum [#"../hillel.rs" 156 0 156 30] (s : slice uint32) : usize + requires {[#"../hillel.rs" 152 11 152 45] SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) <= 1000} + requires {[#"../hillel.rs" 153 11 153 23] Seq.length (ShallowModel0.shallow_model s) > 0} + ensures { [#"../hillel.rs" 154 10 154 44] 0 <= UIntSize.to_int result /\ UIntSize.to_int result < Seq.length (ShallowModel0.shallow_model s) } + ensures { [#"../hillel.rs" 155 0 155 88] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model s) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int result) <= Score0.score (ShallowModel0.shallow_model s) i } end module Hillel_Fulcrum @@ -3823,11 +3838,11 @@ module Hillel_Fulcrum predicate IntoIterPre0.into_iter_pre = IntoIterPre0.into_iter_pre, predicate Inv0.inv = Inv2.inv, predicate IntoIterPost0.into_iter_post = IntoIterPost0.into_iter_post - let rec cfg fulcrum [#"../hillel.rs" 155 0 155 30] [@cfg:stackify] [@cfg:subregion_analysis] (s : slice uint32) : usize - requires {[#"../hillel.rs" 151 11 151 45] SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) <= 1000} - requires {[#"../hillel.rs" 152 11 152 23] Seq.length (ShallowModel0.shallow_model s) > 0} - ensures { [#"../hillel.rs" 153 10 153 44] 0 <= UIntSize.to_int result /\ UIntSize.to_int result < Seq.length (ShallowModel0.shallow_model s) } - ensures { [#"../hillel.rs" 154 0 154 88] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model s) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int result) <= Score0.score (ShallowModel0.shallow_model s) i } + let rec cfg fulcrum [#"../hillel.rs" 156 0 156 30] [@cfg:stackify] [@cfg:subregion_analysis] (s : slice uint32) : usize + requires {[#"../hillel.rs" 152 11 152 45] SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) <= 1000} + requires {[#"../hillel.rs" 153 11 153 23] Seq.length (ShallowModel0.shallow_model s) > 0} + ensures { [#"../hillel.rs" 154 10 154 44] 0 <= UIntSize.to_int result /\ UIntSize.to_int result < Seq.length (ShallowModel0.shallow_model s) } + ensures { [#"../hillel.rs" 155 0 155 88] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model s) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int result) <= Score0.score (ShallowModel0.shallow_model s) i } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : usize; @@ -3864,26 +3879,26 @@ module Hillel_Fulcrum goto BB0 } BB0 { - total <- ([#"../hillel.rs" 156 25 156 26] (0 : uint32)); - iter <- ([#"../hillel.rs" 158 4 158 60] IntoIter0.into_iter s); + total <- ([#"../hillel.rs" 157 25 157 26] (0 : uint32)); + iter <- ([#"../hillel.rs" 159 4 159 60] IntoIter0.into_iter s); goto BB1 } BB1 { - iter_old <- ([#"../hillel.rs" 158 4 158 60] Ghost.new iter); + iter_old <- ([#"../hillel.rs" 159 4 159 60] Ghost.new iter); goto BB2 } BB2 { - produced <- ([#"../hillel.rs" 158 4 158 60] Ghost.new (Seq.empty )); + produced <- ([#"../hillel.rs" 159 4 159 60] Ghost.new (Seq.empty )); goto BB3 } BB3 { goto BB4 } BB4 { - invariant { [#"../hillel.rs" 158 4 158 60] Inv0.inv iter }; - invariant { [#"../hillel.rs" 158 4 158 60] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; - invariant { [#"../hillel.rs" 158 16 158 58] UInt32.to_int total = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (Ghost.inner produced)) }; - invariant { [#"../hillel.rs" 159 16 159 52] UInt32.to_int total <= SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) }; + invariant { [#"../hillel.rs" 159 4 159 60] Inv0.inv iter }; + invariant { [#"../hillel.rs" 159 4 159 60] Produces0.produces (Ghost.inner iter_old) (Ghost.inner produced) iter }; + invariant { [#"../hillel.rs" 159 16 159 58] UInt32.to_int total = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (Ghost.inner produced)) }; + invariant { [#"../hillel.rs" 160 16 160 52] UInt32.to_int total <= SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) }; goto BB5 } BB5 { @@ -3891,7 +3906,7 @@ module Hillel_Fulcrum iter <- ^ _21; _20 <- Borrow.borrow_mut ( * _21); _21 <- { _21 with current = ( ^ _20) }; - _19 <- ([#"../hillel.rs" 158 4 158 60] Next0.next _20); + _19 <- ([#"../hillel.rs" 159 4 159 60] Next0.next _20); _20 <- any borrowed (Core_Slice_Iter_Iter_Type.t_iter uint32); goto BB6 } @@ -3903,11 +3918,11 @@ module Hillel_Fulcrum end } BB7 { - assert { [@expl:assertion] [#"../hillel.rs" 164 20 164 56] UInt32.to_int total = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) }; - min_i <- ([#"../hillel.rs" 166 27 166 28] (0 : usize)); + assert { [@expl:assertion] [#"../hillel.rs" 165 20 165 56] UInt32.to_int total = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (ShallowModel0.shallow_model s)) }; + min_i <- ([#"../hillel.rs" 167 27 167 28] (0 : usize)); min_dist <- total; - sum <- ([#"../hillel.rs" 169 23 169 24] (0 : uint32)); - _37 <- ([#"../hillel.rs" 175 16 175 23] Len0.len s); + sum <- ([#"../hillel.rs" 170 23 170 24] (0 : uint32)); + _37 <- ([#"../hillel.rs" 176 16 176 23] Len0.len s); goto BB12 } BB8 { @@ -3918,41 +3933,41 @@ module Hillel_Fulcrum } BB10 { __creusot_proc_iter_elem <- Core_Option_Option_Type.some_0 _19; - _24 <- ([#"../hillel.rs" 158 4 158 60] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); + _24 <- ([#"../hillel.rs" 159 4 159 60] Ghost.new (Seq.(++) (Ghost.inner produced) (Seq.singleton __creusot_proc_iter_elem))); goto BB11 } BB11 { produced <- _24; _24 <- any Ghost.ghost_ty (Seq.seq uint32); x <- __creusot_proc_iter_elem; - total <- ([#"../hillel.rs" 161 8 161 18] total + x); + total <- ([#"../hillel.rs" 162 8 162 18] total + x); _18 <- (); goto BB4 } BB12 { - iter1 <- ([#"../hillel.rs" 170 4 170 58] IntoIter1.into_iter (Core_Ops_Range_Range_Type.C_Range ([#"../hillel.rs" 175 13 175 14] (0 : usize)) _37)); + iter1 <- ([#"../hillel.rs" 171 4 171 58] IntoIter1.into_iter (Core_Ops_Range_Range_Type.C_Range ([#"../hillel.rs" 176 13 176 14] (0 : usize)) _37)); _37 <- any usize; goto BB13 } BB13 { - iter_old1 <- ([#"../hillel.rs" 170 4 170 58] Ghost.new iter1); + iter_old1 <- ([#"../hillel.rs" 171 4 171 58] Ghost.new iter1); goto BB14 } BB14 { - produced1 <- ([#"../hillel.rs" 170 4 170 58] Ghost.new (Seq.empty )); + produced1 <- ([#"../hillel.rs" 171 4 171 58] Ghost.new (Seq.empty )); goto BB15 } BB15 { goto BB16 } BB16 { - invariant { [#"../hillel.rs" 170 4 170 58] Inv1.inv iter1 }; - invariant { [#"../hillel.rs" 170 4 170 58] Produces1.produces (Ghost.inner iter_old1) (Ghost.inner produced1) iter1 }; - invariant { [#"../hillel.rs" 170 16 170 56] UInt32.to_int sum = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (Ghost.inner produced1)) }; - invariant { [#"../hillel.rs" 171 16 171 30] UInt32.to_int sum <= UInt32.to_int total }; - invariant { [#"../hillel.rs" 172 16 172 61] UIntSize.to_int min_i <= Seq.length (Ghost.inner produced1) /\ UIntSize.to_int min_i < Seq.length (ShallowModel0.shallow_model s) }; - invariant { [#"../hillel.rs" 173 16 173 46] UInt32.to_int min_dist = Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int min_i) }; - invariant { [#"../hillel.rs" 170 4 170 58] forall j : int . 0 <= j /\ j < Seq.length (Ghost.inner produced1) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int min_i) <= Score0.score (ShallowModel0.shallow_model s) j }; + invariant { [#"../hillel.rs" 171 4 171 58] Inv1.inv iter1 }; + invariant { [#"../hillel.rs" 171 4 171 58] Produces1.produces (Ghost.inner iter_old1) (Ghost.inner produced1) iter1 }; + invariant { [#"../hillel.rs" 171 16 171 56] UInt32.to_int sum = SumRange0.sum_range (ShallowModel0.shallow_model s) 0 (Seq.length (Ghost.inner produced1)) }; + invariant { [#"../hillel.rs" 172 16 172 30] UInt32.to_int sum <= UInt32.to_int total }; + invariant { [#"../hillel.rs" 173 16 173 61] UIntSize.to_int min_i <= Seq.length (Ghost.inner produced1) /\ UIntSize.to_int min_i < Seq.length (ShallowModel0.shallow_model s) }; + invariant { [#"../hillel.rs" 174 16 174 46] UInt32.to_int min_dist = Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int min_i) }; + invariant { [#"../hillel.rs" 171 4 171 58] forall j : int . 0 <= j /\ j < Seq.length (Ghost.inner produced1) -> Score0.score (ShallowModel0.shallow_model s) (UIntSize.to_int min_i) <= Score0.score (ShallowModel0.shallow_model s) j }; goto BB17 } BB17 { @@ -3960,7 +3975,7 @@ module Hillel_Fulcrum iter1 <- ^ _52; _51 <- Borrow.borrow_mut ( * _52); _52 <- { _52 with current = ( ^ _51) }; - _50 <- ([#"../hillel.rs" 170 4 170 58] Next1.next _51); + _50 <- ([#"../hillel.rs" 171 4 171 58] Next1.next _51); _51 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize); goto BB18 } @@ -3980,18 +3995,18 @@ module Hillel_Fulcrum } BB21 { __creusot_proc_iter_elem1 <- Core_Option_Option_Type.some_0 _50; - _55 <- ([#"../hillel.rs" 170 4 170 58] Ghost.new (Seq.(++) (Ghost.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); + _55 <- ([#"../hillel.rs" 171 4 171 58] Ghost.new (Seq.(++) (Ghost.inner produced1) (Seq.singleton __creusot_proc_iter_elem1))); goto BB22 } BB22 { produced1 <- _55; _55 <- any Ghost.ghost_ty (Seq.seq usize); i <- __creusot_proc_iter_elem1; - dist <- ([#"../hillel.rs" 176 19 176 44] AbsDiff0.abs_diff sum ([#"../hillel.rs" 176 32 176 43] total - sum)); + dist <- ([#"../hillel.rs" 177 19 177 44] AbsDiff0.abs_diff sum ([#"../hillel.rs" 177 32 177 43] total - sum)); goto BB23 } BB23 { - switch ([#"../hillel.rs" 177 11 177 26] dist < min_dist) + switch ([#"../hillel.rs" 178 11 178 26] dist < min_dist) | False -> goto BB25 | True -> goto BB24 end @@ -4008,12 +4023,12 @@ module Hillel_Fulcrum } BB26 { _70 <- i; - _72 <- ([#"../hillel.rs" 182 15 182 19] _70 < Slice.length s); - assert { [@expl:index in bounds] [#"../hillel.rs" 182 15 182 19] _72 }; + _72 <- ([#"../hillel.rs" 183 15 183 19] _70 < Slice.length s); + assert { [@expl:index in bounds] [#"../hillel.rs" 183 15 183 19] _72 }; goto BB27 } BB27 { - sum <- ([#"../hillel.rs" 182 8 182 19] sum + Slice.get s _70); + sum <- ([#"../hillel.rs" 183 8 183 19] sum + Slice.get s _70); _18 <- (); goto BB16 } diff --git a/creusot/tests/should_succeed/hillel.rs b/creusot/tests/should_succeed/hillel.rs index 1067bc8c6d..4b8e81c428 100644 --- a/creusot/tests/should_succeed/hillel.rs +++ b/creusot/tests/should_succeed/hillel.rs @@ -79,10 +79,11 @@ fn subset_push(s: Seq, elem: T) {} fn insert_unique(vec: &mut Vec, elem: T) { gh! { subset_push:: }; proof_assert! { is_subset(vec.deep_model(), vec.deep_model().push(elem.deep_model())) }; + let ghost_vec = gh! { *vec }; #[invariant(forall 0 <= j && j < produced.len() ==> produced[j].deep_model() != elem.deep_model())] for e in vec.iter() { - proof_assert! { *e == (*vec)[produced.len()-1] }; + proof_assert! { *e == ghost_vec[produced.len()-1] }; if e == &elem { proof_assert! { contains(vec.deep_model(), elem.deep_model()) }; return; diff --git a/creusot/tests/should_succeed/hillel/why3session.xml b/creusot/tests/should_succeed/hillel/why3session.xml index c6edfb4889..2e22c83cf4 100644 --- a/creusot/tests/should_succeed/hillel/why3session.xml +++ b/creusot/tests/should_succeed/hillel/why3session.xml @@ -4,8 +4,10 @@ + + @@ -27,110 +29,113 @@ - + - - + + - - + + - - + + - + - + - - + + - - + + - + - + - - + + - - + + - - + + - + - - + + - + - + - + - - + + - - + + - + - - + + - + - - + + - + - + - - + + - + + + + - - + + - + - - + + - - + + - - - - + - + + + + diff --git a/creusot/tests/should_succeed/hillel/why3shapes.gz b/creusot/tests/should_succeed/hillel/why3shapes.gz index bc15f6df8eb26d4df43be5fd67294e0784c2ae9d..c0716c8121e6b22a7c5eebf3c8ba838f9375641f 100644 GIT binary patch literal 7185 zcmV+s9PZ;EiwFP!00000|LuHRj~q9$=DU7Hzs;@%0}S4|7#S!C7ODZ`9ANh#u}`PL zB$;-5TV0y&mS@ht-;ZS8tFlzO*hg)7Fmf@;U@#&Wj0-ce|HpS%kH7eL>GA5f^ze9l zxc^^Q`s%y?`Qqsx{`UU2hP~-q)X>o64Ii4K5kpfp^34nX_gDTd-T(abiwD-byTd`2TE7L#lDt z{_pthkv4X>wJ;Ub@=t{O(P8ye#%Weq4w=XU+?YKOmT$Tgf* zP2p^VE^?ci!y96lc%(WNF)jP>be|r|3@QuKCeB`mIBn`sCTnwg)~U@&7aWHf6bRj1 z=EJB8)Ycl;U~Rq4Wc}m)AshkQX%B~uw$&D3(u?NxRd;x}dbs`hm#3R|KAy4&{$)eP zfB(@+d3^p&Isa$0xSoG=+Mw9pF4<3@Wk7Auo0jKraQSd>`LLh-qYf^ohU@;|>b25w zH5?#);%MfnX5(o3@AKFZy0Xj``<#mYA5FrHvii}$#?I50MG(azY#r7!leX;uCS70$ zW>8ypKwM-8#I_yCw(wPvmV8rM(%+|lHeBQ<{~ma?{9DG(g?|}n(Zk_(dj>TSP>t4P2U|8JHfW4kT?Eo~JU8dSOMks!I`|jz#vIic7BC@^>4>Bw0@W8X~ z4i8XdHJ9C5-N(2wru42?2d)R%EjqKwnK~BH1l8g5c1aIb&{SdSCHh`XU?Uf2!}f>6 zHoS^Z4GpYlEA0FG+kd=IGj!blmcomoVPnhrbeG;{QQX*kru~1se|MMIi^0sJd$#Zz zS&akMopW(i?2nJ>;Rz{8Ugzgu4v$Ya87?pP-AD;^Z5(>>^k47N6*~RHt%sQyoz4uT z9LawEyN47G_wjaEW2yH3CPyp_Q#W6?jE_t7Pb(Y}y}FLzT;p&*rH31=n!76&F*L_f z5L#yCrvaw6UzOjR!(A*gsGa@#VjRnGy|P!hqU{xv97o29v#z_t;oT%Xv~HiKb5q^u zL_vKV7plZ$mGr;j*Z(>w?h@|Bzk#}Gqs3hB`GoD)V`aE#A~k{?P0a^Mu+#KVe~bis zGsyZoezjW&+^30*itq9E{%61(?i)cpiq|*)=kPW)XxqvH)n>oHsw`bd!11qG$3eXS zHI;|C6}a%A7Ivi@j>oI~bHuJ3*d30LslB~vDXrD{p?=!Cb7ZAOkka!ux#jOqi-q^cQqpu<(d>WGT}5VZ{TqMx znEZb{!0gOTz4U4ERHpO{<>o~DG>~T9sb8StpL#~Q8V_9N0r+4vH+>$z z%y;oqUau!T3uR=<4lDN0gBcux9aar2BAX|y^mu{!9uZd~dMXHnAubUUc6$n$UUyZf zPrJ)k+bvexjmCSoWM?-;nY$Th)yWnefm~j^e%ej0EE7NBqobtl5@)iT`K8?jer#7% z+xf$;_`pN;fV+?Npu3d|o(T#5X*ap`-hqFX;Ppof-mK(4-;uN%&fL5gXK^^{f%EU4Nv>gNsQ?yPy;oiNC|wbkCO?fP!!DGr5Q{1hK|;0qsi5KFgppt%n^ zi0pR8>C%@TS*FMdXmG%Ce!F;}DUdi!_zSIh>}BrlAH}gt&r9+%QOhXa$sy9T0)@9c74DKquER) z#E*s{(}NXiRJqccJ|`?!;P^$bB8&;c${4)x)V2;F5miZTws>Lau2-qV!#bo!K~h1ss-xn zdc@`z+kBJchQu++9KFXx=iYqDy?O6ih6~|x3uh%;9+RDitNcmKZ{F4X<{g{xx^g7h zX@i~bwCBRug2TXS)@id2xcuftvV6ab7St)D0?>U(D-7ZEcJU=ib*(Ri=z7N7=i+Nh zu<#|(&E9F6{+7JRxi*F?x{q73w?m8j`r>I%ZL*S=ZE{AiOjq;Eh+!#&eS>Ask>Ti| zbgi%;8og5OE2dww^2$!LYS~?RWrtt*nQEcSjgRI_Yo1Lr@2$9-hN|5hpIv#MH;(>P z-%1p)!BFSd5|jNk{re16rEf~l>99)ah4WV1VHF@(VTHVO_6o2d+YGD9P>v3IH(~~d z@BvSdjq&=0pgaPZjOBJU2|Hob>ucwgRnG>Cw(MgaE#~p`YiXLQTZm2=c49rTi}#d# zX6D5iGk@A7%adllyqerL^T+Qg*Ekn1DpzK{ce5XSPg%-`YHN67nI&k4E;DxN&w7hF zE;fJT%ja)=^ZU%f@0cyW!{x$lY`|e)HEYZ7nBsR#Bh-1n!{w$u=JIH*FNEk4zjG-* zaCnK|`3Q8A-{Eq2J1ciX<8r?^K|BJ*a*VPD~>uRzgZD5abegRNu&yW6xTsGBE$dUTrUp1q@FP6Sh4e!ODx1oTl zI-z#g_D{J$FVOXb?D_;Q8gbFAR_E=_gTMc|T;h)pg+_i0^e+bw*;77;sf%KjiG?hI z83;7AQ9UtZj#+~IJkS#(-z?YG4KgS!yzFs{XV=*4+o#nu9E0^dbRA91!ZJ|PAMjAp z-Lb^CDMcR{rpjxUM^Tl2F8e7zW)wf#J;v*b^7;%)Gh#HyTX6IE?k-mZ%($vuRV0nO z?W;igpP!E5Dj^xR(y|h5PLXmRwUAQZDOX*xdMF5Rh=DcXy-hc zBVrc3ZBag{VmLgcv6gOjqp?;bTdp9E41`^rHXO#rg%TcT3z5&_v56Q|vbPe)$~M0i z;BQWyjuLKG{y%s^pyn^LXsN>Elu-G8VRcSQWjm+khSW~J>f*H`{nb=U+Ur&ws;xY4 zP-C_TGer(-xg1K;N(|XIhB7l-ifBuR96H1-e9iTrb@mKx!KoHY*&(8}0~R}_2Hc(b zxI_$Ps%r6E z$=~JXvUKmUuU&dPs@i*;YW7^;97TJ+h+r)6>y1@e`Xbg=<#p4CK_7u*J+dZ*K7kTC zBIPnH$Fvk_=IS@PSe!J#&#Ln3WA10uD1MHs^4L(72bg759$Q!CQIBwXZy!(hEqZJ$fKV>5qJDG8;HY1lXjczon(3Ws_6P^|1@roz5JUfH!4J-K0R8#eAT!Li_=+~tz zKgqoDl`!dqG*?2RGpIHoFE~PUkti+~+7`Y>mO2!k0KbXa8owyWL{wtf zXuxMXesfN7PC$K$oxWk0?D7rU+~M->Q_2tRaQV*r0v`Hca7i9I%JJT`E}z8%aDV)k z%TrrE?Cggt$!RPlR|}W)!9pjxxR#vGlv&Z)YVu18u4uEKoPPu}8x;I)f1e>YNGXKs&)kMHwdD|ouEpg_Z4{SZw8SDF$tFz|dwXue z^bzLw^Q+>~pU?WTAAEsE`Z+yZ9ezs>9nNO160S$^wvSEoG(MTN-4L?!!2`{~@_%O# zw=f;E71tCjke0zxncG{^!+1e=%5&E$%o(x+UB>e6ya;zkGT+TMvesAPr|989EY$2E zmx^`Zi`q|_wPKuZeCa7wR?$F0ii7#N97J3kPH!&u>y-U}#K&snKH~!_#J1~cAByVdLH(z%D=++TYcup* z#-(5U!!23g@!izFPw+)P+~P8K{EN>~VxS}cWKD({VLT=~QTyX$gYF8*68XPmCJ_%2r&5PoHO$2q=8akT<& z)}iO+_%8EX|3pyd_afOqmCLfq`tJlj~lkX&u6kaCa zMNR(j7PxzV7arcfeept@n7Gs0NZoO-t&%#}&>GiS>0%UDc5n82ul8~;_Iyu!_QINE zd9c1qoifZw5}bs^6pQ~!*sGbC^E|a&w1KB^MS!CM$}Evr z+(i+%3Mz4{P0)&X>qOKV=(*ez7kk0>-0ivDbF=4q&($6S=;wUTY0uf7+@9>7%%1d~ z6euE06eCTkb*)!2CK-iDfg26t7$nh2EtC{j!t90K3$+(u1oQY_&}Xk|Ja5T_Rx6oE zGb_4i$Z5wk)2dDKO0vChdtrZvwIgSev~S^zd1Mw+wyu>f=r%|K`&UxzCErW>-6(*r z1=)63*0I*=7^Mm(IMF&6ybXnWsmlN5?@C7}nQfW0$#gA;T(q%KXv>1_+D?Wd2@s+G z5Na%TgSl3*4ksj~B(;WUI$=mT>zFUp*u6A=6hSUZ5xXFhRvwB$!nHzrkz7bJ2~icr z{joGDZ)D3|a$Lp8^HxP4S}&x6QDD|()lq7%T`5y&(*LbgLSW3;R!YVNjv$Z1D+)eAlwH7%7b@*nK&X$L3$i|NXSIwz zN*M(A4)&UOQX&(oX|J*A?(3j9ByGARrEXhgaEQs+1fSTZ&Uxls$_lF8-q7BZhPHbR z9`s%Vm)vWy*ZjYm2PTCSI(P=R#3d74tI%nN!|$BShYUW^$h{GJ!@qiFgn>)(#&&^4 zN|d~WMYE|xmZ`AW)tV?7h{ALVB+O~5H%)xJ2L^9x374s~fDQ~c! zE_U9kqVgg7BF8j+ZRRslAhb z7KRfGNhuMO51m(mxJfFf@U12|J{hy|bl_S4x!7jjBXUO}<))Mc6=vq>R zZTn~BTp-Jnhy=9ix&%&RhZCH9rxTJ+(j_h#dmo{TM5mXJcez$NxANF+uckRB_+q^5wNDOu6+R`X~)GO{X> ze51|3F~L}-JC&3WQE+HXD?7Lw#)5`r(MGTwO;Vmh;@cFEhmlnV=GHsYAr3{h%MBBj zd=xHNxT8EZ&jq5dmyLW~AA&dDb|FUNI%l<$Wc7><^=#91ZDdr~9&U|gj{9Iz zN-%ivmoZ2`XVQKPx@(=*tZjYkku*`{*lUDVj3`rCng5xvc!5Xr<` z5Zna~)s-A)(f6#-GhxT1j)H_m@vQT~wfS#YbjdrBR1ocO9D(imu+(Z6T`*iB_K;nY z+ToN59hrz$li*i`1xe5PbS0|TSE%oO9xxm5t%luk$o1JBT?z+?i_0G7|gm%GUQK?0@)}%^QJYnOG^o;m%OSDKVgQ`dMGn)ef3LamZ47W1Bm;A#TSy}%jI2|Bm@9cbdGgM{k;_-+Q4n6ql7o{B0^D1 zAqF9`BWJ%_9zxeDxEd8LB_WOUl8e-7m^=|#lEvb2#=d$!I`~29I)*p~ylCGcka78? zCu^k>&?U^`2)H>zT){-&rmvbOt*Lb|F%+5eQfiVh1qz)_EP58(%9DC_d^xTVLZub~ zbqX?Pfo+>amzeY+1>-7T`dRW8UCV-L5lSZCIv%Z%ow5ihR7rk%-kvXih@Dd#IKn^R z=~%0DzTfkVlJ(LjQTeman#TwRTh~VIB2-mH-%4zzO^yXPdaf&v?%DH+fWdpOJm}Q| z$vWaoxZi9*k#-sFDhkIe+HJlwG=h);ILIRJUI>OI8U*&R)MkN?n>SXUUKG% z)RQB3<48U^WpRLSByb$*CrAFt>3Q)VbwY5}N!VO4oTDzDI;4C$hBhdtO6t#%w<1Nv zKQN!u@|>6F#5`x_IW^C@`AGpiKY?gs$jOyL%p)ZtXHvn&ASngTI*Otf2$&Z6LPC5~ z!b!+;grLBLv>KspCrv<561ir~cSr)c1Y;7+OE532?0n5KtKQjaAGDT zq5rf;jO&2qdA>>j0M_WNLL?njs}Tx#e#JonR{#eYTtNT|0+8;T5RT_25hWIooZ`nC z<0+^P(XHrAvZcrpF87<2kLs9DK`2;bX&j}_wWjTIi6ga9NvbDK>2Fp*AqYfe3?!28 z3}Q~xMbD-0v}HayL%Oq0TH7hn8qPg&nKUD>Tyn%x?1d)& z65QIBSr66_RJD<_q@rfX>bz{T2AZh4UT|O#sI$EOlHu_!GD!e?ub4yfXDNCW1d~BV z?X-|>4ZpB7$I={2Bg}{JvM}vbpTTv0iLF1#%^&ri#YvwGi%v4fV^_W=X(LQIGuUTr zf7J|wZ8P$Dah7z{WPQFKhv(M$9e0vW2?Fpne2EgIxK00R?epA zgb2p>+?nUgp(UQ2(V^>9eb+4mQs-PMmO2$f_xw2&E@&>C>R_Ikj4gMOGy(ugowJ?k TV*q2HH<$k(r>HwA(~tlF;wDP` literal 7117 zcmV;;8#3e{iwFP!00000|Lt7sZydRi|E|A6-*UG`02bdo#0w0JHAcW90q%mveTu*) z*&FT28b^{h$$x)8lKq}(dHhN&?=DuJZn9XcDi-TO*35r=clq#F|292b{*vw=ZVq?< zb*V4E`_GHVzxkWHUmEthf1-wlN8a$^Q8Z$Bl#P6S;s5Z`-=@2t9{=ir_4fAg_v<%@ zm~I>89}m|zcaQ$f?tg!`D+t#RR~5G!5UNJMzPRx(@f_1Xu5S-N-30%a#x$fFcjf

q^6jCrK$%6~sTZ=-wy(Z-mo%?;3IqXH`=; z+n|fwrsnX57zQ4xPDM=1HoV=X`!a&cgtUpX*C9@uI+V%U9G-P*bI=*vVFm?4H>Y_& zssgn&#}!yxFEd&HaCZntz;;^0VWDlc1sHVEyt?cT_m}rKKmGOb`mK+rEP{X0knz9& zV5L0X|EBE!C$zZke{8VdL^)J^2T1Tuu$w{l?X6rQ>SY zK>Ebi%tOt_*7U#6eMjiZG+XR*D*Ask2qVhuM;#k0Pg@p26pOI6S)UlRZ3i&u3_CD` z+Oh-UEIS~!?LfALFN?I~>+&T1UHW^&MSk<|fLF`kW$aw|7l9Tn{B_ok>-O;OEyY?YrU@OT&6y&C{14`4l;n89thGz$7IYw@EOCOk>!akTd^}5=HWpCk(@?;?I?foIX z3+W-pVlT3FuiktxEN*y!y`Dhr05lt2hT1tsD1LhL_VJ(D0}nzGS>J{inH6++;aPVt zwm0a=X-w&DuL0RaRdFpEvoV_*76Am+?%v{UO*J=sS(}#Vd(Gg`w)u82{eD1CRUS1w z=xoFa?7O?0zr9N{blm@v!bMT4@yYpgo8DwmT-&^j{h!~xy-n<5uZ*F*V&D4sR#c@O1MyseAQ)69x5koTw6$)yn^jPyh3vd`q~CKZ3ex zvBX?=`GoD~;{`oyAe7r34K16&ou-F|t>9h{vi{Crb9*k|G=SH&A^(@*HMg6o7a!!? z!~Ol??&-K&wc+L`EH}@i(i1pK@b*OiXaJrfD=h+z zy4R;HWyvb!Kha!!^^Je+Zy%EX^F55s+`vnp7H?%p&qjWnD4sgftU2`) zRQz*4N^3s{e~eh+7hi*d^Xxt!Oy#Dh@Ld@uHyn1w?;Yw+*nOzi+^yX1Oh)iYyUCUJPWzMO zu0B}qdL{SSf~4KB;bx84hr4Nm?mm2b?`HO5_u=MdPRge3e%cQ1p0uL76LxpEHqN`X z`QFVO!lAt3qqwpIU%0A+SbC=e&0WnwWbZN#7rwOAAz}g={H&Ot{T*nE7Y-9}p*8ot z$gTaWIQHCmO8!JJGoOjqEeO`m@uVC2zI%Vv_Edg&WWG+q*1mJ&+Y=kEM{p+WDlb9w zzS|%xL$0Yhck~LdAlq$Nc643MOlhO4GTZWSY(*PICyb~-bET$OP`qI*Ff7ey9$Ty@ z=KP@mP@~un#eCu+pSI@qZToqO|M3`D%JGFavNu9#cIVm6CvaEkWtrrMVfPRGx-}Wa z$~AhjM6ywXO)O7ivt~ncetL;9n}!k+c8gbC1cwhyUxn#bhB9-sw3CgpVL_G{$r2R> z9)6gd1>k$jR-OO=wJ>!yQ%+u$F3X3{Mss{f*fKrXu11x^yV<***)sH^>-9KX_|j5r znHCdJZ_D)DmSMnX%K$Py$shCK9?;~c%Ce+7gA6^F6L6p(XNh#~JgGm0UC~<{y#LVW zm47dNgPUwh(14~!+8_GC!vQf=E!{u%TKzeWh~;~Zh}CpNEc2!JaI|ZmIC&gTMrMbA z?!>vH%g6H@$Bw159N2E1;Je|>men&ywLpDUx7qvzns1WakT@opqxG2R+?r3LH&07T zcOhJE;jCoKW3qF1l|PC35xJTlkz)~FRgUC_(awj@b75@3p<^}bv}p%iz9NyV;Wl57 zK%Fuw0NsVO!Vpd`7hjT8=lV>Du4c@ADn4+y`@HC8myf1D+b(jh55u9{hfUerqs1w^ zk{gSxHeBeJ!)d)FQcp+z3rn;6w5EVByJY5wR1ea3o)->G-O zxA<6Dbvu~o!J50NtA+yOyDJxOWABgkE}?)81{?9nWQUdMZy{8bz9}uILo2no4Ji|E zgjRrDg%RnG>C zHqCnJE#~p`{V`2tC`2a=JF%YF#f2iDnR)SqnLllkS@2j<)%I6@@THlgyQoy4} z=c32dz*WDa_0&}pmhoNB{f<_>-zi{&-w}G|ceL#Nj+VROVaxAmvGg2v)9(QC$nTsv zdIeaJZTcN82ESu_zvI7u*@(cdZhZO7|003P1u%l=0+?(_8`z_qUjP)^^Mn6B*Ecm3 za-{x;m(A$!i=}T=!+Y`PWhkJk4yeub`Nv#I7wBq2c69<5jksu5RP*Ng-rxOH4)Dj9 zLL?xna)JZYR#6p(93x{T?r+d~dA9ZA#*tVXC}lc@$OY=lY!TVMg)exyN`_QC>ZP z(u^3*@e*7=yuHme05h&?Qx!?$Zu;7d{^Q4ExJpQdt+cE}n^UBmM=hk(H_BC$EcsRz z!+1(ir0}wK)u*{LFDYd9n=?FWw2vhscsbQ*mQ-nJ;8R52Xx(^&L2JJDDxk}XFNM+U+!b{jTh z<3b6KvxUfe@z_KRD%o3!V`ZBk3-H&cc1H;}EC27^AyD%dS+rE)u}i3Y(O|VtN(nlr z<$}~kzG~vNbo}L1^x5lH?W#|C+@Qv65oU@U)^eFEXSwOa_x_<&memH;H^`wu%)-}F zgH{I3&=#C(F_j%6T03B|Q)*C3a<-1l#86L48;529xQWA2?fM%cg7se!5p1J^QEcTq z^+sn^!6?d&&OC7{Ez1j?1^jSP!-opIMQykl_7 z)KfL!TVGN+on*hsV}+c+?}D?hhpIag2p{R4Y|4S+*pS9dF1udzqz@)z8Q45 zo*$tl-eeX1w1xa2JWr_AC*#4m%HRgf=nt-iS#RK1*Z-Yo%$L|=C^tN6n{RAdc2}LE ze&p~nmE+P_k6YVENz%LkccZe1*5aobre1nr{$mz$v630bYB6&8(&$FB3T+8@H{n@9 z9?y7U$+I)qUa*4iiAt)TjdQSU0sXv`p*2XNlr` zp>5%7WVw@-VvCExFN@dx&VXrD{Cq{{!+_ps7eiX#a|cb`_&BoKLs3D6DJSJYNGXKs zPh5s4s>vY?UCYUp+9)SKYl=lYl1-W__V%d()3+smKR+rS{rRjd`@su5q@U9L<>8lf z-(hd&65+Z9Z~E9Y595E99>xQ@Q=YpP zWX_Ns=scEpPm6GOB=g;DA#156K8hY5#6ryua;aDcz9<8gSu4ij#+R1zU2|zBpkbSs zMHwicm4S{H{~-E;&0Gd5hgW%G=jA!YQ&wp{m*@*Y#d*8nJX3pQu1)bQ^DhAV!)QCw z?c+oBs@H}u>g)b6ACQqO#`hy?^?f4&WFT`Uz6 zBonzEG-2+G7bVjk@BkBOMYDq`mE%|H103CPxWe8h=3ik}q+^QUqUadtSpIoZ!s z_WuE2Pb2pUUztK|yB_wwsD2*QfBd}i%&%%~hMvo~^s|3eOV&HS>-s|ipXIAsT;_&< z(34-oI%ypG!=G8pKWJqK3J5=E*mx9q{^8m9Wv1nE)W__3eslfCB<(ViY|L;UW$Q0F^}k7B)EQIlCS#Q+K7BnP`P@>?;O6s>KZP+A{x;Ii zsIhWWWWc|!@5m@u1sU3meT~t53A@qxyxq#iPCuGa)dnpK#cB*KdRIT7@f75bqdUs7 zoBaxh$rn(|hPmeibfK<(-Do#G*49n$ozcwREL;B`h-Is3N~wu)jj^w<=3y#ypfRNw z-^g5RQW}U2EygaQ(A=|-LxDqMYV+M#T;XbMJ}|klHs6RkORmj#^V)p3tj!;8fxCCN;r`v5iwkXH;!bNLb;rH7 zO6p)kYg}igi&0$Kz1i!%+RMGz^F8g^g*D0YV11W5Wtfp9I0=g(7XL}vT@u^7)flZT zlPU?`2`h=~R<*wKJhfc3fv0dufTIE`xXxwqphIdMHPCisS)`7%m4+lh8DQO>_DEJ=r~(J?T9ukVA4$Vj?I=3P~~TwKJ`uPH`221Y6M?*`-UN z_d@LjSim5@7ql1b)28ff;xZZEDdmLi1P41xHTQHr(L zKZ2>?S_vn`btf(*?Ip|q3-`I_mLX^|q>^hr(=Ir}xZ`B0^Z19^%yFKZe=!Pz5ZKFF zTCS4kom0XZ4+^;OnpqJG1#&ON7bSvpD}BPQ3Rv&tK?HA!X_7`@2egF<_2ua>x>HcW zHnyP^l9Y-`b8m!KZL7WUSrrui$MkM5L6g}_{e@`~-l;@MdfnO91<#SFLoU)#X)tS&)YKHi^&$nJH89-$Y#Oh={qMb!eS35r14U!A%T? zjE#jjPzEck{(V#?(^}n{F7aU6;B^~y#KwmlxgsZ0Ryd7e@G!bO$h{VO&G#DZY_Hs2 z*?$M!L1+;I40Q5VYoAS~_0kDajFYq~I|sw|8eYzRl?))(6L79J1kSMOIcFR}iuIa= z58hF>I7aS`*c-k#^mQ}iyBNSl$BmYqwD8<4A!dLF6RM-i3}$*Z{HRt$VT5w9aLQsc zFz^(xIVkDSMV)trfr6=L!VmFQa)%($=O9uA5oBtib1o|Qy`=kHZlH2s9qBQ4u}cZo z(+VVlx`lHN%90=!6xmF=)qAVpAZL)g7(FNUjz51^+tx&{D0Bj$l`+~P_hV37#9U4?qYJC@Tj93zR;rM= zva(~EM;`)Xrq!f6C896Z(m{dMH^D7a4(tWhc}c{LON5LtSi_`frC_0Oi{&-n5YL@r zj75v2!N3`68$3g{X^hYjrr5AcVgO`>Kel)7o8zB%UL)W{m+o-z4J@Ubpf?%!HqP4#3wCp0y7?aJq1*PFC+D^7HpBK5rZGzn$^wNCA zEO2I+bH;g#m_a5kqwWmIjJz`~ntK-PSI$POS#$`06mRpb8k|39Mj*^Yw3-CJq-^75 z{sS(|Pe}Gi09|$iAcjQ72UfEaz}%RFFhBA9N|O=QtqI7eB0Nf9mM0TpjIAL=UHL|{ z&I4`;>=5`tGJ-!{=;!Jw)ZQ_IIwcwM7fAvkJ@w3E5p0{hXvHN#ge3We>LQOJdXbz# zf}@$}LNXB{ufcdJ0f;$e77=EW@&W`a-wf!&1HYI&!UBWx3db`D_z zAxyT&K0yaVEmEq%Va~O?q zhg^QfEY_XH$Csu*hR(6B^A>qkh&FKB=_uh{yogX#U+71qhHdoK@_=kn!POvop(Lb{ zUUHE-4U;D#OR`!#r@wkWI`~29I@To*UbOEJMI#^xks%%v(4{;I;WKABmT={n5KDi} zJZVk2j>b@A&P%CD#uO-YHnHegY%@V(qvyKvsGdEa2pGKg%7X_jv}TAe;eN9LMcRS*zw(KM zjFs}9Z-HfREk(^cIBXRSPfmkc&Qt8HRp2$dJDzJkDSv`>q?;TG8%Mgyk#BO!2`MsC zLc+=b$DSAeQ6~gforKK=!#V2WsRNjfp$*EZlJ4`Ihv!5*XW}^(&$)O>#=(3}$B~bp z6wosih$ekkqeUP{`K2b7U}Y%ezh>_(g&(;QN^o zM!Q~6`Zr-^+oY_sJRfWcEq!!}SZreo4&jms`2x8J%lsy=@pjiMD>e7p$X3Kw5;!sf zQI(5Y2G$GA{wB2f;gIgElh$@hw1#s}Tqe!PE0-Lx6nmk$-vqa|W!8gD1XXS1EUBm& zvN|u@tbrz~t_lvQdA_Jszsc}~47*%8n2Rx(L-J=SdKCndK}PMgkZldWFg3^2T<5!L z2mn)aOg+|HaL~Xr4PVJUi_7)SEIP>?j~&M=ZzD`OGgxbAMAZy~Wi#w~ah7z{WPLs! zhv(M$j=M`t7{PdJW7Iuo&y+jTu~l7)Om@5#9Z0Z3D`!)5LImS`?!@!u&=OD1=+Jel z-gV1>)HwuiQm10*o Date: Mon, 16 Oct 2023 16:50:15 +0200 Subject: [PATCH 6/8] Fix prover version --- creusot/tests/should_succeed/hillel/why3session.xml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/creusot/tests/should_succeed/hillel/why3session.xml b/creusot/tests/should_succeed/hillel/why3session.xml index 2e22c83cf4..738919c0ad 100644 --- a/creusot/tests/should_succeed/hillel/why3session.xml +++ b/creusot/tests/should_succeed/hillel/why3session.xml @@ -4,10 +4,10 @@ - + - + From bb201f5461e26e10beb8c02cf7d4ec748a4b840c Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Wed, 18 Oct 2023 12:11:39 +0200 Subject: [PATCH 7/8] Deny borrowed variables in loop invariants --- creusot/src/translation/function.rs | 1 + creusot/tests/should_succeed/hashmap.mlcfg | 215 +++++++++--------- creusot/tests/should_succeed/hashmap.rs | 1 - .../should_succeed/hashmap/why3session.xml | 168 +++++++------- .../should_succeed/hashmap/why3shapes.gz | Bin 9919 -> 9859 bytes 5 files changed, 190 insertions(+), 195 deletions(-) diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs index ee1f5149aa..1463726d9a 100644 --- a/creusot/src/translation/function.rs +++ b/creusot/src/translation/function.rs @@ -167,6 +167,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> { &self.locals, *self.body.source_info(bb.start_location()), )); + self.check_ghost_term(&body, bb.start_location()); match kind { LoopSpecKind::Variant => self.emit_statement(fmir::Statement::Variant(body)), LoopSpecKind::Invariant => { diff --git a/creusot/tests/should_succeed/hashmap.mlcfg b/creusot/tests/should_succeed/hashmap.mlcfg index 3f6a723c02..f86ab5c13f 100644 --- a/creusot/tests/should_succeed/hashmap.mlcfg +++ b/creusot/tests/should_succeed/hashmap.mlcfg @@ -636,7 +636,7 @@ module Hashmap_Impl5_GoodBucket_Stub use prelude.Int use Hashmap_List_Type as Hashmap_List_Type use Hashmap_MyHashMap_Type as Hashmap_MyHashMap_Type - predicate good_bucket [#"../hashmap.rs" 201 4 201 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) + predicate good_bucket [#"../hashmap.rs" 200 4 200 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) end module Hashmap_Impl5_GoodBucket_Interface @@ -645,9 +645,9 @@ module Hashmap_Impl5_GoodBucket_Interface use prelude.Int use Hashmap_List_Type as Hashmap_List_Type use Hashmap_MyHashMap_Type as Hashmap_MyHashMap_Type - predicate good_bucket [#"../hashmap.rs" 201 4 201 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) + predicate good_bucket [#"../hashmap.rs" 200 4 200 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) - val good_bucket [#"../hashmap.rs" 201 4 201 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) : bool + val good_bucket [#"../hashmap.rs" 200 4 200 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) : bool ensures { result = good_bucket self l h } end @@ -672,11 +672,11 @@ module Hashmap_Impl5_GoodBucket type t = DeepModelTy0.deepModelTy clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = v - predicate good_bucket [#"../hashmap.rs" 201 4 201 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) + predicate good_bucket [#"../hashmap.rs" 200 4 200 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) = - [#"../hashmap.rs" 202 8 204 9] forall v : v . forall k : DeepModelTy0.deepModelTy . Inv0.inv v -> Inv1.inv k -> Get0.get l k = Core_Option_Option_Type.C_Some v -> BucketIx0.bucket_ix self k = h - val good_bucket [#"../hashmap.rs" 201 4 201 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) : bool + [#"../hashmap.rs" 201 8 203 9] forall v : v . forall k : DeepModelTy0.deepModelTy . Inv0.inv v -> Inv1.inv k -> Get0.get l k = Core_Option_Option_Type.C_Some v -> BucketIx0.bucket_ix self k = h + val good_bucket [#"../hashmap.rs" 200 4 200 57] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (l : Hashmap_List_Type.t_list (k, v)) (h : int) : bool ensures { result = good_bucket self l h } end @@ -685,15 +685,15 @@ module Hashmap_Impl5_HashmapInv_Stub type v use prelude.Borrow use Hashmap_MyHashMap_Type as Hashmap_MyHashMap_Type - predicate hashmap_inv [#"../hashmap.rs" 210 4 210 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) + predicate hashmap_inv [#"../hashmap.rs" 209 4 209 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) end module Hashmap_Impl5_HashmapInv_Interface type k type v use prelude.Borrow use Hashmap_MyHashMap_Type as Hashmap_MyHashMap_Type - predicate hashmap_inv [#"../hashmap.rs" 210 4 210 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) - val hashmap_inv [#"../hashmap.rs" 210 4 210 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) : bool + predicate hashmap_inv [#"../hashmap.rs" 209 4 209 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) + val hashmap_inv [#"../hashmap.rs" 209 4 209 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) : bool ensures { result = hashmap_inv self } end @@ -729,9 +729,9 @@ module Hashmap_Impl5_HashmapInv val Max0.mAX' = Max0.mAX', predicate Inv1.inv = Inv1.inv, axiom . - predicate hashmap_inv [#"../hashmap.rs" 210 4 210 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) = - [#"../hashmap.rs" 211 8 214 9] 0 < Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets self)) /\ (forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets self)) -> GoodBucket0.good_bucket self (IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets self) i) i /\ NoDoubleBinding0.no_double_binding (IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets self) i)) - val hashmap_inv [#"../hashmap.rs" 210 4 210 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) : bool + predicate hashmap_inv [#"../hashmap.rs" 209 4 209 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) = + [#"../hashmap.rs" 210 8 213 9] 0 < Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets self)) /\ (forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets self)) -> GoodBucket0.good_bucket self (IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets self) i) i /\ NoDoubleBinding0.no_double_binding (IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets self) i)) + val hashmap_inv [#"../hashmap.rs" 209 4 209 33] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) : bool ensures { result = hashmap_inv self } end @@ -1752,9 +1752,9 @@ module Hashmap_Impl5_Add var v : borrowed v; var tl : borrowed (Hashmap_List_Type.t_list (k, v)); var tl1 : borrowed (Hashmap_List_Type.t_list (k, v)); - var _39 : bool; + var _38 : bool; + var _45 : borrowed (Hashmap_List_Type.t_list (k, v)); var _46 : borrowed (Hashmap_List_Type.t_list (k, v)); - var _47 : borrowed (Hashmap_List_Type.t_list (k, v)); { goto BB0 } @@ -1807,13 +1807,12 @@ module Hashmap_Impl5_Add goto BB7 } BB7 { - invariant { [#"../hashmap.rs" 114 20 114 46] ^ Ghost.inner old_self = ^ self }; - invariant { [#"../hashmap.rs" 115 20 115 52] GoodBucket0.good_bucket ( * Ghost.inner old_self) ( * l) (UIntSize.to_int index) }; - invariant { [#"../hashmap.rs" 114 8 114 48] GoodBucket0.good_bucket ( * Ghost.inner old_self) ( ^ l) (UIntSize.to_int index) -> GoodBucket0.good_bucket ( * Ghost.inner old_self) ( ^ Ghost.inner old_l) (UIntSize.to_int index) }; - invariant { [#"../hashmap.rs" 114 8 114 48] Get0.get ( ^ l) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some val' -> Get0.get ( ^ Ghost.inner old_l) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some val' }; - invariant { [#"../hashmap.rs" 114 8 114 48] forall i : DeepModelTy0.deepModelTy . Inv5.inv i -> Get0.get ( ^ l) i = Get0.get ( * l) i -> Get0.get ( ^ Ghost.inner old_l) i = Get0.get ( * Ghost.inner old_l) i }; - invariant { [#"../hashmap.rs" 119 20 119 44] NoDoubleBinding0.no_double_binding ( * l) }; - invariant { [#"../hashmap.rs" 114 8 114 48] (forall i : DeepModelTy0.deepModelTy . Inv5.inv i -> Get0.get ( * l) i = Get0.get ( ^ l) i \/ i = DeepModel0.deep_model key) /\ NoDoubleBinding0.no_double_binding ( ^ l) -> NoDoubleBinding0.no_double_binding ( ^ Ghost.inner old_l) }; + invariant { [#"../hashmap.rs" 114 20 114 52] GoodBucket0.good_bucket ( * Ghost.inner old_self) ( * l) (UIntSize.to_int index) }; + invariant { [#"../hashmap.rs" 114 8 114 54] GoodBucket0.good_bucket ( * Ghost.inner old_self) ( ^ l) (UIntSize.to_int index) -> GoodBucket0.good_bucket ( * Ghost.inner old_self) ( ^ Ghost.inner old_l) (UIntSize.to_int index) }; + invariant { [#"../hashmap.rs" 114 8 114 54] Get0.get ( ^ l) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some val' -> Get0.get ( ^ Ghost.inner old_l) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some val' }; + invariant { [#"../hashmap.rs" 114 8 114 54] forall i : DeepModelTy0.deepModelTy . Inv5.inv i -> Get0.get ( ^ l) i = Get0.get ( * l) i -> Get0.get ( ^ Ghost.inner old_l) i = Get0.get ( * Ghost.inner old_l) i }; + invariant { [#"../hashmap.rs" 118 20 118 44] NoDoubleBinding0.no_double_binding ( * l) }; + invariant { [#"../hashmap.rs" 114 8 114 54] (forall i : DeepModelTy0.deepModelTy . Inv5.inv i -> Get0.get ( * l) i = Get0.get ( ^ l) i \/ i = DeepModel0.deep_model key) /\ NoDoubleBinding0.no_double_binding ( ^ l) -> NoDoubleBinding0.no_double_binding ( ^ Ghost.inner old_l) }; goto BB8 } BB8 { @@ -1837,13 +1836,13 @@ module Hashmap_Impl5_Add assume { Inv8.inv ( ^ tl) }; tl1 <- tl; tl <- any borrowed (Hashmap_List_Type.t_list (k, v)); - _39 <- ([#"../hashmap.rs" 124 15 124 24] Eq0.eq ( * k) key); + _38 <- ([#"../hashmap.rs" 123 15 123 24] Eq0.eq ( * k) key); goto BB11 } BB11 { assert { [@expl:type invariant] Inv9.inv k }; assume { Resolve3.resolve k }; - switch (_39) + switch (_38) | False -> goto BB13 | True -> goto BB12 end @@ -1866,25 +1865,25 @@ module Hashmap_Impl5_Add assume { Resolve1.resolve l }; assert { [@expl:type invariant] Inv12.inv self }; assume { Resolve8.resolve self }; - assert { [@expl:assertion] [#"../hashmap.rs" 126 32 126 52] HashmapInv0.hashmap_inv ( * self) }; + assert { [@expl:assertion] [#"../hashmap.rs" 125 32 125 52] HashmapInv0.hashmap_inv ( * self) }; _0 <- (); goto BB20 } BB13 { assert { [@expl:type invariant] Inv10.inv v }; assume { Resolve4.resolve v }; - _47 <- Borrow.borrow_mut ( * tl1); - tl1 <- { tl1 with current = ( ^ _47) }; - assume { Inv2.inv ( ^ _47) }; - _46 <- Borrow.borrow_mut ( * _47); - _47 <- { _47 with current = ( ^ _46) }; + _46 <- Borrow.borrow_mut ( * tl1); + tl1 <- { tl1 with current = ( ^ _46) }; assume { Inv2.inv ( ^ _46) }; + _45 <- Borrow.borrow_mut ( * _46); + _46 <- { _46 with current = ( ^ _45) }; + assume { Inv2.inv ( ^ _45) }; assert { [@expl:type invariant] Inv3.inv l }; assume { Resolve1.resolve l }; - l <- _46; - _46 <- any borrowed (Hashmap_List_Type.t_list (k, v)); - assert { [@expl:type invariant] Inv3.inv _47 }; - assume { Resolve1.resolve _47 }; + l <- _45; + _45 <- any borrowed (Hashmap_List_Type.t_list (k, v)); + assert { [@expl:type invariant] Inv3.inv _46 }; + assume { Resolve1.resolve _46 }; assert { [@expl:type invariant] Inv11.inv tl1 }; assume { Resolve5.resolve tl1 }; goto BB7 @@ -1915,7 +1914,7 @@ module Hashmap_Impl5_Add assume { Resolve1.resolve _19 }; assert { [@expl:type invariant] Inv12.inv self }; assume { Resolve8.resolve self }; - assert { [@expl:assertion] [#"../hashmap.rs" 134 24 134 44] HashmapInv0.hashmap_inv ( * self) }; + assert { [@expl:assertion] [#"../hashmap.rs" 133 24 133 44] HashmapInv0.hashmap_inv ( * self) }; _0 <- (); goto BB20 } @@ -1987,15 +1986,15 @@ module Hashmap_Impl5_Get_Interface clone Hashmap_Impl5_HashmapInv_Stub as HashmapInv0 with type k = k, type v = v - val get [#"../hashmap.rs" 142 4 142 43] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (key : k) : Core_Option_Option_Type.t_option v - requires {[#"../hashmap.rs" 137 15 137 33] HashmapInv0.hashmap_inv self} - requires {[#"../hashmap.rs" 142 16 142 20] Inv0.inv self} - requires {[#"../hashmap.rs" 142 22 142 25] Inv1.inv key} - ensures { [#"../hashmap.rs" 138 14 141 5] match (result) with + val get [#"../hashmap.rs" 141 4 141 43] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (key : k) : Core_Option_Option_Type.t_option v + requires {[#"../hashmap.rs" 136 15 136 33] HashmapInv0.hashmap_inv self} + requires {[#"../hashmap.rs" 141 16 141 20] Inv0.inv self} + requires {[#"../hashmap.rs" 141 22 141 25] Inv1.inv key} + ensures { [#"../hashmap.rs" 137 14 140 5] match (result) with | Core_Option_Option_Type.C_Some v -> Map.get (ShallowModel0.shallow_model self) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some v | Core_Option_Option_Type.C_None -> Map.get (ShallowModel0.shallow_model self) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_None end } - ensures { [#"../hashmap.rs" 142 33 142 43] Inv2.inv result } + ensures { [#"../hashmap.rs" 141 33 141 43] Inv2.inv result } end module Hashmap_Impl5_Get @@ -2223,15 +2222,15 @@ module Hashmap_Impl5_Get function DeepModel0.deep_model = DeepModel1.deep_model, function HashLog0.hash_log = HashLog0.hash_log, type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy - let rec cfg get [#"../hashmap.rs" 142 4 142 43] [@cfg:stackify] [@cfg:subregion_analysis] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (key : k) : Core_Option_Option_Type.t_option v - requires {[#"../hashmap.rs" 137 15 137 33] HashmapInv0.hashmap_inv self} - requires {[#"../hashmap.rs" 142 16 142 20] Inv0.inv self} - requires {[#"../hashmap.rs" 142 22 142 25] Inv5.inv key} - ensures { [#"../hashmap.rs" 138 14 141 5] match (result) with + let rec cfg get [#"../hashmap.rs" 141 4 141 43] [@cfg:stackify] [@cfg:subregion_analysis] (self : Hashmap_MyHashMap_Type.t_myhashmap k v) (key : k) : Core_Option_Option_Type.t_option v + requires {[#"../hashmap.rs" 136 15 136 33] HashmapInv0.hashmap_inv self} + requires {[#"../hashmap.rs" 141 16 141 20] Inv0.inv self} + requires {[#"../hashmap.rs" 141 22 141 25] Inv5.inv key} + ensures { [#"../hashmap.rs" 137 14 140 5] match (result) with | Core_Option_Option_Type.C_Some v -> Map.get (ShallowModel0.shallow_model self) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_Some v | Core_Option_Option_Type.C_None -> Map.get (ShallowModel0.shallow_model self) (DeepModel0.deep_model key) = Core_Option_Option_Type.C_None end } - ensures { [#"../hashmap.rs" 142 33 142 43] Inv6.inv result } + ensures { [#"../hashmap.rs" 141 33 141 43] Inv6.inv result } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : Core_Option_Option_Type.t_option v; @@ -2252,25 +2251,25 @@ module Hashmap_Impl5_Get goto BB0 } BB0 { - _8 <- ([#"../hashmap.rs" 143 27 143 37] Hash0.hash key); + _8 <- ([#"../hashmap.rs" 142 27 142 37] Hash0.hash key); goto BB1 } BB1 { - _10 <- ([#"../hashmap.rs" 143 49 143 67] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets self)); + _10 <- ([#"../hashmap.rs" 142 49 142 67] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets self)); goto BB2 } BB2 { - _12 <- ([#"../hashmap.rs" 143 27 143 67] _10 = ([#"../hashmap.rs" 143 27 143 67] (0 : usize))); - assert { [@expl:remainder by zero] [#"../hashmap.rs" 143 27 143 67] not _12 }; + _12 <- ([#"../hashmap.rs" 142 27 142 67] _10 = ([#"../hashmap.rs" 142 27 142 67] (0 : usize))); + assert { [@expl:remainder by zero] [#"../hashmap.rs" 142 27 142 67] not _12 }; goto BB3 } BB3 { - index <- ([#"../hashmap.rs" 143 27 143 67] UIntSize.of_int (UInt64.to_int _8) % _10); + index <- ([#"../hashmap.rs" 142 27 142 67] UIntSize.of_int (UInt64.to_int _8) % _10); _8 <- any uint64; _10 <- any usize; assert { [@expl:type invariant] Inv0.inv self }; assume { Resolve0.resolve self }; - _14 <- ([#"../hashmap.rs" 144 21 144 40] Index0.index (Hashmap_MyHashMap_Type.myhashmap_buckets self) index); + _14 <- ([#"../hashmap.rs" 143 21 143 40] Index0.index (Hashmap_MyHashMap_Type.myhashmap_buckets self) index); goto BB4 } BB4 { @@ -2280,7 +2279,7 @@ module Hashmap_Impl5_Get goto BB5 } BB5 { - invariant { [#"../hashmap.rs" 146 20 146 101] Get0.get (Bucket0.bucket self (DeepModel0.deep_model key)) (DeepModel0.deep_model key) = Get0.get l (DeepModel0.deep_model key) }; + invariant { [#"../hashmap.rs" 145 20 145 101] Get0.get (Bucket0.bucket self (DeepModel0.deep_model key)) (DeepModel0.deep_model key) = Get0.get l (DeepModel0.deep_model key) }; goto BB6 } BB6 { @@ -2300,7 +2299,7 @@ module Hashmap_Impl5_Get assume { Resolve1.resolve l }; assert { [@expl:type invariant] Inv2.inv k }; assume { Resolve2.resolve k }; - _25 <- ([#"../hashmap.rs" 148 15 148 24] Eq0.eq k key); + _25 <- ([#"../hashmap.rs" 147 15 147 24] Eq0.eq k key); goto BB9 } BB9 { @@ -2431,12 +2430,12 @@ module Hashmap_Impl5_Resize_Interface val Max0.mAX' = Max0.mAX', predicate Inv1.inv = Inv3.inv, axiom . - val resize [#"../hashmap.rs" 162 4 162 24] (self : borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v)) : () - requires {[#"../hashmap.rs" 157 15 157 41] Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) < 1000} - requires {[#"../hashmap.rs" 158 15 158 36] HashmapInv0.hashmap_inv ( * self)} - requires {[#"../hashmap.rs" 162 19 162 23] Inv0.inv self} - ensures { [#"../hashmap.rs" 159 14 159 35] HashmapInv0.hashmap_inv ( ^ self) } - ensures { [#"../hashmap.rs" 160 4 160 74] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> Map.get (ShallowModel1.shallow_model ( ^ self)) k = Map.get (ShallowModel2.shallow_model self) k } + val resize [#"../hashmap.rs" 161 4 161 24] (self : borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v)) : () + requires {[#"../hashmap.rs" 156 15 156 41] Seq.length (ShallowModel0.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) < 1000} + requires {[#"../hashmap.rs" 157 15 157 36] HashmapInv0.hashmap_inv ( * self)} + requires {[#"../hashmap.rs" 161 19 161 23] Inv0.inv self} + ensures { [#"../hashmap.rs" 158 14 158 35] HashmapInv0.hashmap_inv ( ^ self) } + ensures { [#"../hashmap.rs" 159 4 159 74] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> Map.get (ShallowModel1.shallow_model ( ^ self)) k = Map.get (ShallowModel2.shallow_model self) k } end module Hashmap_Impl5_Resize @@ -2700,12 +2699,12 @@ module Hashmap_Impl5_Resize function ShallowModel0.shallow_model = ShallowModel4.shallow_model clone CreusotContracts_Resolve_Resolve_Resolve_Interface as Resolve0 with type self = Ghost.ghost_ty (borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v)) - let rec cfg resize [#"../hashmap.rs" 162 4 162 24] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v)) : () - requires {[#"../hashmap.rs" 157 15 157 41] Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) < 1000} - requires {[#"../hashmap.rs" 158 15 158 36] HashmapInv0.hashmap_inv ( * self)} - requires {[#"../hashmap.rs" 162 19 162 23] Inv3.inv self} - ensures { [#"../hashmap.rs" 159 14 159 35] HashmapInv0.hashmap_inv ( ^ self) } - ensures { [#"../hashmap.rs" 160 4 160 74] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> Map.get (ShallowModel1.shallow_model ( ^ self)) k = Map.get (ShallowModel3.shallow_model self) k } + let rec cfg resize [#"../hashmap.rs" 161 4 161 24] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v)) : () + requires {[#"../hashmap.rs" 156 15 156 41] Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) < 1000} + requires {[#"../hashmap.rs" 157 15 157 36] HashmapInv0.hashmap_inv ( * self)} + requires {[#"../hashmap.rs" 161 19 161 23] Inv3.inv self} + ensures { [#"../hashmap.rs" 158 14 158 35] HashmapInv0.hashmap_inv ( ^ self) } + ensures { [#"../hashmap.rs" 159 4 159 74] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> Map.get (ShallowModel1.shallow_model ( ^ self)) k = Map.get (ShallowModel3.shallow_model self) k } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (); @@ -2730,22 +2729,22 @@ module Hashmap_Impl5_Resize goto BB0 } BB0 { - old_self <- ([#"../hashmap.rs" 163 23 163 35] Ghost.new self); + old_self <- ([#"../hashmap.rs" 162 23 162 35] Ghost.new self); goto BB1 } BB1 { assert { [@expl:type invariant] Inv0.inv old_self }; assume { Resolve0.resolve old_self }; - _10 <- ([#"../hashmap.rs" 164 32 164 50] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))); + _10 <- ([#"../hashmap.rs" 163 32 163 50] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))); goto BB2 } BB2 { - new <- ([#"../hashmap.rs" 164 22 164 55] New0.new ([#"../hashmap.rs" 164 32 164 54] _10 * ([#"../hashmap.rs" 164 53 164 54] (2 : usize)))); + new <- ([#"../hashmap.rs" 163 22 163 55] New0.new ([#"../hashmap.rs" 163 32 163 54] _10 * ([#"../hashmap.rs" 163 53 163 54] (2 : usize)))); _10 <- any usize; goto BB3 } BB3 { - i <- ([#"../hashmap.rs" 166 27 166 28] (0 : usize)); + i <- ([#"../hashmap.rs" 165 27 165 28] (0 : usize)); goto BB4 } BB4 { @@ -2755,21 +2754,21 @@ module Hashmap_Impl5_Resize goto BB6 } BB6 { - invariant { [#"../hashmap.rs" 167 8 167 111] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k < UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; - invariant { [#"../hashmap.rs" 167 8 167 111] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> UIntSize.to_int i <= BucketIx0.bucket_ix ( * Ghost.inner old_self) k /\ BucketIx0.bucket_ix ( * Ghost.inner old_self) k <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> Map.get (ShallowModel1.shallow_model new) k = Core_Option_Option_Type.C_None }; - invariant { [#"../hashmap.rs" 167 8 167 111] forall j : int . UIntSize.to_int i <= j /\ j < Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self)) j = IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self)) j }; - invariant { [#"../hashmap.rs" 173 20 173 37] HashmapInv0.hashmap_inv new }; - invariant { [#"../hashmap.rs" 174 20 174 46] ^ Ghost.inner old_self = ^ self }; - invariant { [#"../hashmap.rs" 175 20 175 66] Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) = Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) }; - invariant { [#"../hashmap.rs" 176 20 176 45] UIntSize.to_int i <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) }; + invariant { [#"../hashmap.rs" 166 8 166 111] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k < UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; + invariant { [#"../hashmap.rs" 166 8 166 111] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> UIntSize.to_int i <= BucketIx0.bucket_ix ( * Ghost.inner old_self) k /\ BucketIx0.bucket_ix ( * Ghost.inner old_self) k <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> Map.get (ShallowModel1.shallow_model new) k = Core_Option_Option_Type.C_None }; + invariant { [#"../hashmap.rs" 166 8 166 111] forall j : int . UIntSize.to_int i <= j /\ j < Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self)) j = IndexLogic0.index_logic (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self)) j }; + invariant { [#"../hashmap.rs" 172 20 172 37] HashmapInv0.hashmap_inv new }; + invariant { [#"../hashmap.rs" 173 20 173 46] ^ Ghost.inner old_self = ^ self }; + invariant { [#"../hashmap.rs" 174 20 174 66] Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) = Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) }; + invariant { [#"../hashmap.rs" 175 20 175 45] UIntSize.to_int i <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))) }; goto BB7 } BB7 { - _24 <- ([#"../hashmap.rs" 177 18 177 36] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))); + _24 <- ([#"../hashmap.rs" 176 18 176 36] Len0.len (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self))); goto BB8 } BB8 { - switch ([#"../hashmap.rs" 177 14 177 36] i < _24) + switch ([#"../hashmap.rs" 176 14 176 36] i < _24) | False -> goto BB29 | True -> goto BB9 end @@ -2778,7 +2777,7 @@ module Hashmap_Impl5_Resize _30 <- Borrow.borrow_mut (Hashmap_MyHashMap_Type.myhashmap_buckets ( * self)); self <- { self with current = (let Hashmap_MyHashMap_Type.C_MyHashMap a = * self in Hashmap_MyHashMap_Type.C_MyHashMap ( ^ _30)) }; assume { Inv4.inv ( ^ _30) }; - _29 <- ([#"../hashmap.rs" 178 56 178 71] IndexMut0.index_mut _30 i); + _29 <- ([#"../hashmap.rs" 177 56 177 71] IndexMut0.index_mut _30 i); _30 <- any borrowed (Alloc_Vec_Vec_Type.t_vec (Hashmap_List_Type.t_list (k, v)) (Alloc_Alloc_Global_Type.t_global)); goto BB10 } @@ -2789,7 +2788,7 @@ module Hashmap_Impl5_Resize _27 <- Borrow.borrow_mut ( * _28); _28 <- { _28 with current = ( ^ _27) }; assume { Inv5.inv ( ^ _27) }; - l <- ([#"../hashmap.rs" 178 33 178 83] Replace0.replace _27 (Hashmap_List_Type.C_Nil)); + l <- ([#"../hashmap.rs" 177 33 177 83] Replace0.replace _27 (Hashmap_List_Type.C_Nil)); _27 <- any borrowed (Hashmap_List_Type.t_list (k, v)); goto BB11 } @@ -2816,15 +2815,15 @@ module Hashmap_Impl5_Resize goto BB17 } BB17 { - invariant { [#"../hashmap.rs" 180 24 180 41] HashmapInv0.hashmap_inv new }; - invariant { [#"../hashmap.rs" 180 12 180 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k < UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; - invariant { [#"../hashmap.rs" 180 12 180 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> UIntSize.to_int i < BucketIx0.bucket_ix ( * Ghost.inner old_self) k /\ BucketIx0.bucket_ix ( * Ghost.inner old_self) k <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> Map.get (ShallowModel1.shallow_model new) k = Core_Option_Option_Type.C_None }; - invariant { [#"../hashmap.rs" 180 12 180 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k = UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = match (Get0.get l k) with + invariant { [#"../hashmap.rs" 179 24 179 41] HashmapInv0.hashmap_inv new }; + invariant { [#"../hashmap.rs" 179 12 179 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k < UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; + invariant { [#"../hashmap.rs" 179 12 179 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> UIntSize.to_int i < BucketIx0.bucket_ix ( * Ghost.inner old_self) k /\ BucketIx0.bucket_ix ( * Ghost.inner old_self) k <= Seq.length (ShallowModel2.shallow_model (Hashmap_MyHashMap_Type.myhashmap_buckets ( * Ghost.inner old_self))) -> Map.get (ShallowModel1.shallow_model new) k = Core_Option_Option_Type.C_None }; + invariant { [#"../hashmap.rs" 179 12 179 43] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k = UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = match (Get0.get l k) with | Core_Option_Option_Type.C_None -> Map.get (ShallowModel1.shallow_model new) k | Core_Option_Option_Type.C_Some v -> Core_Option_Option_Type.C_Some v end }; - invariant { [#"../hashmap.rs" 187 24 187 45] NoDoubleBinding0.no_double_binding l }; - invariant { [#"../hashmap.rs" 188 24 188 51] GoodBucket0.good_bucket ( * Ghost.inner old_self) l (UIntSize.to_int i) }; + invariant { [#"../hashmap.rs" 186 24 186 45] NoDoubleBinding0.no_double_binding l }; + invariant { [#"../hashmap.rs" 187 24 187 51] GoodBucket0.good_bucket ( * Ghost.inner old_self) l (UIntSize.to_int i) }; goto BB18 } BB18 { @@ -2850,7 +2849,7 @@ module Hashmap_Impl5_Resize assume { Resolve5.resolve k }; assert { [@expl:type invariant] Inv8.inv v }; assume { Resolve6.resolve v }; - _44 <- ([#"../hashmap.rs" 190 16 190 29] Add0.add _45 k v); + _44 <- ([#"../hashmap.rs" 189 16 189 29] Add0.add _45 k v); _45 <- any borrowed (Hashmap_MyHashMap_Type.t_myhashmap k v); goto BB21 } @@ -2871,14 +2870,14 @@ module Hashmap_Impl5_Resize BB25 { assert { [@expl:type invariant] Inv5.inv l }; assume { Resolve4.resolve l }; - assert { [@expl:assertion] [#"../hashmap.rs" 193 12 193 121] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k = UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; + assert { [@expl:assertion] [#"../hashmap.rs" 192 12 192 121] forall k : DeepModelTy0.deepModelTy . Inv1.inv k -> BucketIx0.bucket_ix ( * Ghost.inner old_self) k = UIntSize.to_int i -> Map.get (ShallowModel0.shallow_model old_self) k = Map.get (ShallowModel1.shallow_model new) k }; goto BB27 } BB26 { goto BB17 } BB27 { - i <- ([#"../hashmap.rs" 194 12 194 18] i + ([#"../hashmap.rs" 194 17 194 18] (1 : usize))); + i <- ([#"../hashmap.rs" 193 12 193 18] i + ([#"../hashmap.rs" 193 17 193 18] (1 : usize))); _21 <- (); goto BB28 } @@ -2907,7 +2906,7 @@ module Hashmap_Impl5_Resize end module Hashmap_Main_Interface - val main [#"../hashmap.rs" 218 0 218 13] (_1 : ()) : () + val main [#"../hashmap.rs" 217 0 217 13] (_1 : ()) : () end module Hashmap_Main use prelude.Int @@ -3083,7 +3082,7 @@ module Hashmap_Main predicate Inv0.inv = Inv0.inv, function ShallowModel0.shallow_model = ShallowModel0.shallow_model, predicate Inv1.inv = Inv1.inv - let rec cfg main [#"../hashmap.rs" 218 0 218 13] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : () + let rec cfg main [#"../hashmap.rs" 217 0 217 13] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : () = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (); var h1 : Hashmap_MyHashMap_Type.t_myhashmap usize isize; @@ -3108,56 +3107,56 @@ module Hashmap_Main goto BB0 } BB0 { - h1 <- ([#"../hashmap.rs" 225 42 225 60] New0.new ([#"../hashmap.rs" 225 57 225 59] (17 : usize))); + h1 <- ([#"../hashmap.rs" 224 42 224 60] New0.new ([#"../hashmap.rs" 224 57 224 59] (17 : usize))); goto BB1 } BB1 { - h2 <- ([#"../hashmap.rs" 226 42 226 60] New0.new ([#"../hashmap.rs" 226 57 226 59] (42 : usize))); + h2 <- ([#"../hashmap.rs" 225 42 225 60] New0.new ([#"../hashmap.rs" 225 57 225 59] (42 : usize))); goto BB2 } BB2 { - _x <- ([#"../hashmap.rs" 227 17 227 26] Get0.get h1 ([#"../hashmap.rs" 227 24 227 25] (1 : usize))); + _x <- ([#"../hashmap.rs" 226 17 226 26] Get0.get h1 ([#"../hashmap.rs" 226 24 226 25] (1 : usize))); goto BB3 } BB3 { - _y <- ([#"../hashmap.rs" 228 17 228 26] Get0.get h1 ([#"../hashmap.rs" 228 24 228 25] (2 : usize))); + _y <- ([#"../hashmap.rs" 227 17 227 26] Get0.get h1 ([#"../hashmap.rs" 227 24 227 25] (2 : usize))); goto BB4 } BB4 { - _z <- ([#"../hashmap.rs" 229 17 229 26] Get0.get h2 ([#"../hashmap.rs" 229 24 229 25] (1 : usize))); + _z <- ([#"../hashmap.rs" 228 17 228 26] Get0.get h2 ([#"../hashmap.rs" 228 24 228 25] (1 : usize))); goto BB5 } BB5 { - _t <- ([#"../hashmap.rs" 230 17 230 26] Get0.get h2 ([#"../hashmap.rs" 230 24 230 25] (2 : usize))); + _t <- ([#"../hashmap.rs" 229 17 229 26] Get0.get h2 ([#"../hashmap.rs" 229 24 229 25] (2 : usize))); goto BB6 } BB6 { _12 <- Borrow.borrow_mut h1; h1 <- ^ _12; - _11 <- ([#"../hashmap.rs" 234 4 234 17] Add0.add _12 ([#"../hashmap.rs" 234 11 234 12] (1 : usize)) ([#"../hashmap.rs" 234 14 234 16] (17 : isize))); + _11 <- ([#"../hashmap.rs" 233 4 233 17] Add0.add _12 ([#"../hashmap.rs" 233 11 233 12] (1 : usize)) ([#"../hashmap.rs" 233 14 233 16] (17 : isize))); _12 <- any borrowed (Hashmap_MyHashMap_Type.t_myhashmap usize isize); goto BB7 } BB7 { - _13 <- ([#"../hashmap.rs" 235 9 235 18] Get0.get h1 ([#"../hashmap.rs" 235 16 235 17] (1 : usize))); + _13 <- ([#"../hashmap.rs" 234 9 234 18] Get0.get h1 ([#"../hashmap.rs" 234 16 234 17] (1 : usize))); goto BB8 } BB8 { _x <- _13; _13 <- any Core_Option_Option_Type.t_option isize; - _15 <- ([#"../hashmap.rs" 236 9 236 18] Get0.get h1 ([#"../hashmap.rs" 236 16 236 17] (2 : usize))); + _15 <- ([#"../hashmap.rs" 235 9 235 18] Get0.get h1 ([#"../hashmap.rs" 235 16 235 17] (2 : usize))); goto BB9 } BB9 { _y <- _15; _15 <- any Core_Option_Option_Type.t_option isize; - _17 <- ([#"../hashmap.rs" 237 9 237 18] Get0.get h2 ([#"../hashmap.rs" 237 16 237 17] (1 : usize))); + _17 <- ([#"../hashmap.rs" 236 9 236 18] Get0.get h2 ([#"../hashmap.rs" 236 16 236 17] (1 : usize))); goto BB10 } BB10 { _z <- _17; _17 <- any Core_Option_Option_Type.t_option isize; - _19 <- ([#"../hashmap.rs" 238 9 238 18] Get0.get h2 ([#"../hashmap.rs" 238 16 238 17] (2 : usize))); + _19 <- ([#"../hashmap.rs" 237 9 237 18] Get0.get h2 ([#"../hashmap.rs" 237 16 237 17] (2 : usize))); goto BB11 } BB11 { @@ -3165,30 +3164,30 @@ module Hashmap_Main _19 <- any Core_Option_Option_Type.t_option isize; _22 <- Borrow.borrow_mut h2; h2 <- ^ _22; - _21 <- ([#"../hashmap.rs" 241 4 241 17] Add0.add _22 ([#"../hashmap.rs" 241 11 241 12] (1 : usize)) ([#"../hashmap.rs" 241 14 241 16] (42 : isize))); + _21 <- ([#"../hashmap.rs" 240 4 240 17] Add0.add _22 ([#"../hashmap.rs" 240 11 240 12] (1 : usize)) ([#"../hashmap.rs" 240 14 240 16] (42 : isize))); _22 <- any borrowed (Hashmap_MyHashMap_Type.t_myhashmap usize isize); goto BB12 } BB12 { - _23 <- ([#"../hashmap.rs" 242 9 242 18] Get0.get h1 ([#"../hashmap.rs" 242 16 242 17] (1 : usize))); + _23 <- ([#"../hashmap.rs" 241 9 241 18] Get0.get h1 ([#"../hashmap.rs" 241 16 241 17] (1 : usize))); goto BB13 } BB13 { _x <- _23; _23 <- any Core_Option_Option_Type.t_option isize; - _25 <- ([#"../hashmap.rs" 243 9 243 18] Get0.get h1 ([#"../hashmap.rs" 243 16 243 17] (2 : usize))); + _25 <- ([#"../hashmap.rs" 242 9 242 18] Get0.get h1 ([#"../hashmap.rs" 242 16 242 17] (2 : usize))); goto BB14 } BB14 { _y <- _25; _25 <- any Core_Option_Option_Type.t_option isize; - _27 <- ([#"../hashmap.rs" 244 9 244 18] Get0.get h2 ([#"../hashmap.rs" 244 16 244 17] (1 : usize))); + _27 <- ([#"../hashmap.rs" 243 9 243 18] Get0.get h2 ([#"../hashmap.rs" 243 16 243 17] (1 : usize))); goto BB15 } BB15 { _z <- _27; _27 <- any Core_Option_Option_Type.t_option isize; - _29 <- ([#"../hashmap.rs" 245 9 245 18] Get0.get h2 ([#"../hashmap.rs" 245 16 245 17] (2 : usize))); + _29 <- ([#"../hashmap.rs" 244 9 244 18] Get0.get h2 ([#"../hashmap.rs" 244 16 244 17] (2 : usize))); goto BB16 } BB16 { diff --git a/creusot/tests/should_succeed/hashmap.rs b/creusot/tests/should_succeed/hashmap.rs index baf36a62a9..96ce8163e0 100644 --- a/creusot/tests/should_succeed/hashmap.rs +++ b/creusot/tests/should_succeed/hashmap.rs @@ -111,7 +111,6 @@ impl MyHashMap { let mut l: &mut List<_> = &mut self.buckets[index]; let old_l = gh! { l }; - #[invariant(^old_self.inner() == ^self)] #[invariant(old_self.good_bucket(*l, index@))] #[invariant(old_self.good_bucket(^l, index@) ==> old_self.good_bucket(^old_l.inner(), index@))] #[invariant((^l).get(key.deep_model()) == Some(val) ==> (^*old_l).get(key.deep_model()) == Some(val))] diff --git a/creusot/tests/should_succeed/hashmap/why3session.xml b/creusot/tests/should_succeed/hashmap/why3session.xml index ce1d25a0e2..bad25816c1 100644 --- a/creusot/tests/should_succeed/hashmap/why3session.xml +++ b/creusot/tests/should_succeed/hashmap/why3session.xml @@ -4,6 +4,8 @@ + + @@ -57,188 +59,182 @@ - + - + - + - + - + - + - - + + - + - - + + - + - + - + - + - - + + - + - + - + - + - + - - + + - - + + - + - + - + - + - + - - - - + - - - - + - + - - + + - + - + - - + + - - + + + + + + + + - + - - + + - - + + - + - + - + - - - - - - - + - + - + - - + + - + - + - - + + - - + + - - + + - + - + - + - + - + - + - + - - + + @@ -252,8 +248,8 @@ - - + + diff --git a/creusot/tests/should_succeed/hashmap/why3shapes.gz b/creusot/tests/should_succeed/hashmap/why3shapes.gz index dd6a38a6281103e3e5ff7a3131e3e11dab263f81..21841afd8a906a45f82f8e6aa35f084af1d9fb26 100644 GIT binary patch literal 9859 zcmV-}CVbf+iwFP!00000|LuL*ZyY(3=ezz2y?wjh7Y2jpq7AHIv{3?PdLMRB*e44- zyERr@y|&wS&tJb0%%d`^vPvacmam%m)Xrq`2nK@@zX%@n-=3Yn`y>2S-kpCaZ{JxVpLhJ>*jUy881rmz%Y?4A0lNmM`hw@Hgc% z>R+5&uHofHxPEgLZ~uOi->u=_reDR&v-OMfdi(aA>pXk^|0w4NP7S|24>#q_@9#N1 z+}zxL?Aw8!jPU2h|NR$N`~kLeTyiS6+t&v~RsSg0I6UH74UcNAhey3O)Obq+yr8c9 zUf$2^2l}uE6<%EZcKfDWc7;GuCz;eg!(Uh21;Br!9RL2$iqif){Iv$j`~jj0UbZKy zMs!bN?O*mJdv5XiO)j69z1L~&*Pz$#GW8Qbrl@;#Yd1W4V$eXG zV73h}z}y^Oh_xfNJVGPApm=zO7tMSdUd$TIX5?XP9PApX`RRy;XW?DBsZBP_<`HCg zUH<7FA$$lo|Kgc)dy}s?OCYvR^4jsk+53O~D(777+w1V={aJWh-re4OD4Pt8(=XQG zXJRx^@z>juZr|kV_cTE_Q?nltSR5JHTUi_5t{Y=bSFkwEhg?@Aj(ubOYZCK`-=%dQ z&2@MgZr+vfA8-FIL-w=Zx^FG<>}~n83I5yj_|N%&mAAKN8=Wz)70>A3@;l|cB@I=n ze`oWCZ@2URwnSLI{&3CeZK*x#>VXRNR(ox}9#iI7xRT<A{>m&h5ofu88=N|^f^_RG-j2<`|r26`6~XMUXx{d zMp@sKw;P4SwDnWC8^)X4+rKu7hMun9-%-V@?JDldzDanbf|vIturt$~zEM@cx{4;s z|GE9MjEcF-Hf{GY3tS#cNHbC4dP?|pd*b1{UT$~DFiTs^x|Xn;ml7xBZL)M9I-4oU znua&GSNZnucvG$-argSo@0^L+SxdRyssG(q*lLlRy5(4*T&%FohNa{Qy?4twJe9C* zH}r6+fP0JE5n~CH!Gxnm6Yk{xB1c+0bwKPZLRjzkz3$slyAP>$qBxIP*MSEj~V>MkZ zEra78^%>OAyDMc{AE75@#}w1|j`H`zV3{s?D6hL(T6@aumLJBt<=K?igF(Jg6LWmi zaZ*n+aII5|-Co&SY4na?bpLvn-qHsRG$H$UjlYS~4xZTjGee{>Iphs3r z`9{;J_Zmc8QldC*ZIh=xk9rIDDN)^QqB@`pHGkgJuf{snKC7sQNz;6yQN|{-X8NYP zsn@@mkue|UbAXfkDez%XE~L<4QnGvPrsyW!4yheT4dng zBow#5nsCi!I^{H-<(*8EsL_0XxviS}lE>B0-Ft9xYQ9nR3u~kMF{lqT?$KArw*K{+ z#*5Ek8#clHg+=*cwByT*hX{9gM*yHR|GV)=nBc$Pu5Zrj+23#8mXQ7k#GmuOZm&6* zI3iWfvBA*oZ3ECIwnL4!;~;uwBiyV>t7{8Fo7U*WI6WJ|te$>=>C0d~UX1@&JHYt< zVyW{Nn@alkjS0Hg1WIl$hGr*;WU_|j_Bb-)!$oiTE;j6V)~9x+lEdsD_S#gqn6q&x z*ga2e^+gyX#upn7yua!C(M){@w+RAVY^?C>iymHI+#i`=i~#>)0{h##!NNeV(ad~> z!Sh>VU3KBMJv^g-C$0$$9e>q$@|=tBm8CVRmT!$XdOpLa^~|N3Qy?!ofO9K* z3aBPnEI2UxRmZox+`_f=YiUO(X{k!wqNS}5y$-k7lfuaEaJkQt>OBHX;;u${R~H-e z`fU7Q`saNv;=$>S4-xNyKlcY1bEWsHU+%bl_kOnC@xSKU6#IZID}t*3HgzC) zooySy^biZaNZm&&Hg!M*V0olFG(Hgxm<-DY7_=K)%<=w2zrn>}ui;|uV=PL5-KXH( z9tC%HtggpLWr3sL4bpF!xXMi&c5N)fuvwIlkI|d8K!NMa4 zYsWb22O8(^YoL~*hGe2<1EsbGN*%J!YR5VsFa>N0n{}4vbFK5TNt9>zf_ryJl^mr? zo}}uKR4rj3Mqmf0{~@Wu9jQ7H?q;OcVLq`D;RWGXl4BAY>{RDwf@sG4uf2i!*B}CgGm>6ys_y?{vG! zAsD5yJ-1-nBoWre_LHnVjmc`5d+lk!s%tB{sn;IH+5K!t=gHTepVNP*gU7vVp1b~rKQ@XiDz`n(D%#8UuUvL39YDF8~n8iK0S<6kF$?+k9g9u9&mBiMznlu z?FT-pUv~wbQs+eIMn9J`JrUZhwH}IooE06XU(Z2(aQ;!IwZ^p`23DCRf|QvPqzu@_(i10==WBMdXe<(GG>d z?al@}xt-&(i@Dp)wmP@jR_8a{>Ly$1#B?hiOt;eY@$o79rn}$9XS>-5C$=|}x&3>| zxWAjo*0}p@Icf%*oRno@%b6IqoXMRnXJXuPCdcKKr4458;C3>%yPK@FdFP!AkWp)n?kZ7wWd(IseYG z-$N@JmbH2Rz(SS%?4RZu!W;AL1`9bpVYe#1S#h6a8dx(+8acC*QA}3DWxpCO^?n?; zyQJOxAP_;%wm#+w8d+pB^-pi=1a_yNNXtIV0(_#+=pU zPMgDkOat4)`vlZ5ZDK@Ulfc=B9%X-+K#>8n+Zkk61Da+w_kdmMi~A1hG+s7fgx6C~ zW(+}$q1IjyyY~;gg?HOVcAs9ac`NPCr_p#0OyEuHcXoG9$w!90FBXGia(N5~L^^PN zeZRs?;N?u3C}F4%)dWVU9zISI zsczjvPJS3+FzOx#V>f3S^mtDH-48j}INNtc^-Xaw_CBy^Pa_V-0amxC=iFQ;Q1ssL zDpDTYL32ZHcG-526}xW(t{Rvzld9!T&x!fiHPJ~$rw(?9VgANhx$Rl%uT#+PMqj|S zC2I1H8c3vn*3$kuezg}HgUBI{ZLdmoxktAF%-~Hx8zy!ebwi)igD!f@jI(PweUm#S z=HF>Re(M(2dGNb6_PIDv9jO~Oe%L-}LrL8y0+y|*{*Z@U-ipBe?CK)y=cffo$1K3L zCUGw>cqTkx+_asiUJhQx%gfCGYBMaEYjZI^jTz*y?oT!D$H)FoeC#i~dFrRfMcSE` z#Ts998ewNgMgk$kVC*-L80Tj=@CEZ{&xVe>;O_pi8wmJp8;!~x0K1fBa|$Tj&e8q! zY{8rIabLt^JKIJPTn>}PzTDX8-8!$67?02}@26Wawl<)>9(SKD5`)v6N08dVu>;kx z#W1IPUq$N!VX?LYSsu(SPYmvxgJBrm!M+|CrG`scauaJ5X-Q57?R z_o}&V3IAoE8F;~F=y;BIyUL%>mT~(%q62gGw6dc^w<_3EY>)n%4(Fbd_Ru!E&zku1 zUK1Z?Gyj-*B%gX7!96C@Q9=q|S4yE1(*ssb9uQ)9A}NNm`54?sj$r^7((U=YK^J>A z-@$>xzszD(FvAa0^_x|ZH>)llDTU2x#<}euk27wEs%OU;aeAB)`rt=PpT)j*wqo=d zKEU`ynU)SRE|uIpK8OcTG2$|2>#3Lo+!h<-y}tfXw!Vp1UB2d_x2JBKup27i0L1R` zML8Z{>b7ujBqM1{*3^`5X$-VFCYD*yjy&x$2cEVlIG__4+_;Z z>wK_#+i(!S)7EwQJpBEVOi|%p0v9=}c*~>!T)~FY@oap}3W-m*NDNk29#=-5+PpRoD zknYc%QY-v$KnKZ;ubJ~5R@Axeb)tq)@y1f$&+)K`mQL+=>jY`&U*=Tu;F#4lf>nfkN zro?t@l;szI){I(vWHZ+2zr%joBoX!jkPW%6u2Nn`+?}w2~S&noA<)dhAyqDINbFICJ=g2SPz&(o6 z#(O$&_%u5EIOc6D?OCydp?y4JRb&>lREuY|<#ude-QiU)#P;{p%p~5c>ZY%M;bO~O zR(Jat6ZUnAd~aY>?hlNryOuZh6x)gF_U+6Dbx+yFRatrV+Y!;r!y(A#sc%Oh+qrd_jfxXUblmUGLoyuGx89+7Qkk#@Vs3=UZRCzufFt>9w?= zr*ZoTTu!<-X6c?UCeQ7@&%L+OjVDLeQon3F%$E$|8Vv7R9yTi2g#&}#Hs}Sd-pVdn z|M`qDz}u$hw%^QcKQ%#l7HwPC$cDgywFX}EfSa9FgQ3g@-}3Un zo?1s*^)js;2kkMPu#5JvFTcwiyCrw?>Mq+>^|e-;tsnf>N~>WPxoRnU#NUXuaf=5c z+LvK)HMR};(~T#3#3jb|HX~ExS-ZiCMZnj@(yqp!)EoHN@rE7Mq z(2Rt1-MO4Q{KTY|JnVO&danPg?BDV-qUe2huJ$TnbDisWVTw+&r%2iP4Ytb8Z?I*n z`+Th^qkh?smD2lm;;HGqI0;67^JU|ZbNjD8=@=oa~`#bKIvi%n^!hPU|4 zXVa!Mqg$YPd9EVM`r=$|UwS$d;gsk6Iwh<1-cjn#Ozlr>NGdj?6x)~iJY_Kdd`l`? z747zAA_8^0v-(*V)|y<|th*e%LvkDm+&dC-QF^qzVAzRaEb#HYP_r z2eI-ix3Vj<(kr#Xl{_;^EAKtkQEIg)a|I=B62%e{3|z6(D+z8T>3?=5%}Ua{T1hG_ z>BCBj75Eip0J{RS0=)vY0$hPy0ewBoBA8sVvj|;0omm zVTEEP{exR0kuc7eT!}kH3K3ih2o{Wjm`Uo+(XG&~&^%(BN}%=LCM}75CL2g5)sT(V zH5g$fx2ePm{o^)^-sTXkt2O9gu-2jijkwa)cofl`E3;BG%xa}@rQ}M%qmy8)sKt`J zxS%vt$XZlkbJiB3DI%UL>bd>WRA8_+MJt@h3bGQ?LZ}%XSxr~1%;y?bTC9}+(uCxg zW!6xVHfWe8pG)vbJ7tM2(lR@=d>UFr^bu8-nydjj(kkAY;G?TaUHc2l4uOX zxh0!wSJr&v{V2(yK#~`5g_M$$WFfPN$&$_t(q!(36D#Y#i{4~eG?HKymsK!I`)IR~ zwS+=ekt{*$4X&JAIruI*=c_094YvAVoeyNbY6_loLghYrx$>~` z;`{4dHp-y`8lIwnTnF6-%7%cdM#yXjflF~QF4qbI{ZYk&Y8LceP~Czm7nDy>K0)~e z*j8-mJV{dA0KR?Q=$n=!B^?#+(oZIC9B|F+~&JujF_2NdM<#j&Tt+ zS$ATGAV?m)A|3zr#vQJN zYvF2sT24jslprdfqjI)7UscWYBniBrk)?K=qT*CLQ1u}BovM&r2US9CoH*GW8a3Q#jZ?VPxJ)J!fWLlQMw2gX>)B4s3*6;cc9s_nQ+ z`KhrJckj#HRD~+lYDn2cudMc{03A8FBBW^G9H=>HELJBre}=D-eRN)B64@-BAn%+& zjm}AyqGhg)&EyLL+7q`wKeAMWC2x+H=u`GUoF>O1I1M$(BoubsX6{lgjIK`{|J-$e zpq$pqNR&k;ZA}(Vi=2ZqAPG)%9H+9>w&TL$#Q4X-94cF{MI~;!paKbZAifiV%gLLd zbEm(ld7$=BY=1PL9VPgHB?^fgSpoLAGE}9lvS2%X?wR9UQk_QN@!giFLa8pgL~_sa zPY$q**?5V?g)YnuiZzb;$vK6xlJRq*6vR@avlC$ck5>Gt7|K5Uv(P&75EV}flq%a{@2&NeCOvQ7cUI29lI6iP<_U8$- zCkP-zbt-11mC-U~W33JO_G7?&s5yq@q9_$bvBmJdPg2QMN(WZ9ou%Nu zLCFRuncLvt5!ek*Eb|-e9)^Quo>KeNCQze5tpYVmJflA@NWGz^f!YSc%%^};cO70^fQ9{&7C%<0r|oMLf*4bCaWT&3<{;gB4ka{lP#dZ%Kd=2(||nDfaubI zkj|!hrv>oFR_9!*rbblI+YAqthzS#$CwCY_ac zSr_BbNvU$QMe%W~A;$IdaD-5sE_@8FR7Z0rC8ttOQtO1-)-(p99>$R$4EZZ8AhO}J z<%M7Z%_HOkAjL+)y5Q;gqprn8w5Fn$Wb zN$!NKO4ndPkT(;lkY+%l!g2}5lK)XRBKA|-g!^3ldNLTcR2C=v3Khz6$IIAs|n&)@~J(kP8E4u zAKB0EgYORpdP|)D`amy*WK597XX9)3q>x0Gd_|f9o1y3>9rUEJkFRRdq96ztvjGet z*u?RmXlqKgI=;B;T+%Q}8WG8LbLCuntDfrT2Dk*0O0308W3tw&O{M4mKHMrSxB1~Yod{r?+YV1{`d`( z*&q)j8SQnb$yefO(FApBRFq`fjcJlZQ8xBIcCTwSDVvau2sU_?oR@s~!+Xm|_Mr7z zi7!Whj-)nZB{#4FWO`1*dA{;6RuM{RS24886?_>22xjtztiT7hvUXV#X7Z8m63NEo z5}Q<$N+AFK3ljnu5t7Z-s*=c4=8dOlgwK(*p^D@5dJWF2F`wbCoe91Nv!3Al&No(k~C57|{ zkn&KaO_D~m{q~4Yx=6)mu$3lzE@L1ZolPpykkY|eM#%83cAzLy3B_UZ3T4g(Q%w#v z66};AfoURRxC7LPcHd?vfLbqPTlp zHS#SiS=*p>Dvlt92%7p?yNPW0Pkmn<;{c^XOI9Z-zAD03pKYRvj}E=9q8;j%@={ddlU&q8Lis}RA!@6oB0Ia0$8We3IYuXJjHp3oFUW62CCIa-$)>#v z&|yk;wZymI86(JMb6gmOh>^MwbxBcZYbArRGO9TX-%qEIV3LeFS?!W{nYY}#;1N`@ zG-RnAW|QQ`ODn$;*E4EE>>^LsIT^@rkC_G{BrlV6-AUVy+v@8QS`%Md7s>CpiI93F z_rI!GjTBIfNu~?9SSo6Dr=GrwT2VSWvTc#P2T~<~2}%rP=0t%U>OiIa`ji$OQ`TO2 zrL47q&_v3@g&KtrgzxLQqFNQ#>R`8azNBdg|13CFTrUzZj{ji#Fy+a5cmllqQ8=h4Vn-)Af<7caPdGO|Kw? z2cZpC4WbetU_Ft^y~0Rt75jXiN_wi2qnn;vqo#N-0Poa!WO^`5ay&z%y1fv*^E4+# zV^IvbPFA#wipg|P3)F;nJx%tD(^bg;Y0yRS72QdLC2dby)q96P!d^SNs3C#$C+QEK zgf7BrrlJ<9l9#T?LS|D<(V9qd7;Ha&g6PptMw7`t1acdVjn%R$C*&Upc_k96T5CUs z=E>=TDhOsIg6$+ymhhC;**T|$t3qgRI=bvvq0JM*D+G?BNY++KpePFyN%nc4M8eq7 z_Vwr^WK%48aipd~G^8d}x`8jH#NL7k) zC6QfrSdGX|5(|->HdPyqk{3USF3Bq}y!^t;VNARIsxCWDK&y zeVXXu9WuPW#XM0zzMObXE^XlxUNWOIE|d&p3$lwb5(eoor>2HD#>PC+@~7a7C9fdM zYNeJ^W~x0AlySUxT>^VG9bc$Dt$!MxgdoW)QO1JFIi=*FWG@t|s(h5zbv&^@9baVT zA0M(2NKiCi1ldkPqbUW*d$YdTTEjc9h*rbD4#{nE8Z~Z+UPJU6qSp|;n(}G)L-R{j zGC(3EsRRT*52lnB#3&#<7NYI$8@1GsCE6^}W{EZ{PCT6L(8Z96C`X1pc+ZDW6bc0{ z+9YLnLKk`WBhz}~*rs3)3NYH1|Ve@GvM8%O!tYW$Ho6b zu~h{=goIJV==kOf@YQv(3~Nt(y(eF@nf)9nUkUY_{-&~+xAb>%J3EK z_VX_O6K{{VVTPm^$Y~*uB^kaw$>u0iAZ05<65a1&AT@zhKT`cCMnBLABA+Mg0$CyH z0Ix+UBJ;KipA@eI_KfB~mS%Ng`eSGgtP+ASI#pei0hQ5%EESTF(ks(3otMKL5loGD zjJGG|KZeAoXq<|nRGF*uL1rNw#w0xeSV?Gh)Wyg3AC+0uaUI^Y2mjXE@WG+Q8 z5QyqvM79K?4ceahM4&%0{!tgmyhsG7CDlvXoj0No+(yAalj1}P1LIH3|04R{1{DnH z6d92Zkkz69Bk@0w-6icmUJ8l+#4H~*-^v$^HJXZ4C^kC*B){I&VA{`qVEg50qQ?`> z-u*PZ5jk30bcu#$v+&?UP}vvI8AYKw+HGZu_iFX)8;Vcm{-n%`S{4+T$kt;}Mb%KO zRG~x{awVL_dmfcw9^p^TC$B^epp8#P>Zo|nUBDz`PB{`Ux^ojOR7#j$sPs?Iw8X)` zSYwr1LoGRnWF;jQmy#7ec1$B;$kx)I>ltTH%wshcF)AX6kVp_!Spp$i2JNWdeCi<<8a!yU=Ih)=*$5@t~EJbSR%d3)T!dN$fjC?_@u?D pmI2!;rO9K0l*wHpk5frrh{@7WM@><=&rS57{eKX#|Rp_x3!@jf#1) zf@`;~)mD$~w%zyF55Qb1vns1pl4W_Tb6Qp|TtE;6K7e5AzdbvD_ec1vygUC;-oCrO zee*xh&H1zceiojG_qSKqZ{DvV{1M*$admV1d&s5yb@k_ME;nm&8J@3UtzOda@Hdq+ z_%AN4*7D^=xPEgLZ~uOi->v1pP2Y-_XX_W|_4e&Kw|Vyd|53>g{51UXJlvEwzrW|_ z;pXP{W8aVL$q0X5{NI0Z!yn{!iA#RU{r2riqN=}CYZxwJjl(6b^>C@zhB|N0BwWx? zelPFm?Mr&GmKa`K{dW7NTy~Wt(jb}CKf_;FJOl~l&_JWv`1U-4l#TU8c$HI;IG+4*< z{C0gqZ6&dJJFx#v`8aY*Zn&j3+=30a@WA}&o%z`=(6el0xnY)fmzF8&F5TJBJ;RM=z702KEzM@;<=DBjYf0TtXEZzu@5)VWvSBut zQia#$pYBqI58>utyi#s&@)Z{e#MVh!JH9x3|Ic6LoSS`n9p1b@3vbK2+nWz%Q=oDB z#ajBA7!6eX^|qwjH~IQKEzr%<>}NzS&WzmKSexH&7-LIUa&egtrLIUE`_B5?B<2gh zd)B=)*WqQjc~`=Jy#2cj#m|20-nEBkZ_A%e@ZX-tf6o7_yuCf!=!|)*a7Mq&?^N=Z zG*qSWoy|MG-7f#z5@GrJ!!@h7rT%EB2O88{{k8RaOr2-pN{JV1C6;I5d4Dy18$R)K zekwz}ef#$IW6A&e^YyIAD{eN_>o?(MGoQM9JRMa>=S(KlQ0BwtN_GWDk-RE5?>_!f z-j=-$%pVOMFYAY%+ND=L3H0=e*3sVw`Xfe4e@Dr_qgP$gw(`5nHV@Jbjj#;*IdfmN z_Z>sW+NOKl)xYW5=xV#|+Baiex2b!xA;QU#xw60QRK`uy7kx?W9*srSaQ~cIyMFVg zyxpjoSDlEQ-Q3>(wb3ecbxo?}_uJci75`4J$&x+WuE}HRmwZ3%2aCVDZ}H88N2+*v zUjjQ5&d)b$OtK!MMf87e|16`@?ut$Oeas4%#}d-aSGb-Me%-Eks;-y&9SY2zEf!rX zxm%VVPRQF7>0Wg9RFS0(Z*H&h?cedHTt(vU^_$Lqa+4u0;3lKmPvfhScD*@H%{gof;TE={+?*nefRri=?)!XsgXAcxDnqRFS027=Up zGhYpTzQ5_Zkle+<6WDMO=m%R@xYQLFc*TwM9YEKCXb&42WC6eF5#qCs4Oif|@Z1C+ z^5ks8MTYQPwKrriHq*7z3OF87UjT>EU7>AblszdsW}4o2l)oP)%XE*2`lf58^@n!1 zz8Oq4m)X=egR#EBiK)KnIH{)vxYemOZ@28pGC_8nuu9QWo^chN;|WI`v+I2un&7roC;-wChoC!9FFbn@z+6x={1$P5U^u ziTkXg9u`gWmqrqVJ1s7a*;W(bq1s3E$mS~}b zA*#@m#xaGSxEAy2FR_IXhG;_H4aXAtj&v71=;H|f{q9jZMl4{`>9v z=B%Fm{pM{6>5oACIsfbSngfj^QsojG4BhTF0BvGBaI_r<(K8$2W=&dKTM*i`PAA6c z*$8I!^o5+>4Cdp-_`li##`hOXgTL4`(%)}P(8VT*a&s|sJ9$VZYk1r)M@D?O=q=yH zh8@rPr=6+f5d4R|HdS8C**H|}uBW#8B8<`Giwy_f-*n?>roMyQ1OYBKR`~Tr53euo zkIXMdfPXQ8{cTTSVWQVyX1>DUd9By=W0Rt;xp3Pqp3(1#Ya)k%ziK>r&eiwI(i*Up zTLX-q&+uwJbE)POsEZEZ+^U`eYDq3u9GLy8-e*bm9swqC$5Gz#Vq;#PjW0}pz0XBFxV+&Z;yv)^{s3dH^j`H_A-C_|&-Oz8 z*Ib)IUoc!ZUtnvu5c_vi2ZHzDwgF5JvE&zN`$)xx2Sh+F&vb{zC!!%I)AB(M+D%@} z@%}`=$&15Y!^PakSd;*}Prg--{?+&R_qg1JrR2`D4B@Dy}?BMc0Bvr5@RR_Y|jMO^JCpIFyARLQw zy(Lv{vEnx7JA`%`<})mxBiLPNat8qqahRlsGa1`zjxA6o&V@MJ3exbWzvJ+(^<&*)a5AD2fo`d?} z`lCW?4QoA2ESe>P(98)!!!1))bUi`n)@aA79~Y{A{P+O5UKC)tw&Pwp zB*BOLUnROg@91d}xnq{vp)k1JNxoCtB`&*|yWOPRxlPKQ-=y44((J@E%}!3!?E3il zlzr38xbfO1bk1M^oeW%2M)~ zJD6(bb~DXdpT{Pai3cQ>iB0O@!0iM1UL%iqyCwA7bqCX^`Wn;|4*Nq_{f=^XF@aP# zSgAgy+DzN_M&0&3m*3g;duT($wl?PvEHv4#{%NTpyfIHVSSaxcx?Snbj{Bt0z?#{k zkuy65#bh^J^}FFp@5gbwTk5UCWc%Dtw$FP)uVCD|ckN=bPdH8`%r@?zt)83l>Oph4 z$a$u=TUaBJGm<`Q&RI?F^f^q(G_XC~Pe2XRCPwr%37mcCQTB%k6d5qPok4aS&@{8T z2kc5;+;>u^@v;FUyq||TH1>ji%^+4Faf`E+?11UPR9}TCL~aY zmosUi2Sa;+6BvO#e4IR_wsj9V`C^2@pnDh$-I{68<2n7iA9Ai?mUl(%O>r>vKCoz4 zBMycER=2C?++8P7bl>nQP#M@kb3;c>yKe)o8kjMYs^vk?iTT)d(Md(84tA$u ze#b?*@7dE|r=Z`BzJP06)Z`sCkVwDQ%KkdOwHF(M$RUnxuL`@;quU_O;7!OjP3$)6 zhCZi-0-_wNr)@`iwShlYE10ZTS z6@kauwME#^Pb-j)S%7Oz;$B|xN_fD$X*+*FEaGd-SGV2xLe7CjM*cxJEwr=6_1?L z@VcMUqh-L4GH{S^F1SqjZhF+b=Eae`Qy zb5BisD2?v37QVXI!k4p^f6O{kPrZ)hJr>eYLMp$ml*&#_4_GzzM3O4c=6t@7tjYmE zD7WYJ20`peu#*QW|1yh1$r(ma*e9d{C!{VODV3YkjC1=w9%tMRN6(Hk!t^+!>;oL_ z`7FM*lWx%$_#nqCDztQvajE9+@j*CviV>D^Sx?0zsJ7S{=kxkQ#riH@b>*5D-mbb- zU^g_tL5AJqi)uW+*jIMl)1kWU8tJOI39i?FNI-?mrJx?<0} zvyzj#^IUP|<@jcPF0$PoiTsvv=slsIx*Ph@gdC%xLEK>hK{ElVV@q~){Bb4=HXQHZ$|FhGi+eF{3=+W@erj&>%@INfM|IUT zJ?jg%`l2G22N}R^>2R1@@|+9mnD!Sb&*zFED^z$46;SyN~o8zvZEt(~eBHcY=X?$=NYVcEY<+$@(oD zt&R~!e^hT>=$od zPk1oehhs*6lv@KwAWD545A|Kl(F@G!%)sEZ|BrcKA<6BW7qwL6NHB#v z+M9Te`Z5mOqbO~-rvnF1qqC1=-nP=7RXZ5Iha+}AW`RjuJddrmlFFk2>yYszz)xRmtGFUHlekk_p* z-(POBQhF^d=xR(6k(ZO)=Ix@S>#KGa4ijICJ)I7cHvN9 zm+HKr)mz;q>px#HMsjNO-1eKf?WZoN%%W}UI@u67u-3rK<&T5z^sNu-&DOr&Bj9Fd z*I=l#!MD6Uu&33LR=rGX$3c6{Anc+&?Cb9`$8O2pyt&Jkj=t8oN$=phRvU**acoca zh`$kQ;}#D+v^T@#YG_IK)8rC8;u7O_7KiC_kTg~7lfL!1Eco5byQU|Xn-nVzm$Rz6 zJ=r9$blr{(nvsxhIG1yWpP1Ah4>>K=&h>wl{b?;Dir)9l)m|lRKIb}q6h$Z1Q-pT@ z1zWW9FW9oxeZEF2s9*MTg?eAM9ZtV}ljP`c+>vazTWy+ahr0Witxf|M5w~c@MVf)k z;7GIDOY<~yHH}AS(BDDxPPG}$YM^=Kv)rOt&S`F6Xd!&Swz#Jm{63n&E%I55!!++! zo6<}jZ}A!2oMvzfG%v4JU|C;WtL;rsXCj>PoNuROwb46zy0cRIQyGe?%_xQTX1-1t z%s=0fiq=H?`Z5s#x_z_ySr^ute6m@0B{&OmoC(-F6KYXh+xG|$m*`04PeYw4qY+hcP>av82$dbk;;Paq24md0T!}Luq=y(QgcPHJD3q>M zRPU8GCPz4zV&zwEWmjgUSGam3Kr@cI8V@3xb2KZYX~q@83e^hb zqmy8)sKuhPE})iGW-Y3)IcqDUDI%UDjof}|Dj-;!q7_bLlo^GxGSm!?tfs40<#R1p zTCC82X+m<$Dr;GiHei@0pG)vbJG8_WWtkmXJq;})`UsenCTjqWw2Jp8_~>d9kU~i; zl$!ptD^1EkuQaYSJON$aVPc7egcTtB=zS3((*m_V71MoxrXXoC2ko_h}emwV#<>Bs8uT~S5~ZyUl}5n6uns) zy)w8murg|8%YTD{H>-ad;Q1ab%Uetto1uB;m`;C3BTFD0d6ULQi7shLK2pg9$c(c}5C-Lu zd9iZ-`x;gaGFB6n2!(#3_SvB!jhzL#2$|3`4+~aat-Smm$0s$CZ;Vw3CCMWZmb6D8 z)RB}ggw!2dc*zyHCRgRUt+J#aYFtq3g31VLUr;$g8Qg<{EdE)eE$HmA;6v@P*YR(pgN>at*AX;64bS`sRf<1BjQMfHk zWmjEfvHSq5vA(q7vdV#jUATy-a=KOWOV5ZaJH6DqYjxr{{s7AOj>Cw1MJPE{Dp zQ|BkfKbrd-i&oiJ02&xLC=mn__N}^zDtg9Kb?V+xeUvBuKPsL^>8uytD5;HdDMZXE zYVTA8;*RQcJF?`%iTjVu{eVSgz>EP&zbgodSnWh9vKj*9(75lJ@jMCoG!b76t}9(! zbSSckS!2~2gbhs*AvhZvTt`+z_Qb6-NY+@AQ(uiM1(V28liX>ES>$9&%TJ&I5+x_5 zjS$1=AX0WA_$+nuinl0KBuo*|s#OH^3S1D#!MG3(OZ5`&Sf+Ia4tN*GF(c! z(94QCWuawuo@PQ;P|j6g0QIEgeCq59KP4V(_|MiT{S0BjBw5x z^2e3NBqWZ*SG*v;>!D_)g()ZvjVlN3b=Kb6YO`{@Eo}S1w)$=dC^KjK*N}BeGLuV6 z>Y)e?cf!)EHzsF|2oQD{%{4^@uv5ZO3>aVFGVG z^`&+KK_|v_j8lZ%auLP{m!Zn&2(Nl@%F0;Dw#S`d&53ax<2*^6Qy8;0m0Y)EWb$;2 zm?1djHUX6r!#ajZ6{;^}2MsdU$f1=fL|XtW8jt#1v8|BQxA0GAu0tUEOt8g@6s^`p zLBUE>3dt!Mu_wx{+Sg{DmNpV8MM9!Q){&THQejAeMYDS)vh8Vukv4AUvqJ+-Y&sEo zdPG?b`N@zxX>S^PNjZodIUYiyQ;Xjn@t24LeN7HPu9nn^NZCeLLnYC((WfK{QHPZE zE(i1z1_-|xWiWz%1Gth^0{&bg%$=8%y z9R*>}n2m%Gf+dSzIMF91TOEJU?p)DKDVh|;&2#(Q0r$|lpg#Dx2|pIwF&JmF0K(fC zR8WB4Xh>QVG}N-unZKf;n0Gt?9sv*GzMT-F&xD{uu9ZKk6Fse|6f6WC3PEbsbwZ8s zTzyVQw7fHoA^l323E7BX zgC`a0l~XZ!Z=KdC+oq9H52}zAzyYBFJRPNx+h7G?nxy7~yjyWr%THUQa@dK<8*y zLa|w<0!Br$xvr9nOe>=5jw|}<2qKR$Mou@%sfb)mA*Wt>UBE?I6Sln>a`oxQ^}o%R zC(4y-Xp!=liV}b337j*=q9`?#98CLkl_C_O&_6wKM)R^VNyn&3k@|pwqzSZD&XJ?g zj{GRiKhzl6KSjt#HC^)+h;>pEREXLZiyZ8w&WWWFJZH|tfE}^as5ajY(Z(0@a$I> z@WFw%RkV}lirfuF{)RI4`y8b<4#-QvgglEr6UrCtSEJPm$F@lyV zdqHk1pdiPV7Mu1iv`?J14y^q42V(@;>}pd5A!4KS+kj0o}x|oZlR&B4IzKU8w9bMp4sG*W7k&tAGfy|sJGKV@) z>ApUth0{2-M~`T&4TL6A7A{mi=t=m#o+Gu0+@e#vt@BrA-!m0js#ajtN}GC{3@K6WP{rn zJxPM|kJ>LSuONh%LK~=Bib{Zh^+YE33L?2xEXAD5?Wr~gI6e19U2(PmC-posJ&+YS zo*~j$y%4fillgPQv6#%CjF(IgaO6~Q?9%r%xi3yvr6sJTE*KKXq@^WoPg>P`2a<%n zc63ok0_g|nM?DE$gw;$1Em9>f9mzUoQ%%vDNOBNtKYz?G^JFxc>_Z^8(b!lmt8zmA zfsj`sp{lj^b7-HOE?EV^j6|@VM9LDL(mFfmv~X1j?M+A5*P+c5!sD-lMv<(oia=2o zCX(!fH8nx(X!Bovibq|V%O692QZ*Z8Yx|FlP z62V4t>7A@5I!UfTB?ODzO#K)`MPocz!cfwMC}?6cf#1r1zolwRv~_?GnHK$dKscN()MU1kYOeAwsyzYifLnF822OGLo!rP!ku9$r!O&X<%ScNnp z@KSE}lWD>qmIcz*BqUTRQ{g{57{F%}MMV(}LT!Kk2FURQ?4bM)&W;d-BaG*4CREH{ za7qXU|nhQ>iP zW{Flm16wS40$Ek7v{EXQcb^EsINq=>fjyayEkwHhX;>11B1Z&`l_uwul9MHSft&;H zqq44JiT&BwqO#GLZImP?T1VhBg&M(>BFSH~?Ii}YDbrMega=Z-Sz zCzc)+?F%ufP=&D-gZ0)!6fwG>keF9p7rS7(PHepoTeGtvs@lSUf&cV}AR+@wR4!_r zdr8F;Yabx7{MA^{)hpwjE!I`7gv}*@CCt-h{xU01?0w*tlFqtvb~CwLKILSxH=2N? z3Fw?^xsAX{{FYhiPOQC$`7$KCl3W$?Q*+tkG1w%3`wR0;@y(WB|uJq6~-eJ&{bq9rOC9231k@A^Uj|5 zw`V(8XK&D>(bbEn9XVgtDk*$WppCXY|J;d(2fU}`m6gR4_$A#}g{r|RUpyh;nv-f7 z2uLI&)x<{fS4Qd5lV-^>p%K1DRe>~(%aS_N(0zv*6@R5heM@9(S5a4;veXqF4S^g~ zZA*fdS()qj4M?Q6zCrq(bx~9je;EP^d<>FIqK+ga{3)868vV#^@e!JDcO03w>IqKr zA0!Xis3L6SujrB6!hg6Yp3?|d*bd22`;B(Lax1$sE0!zQubEJs%e5w_3yY)2Ok*lu xi)^YTTu=I&S{V>6q9!j%rc5ppIhm+<&m}8EgER$mUz%t?`~O7D7`oQ>001R+egpsj From 13c326e59d27a7d7d90c97f8de68d43511dac0f0 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Wed, 18 Oct 2023 22:38:28 +0200 Subject: [PATCH 8/8] provers --- creusot/tests/should_succeed/hashmap/why3session.xml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/creusot/tests/should_succeed/hashmap/why3session.xml b/creusot/tests/should_succeed/hashmap/why3session.xml index bad25816c1..b4e5cd3df8 100644 --- a/creusot/tests/should_succeed/hashmap/why3session.xml +++ b/creusot/tests/should_succeed/hashmap/why3session.xml @@ -4,8 +4,8 @@ - - + +