Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472147314741475147614771478147914801481148214831484148514861487148814891490149114921493149414951496149714981499150015011502150315041505150615071508150915101511151215131514151515161517151815191520152115221523152415251526152715281529153015311532153315341535153615371538153915401541154215431544154515461547154815491550155115521553155415551556155715581559156015611562156315641565156615671568156915701571157215731574157515761577157815791580158115821583158415851586158715881589159015911592159315941595159615971598159916001601160216031604160516061607160816091610161116121613161416151616161716181619162016211622162316241625162616271628162916301631163216331634163516361637163816391640164116421643164416451646164716481649165016511652165316541655165616571658165916601661166216631664166516661667166816691670167116721673167416751676167716781679168016811682168316841685168616871688168916901691169216931694169516961697169816991700170117021703170417051706170717081709171017111712171317141715171617171718171917201721172217231724172517261727172817291730173117321733173417351736173717381739174017411742174317441745174617471748174917501751175217531754175517561757175817591760176117621763176417651766176717681769177017711772177317741775177617771778177917801781178217831784178517861787178817891790179117921793179417951796179717981799180018011802180318041805180618071808180918101811181218131814181518161817181818191820182118221823182418251826182718281829183018311832183318341835183618371838183918401841184218431844184518461847184818491850185118521853185418551856185718581859186018611862186318641865186618671868186918701871187218731874187518761877187818791880188118821883188418851886188718881889189018911892189318941895189618971898189919001901190219031904190519061907190819091910191119121913191419151916191719181919192019211922192319241925192619271928192919301931193219331934193519361937193819391940194119421943194419451946194719481949195019511952195319541955use core::marker;
#[allow(unused_imports)]use super::pervasive::*;#[allow(unused_imports)]use super::prelude::*;
verus! {
#[verifier::ext_equal]#[verifier::accept_recursive_types(A)]tracked enum SeqInner<A> { Nil, Cons { head: Tracked<A>, tail: Tracked<SeqInner<A>> },}
// This indirection is required to show the termination of `Seq::len`//// If we translated this to `Seq` we the decrease clauses wouldn't work,// because we would have had to re-internalize the tail into a `Seq`impl<A> SeqInner<A> { spec fn len(self) -> nat decreases self, { match self { SeqInner::Nil => 0, SeqInner::Cons { tail, .. } => { 1 + tail.len() }, } }
spec fn index(self, i: int) -> A recommends 0 <= i < self.len(), decreases self.len(), { match self { SeqInner::Nil => arbitrary(), SeqInner::Cons { head, tail } => if i == 0 { head@ } else { tail.index(i - 1) }, } }
#[verifier::inline] spec fn spec_index(self, i: int) -> A recommends 0 <= i < self.len(), { self.index(i) }
#[verifier::inline] spec fn spec_index_range<I: Integer, J: Integer>(self, i: I, j: J) -> Self recommends 0 <= i as int <= j as int <= self.len(), { self.subrange(i as int, j as int) }
spec fn first(self) -> A recommends 0 < self.len(), { self[0] }
spec fn last(self) -> A recommends 0 < self.len(), { self[self.len() as int - 1] }
spec fn push(self, a: A) -> SeqInner<A> decreases self.len(), { match self { SeqInner::Nil => SeqInner::Cons { head: Tracked(a), tail: Tracked(SeqInner::Nil) }, SeqInner::Cons { head, tail } => { let new_tail = tail.push(a); SeqInner::Cons { head, tail: Tracked(new_tail) } }, } }
spec fn update(self, i: int, a: A) -> SeqInner<A> recommends 0 <= i < self.len(), decreases self.len(), { if !(0 <= i < self.len()) { // this supports weakening some preconditions self } else { match self { SeqInner::Nil => arbitrary(), SeqInner::Cons { head, tail } => if i == 0 { SeqInner::Cons { head: Tracked(a), tail } } else { let new_tail = tail.update(i - 1, a); SeqInner::Cons { head, tail: Tracked(new_tail) } }, } } }
spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> SeqInner<A> recommends 0 <= start_inclusive <= end_exclusive <= self.len(), decreases start_inclusive, end_exclusive - start_inclusive, { match self { SeqInner::Nil => SeqInner::Nil, SeqInner::Cons { head, tail, } => // skip elements until start_inclusive becomes 0 if start_inclusive > 0 { tail.subrange(start_inclusive - 1, end_exclusive - 1) } else { if end_exclusive <= 0 { SeqInner::Nil } else { let new_tail = tail.subrange(start_inclusive, end_exclusive - 1); SeqInner::Cons { head, tail: Tracked(new_tail) } } }, } }
spec fn add(self, rhs: SeqInner<A>) -> SeqInner<A> decreases self.len(), { match self { SeqInner::Nil => rhs, SeqInner::Cons { head, tail } => { let new_tail = tail.add(rhs); SeqInner::Cons { head, tail: Tracked(new_tail) } }, } }
spec fn insert(self, i: int, a: A) -> SeqInner<A> recommends 0 <= i <= self.len(), { self.subrange(0, i).push(a).add(self.subrange(i, self.len() as int)) }
spec fn remove(self, i: int) -> SeqInner<A> recommends 0 <= i < self.len(), { self.subrange(0, i).add(self.subrange(i + 1, self.len() as int)) }
// return the suffix proof fn tracked_split_at(tracked &mut self, i: int) -> (tracked ret: Self) requires 0 <= i <= old(self).len(), ensures *final(self) == old(self)[0..i], ret == old(self)[i..old(self).len()], final(self).len() == i, ret.len() == old(self).len() - i, decreases self.len(), { let tracked mut s = SeqInner::Nil; super::modes::tracked_swap(&mut s, self); let tracked ret = if i == 0 { seq_inner::lemma_subrange_len(*old(self), 0, i); seq_inner::lemma_empty(old(self)[0..i]); seq_inner::lemma_full_subrange_idempotent(*old(self));
s } else { let ghost old_self = s; match s { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { head, tail } => { let tracked Tracked(mut tail) = tail; let ghost old_tail = tail; let tracked suff = tail.tracked_split_at(i - 1);
let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) };
super::modes::tracked_swap(&mut new, self);
suff }, } };
assert(*final(self) == old(self)[0..i]); assert(ret == old(self)[i..old(self).len()]); seq_inner::lemma_subrange_len(*old(self), 0, i); seq_inner::lemma_subrange_len(*old(self), i, old(self).len() as int);
ret }
proof fn tracked_add(tracked &mut self, tracked mut b: Self) ensures *final(self) == old(self).add(b), final(self).len() == old(self).len() + b.len(), decreases self.len(), { let tracked mut s = SeqInner::Nil; super::modes::tracked_swap(&mut s, self); match s { SeqInner::Nil => { seq_inner::lemma_empty(*old(self)); super::modes::tracked_swap(&mut b, self); }, SeqInner::Cons { head, tail } => { let tracked Tracked(mut tail) = tail; tail.tracked_add(b); let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) }; super::modes::tracked_swap(&mut new, self); seq_inner::lemma_add_len(s, b); }, } }
proof fn tracked_insert(tracked &mut self, i: int, tracked v: A) requires 0 <= i <= old(self).len(), ensures final(self).len() == old(self).len() + 1, *final(self) == old(self).insert(i, v), decreases self.len(), { if i == self.len() { seq_inner::lemma_subrange_len(*old(self), i, self.len() as int); seq_inner::lemma_empty(old(self)[i..self.len()]); seq_inner::lemma_full_subrange_idempotent(*old(self)); seq_inner::lemma_add_empty(self.push(v)); self.tracked_push(v); } else { let tracked suff = self.tracked_split_at(i); self.tracked_push(v); self.tracked_add(suff); } }
proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A) requires 0 <= i < old(self).len(), ensures ret == old(self)[i], final(self).len() == old(self).len() - 1, *final(self) == old(self).remove(i), decreases self.len(), { if i == 0 { self.tracked_pop_front() } else { let tracked suff = self.tracked_split_at(i + 1); assert(suff == old(self)[i + 1..old(self).len()]);
let tracked ret = self.tracked_pop(); seq_inner::lemma_subrange_index(*old(self), 0, i + 1, i); assert(ret == old(self)[i]); assert(*self == old(self)[0..i + 1][0..i]); seq_inner::lemma_subrange_composition(*old(self), 0, i + 1, 0, i);
self.tracked_add(suff); ret } }
proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A) requires 0 <= i < self.len(), ensures *ret == self[i], decreases self.len(), { if i == 0 { match self { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { head, .. } => { head.borrow() }, } } else { match self { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { tail, .. } => { tail.tracked_borrow(i - 1) }, } } }
proof fn tracked_borrow_mut(tracked &mut self, i: int) -> (tracked ret: &mut A) requires 0 <= i < old(self).len(), ensures *ret == old(self)[i], *final(self) == old(self).update(i, *final(ret)), decreases self.len(), { if i == 0 { match self { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { head, .. } => { head.borrow_mut() }, } } else { match self { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { tail, .. } => { tail.tracked_borrow_mut(i - 1) }, } } }
proof fn tracked_push(tracked &mut self, tracked v: A) ensures *final(self) == old(self).push(v), final(self).len() == old(self).len() + 1, decreases self.len(), { let tracked mut s = SeqInner::Nil; super::modes::tracked_swap(&mut s, self); match s { SeqInner::Nil => { let tracked mut new = SeqInner::Cons { head: Tracked(v), tail: Tracked(SeqInner::Nil), }; super::modes::tracked_swap(&mut new, self); }, SeqInner::Cons { head, tail } => { let tracked Tracked(mut tail) = tail; tail.tracked_push(v); let tracked mut new = SeqInner::Cons { head, tail: Tracked(tail) }; super::modes::tracked_swap(&mut new, self); }, } assert(*final(self) == old(self).push(v)); seq_inner::lemma_push_len(*old(self), v); }
proof fn tracked_push_front(tracked &mut self, tracked v: A) ensures *final(self) == old(self).insert(0, v), final(self).len() == old(self).len() + 1, decreases self.len(), { self.tracked_insert(0, v); }
proof fn tracked_pop(tracked &mut self) -> (tracked ret: A) requires old(self).len() > 0, ensures ret == old(self).last(), final(self).len() == old(self).len() - 1, *final(self) == old(self)[0..old(self).len() - 1], decreases self.len(), { let tracked mut s = SeqInner::Nil; super::modes::tracked_swap(&mut s, self);
let tracked ret = match s { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { head, tail } => { let tracked Tracked(mut tail) = tail; let tracked Tracked(head) = head;
let tracked v = match tail { SeqInner::Nil => { let tracked mut new = SeqInner::Nil; super::modes::tracked_swap(&mut new, self);
seq_inner::lemma_empty(tail); seq_inner::lemma_subrange_len(*old(self), 0, old(self).len() - 1); seq_inner::lemma_empty(old(self)[0..old(self).len() - 1]);
head }, SeqInner::Cons { head: thead, tail: ttail } => { let tracked mut tail = SeqInner::Cons { head: thead, tail: ttail }; let tracked v = tail.tracked_pop();
let tracked mut new = SeqInner::Cons { head: Tracked(head), tail: Tracked(tail), }; super::modes::tracked_swap(&mut new, self);
v }, };
v }, };
assert(*final(self) == old(self)[0..old(self).len() - 1]); seq_inner::lemma_subrange_len(*old(self), 0, old(self).len() - 1);
ret }
proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A) requires old(self).len() > 0, ensures ret == old(self).first(), final(self).len() == old(self).len() - 1, *final(self) == old(self)[1..old(self).len()], { let tracked mut s = SeqInner::Nil; super::modes::tracked_swap(&mut s, self); let tracked ret = match s { SeqInner::Nil => { assert(false); proof_from_false() }, SeqInner::Cons { head, tail } => { let tracked Tracked(mut tail) = tail; let tracked Tracked(head) = head; seq_inner::lemma_tail_subrange(head, tail); assert(tail == old(self)[1..old(self).len()]); super::modes::tracked_swap(&mut tail, self); head }, };
assert(*final(self) == old(self)[1..old(self).len()]); seq_inner::lemma_subrange_len(*old(self), 1, old(self).len() as int);
ret }}
mod seq_inner { use super::*;
// empty pub(super) proof fn lemma_empty<A>(s: SeqInner<A>) ensures s.len() == 0 <==> s == SeqInner::Nil, { if s.len() == 0 { assert(s == SeqInner::Nil) } if s == SeqInner::Nil { assert(s.len() == 0); } }
// push lemmas pub(super) proof fn lemma_push_len<A>(s: SeqInner<A>, a: A) ensures s.push(a).len() == s.len() + 1, decreases s.len(), { match s { SeqInner::Nil => {}, SeqInner::Cons { tail, .. } => { lemma_push_len(tail@, a); }, } }
pub(super) proof fn lemma_push_index_different<A>(s: SeqInner<A>, a: A, i: int) requires i < s.len(), ensures #[trigger] s.push(a)[i] == s[i], decreases s, { match s { SeqInner::Nil => { lemma_index_out_of_bounds(s.push(a), i); }, SeqInner::Cons { tail, .. } => { if i == 0 { } else { lemma_push_index_different(tail@, a, i - 1); } }, } }
pub(super) proof fn lemma_push_index_same<A>(s: SeqInner<A>, a: A, i: int) requires i == s.len(), ensures #[trigger] s.push(a)[i] == a, decreases s, { match s { SeqInner::Nil => { assert(s.push(a) == SeqInner::Cons { head: Tracked(a), tail: Tracked(SeqInner::Nil), }); assert(s.push(a)[0] == a); }, SeqInner::Cons { tail, .. } => { lemma_push_index_same(tail@, a, i - 1); }, } }
// update lemmas pub(super) proof fn lemma_update_len<A>(s: SeqInner<A>, i: int, a: A) ensures s.update(i, a).len() == s.len(), decreases i, { if !(0 <= i < s.len()) { assert(s.update(i, a) == s); } else { let s_upd = s.update(i, a); match s { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { match s_upd { SeqInner::Nil => {}, SeqInner::Cons { head: head_upd, tail: tail_upd } => { if i == 0 { assert(head_upd == a); } else { lemma_update_len(tail@, (i - 1), a); } }, } }, } } }
pub(super) proof fn lemma_update_index_same<A>(s: SeqInner<A>, i: int, a: A) requires 0 <= i < s.len(), ensures #[trigger] s.update(i, a)[i] == a, decreases s, { match s { SeqInner::Nil => {}, SeqInner::Cons { tail, .. } => { if i == 0 { assert(s.update(i, a)[i] == a) } else { lemma_update_index_same(tail@, i - 1, a); } }, } }
pub(super) proof fn lemma_update_index_different<A>(s: SeqInner<A>, i1: int, i2: int, a: A) requires i1 != i2, ensures #[trigger] s.update(i2, a)[i1] == s[i1], decreases s, { if !(0 <= i2 < s.len()) { assert(s.update(i2, a) == s); } else { match s { SeqInner::Nil => {}, SeqInner::Cons { tail, .. } => { if i2 == 0 { assert(s.update(i2, a)[i1] == s[i1]); } else if i1 == 0 { assert(s.update(i2, a)[i1] == s[i1]); } else { lemma_update_index_different(tail@, i1 - 1, i2 - 1, a); } }, } } }
// subrange lemmas pub(super) proof fn lemma_subrange_len<A>(s: SeqInner<A>, j: int, k: int) requires 0 <= j <= k <= s.len(), ensures s[j..k].len() == k - j, decreases j, k, { match s { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { if j > 0 { assert(s[j..k] == tail[j - 1..k - 1]); lemma_subrange_len(tail@, j - 1, k - 1); } else if k > 0 { let new_tail = tail@[j..k - 1]; lemma_subrange_len(tail@, j, k - 1); assert(new_tail.len() == k - j - 1); let sub = SeqInner::Cons { head, tail: Tracked(new_tail) }; assert(sub.len() == 1 + new_tail.len()); } else { assert(j == k == 0); assert(s[j..k].len() == 0); } }, } }
pub(super) proof fn lemma_subrange_composition_aux2<A>(s: SeqInner<A>, j1: int, j2: int) requires 0 <= j2 <= j1 <= s.len(), ensures s[0..j1][0..j2] == s[0..j2], decreases s.len(), { if j1 == j2 { lemma_subrange_len(s, 0, j1); lemma_full_subrange_idempotent(s[0..j1]); } else if j1 == 0 { assert(false); } else if j2 == 0 { lemma_subrange_len(s[0..j1], 0, j2); lemma_empty(s[0..j1][0..j2]); } else { match s { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { lemma_subrange_composition_aux2(tail@, j1 - 1, j2 - 1); }, } } }
pub(super) proof fn lemma_subrange_index_aux<A>(s: SeqInner<A>, k: int, i: int) requires 0 <= k <= s.len(), 0 <= i < k, ensures s[0..k][i] == s[i], decreases s, { lemma_subrange_len(s, 0, k); // assert(s[0..k].len() == k); // assert(0 <= i < s[0..k].len()); match s { SeqInner::Nil => { // assert(false); }, SeqInner::Cons { head, tail } => { if i == 0 { // assert(s[0] == head); assert(s[0..k][0] == head); } else { lemma_subrange_index_aux(tail@, k - 1, i - 1); } }, } }
pub(super) proof fn lemma_subrange_index<A>(s: SeqInner<A>, j: int, k: int, i: int) requires 0 <= j <= k <= s.len(), 0 <= i < k - j, ensures s[j..k][i] == s[i + j], decreases s, { lemma_subrange_len(s, j, k); if j == 0 { lemma_subrange_index_aux(s, k, i); } else { match s { SeqInner::Nil => { assert(false); }, SeqInner::Cons { head, tail } => { lemma_subrange_index(tail@, j - 1, k - 1, i); }, } } }
pub(super) proof fn lemma_subrange_composition_aux1<A>( s: SeqInner<A>, j1: int, i2: int, j2: int, ) requires 0 <= j1 <= s.len(), 0 <= i2 <= j2 <= j1, ensures s[0..j1][i2..j2] == s[i2..j2], decreases s.len(), { if i2 == 0 { lemma_subrange_composition_aux2(s, j1, j2); } else { match s { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { lemma_subrange_composition_aux1(tail@, j1 - 1, i2 - 1, j2 - 1); }, } } }
pub(super) proof fn lemma_subrange_composition<A>( s: SeqInner<A>, i1: int, j1: int, i2: int, j2: int, ) requires 0 <= i1 <= j1 <= s.len(), 0 <= i2 <= j2 <= j1 - i1, ensures s[i1..j1][i2..j2] == s[i1 + i2..i1 + j2], decreases s.len(), { if i1 == 0 { lemma_subrange_composition_aux1(s, j1, i2, j2); } else { match s { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { lemma_subrange_composition(tail@, i1 - 1, j1 - 1, i2, j2); }, } } }
pub(super) open spec fn cons_list<A>(head: A, tail: SeqInner<A>) -> SeqInner<A> { SeqInner::Cons { head: Tracked(head), tail: Tracked(tail) } }
pub(super) proof fn lemma_tail_subrange<A>(head: A, tail: SeqInner<A>) ensures cons_list(head, tail)[1..cons_list(head, tail).len()] == tail, { let s = SeqInner::Cons { head: Tracked(head), tail: Tracked(tail) }; match s { SeqInner::Nil => { assert(false); }, SeqInner::Cons { head: h, tail: t } => { lemma_full_subrange_idempotent(tail) }, } }
pub(super) proof fn lemma_full_subrange_idempotent<A>(s: SeqInner<A>) ensures s[0..s.len()] == s, decreases s.len(), { match s { SeqInner::Nil => { assert(s[0..s.len()] == s); }, SeqInner::Cons { head, tail } => { lemma_subrange_index(s, 0, s.len() as int, 0); lemma_full_subrange_idempotent(tail@); }, } }
// decrease to index pub(super) proof fn lemma_index_decreases<A>(s: SeqInner<A>, i: int) requires 0 <= i < s.len(), ensures (decreases_to!(s => s[i])), decreases i, { match s { SeqInner::Nil => { assert(s.len() == 0); assert(false); }, SeqInner::Cons { head, tail } => { if i == 0 { assert(decreases_to!(s => s[i])); } else { assert(tail[i - 1] == s[i]); lemma_index_decreases(tail@, i - 1); assert(decreases_to!(s => tail@)); assert(decreases_to!(tail@ => tail[i-1])); } }, } }
// add lemmas pub(super) proof fn lemma_add_empty<A>(s: SeqInner<A>) ensures s.add(SeqInner::Nil) == s, SeqInner::Nil.add(s) == s, decreases s.len(), { assert(SeqInner::Nil.add(s) == s);
let sum = s.add(SeqInner::Nil); match s { SeqInner::Nil => { assert(sum == SeqInner::Nil); assert(s == SeqInner::Nil); }, SeqInner::Cons { head, tail } => { assert(sum == SeqInner::Cons { head, tail: Tracked(tail@.add(SeqInner::Nil)) }); lemma_add_empty(tail@); }, } }
pub(super) proof fn lemma_add_len<A>(s1: SeqInner<A>, s2: SeqInner<A>) ensures s1.add(s2).len() == s1.len() + s2.len(), decreases s1.add(s2).len(), { let sum = s1.add(s2); match s1 { SeqInner::Nil => { assert(sum == s2); }, SeqInner::Cons { head, tail } => { let new_tail = tail@.add(s2); lemma_add_len(tail@, s2); assert(new_tail.len() == (s1.len() - 1) + s2.len()); assert(sum.len() == 1 + new_tail.len()); }, } }
pub(super) proof fn lemma_add_index1<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int) requires i < s1.len(), ensures s1.add(s2)[i] == s1[i], decreases s1, { if i < 0 { lemma_index_out_of_bounds(s1, i); lemma_index_out_of_bounds(s1.add(s2), i); } else { match s1 { SeqInner::Nil => {}, SeqInner::Cons { head, tail } => { if i == 0 { assert(s1[i] == s1.add(s2)[i]); } else { lemma_add_index1(tail@, s2, i - 1); } }, } } }
pub(super) proof fn lemma_add_index2<A>(s1: SeqInner<A>, s2: SeqInner<A>, i: int) requires s1.len() <= i < s1.len() + s2.len(), ensures s1.add(s2)[i] == s2[i - s1.len()], decreases s1, { match s1 { SeqInner::Nil => { assert(s1.add(s2) == s2); assert(s1.add(s2)[i] == s2[i - s1.len()]); }, SeqInner::Cons { head, tail } => { if i == 0 { assert(s1.add(s2)[i] == s2[i - s1.len()]); } else { lemma_add_index2(tail@, s2, i - 1); assert(s1.add(s2)[i] == s2[i - s1.len()]); } }, } }
// index lemma pub(super) proof fn lemma_index_out_of_bounds<A>(s: SeqInner<A>, i: int) requires !(0 <= i < s.len()), ensures s[i] == arbitrary::<A>(), decreases s, { match s { SeqInner::Nil => {}, SeqInner::Cons { tail, .. } => { lemma_index_out_of_bounds(tail@, i - 1); }, } }
}
/// `Seq<A>` is a sequence type for specifications./// To use a "sequence" in compiled code, use an `exec` type like `vec::Vec`/// that has `Seq<A>` as its specification type.////// An object `seq: Seq<A>` has a length, given by [`seq.len()`](Seq::len),/// and a value at each `i` for `0 <= i < seq.len()`, given by [`seq[i]`](Seq::index).////// Sequences can be constructed in a few different ways:/// * [`Seq::empty`] construct an empty sequence (`len() == 0`)/// * [`Seq::new`] construct a sequence of a given length, initialized according/// to a given function mapping indices `i` to values `A`./// * The [`seq!`] macro, to construct small sequences of a fixed size (analagous to the/// [`std::vec!`] macro)./// * By manipulating an existing sequence with [`Seq::push`], [`Seq::update`],/// or [`Seq::add`].////// To prove that two sequences are equal, it is usually easiest to use the/// extensional equality operator `=~=`.#[verifier::ext_equal]#[verifier::accept_recursive_types(A)]pub tracked struct Seq<A> { inner: SeqInner<A>,}
impl<A> Seq<A> { /// An empty sequence (i.e., a sequence of length 0). #[rustc_diagnostic_item = "verus::vstd::seq::Seq::empty"] pub closed spec fn empty() -> Seq<A> { Seq { inner: SeqInner::Nil } }
/// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`. #[rustc_diagnostic_item = "verus::vstd::seq::Seq::new"] pub closed spec fn new(len: nat, f: spec_fn(int) -> A) -> Seq<A> decreases len, { if len == 0 { Seq { inner: SeqInner::Nil } } else { Self::new((len - 1) as nat, f).push(f(len - 1)) } }
/// The length of a sequence. #[rustc_diagnostic_item = "verus::vstd::seq::Seq::len"] pub closed spec fn len(self) -> nat { self.inner.len() }
/// Gets the value at the given index `i`. /// /// If `i` is not in the range `[0, self.len())`, then the resulting value /// is meaningless and arbitrary. #[rustc_diagnostic_item = "verus::vstd::seq::Seq::index"] pub closed spec fn index(self, i: int) -> A recommends 0 <= i < self.len(), { self.inner.index(i) }
/// `[]` operator, synonymous with `index` #[verifier::inline] pub open spec fn spec_index(self, i: int) -> A recommends 0 <= i < self.len(), { self.index(i) }
/// `[..]` operator, which returns the original Seq #[verifier::inline] pub open spec fn spec_index_range_full(self) -> Seq<A> { self }
/// `[i..]` operator, synonymous with `skip` #[verifier::inline] pub open spec fn spec_index_range_from<I: Integer>(self, i: I) -> Seq<A> recommends 0 <= i as int <= self.len(), { self.skip(i as int) }
/// `[..j]` operator, synonymous with `take` #[verifier::inline] pub open spec fn spec_index_range_to<J: Integer>(self, j: J) -> Seq<A> recommends 0 <= j as int <= self.len(), { self.take(j as int) }
/// `[..=j]` operator, synonymous with `take` on j + 1 #[verifier::inline] pub open spec fn spec_index_range_to_inclusive<J: Integer>(self, j: J) -> Seq<A> recommends 0 <= (j as int) < self.len(), { self.take(j as int + 1) }
/// `[i..j]` operator, synonymous with `subrange` #[verifier::inline] pub open spec fn spec_index_range<I: Integer, J: Integer>(self, i: I, j: J) -> Seq<A> recommends 0 <= i as int <= j as int <= self.len(), { self.subrange(i as int, j as int) }
/// `[i..=j]` operator, synonymous with `subrange` on j + 1 #[verifier::inline] pub open spec fn spec_index_range_inclusive<I: Integer, J: Integer>(self, i: I, j: J) -> Seq<A> recommends 0 <= i as int <= (j as int) < self.len(), { self.subrange(i as int, j as int + 1) }
/// Appends the value `a` to the end of the sequence. /// This always increases the length of the sequence by 1. /// This often requires annotating the type of the element literal in the sequence, /// e.g., `10int`. /// /// ## Example /// /// ```rust /// proof fn push_test() { /// assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]); /// } /// ``` #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"] pub closed spec fn push(self, a: A) -> Seq<A> { Seq { inner: self.inner.push(a) } }
/// Updates the sequence at the given index, replacing the element with the given /// value, and leaves all other entries unchanged. /// /// ## Example /// /// ```rust /// proof fn update_test() { /// let s = seq![10, 11, 12, 13, 14]; /// let t = s.update(2, -5); /// assert(t =~= seq![10, 11, -5, 13, 14]); /// } /// ``` #[rustc_diagnostic_item = "verus::vstd::seq::Seq::update"] pub closed spec fn update(self, i: int, a: A) -> Seq<A> recommends 0 <= i < self.len(), { Seq { inner: self.inner.update(i, a) } }
/// Returns a sequence for the given subrange. /// /// ## Example /// /// ```rust /// proof fn subrange_test() { /// let s = seq![10int, 11, 12, 13, 14]; /// // ^-------^ /// // 0 1 2 3 4 5 /// let sub = s[2..4]; /// assert(sub =~= seq![12, 13]); /// } /// ``` #[rustc_diagnostic_item = "verus::vstd::seq::Seq::subrange"] pub closed spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A> recommends 0 <= start_inclusive <= end_exclusive <= self.len(), { Seq { inner: self.inner.subrange(start_inclusive, end_exclusive) } }
/// Returns a sequence containing only the first n elements of the original sequence #[verifier::inline] pub open spec fn take(self, n: int) -> Seq<A> { self.subrange(0, n) }
/// Returns a sequence without the first n elements of the original sequence #[verifier::inline] pub open spec fn skip(self, n: int) -> Seq<A> { self.subrange(n, self.len() as int) }
/// Concatenates the sequences. /// /// ## Example /// /// ```rust /// proof fn add_test() { /// assert(seq![10int, 11].add(seq![12, 13, 14]) /// =~= seq![10, 11, 12, 13, 14]); /// } /// ``` #[rustc_diagnostic_item = "verus::vstd::seq::Seq::add"] pub closed spec fn add(self, rhs: Seq<A>) -> Seq<A> { Seq { inner: self.inner.add(rhs.inner) } }
/// `+` operator, synonymous with `add` #[verifier::inline] pub open spec fn spec_add(self, rhs: Seq<A>) -> Seq<A> { self.add(rhs) }
/// Returns the last element of the sequence. #[rustc_diagnostic_item = "verus::vstd::seq::Seq::last"] pub open spec fn last(self) -> A recommends 0 < self.len(), { self[self.len() as int - 1] }
/// Returns the first element of the sequence. #[rustc_diagnostic_item = "vstd::seq::Seq::first"] pub open spec fn first(self) -> A recommends 0 < self.len(), { self[0] }
/// Create an empty sequence pub proof fn tracked_empty() -> (tracked ret: Self) ensures ret == Seq::empty(), { Seq { inner: SeqInner::Nil } }
/// Insert a tracked element into a sequence /// /// ## Example /// /// ```rust /// proof fn insert_test(tracked &mut s: Seq<int>, tracked v: int) /// requires /// old(s)@ == seq![0, 1, 2] /// ensures /// final(s)@ == seq![0, 1, v, 2] /// { /// s.tracked_insert(2, v) /// } /// ``` pub proof fn tracked_insert(tracked &mut self, i: int, tracked v: A) requires 0 <= i <= old(self).len(), ensures final(self).len() == old(self).len() + 1, *final(self) == old(self).insert(i, v), { self.inner.tracked_insert(i, v) }
/// Remove a tracked element from a sequence pub proof fn tracked_remove(tracked &mut self, i: int) -> (tracked ret: A) requires 0 <= i < old(self).len(), ensures ret == old(self)[i], final(self).len() == old(self).len() - 1, *final(self) == old(self).remove(i), { self.inner.tracked_remove(i) }
/// Obtain a tracked borrow into an element of a sequence pub proof fn tracked_borrow(tracked &self, i: int) -> (tracked ret: &A) requires 0 <= i < self.len(), ensures *ret == self[i], { self.inner.tracked_borrow(i) }
/// Obtain a tracked mutable borrow into an element of a sequence pub proof fn tracked_borrow_mut(tracked &mut self, i: int) -> (tracked ret: &mut A) requires 0 <= i < old(self).len(), ensures *ret == old(self)[i], *final(self) == old(self).update(i, *final(ret)), { self.inner.tracked_borrow_mut(i) }
/// Push a tracked value into the end of a sequence pub proof fn tracked_push(tracked &mut self, tracked v: A) ensures *final(self) == old(self).push(v), final(self).len() == old(self).len() + 1, { self.inner.tracked_push(v) }
/// Push a tracked value into the beginning of a sequence pub proof fn tracked_push_front(tracked &mut self, tracked v: A) ensures *final(self) == old(self).insert(0, v), final(self).len() == old(self).len() + 1, { self.inner.tracked_push_front(v) }
/// Pop a tracked value from the end of a sequence pub proof fn tracked_pop(tracked &mut self) -> (tracked ret: A) requires old(self).len() > 0, ensures ret == old(self).last(), final(self).len() == old(self).len() - 1, *final(self) == old(self)[..old(self).len() - 1], { self.inner.tracked_pop() }
/// Pop a tracked value from the beginning of a sequence pub proof fn tracked_pop_front(tracked &mut self) -> (tracked ret: A) requires old(self).len() > 0, ensures ret == old(self).first(), final(self).len() == old(self).len() - 1, *final(self) == old(self).drop_first(), { self.inner.tracked_pop_front() }
/// Split a tracked sequence around an index pub proof fn tracked_split_at(tracked &mut self, i: int) -> (tracked ret: Self) requires 0 <= i <= old(self).len(), ensures *final(self) == old(self)[0..i], ret == old(self)[i..old(self).len()], final(self).len() == i, ret.len() == old(self).len() - i, { Seq { inner: self.inner.tracked_split_at(i) } }
proof fn tracked_add(tracked &mut self, tracked b: Self) ensures *final(self) == old(self).add(b), final(self).len() == old(self).len() + b.len(), { self.inner.tracked_add(b.inner) }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_index_decreases<A>(s: Seq<A>, i: int) requires 0 <= i < s.len(), ensures #[trigger] (decreases_to!(s => s[i])),{ lemma_seq_index_decreases(s, i)}
pub broadcast proof fn lemma_seq_index_decreases<A>(s: Seq<A>, i: int) requires 0 <= i < s.len(), ensures #[trigger] (decreases_to!(s => s[i])),{ seq_inner::lemma_index_decreases(s.inner, i)}
// TODO: this should be provablepub axiom fn axiom_seq_len_decreases<A>(s1: Seq<A>, s2: Seq<A>) requires s2.len() < s1.len(), forall|i2: int| 0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) ==> exists|i1: int| 0 <= i1 < s1.len() && s1[i1] == s2[i2], ensures decreases_to!(s1 => s2),;
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int) requires 0 <= i <= j <= s.len(), s[i..j].len() < s.len(), ensures #[trigger] (decreases_to!(s => s[i..j])),{ lemma_seq_subrange_decreases(s, i, j)}
pub broadcast proof fn lemma_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int) requires 0 <= i <= j <= s.len(), s[i..j].len() < s.len(), ensures #[trigger] (decreases_to!(s => s[i..j])),{ broadcast use {lemma_seq_subrange_len, lemma_seq_subrange_index};
let s2 = s[i..j]; assert forall|i2: int| 0 <= i2 < s2.len() && #[trigger] trigger(s2[i2]) implies exists|i1: int| 0 <= i1 < s.len() && s[i1] == s2[i2] by { assert(s[i + i2] == s2[i2]); } axiom_seq_len_decreases(s, s2);}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_empty<A>() ensures #[trigger] Seq::<A>::empty().len() == 0,{ broadcast use lemma_seq_empty;
}
pub broadcast proof fn lemma_seq_empty<A>() ensures #[trigger] Seq::<A>::empty().len() == 0,{ let s = Seq::<A>::empty(); match s.inner { SeqInner::Nil => { assert(s == Seq { inner: SeqInner::Nil }); }, SeqInner::Cons { tail, .. } => { let seq_tail = Seq { inner: tail@ }; assert(s.len() == 1 + seq_tail.len()); assert(s.len() > 0); }, }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_new_len<A>(len: nat, f: spec_fn(int) -> A) ensures #[trigger] Seq::new(len, f).len() == len,{ lemma_seq_new_len(len, f)}
pub broadcast proof fn lemma_seq_new_len<A>(len: nat, f: spec_fn(int) -> A) ensures #[trigger] Seq::new(len, f).len() == len, decreases len,{ let s = Seq::new(len, f); if len == 0 { assert(s.len() == 0); } else { broadcast use lemma_seq_push_len;
let pref = Seq::new((len - 1) as nat, f); lemma_seq_new_len((len - 1) as nat, f); assert(pref.len() == (len - 1) as nat);
let s2 = pref.push(f(len - 1)); assert(s2.len() == pref.len() + 1);
assert(s == s2); assert(s.len() == len); }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int) requires 0 <= i < len, ensures #[trigger] Seq::new(len, f)[i] == f(i),{ lemma_seq_new_index(len, f, i)}
pub broadcast proof fn lemma_seq_new_index<A>(len: nat, f: spec_fn(int) -> A, i: int) requires 0 <= i < len, ensures #[trigger] Seq::new(len, f)[i] == f(i), decreases len,{ broadcast use lemma_seq_new_len;
let s = Seq::new(len, f); assert(s.len() == len);
let pref = Seq::new((len - 1) as nat, f); assert(pref.len() == len - 1);
let a = f(len - 1); assert(s == pref.push(a));
if i == len - 1 { lemma_seq_push_index_same(pref, a, i); assert(s[i] == a); } else { assert(0 <= i < (len - 1)); lemma_seq_new_index((len - 1) as nat, f, i); lemma_seq_push_index_different(pref, a, i); }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_push_len<A>(s: Seq<A>, a: A) ensures #[trigger] s.push(a).len() == s.len() + 1,{ lemma_seq_push_len(s, a)}
pub broadcast proof fn lemma_seq_push_len<A>(s: Seq<A>, a: A) ensures #[trigger] s.push(a).len() == s.len() + 1,{ seq_inner::lemma_push_len(s.inner, a)}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_push_index_same<A>(s: Seq<A>, a: A, i: int) requires i == s.len(), ensures #[trigger] s.push(a)[i] == a,{ lemma_seq_push_index_same(s, a, i)}
pub broadcast proof fn lemma_seq_push_index_same<A>(s: Seq<A>, a: A, i: int) requires i == s.len(), ensures #[trigger] s.push(a)[i] == a,{ seq_inner::lemma_push_index_same(s.inner, a, i);}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_push_index_different<A>(s: Seq<A>, a: A, i: int) requires i < s.len(), ensures #[trigger] s.push(a)[i] == s[i],{ lemma_seq_push_index_different(s, a, i)}
pub broadcast proof fn lemma_seq_push_index_different<A>(s: Seq<A>, a: A, i: int) requires i < s.len(), ensures #[trigger] s.push(a)[i] == s[i],{ seq_inner::lemma_push_index_different(s.inner, a, i);}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_push_index_different_alt<A>(s: Seq<A>, a: A, i: int) requires i < s.len(), ensures (#[trigger] s.push(a))[i] == #[trigger] s[i],{ broadcast use lemma_seq_push_index_different;
}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_update_len<A>(s: Seq<A>, i: int, a: A) ensures #[trigger] s.update(i, a).len() == s.len(),{ lemma_seq_update_len(s, i, a)}
pub broadcast proof fn lemma_seq_update_len<A>(s: Seq<A>, i: int, a: A) ensures #[trigger] s.update(i, a).len() == s.len(), decreases i,{ seq_inner::lemma_update_len(s.inner, i, a)}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_update_same<A>(s: Seq<A>, i: int, a: A) requires 0 <= i < s.len(), ensures #[trigger] s.update(i, a)[i] == a,{ lemma_seq_update_same(s, i, a)}
pub broadcast proof fn lemma_seq_update_same<A>(s: Seq<A>, i: int, a: A) requires 0 <= i < s.len(), ensures #[trigger] s.update(i, a)[i] == a,{ seq_inner::lemma_update_index_same(s.inner, i, a);}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_update_same_alt<A>(s: Seq<A>, i: int, a: A) requires 0 <= i < s.len(), ensures #![trigger s.update(i, a), s[i]] s.update(i, a)[i] == a,{ broadcast use lemma_seq_update_same;
}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A) requires i1 != i2, ensures #[trigger] s.update(i2, a)[i1] == s[i1],{ lemma_seq_update_different(s, i1, i2, a)}
pub broadcast proof fn lemma_seq_update_different<A>(s: Seq<A>, i1: int, i2: int, a: A) requires i1 != i2, ensures #[trigger] s.update(i2, a)[i1] == s[i1],{ seq_inner::lemma_update_index_different(s.inner, i1, i2, a);}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_update_different_alt<A>(s: Seq<A>, i1: int, i2: int, a: A) requires i1 != i2, ensures (#[trigger] s.update(i2, a))[i1] == #[trigger] s[i1],{ broadcast use lemma_seq_update_different;
}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] (s1 =~= s2) <==> { &&& s1.len() == s2.len() &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i] },{ lemma_seq_ext_equal(s1, s2)}
pub broadcast proof fn lemma_seq_ext_equal<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] (s1 =~= s2) <==> { &&& s1.len() == s2.len() &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i] }, decreases s1.len(),{ match s1.inner { SeqInner::Nil => { assert(s1.len() == s2.len() <==> s1 =~= s2); }, SeqInner::Cons { head: head1, tail: tail1 } => { let seq_tail1 = Seq { inner: tail1@ };
match s2.inner { SeqInner::Nil => { assert(s1.len() != s2.len()); }, SeqInner::Cons { head: head2, tail: tail2 } => { if head1 != head2 { assert(s1[0] != s2[0]); } else { let seq_tail2 = Seq { inner: tail2@ }; lemma_seq_ext_equal(seq_tail1, seq_tail2); if seq_tail1 =~= seq_tail2 { assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1 == s2.len()); assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by { if i == 0 { assert(s1[0] == s2[0]); } else { assert(s1[i] == s2[i]); } } } else if seq_tail1.len() == seq_tail2.len() { assert(exists|i: int| 0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]); let i = choose|i: int| 0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]; assert(s1[i + 1] != s2[i + 1]); } else { assert(s1.len() != s2.len()); } } }, } }, }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] (s1 =~~= s2) <==> { &&& s1.len() == s2.len() &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i] },{ lemma_seq_ext_equal_deep(s1, s2)}
pub broadcast proof fn lemma_seq_ext_equal_deep<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] (s1 =~~= s2) <==> { &&& s1.len() == s2.len() &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i] },{ match s1.inner { SeqInner::Nil => { assert(s1.len() == s2.len() <==> s1 =~~= s2); }, SeqInner::Cons { head: head1, tail: tail1 } => { let seq_tail1 = Seq { inner: tail1@ };
match s2.inner { SeqInner::Nil => { assert(s1.len() != s2.len()); }, SeqInner::Cons { head: head2, tail: tail2 } => { if head1 != head2 { assert(s1[0] != s2[0]); } else { let seq_tail2 = Seq { inner: tail2@ }; lemma_seq_ext_equal(seq_tail1, seq_tail2); if seq_tail1 =~~= seq_tail2 { assert(s1.len() == seq_tail1.len() + 1 == seq_tail2.len() + 1 == s2.len()); assert forall|i: int| 0 <= i < s1.len() implies s1[i] == s2[i] by { if i == 0 { assert(s1[0] == s2[0]); } else { assert(s1[i] == s2[i]); } } } else if seq_tail1.len() == seq_tail2.len() { assert(exists|i: int| 0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]); let i = choose|i: int| 0 <= i < seq_tail1.len() && seq_tail1[i] != seq_tail2[i]; assert(s1[i + 1] != s2[i + 1]); } else { assert(s1.len() != s2.len()); } } }, } }, }}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int) requires 0 <= j <= k <= s.len(), ensures #[trigger] s[j..k].len() == k - j,{ lemma_seq_subrange_len(s, j, k)}
pub broadcast proof fn lemma_seq_subrange_len<A>(s: Seq<A>, j: int, k: int) requires 0 <= j <= k <= s.len(), ensures #[trigger] s[j..k].len() == k - j,{ seq_inner::lemma_subrange_len(s.inner, j, k)}
pub broadcast proof fn lemma_seq_subrange_composition<A>( s: Seq<A>, i1: int, j1: int, i2: int, j2: int,) requires 0 <= i1 <= j1 <= s.len(), 0 <= i2 <= j2 <= j1 - i1, ensures #[trigger] s[i1..j1][i2..j2] == s[i1 + i2..i1 + j2],{ seq_inner::lemma_subrange_composition(s.inner, i1, j1, i2, j2)}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int) requires 0 <= j <= k <= s.len(), 0 <= i < k - j, ensures #[trigger] s[j..k][i] == s[i + j],{ lemma_seq_subrange_index(s, j, k, i)}
pub broadcast proof fn lemma_seq_subrange_index<A>(s: Seq<A>, j: int, k: int, i: int) requires 0 <= j <= k <= s.len(), 0 <= i < k - j, ensures #[trigger] s[j..k][i] == s[i + j],{ seq_inner::lemma_subrange_index(s.inner, j, k, i);}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_subrange_index_alt<A>(s: Seq<A>, j: int, k: int, i: int) requires 0 <= j <= k <= s.len(), 0 <= i - j < k - j, ensures (#[trigger] s[j..k])[i - j] == #[trigger] s[i],{ broadcast use lemma_seq_subrange_index;
}
// Less expensive, more limited alternative to lemma_seq_subrange_index_altpub broadcast proof fn lemma_seq_two_subranges_index<A>(s: Seq<A>, j: int, k1: int, k2: int, i: int) requires 0 <= j <= k1 <= s.len(), 0 <= j <= k2 <= s.len(), 0 <= i < k1 - j, 0 <= i < k2 - j, ensures #[trigger] s[j..k1][i] == (#[trigger] s[j..k2])[i],{ broadcast use lemma_seq_subrange_index;
}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] s1.add(s2).len() == s1.len() + s2.len(),{ lemma_seq_add_len(s1, s2)}
pub broadcast proof fn lemma_seq_add_len<A>(s1: Seq<A>, s2: Seq<A>) ensures #[trigger] s1.add(s2).len() == s1.len() + s2.len(),{ seq_inner::lemma_add_len(s1.inner, s2.inner);}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires i < s1.len(), ensures #[trigger] s1.add(s2)[i] == s1[i],{ lemma_seq_add_index1(s1, s2, i)}
pub broadcast proof fn lemma_seq_add_index1<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires i < s1.len(), ensures #[trigger] s1.add(s2)[i] == s1[i],{ seq_inner::lemma_add_index1(s1.inner, s2.inner, i)}
#[deprecated(note = "Seq axioms have been verified, and are now lemmas")]pub broadcast proof fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires s1.len() <= i < s1.len() + s2.len(), ensures #[trigger] s1.add(s2)[i] == s2[i - s1.len()],{ lemma_seq_add_index2(s1, s2, i)}
pub broadcast proof fn lemma_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires s1.len() <= i < s1.len() + s2.len(), ensures #[trigger] s1.add(s2)[i] == s2[i - s1.len()],{ seq_inner::lemma_add_index2(s1.inner, s2.inner, i);}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_add_index1_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires 0 <= i < s1.len(), ensures (#[trigger] s1.add(s2))[i] == #[trigger] s1[i],{ broadcast use lemma_seq_add_index1;
}
// Expensive lemma; not in the default broadcast grouppub broadcast proof fn lemma_seq_add_index2_alt<A>(s1: Seq<A>, s2: Seq<A>, i: int) requires 0 <= i < s2.len(), ensures (#[trigger] s1.add(s2))[i + s1.len()] == #[trigger] s2[i],{ broadcast use lemma_seq_add_index2;
}
#[deprecated(note = "Use `group_seq_lemmas` instead")]pub broadcast group group_seq_axioms { lemma_seq_index_decreases, lemma_seq_subrange_decreases, lemma_seq_empty, lemma_seq_new_len, lemma_seq_new_index, lemma_seq_push_len, lemma_seq_push_index_same, lemma_seq_push_index_different, lemma_seq_update_len, lemma_seq_update_same, lemma_seq_update_different, lemma_seq_ext_equal, lemma_seq_ext_equal_deep, lemma_seq_subrange_len, lemma_seq_subrange_index, lemma_seq_two_subranges_index, lemma_seq_add_len, lemma_seq_add_index1, lemma_seq_add_index2,}
pub broadcast group group_seq_lemmas { lemma_seq_index_decreases, lemma_seq_subrange_decreases, lemma_seq_empty, lemma_seq_new_len, lemma_seq_new_index, lemma_seq_push_len, lemma_seq_push_index_same, lemma_seq_push_index_different, lemma_seq_update_len, lemma_seq_update_same, lemma_seq_update_different, lemma_seq_ext_equal, lemma_seq_ext_equal_deep, lemma_seq_subrange_len, lemma_seq_subrange_index, lemma_seq_two_subranges_index, lemma_seq_add_len, lemma_seq_add_index1, lemma_seq_add_index2,}
// Expensive lemmas not in the default group (may slow down verification)pub broadcast group group_seq_lemmas_expensive { lemma_seq_push_index_different_alt, lemma_seq_update_same_alt, lemma_seq_update_different_alt, lemma_seq_subrange_index_alt, lemma_seq_add_index1_alt, lemma_seq_add_index2_alt,}
// ------------- Macros ---------------- //#[doc(hidden)]#[macro_export]macro_rules! seq_internal { [] => { $crate::vstd::seq::Seq::empty() }; [$elem:expr] => { $crate::vstd::seq::Seq::empty() .push($elem) }; [$elem:expr,] => { $crate::vstd::seq::Seq::empty() .push($elem) }; [$($elem:expr),* $(,)?] => { <_ as $crate::vstd::view::View>::view(&[$($elem),*]) }; [$elem:expr; $n:expr] => { $crate::vstd::seq::Seq::new( $n, $crate::vstd::prelude::closure_to_fn_spec( |_x: _| $elem ), ) };}
/// Creates a [`Seq`] containing the given elements.////// ## Example////// ```rust/// let s = seq![11int, 12, 13];////// assert(s.len() == 3);/// assert(s[0] == 11);/// assert(s[1] == 12);/// assert(s[2] == 13);/// ```#[macro_export]macro_rules! seq { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::seq::seq_internal!($($tail)*)) };}
#[doc(hidden)]pub use seq_internal;pub use seq;
} // verus!