I’m working on a textbook exercise that requires implementing a bounded stack and queue in Dafny with specific behaviors. The stack should behave as a last-in, first-out (LIFO) structure, and the queue as a first-in, first-out (FIFO) structure using two stacks. I have written the code for both classes, but I am facing verification errors that I cannot resolve.

This is my current code and I keep getting the following errors and am unsure where the root of the issue is, nor how to solve it:

class Stack<T(0)> {
    // Abstract state
    ghost var Elements: seq<T>
    ghost var Repr: set<object>
    ghost const max: nat  
    // concrete state
    var data: array<T>
    var top: nat
   
    ghost predicate Valid()
        reads this, Repr
        ensures Valid() ==> this in Repr && 0 <= |Elements| <= max
   {
        this in Repr &&
        data in Repr &&
        data.Length == max && 
        0 <= top <= max &&
        Elements == if top < max then data[..top] else data[..max]
    }

    constructor (max: nat)
        requires max > 0
        ensures Valid() && fresh(Repr)
        ensures Elements == [] && this.max == max
    {
        Elements := [];
        this.max := max;
        data := new T[max];
        top := 0;
        Repr := {this, data};
    }
         
    predicate IsEmpty() 
        reads this
    {this.top == 0}


    method Push(v: T)
        requires Valid() && |Elements| < max
        modifies Repr, this
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Elements == old(Elements) + [v]
    {
        Elements := old(Elements) + [v];
        data[top] := v;
        top := top + 1;
    }

    method Pop() returns (v: T)
        requires Valid() && !(IsEmpty()) && |Elements| != 0 
        modifies Repr
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Elements == old(Elements[..|Elements| - 1])
        ensures v == old(Elements[|Elements| - 1]) // Returned element is last element in stack (LIFO)
    {
        top := top - 1;
        v := data[top];
        Elements := data[..top];
    }
}

class Queue<T(0)> {
    // Abstract state
    ghost var Elements: seq<T>
    ghost var Repr: set<object>
    ghost var max: nat 

    // Concrete state
    var stack1: Stack<T>
    var stack2: Stack<T>

    ghost predicate Valid()
        reads this, Repr, stack1, stack2
        ensures Valid() ==> this in Repr && |Elements| > 0
    {
        this in Repr &&
        stack1 in Repr && stack1.Repr <= Repr && this !in stack1.Repr && stack1.Valid() &&
        stack2 in Repr && stack2.Repr <= Repr && this !in stack2.Repr && stack2.Valid()
    }
    
    constructor (max: nat)
    requires max > 0
    ensures Valid() && fresh(Repr)
    ensures Elements == [] && this.max == max
    {
        this.max := max;
        stack1 := new Stack<T>(max);
        stack2 := new Stack<T>(max);
        Elements := [];
        Repr := {this, stack1, stack2};
    }

    method Add(v: T)
        requires Valid() && |Elements| < max
        modifies Repr
        ensures Valid() && fresh(Repr-old(Repr))
        ensures Elements == old(Elements) + [v]
        ensures max == old(max)
    {
        stack1.Push(v);
        Elements := Elements + [v];
    }
    
    method Remove() returns (v:T)
        requires Valid() && |Elements| != 0
        modifies Repr
        ensures Valid() && fresh(Repr-old(Repr))
        ensures Elements == old(Elements[1..])
        ensures v == old(Elements[0])
        ensures max == old(max)
}

The errors I am getting are:

• This postcondition might not hold: |Elements| > 0 (Stack Valid Predicate)
• Could not prove: stack1.Repr <= Repr (Queue Valid predicate)