From fda7ef92473758f9ab3ae1705875cdcb1bda0552 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 13 May 2024 19:29:50 -0700 Subject: [PATCH] deleted old files --- Test/civl/samples/treiber-stack-v2.bpl | 417 ------------------ Test/civl/samples/treiber-stack-v2.bpl.expect | 2 - Test/civl/samples/treiber-stack.bpl | 333 +++++++------- Test/civl/samples/treiber-stack.bpl.expect | 2 +- 4 files changed, 173 insertions(+), 581 deletions(-) delete mode 100644 Test/civl/samples/treiber-stack-v2.bpl delete mode 100644 Test/civl/samples/treiber-stack-v2.bpl.expect diff --git a/Test/civl/samples/treiber-stack-v2.bpl b/Test/civl/samples/treiber-stack-v2.bpl deleted file mode 100644 index fec92527c..000000000 --- a/Test/civl/samples/treiber-stack-v2.bpl +++ /dev/null @@ -1,417 +0,0 @@ -// RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -datatype LocPiece { Left(), Right() } -const AllLocPieces: [LocPiece]bool; -axiom AllLocPieces == MapConst(false)[Left() := true][Right() := true]; - -type TreiberNode _; -type LocTreiberNode T = Fraction (Loc (TreiberNode T)) LocPiece; -type StackElem T = Node (LocTreiberNode T) T; -type StackMap T = Map (LocTreiberNode T) (StackElem T); -datatype Treiber { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) } - -type X; // module type parameter - -var {:layer 4, 5} Stack: Map (Loc (Treiber X)) (Vec X); -var {:layer 0, 4} {:linear} ts: Map (Loc (Treiber X)) (Treiber X); - -/// Yield invariants - -function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) { - ts->val[loc_t]->stack->dom -} - -yield invariant {:layer 1} Yield(); - -yield invariant {:layer 2} TopInStack(loc_t: Loc (Treiber X)); -invariant Map_Contains(ts, loc_t); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall loc_n: LocTreiberNode X :: Set_Contains(Domain(ts, loc_t), loc_n) ==> - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); - -yield invariant {:layer 2} LocInStack(loc_t: Loc (Treiber X), loc_n: Option (LocTreiberNode X)); -invariant Map_Contains(ts, loc_t); -invariant loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); - -yield invariant {:layer 4} ReachInStack(loc_t: Loc (Treiber X)); -invariant Map_Contains(ts, loc_t); -invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); -invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall {:pool "A"} loc_n: LocTreiberNode X :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> - loc_n == Fraction(loc_n->val, Left(), AllLocPieces) && - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); -invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t)); - -yield invariant {:layer 4} StackDom(); -invariant Stack->dom == ts->dom; - -yield invariant {:layer 4} PushLocInStack( - loc_t: Loc (Treiber X), node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)); -invariant Map_Contains(ts, loc_t); -invariant Set_Contains(Domain(ts, loc_t), new_loc_n); -invariant right_loc_piece->val == Fraction(new_loc_n->val, Right(), AllLocPieces); -invariant new_loc_n == Fraction(new_loc_n->val, Left(), AllLocPieces); -invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !BetweenSet(t->stack->val, t->top, None())[new_loc_n]); - -/// Layered implementation - -atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc (Treiber X)) -modifies Stack; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - - call one_loc_t := One_New(); - loc_t := one_loc_t->val; - assume !Map_Contains(Stack, loc_t); - Stack := Map_Update(Stack, loc_t, Vec_Empty()); -} -yield procedure {:layer 4} Alloc() returns (loc_t: Loc (Treiber X)) -refines AtomicAlloc; -preserves call StackDom(); -{ - var top: Option (LocTreiberNode X); - var {:linear} stack: StackMap X; - var {:linear} treiber: Treiber X; - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - - top := None(); - call stack := Map_MakeEmpty(); - treiber := Treiber(top, stack); - call one_loc_t := One_New(); - call cell_t := Cell_Pack(one_loc_t, treiber); - loc_t := one_loc_t->val; - call AllocTreiber#0(cell_t); - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); - call {:layer 4} AbsLemma(treiber); -} - -atomic action {:layer 5} AtomicPush(loc_t: Loc (Treiber X), x: X) returns (success: bool) -modifies Stack; -{ - if (*) { - Stack := Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x)); - success := true; - } else { - success := false; - } -} -yield procedure {:layer 4} Push(loc_t: Loc (Treiber X), x: X) returns (success: bool) -refines AtomicPush; -preserves call TopInStack(loc_t); -preserves call ReachInStack(loc_t); -preserves call StackDom(); -{ - var loc_n: Option (LocTreiberNode X); - var new_loc_n: LocTreiberNode X; - var {:linear} right_loc_piece: One (LocTreiberNode X); - var {:layer 4} old_treiber: Treiber X; - - call {:layer 4} old_treiber := Copy(ts->val[loc_t]); - call loc_n, new_loc_n, right_loc_piece := AllocNode#3(loc_t, x); - call {:layer 4} FrameLemma(old_treiber, ts->val[loc_t]); - par ReachInStack(loc_t) | StackDom() | PushLocInStack(loc_t, Node(loc_n, x), new_loc_n, right_loc_piece); - call success := WriteTopOfStack#0(loc_t, loc_n, Some(new_loc_n)); - if (success) { - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x))); - assert {:layer 4} ts->val[loc_t]->top != None(); - call {:layer 4} AbsLemma(ts->val[loc_t]); - } -} - -atomic action {:layer 5} AtomicPop(loc_t: Loc (Treiber X)) returns (success: bool, x: X) -modifies Stack; -{ - var stack: Vec X; - - if (*) { - stack := Map_At(Stack, loc_t); - assume Vec_Len(stack) > 0; - x := Vec_Nth(stack, Vec_Len(stack) - 1); - Stack := Map_Update(Stack, loc_t, Vec_Remove(stack)); - success := true; - } else { - success := false; - } -} -yield procedure {:layer 4} Pop(loc_t: Loc (Treiber X)) returns (success: bool, x: X) -refines AtomicPop; -preserves call TopInStack(loc_t); -preserves call ReachInStack(loc_t); -preserves call StackDom(); -{ - call {:layer 4} AbsLemma(ts->val[loc_t]); - call success, x := PopIntermediate(loc_t); - if (success) { - assert {:layer 4} Vec_Len(Map_At(Stack, loc_t)) > 0; - call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Remove(Map_At(Stack, loc_t)))); - } -} - -atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc (Treiber X), x: X) - returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var top: Option (LocTreiberNode X); - var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One (Loc (TreiberNode X)); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); - var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); - - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - Treiber(top, stack) := treiber; - assume loc_n is None || Map_Contains(stack, loc_n->t); - call one_loc_n := One_New(); - call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces); - call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces)); - new_loc_n := left_loc_piece->val; - call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces)); - call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); - call Map_Put(stack, cell_n); - treiber := Treiber(top, stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 3} AllocNode#3(loc_t: Loc (Treiber X), x: X) - returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) -preserves call TopInStack(loc_t); -ensures call LocInStack(loc_t, Some(new_loc_n)); -refines AtomicAllocNode#3; -{ - var {:linear} one_loc_n: One (Loc (TreiberNode X)); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); - var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); - - call loc_n := ReadTopOfStack#2(loc_t); - call one_loc_n := One_New(); - call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces); - call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces)); - new_loc_n := left_loc_piece->val; - call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces)); - call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); - call AllocNode#0(loc_t, cell_n); -} - -atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var loc_n: Option (LocTreiberNode X); - var {:linear} treiber: Treiber X; - var top: Option (LocTreiberNode X); - var {:linear} stack: StackMap X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - - assert Map_Contains(ts, loc_t); - if (success) { - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - Treiber(top, stack) := treiber; - assume top != None(); - assume Map_Contains(stack, top->t); - Node(loc_n, x) := Map_At(stack, top->t); - treiber := Treiber(loc_n, stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); - } -} -yield procedure {:layer 3} PopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X) -refines AtomicPopIntermediate; -preserves call TopInStack(loc_t); -{ - var loc_n, new_loc_n: Option (LocTreiberNode X); - var node: StackElem X; - - success := false; - call loc_n := ReadTopOfStack#2(loc_t); - if (loc_n == None()) { - return; - } - par LocInStack(loc_t, loc_n) | TopInStack(loc_t); - call node := LoadNode#0(loc_t, loc_n->t); - call Yield(); - Node(new_loc_n, x) := node; - call success := WriteTopOfStack#0(loc_t, loc_n, new_loc_n); -} - -right action {:layer 3} AtomicReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -{ - assert Map_Contains(ts, loc_t); - assume loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); -} -yield procedure {:layer 2} ReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -preserves call TopInStack(loc_t); -ensures call LocInStack(loc_t, loc_n); -refines AtomicReadTopOfStack#2; -{ - call loc_n := ReadTopOfStack#0(loc_t); -} - -right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) -{ - assert Map_Contains(ts, loc_t); - assert Map_Contains(Map_At(ts, loc_t)->stack, loc_n); - node := Map_At(Map_At(ts, loc_t)->stack, loc_n); -} - -// primitives - -atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) -modifies ts; -refines AtomicLoadNode#1; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - var top: Option (LocTreiberNode X); - var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One (LocTreiberNode X); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - Treiber(top, stack) := treiber; - call cell_n := Map_Get(stack, loc_n); - call one_loc_n, node := Cell_Unpack(cell_n); - call cell_n := Cell_Pack(one_loc_n, node); - call Map_Put(stack, cell_n); - treiber := Treiber(top, stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} LoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X); -refines AtomicLoadNode#0; - -atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - loc_n := treiber->top; - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)); -refines AtomicReadTopOfStack#0; - -atomic action {:layer 1,4} AtomicWriteTopOfStack#0( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool) -modifies ts; -{ - var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - var {:linear} one_loc_t: One (Loc (Treiber X)); - - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - if (old_loc_n == treiber->top) { - treiber->top := new_loc_n; - success := true; - } else { - success := false; - } - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} WriteTopOfStack#0( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool); -refines AtomicWriteTopOfStack#0; - -atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - call Map_Put(treiber->stack, cell_n); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} AllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); -refines AtomicAllocNode#0; - -atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)) -modifies ts; -{ - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)); -refines AtomicAllocTreiber#0; - -/// Proof of abstraction with a manual encoding of termination - -// Abs and AbsDefinition together model the abstraction function -function Abs(treiber: Treiber X): Vec X; -function {:inline} AbsDefinition(treiber: Treiber X): Vec X { -if treiber->top == None() then - Vec_Empty() else - (var n := Map_At(treiber->stack, treiber->top->t); - (var treiber' := Treiber(n->next, treiber->stack); - Vec_Append(Abs(treiber'), n->val))) -} - -pure procedure AbsCompute(treiber: Treiber X, treiber': Treiber X) returns (absStack: Vec X) -requires treiber->top == treiber'->top; -requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == - MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); -ensures absStack == AbsDefinition(treiber); -ensures absStack == AbsDefinition(treiber'); -free ensures absStack == Abs(treiber); -free ensures absStack == Abs(treiber'); -{ - var loc_n: Option (LocTreiberNode X); - var n: StackElem X; - - if (treiber->top == None()) { - absStack := Vec_Empty(); - } else { - loc_n := treiber->top; - assert Map_Contains(treiber->stack, loc_n->t); // soundness of framing - n := Map_At(treiber->stack, loc_n->t); - assert Between(treiber->stack->val, loc_n, n->next, None()); // soundness of termination (for induction) - call absStack := AbsCompute(Treiber(n->next, treiber->stack), Treiber(n->next, treiber'->stack)); - absStack := Vec_Append(absStack, n->val); - } -} - -/// Useful lemmas obtained by wrapping AbsCompute - -pure procedure AbsLemma(treiber: Treiber X) -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); -ensures Abs(treiber) == AbsDefinition(treiber); -{ - var absStack: Vec X; - call absStack := AbsCompute(treiber, treiber); -} - -pure procedure FrameLemma(treiber: Treiber X, treiber': Treiber X) -requires treiber->top == treiber'->top; -requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == - MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); -requires Between(treiber->stack->val, treiber->top, treiber->top, None()); -requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); -ensures Abs(treiber) == Abs(treiber'); -{ - var absStack: Vec X; - call absStack := AbsCompute(treiber, treiber'); -} diff --git a/Test/civl/samples/treiber-stack-v2.bpl.expect b/Test/civl/samples/treiber-stack-v2.bpl.expect deleted file mode 100644 index b3847fc1a..000000000 --- a/Test/civl/samples/treiber-stack-v2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 31 verified, 0 errors diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 9d0f65431..fec92527c 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -1,8 +1,12 @@ // RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t" // RUN: %diff "%s.expect" "%t" +datatype LocPiece { Left(), Right() } +const AllLocPieces: [LocPiece]bool; +axiom AllLocPieces == MapConst(false)[Left() := true][Right() := true]; + type TreiberNode _; -type LocTreiberNode T = Loc (TreiberNode T); +type LocTreiberNode T = Fraction (Loc (TreiberNode T)) LocPiece; type StackElem T = Node (LocTreiberNode T) T; type StackMap T = Map (LocTreiberNode T) (StackElem T); datatype Treiber { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) } @@ -12,6 +16,47 @@ type X; // module type parameter var {:layer 4, 5} Stack: Map (Loc (Treiber X)) (Vec X); var {:layer 0, 4} {:linear} ts: Map (Loc (Treiber X)) (Treiber X); +/// Yield invariants + +function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) { + ts->val[loc_t]->stack->dom +} + +yield invariant {:layer 1} Yield(); + +yield invariant {:layer 2} TopInStack(loc_t: Loc (Treiber X)); +invariant Map_Contains(ts, loc_t); +invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); +invariant (forall loc_n: LocTreiberNode X :: Set_Contains(Domain(ts, loc_t), loc_n) ==> + (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); + +yield invariant {:layer 2} LocInStack(loc_t: Loc (Treiber X), loc_n: Option (LocTreiberNode X)); +invariant Map_Contains(ts, loc_t); +invariant loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); + +yield invariant {:layer 4} ReachInStack(loc_t: Loc (Treiber X)); +invariant Map_Contains(ts, loc_t); +invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); +invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); +invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); +invariant (forall {:pool "A"} loc_n: LocTreiberNode X :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> + loc_n == Fraction(loc_n->val, Left(), AllLocPieces) && + (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); +invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t)); + +yield invariant {:layer 4} StackDom(); +invariant Stack->dom == ts->dom; + +yield invariant {:layer 4} PushLocInStack( + loc_t: Loc (Treiber X), node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)); +invariant Map_Contains(ts, loc_t); +invariant Set_Contains(Domain(ts, loc_t), new_loc_n); +invariant right_loc_piece->val == Fraction(new_loc_n->val, Right(), AllLocPieces); +invariant new_loc_n == Fraction(new_loc_n->val, Left(), AllLocPieces); +invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !BetweenSet(t->stack->val, t->top, None())[new_loc_n]); + +/// Layered implementation + atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc (Treiber X)) modifies Stack; { @@ -24,7 +69,7 @@ modifies Stack; } yield procedure {:layer 4} Alloc() returns (loc_t: Loc (Treiber X)) refines AtomicAlloc; -preserves call YieldInvDom#4(); +preserves call StackDom(); { var top: Option (LocTreiberNode X); var {:linear} stack: StackMap X; @@ -38,7 +83,7 @@ preserves call YieldInvDom#4(); call one_loc_t := One_New(); call cell_t := Cell_Pack(one_loc_t, treiber); loc_t := one_loc_t->val; - call AllocTreiber(cell_t); + call AllocTreiber#0(cell_t); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty())); call {:layer 4} AbsLemma(treiber); } @@ -46,22 +91,30 @@ preserves call YieldInvDom#4(); atomic action {:layer 5} AtomicPush(loc_t: Loc (Treiber X), x: X) returns (success: bool) modifies Stack; { - if (success) { + if (*) { Stack := Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x)); + success := true; + } else { + success := false; } } yield procedure {:layer 4} Push(loc_t: Loc (Treiber X), x: X) returns (success: bool) refines AtomicPush; -preserves call YieldInv#2(loc_t); -preserves call YieldInv#4(loc_t); -preserves call YieldInvDom#4(); +preserves call TopInStack(loc_t); +preserves call ReachInStack(loc_t); +preserves call StackDom(); { + var loc_n: Option (LocTreiberNode X); + var new_loc_n: LocTreiberNode X; + var {:linear} right_loc_piece: One (LocTreiberNode X); var {:layer 4} old_treiber: Treiber X; call {:layer 4} old_treiber := Copy(ts->val[loc_t]); - call success := PushIntermediate(loc_t, x); + call loc_n, new_loc_n, right_loc_piece := AllocNode#3(loc_t, x); + call {:layer 4} FrameLemma(old_treiber, ts->val[loc_t]); + par ReachInStack(loc_t) | StackDom() | PushLocInStack(loc_t, Node(loc_n, x), new_loc_n, right_loc_piece); + call success := WriteTopOfStack#0(loc_t, loc_n, Some(new_loc_n)); if (success) { - call {:layer 4} FrameLemma(old_treiber, Treiber(old_treiber->top, ts->val[loc_t]->stack)); call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x))); assert {:layer 4} ts->val[loc_t]->top != None(); call {:layer 4} AbsLemma(ts->val[loc_t]); @@ -73,19 +126,21 @@ modifies Stack; { var stack: Vec X; - if (success) { + if (*) { stack := Map_At(Stack, loc_t); assume Vec_Len(stack) > 0; x := Vec_Nth(stack, Vec_Len(stack) - 1); Stack := Map_Update(Stack, loc_t, Vec_Remove(stack)); + success := true; + } else { + success := false; } } yield procedure {:layer 4} Pop(loc_t: Loc (Treiber X)) returns (success: bool, x: X) refines AtomicPop; -preserves call YieldInv#2(loc_t); -preserves call YieldInv#3(loc_t); -preserves call YieldInv#4(loc_t); -preserves call YieldInvDom#4(); +preserves call TopInStack(loc_t); +preserves call ReachInStack(loc_t); +preserves call StackDom(); { call {:layer 4} AbsLemma(ts->val[loc_t]); call success, x := PopIntermediate(loc_t); @@ -95,6 +150,56 @@ preserves call YieldInvDom#4(); } } +atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc (Treiber X), x: X) + returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) +modifies ts; +{ + var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} treiber: Treiber X; + var top: Option (LocTreiberNode X); + var {:linear} stack: StackMap X; + var {:linear} one_loc_n: One (Loc (TreiberNode X)); + var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); + var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); + + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); + Treiber(top, stack) := treiber; + assume loc_n is None || Map_Contains(stack, loc_n->t); + call one_loc_n := One_New(); + call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces); + call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces)); + new_loc_n := left_loc_piece->val; + call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces)); + call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); + call Map_Put(stack, cell_n); + treiber := Treiber(top, stack); + call cell_t := Cell_Pack(one_loc_t, treiber); + call Map_Put(ts, cell_t); +} +yield procedure {:layer 3} AllocNode#3(loc_t: Loc (Treiber X), x: X) + returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) +preserves call TopInStack(loc_t); +ensures call LocInStack(loc_t, Some(new_loc_n)); +refines AtomicAllocNode#3; +{ + var {:linear} one_loc_n: One (Loc (TreiberNode X)); + var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); + var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); + var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); + + call loc_n := ReadTopOfStack#2(loc_t); + call one_loc_n := One_New(); + call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces); + call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces)); + new_loc_n := left_loc_piece->val; + call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces)); + call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x)); + call AllocNode#0(loc_t, cell_n); +} + atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X) modifies ts; { @@ -105,7 +210,7 @@ modifies ts; var {:linear} stack: StackMap X; var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - assume Map_Contains(ts, loc_t); + assert Map_Contains(ts, loc_t); if (success) { call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); @@ -120,135 +225,48 @@ modifies ts; } yield procedure {:layer 3} PopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X) refines AtomicPopIntermediate; -preserves call YieldInv#2(loc_t); -preserves call YieldInv#3(loc_t); +preserves call TopInStack(loc_t); { var loc_n, new_loc_n: Option (LocTreiberNode X); var node: StackElem X; success := false; - call loc_n := ReadTopOfStack#Pop(loc_t); + call loc_n := ReadTopOfStack#2(loc_t); if (loc_n == None()) { return; } - call node := LoadNode(loc_t, loc_n->t); + par LocInStack(loc_t, loc_n) | TopInStack(loc_t); + call node := LoadNode#0(loc_t, loc_n->t); + call Yield(); Node(new_loc_n, x) := node; - call success := WriteTopOfStack#Pop(loc_t, loc_n, new_loc_n); + call success := WriteTopOfStack#0(loc_t, loc_n, new_loc_n); } -atomic action {:layer 3, 4} AtomicPushIntermediate(loc_t: Loc (Treiber X), x: X) returns (success: bool) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var top: Option (LocTreiberNode X); - var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One (LocTreiberNode X); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - - success := false; - if (*) { - success := true; - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - Treiber(top, stack) := treiber; - call one_loc_n := One_New(); - call cell_n := Cell_Pack(one_loc_n, Node(top, x)); - call Map_Put(stack, cell_n); - treiber := Treiber(Some(one_loc_n->val), stack); - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); - } -} -yield procedure {:layer 2} PushIntermediate(loc_t: Loc (Treiber X), x: X) returns (success: bool) -refines AtomicPushIntermediate; -preserves call YieldInv#2(loc_t); -{ - var loc_n: Option (LocTreiberNode X); - var new_loc_n: LocTreiberNode X; - var {:linear} one_loc_n: One (LocTreiberNode X); - var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - - call loc_n := ReadTopOfStack#Push(loc_t); - call one_loc_n := One_New(); - new_loc_n := one_loc_n->val; - call cell_n := Cell_Pack(one_loc_n, Node(loc_n, x)); - call success := WriteTopOfStack(loc_t, loc_n, Some(new_loc_n)); - if (success) { - call AllocNode(loc_t, cell_n); - } -} - -right action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +right action {:layer 3} AtomicReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) { assert Map_Contains(ts, loc_t); assume loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); } -yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -refines AtomicReadTopOfStack#Pop; -preserves call YieldInv#2(loc_t); -{ - call loc_n := ReadTopOfStack(loc_t); -} - -right action {:layer 2} AtomicReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -{ - assert Map_Contains(ts, loc_t); -} -yield procedure {:layer 1} ReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -refines AtomicReadTopOfStack#Push; +yield procedure {:layer 2} ReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +preserves call TopInStack(loc_t); +ensures call LocInStack(loc_t, loc_n); +refines AtomicReadTopOfStack#2; { - call loc_n := ReadTopOfStack(loc_t); + call loc_n := ReadTopOfStack#0(loc_t); } -right action {:layer 3} AtomicLoadNode(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) -modifies ts; +right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) { assert Map_Contains(ts, loc_t); assert Map_Contains(Map_At(ts, loc_t)->stack, loc_n); node := Map_At(Map_At(ts, loc_t)->stack, loc_n); } -yield procedure {:layer 2} LoadNode(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) -refines AtomicLoadNode; -preserves call YieldInv#2(loc_t); -{ - call node := LoadNode#0(loc_t, loc_n); -} - -atomic action {:layer 3} AtomicWriteTopOfStack#Pop( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool) -modifies ts; -{ - assert new_loc_n is None || Set_Contains(Domain(ts, loc_t), new_loc_n->t); - call r := AtomicWriteTopOfStack(loc_t, old_loc_n, new_loc_n); -} -yield procedure {:layer 2} WriteTopOfStack#Pop( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool) -refines AtomicWriteTopOfStack#Pop; -preserves call YieldInv#2(loc_t); -{ - call r := WriteTopOfStack(loc_t, old_loc_n, new_loc_n); -} - -atomic action {:layer 1, 2} AtomicReadTopOfStack(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) -modifies ts; -{ - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - call cell_t := Map_Get(ts, loc_t); - call one_loc_t, treiber := Cell_Unpack(cell_t); - loc_n := treiber->top; - call cell_t := Cell_Pack(one_loc_t, treiber); - call Map_Put(ts, cell_t); -} -yield procedure {:layer 0} ReadTopOfStack(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)); -refines AtomicReadTopOfStack; +// primitives -atomic action {:layer 1,2} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) +atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) modifies ts; +refines AtomicLoadNode#1; { var {:linear} one_loc_t: One (Loc (Treiber X)); var {:linear} treiber: Treiber X; @@ -261,7 +279,6 @@ modifies ts; call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); Treiber(top, stack) := treiber; - assume Map_Contains(stack, loc_n); // problematic assume call cell_n := Map_Get(stack, loc_n); call one_loc_n, node := Cell_Unpack(cell_n); call cell_n := Cell_Pack(one_loc_n, node); @@ -273,8 +290,7 @@ modifies ts; yield procedure {:layer 0} LoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X); refines AtomicLoadNode#0; -left action {:layer 1, 2} AtomicAllocNode( - loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)) +atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) modifies ts; { var {:linear} one_loc_t: One (Loc (Treiber X)); @@ -283,16 +299,15 @@ modifies ts; call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); - call Map_Put(treiber->stack, cell_n); + loc_n := treiber->top; call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} AllocNode( - loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); -refines AtomicAllocNode; +yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)); +refines AtomicReadTopOfStack#0; -atomic action {:layer 1, 3} AtomicWriteTopOfStack( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool) +atomic action {:layer 1,4} AtomicWriteTopOfStack#0( + loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool) modifies ts; { var {:linear} treiber: Treiber X; @@ -303,53 +318,45 @@ modifies ts; call one_loc_t, treiber := Cell_Unpack(cell_t); if (old_loc_n == treiber->top) { treiber->top := new_loc_n; - r := true; + success := true; } else { - r := false; + success := false; } call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} WriteTopOfStack( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool); -refines AtomicWriteTopOfStack; +yield procedure {:layer 0} WriteTopOfStack#0( + loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool); +refines AtomicWriteTopOfStack#0; -atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)) +atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)) modifies ts; { + var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} treiber: Treiber X; + var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + + call cell_t := Map_Get(ts, loc_t); + call one_loc_t, treiber := Cell_Unpack(cell_t); + call Map_Put(treiber->stack, cell_n); + call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} AllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)); -refines AtomicAllocTreiber; +yield procedure {:layer 0} AllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); +refines AtomicAllocNode#0; -function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) { - ts->val[loc_t]->stack->dom +atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)) +modifies ts; +{ + call Map_Put(ts, cell_t); } +yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)); +refines AtomicAllocTreiber#0; -yield invariant {:layer 2} YieldInv#2(loc_t: Loc (Treiber X)); -invariant Map_Contains(ts, loc_t); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); - -yield invariant {:layer 3} YieldInv#3(loc_t: Loc (Treiber X)); -invariant Map_Contains(ts, loc_t); -invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall loc_n: LocTreiberNode X :: - Set_Contains(Domain(ts, loc_t), loc_n) ==> - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; - loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); - -yield invariant {:layer 4} YieldInv#4(loc_t: Loc (Treiber X)); -invariant Map_Contains(ts, loc_t); -invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t)); -invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); -invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); +/// Proof of abstraction with a manual encoding of termination -yield invariant {:layer 4} YieldInvDom#4(); -invariant Stack->dom == ts->dom; - -// The following is a manual encoding of the termination proof for the abstraction. +// Abs and AbsDefinition together model the abstraction function function Abs(treiber: Treiber X): Vec X; - function {:inline} AbsDefinition(treiber: Treiber X): Vec X { if treiber->top == None() then Vec_Empty() else @@ -361,7 +368,8 @@ if treiber->top == None() then pure procedure AbsCompute(treiber: Treiber X, treiber': Treiber X) returns (absStack: Vec X) requires treiber->top == treiber'->top; requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); +requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == + MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); requires Between(treiber->stack->val, treiber->top, treiber->top, None()); requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); ensures absStack == AbsDefinition(treiber); @@ -384,6 +392,8 @@ free ensures absStack == Abs(treiber'); } } +/// Useful lemmas obtained by wrapping AbsCompute + pure procedure AbsLemma(treiber: Treiber X) requires Between(treiber->stack->val, treiber->top, treiber->top, None()); requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); @@ -396,7 +406,8 @@ ensures Abs(treiber) == AbsDefinition(treiber); pure procedure FrameLemma(treiber: Treiber X, treiber': Treiber X) requires treiber->top == treiber'->top; requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val); -requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); +requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == + MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default())); requires Between(treiber->stack->val, treiber->top, treiber->top, None()); requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val); ensures Abs(treiber) == Abs(treiber'); diff --git a/Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/samples/treiber-stack.bpl.expect index d1133fcfb..b3847fc1a 100644 --- a/Test/civl/samples/treiber-stack.bpl.expect +++ b/Test/civl/samples/treiber-stack.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 59 verified, 0 errors +Boogie program verifier finished with 31 verified, 0 errors