Linked List insertion in Dafny

LinkedList.dfy

module LL {
    ghost predicate distinct<T(==)>(items: seq<T>) {
        forall i,j :: 0<= i < j < |items| && i!=j ==> items[i] != items[j]
    }
    class Node {
        var data: int
        var next: Node?
        
        ghost var footprint: set<object>
        ghost var ancestorRepr: set<Node>
        ghost var contents: seq<int>
        
        ghost predicate valid()
            decreases footprint
            reads this, footprint
        {
            (this in footprint &&
            |this.contents| >= 1 && 
            this.contents[0] == this.data && 
            (this.next != null ==> 
                next in footprint &&
                footprint == {this}+next.footprint &&
                next.footprint <= footprint &&
                this !in next.footprint &&
                this.contents == [data]+next.contents && 
                next.valid()) &&
            (next == null ==> |contents| == 1 && footprint == {this} && this.contents == [data])
            )
        }
        
        constructor(data: int, next: Node?)
            requires next != null ==> next.valid()
            ensures fresh(this)
            ensures this.data == data
            ensures this.next == next
            ensures |this.contents| >= 1 && this.contents[0] == data
            ensures next == null ==> this.footprint == {this}
            ensures next != null ==> this.footprint == {this}+next.footprint
            ensures valid()
        {
            this.data := data;
            this.next := next;
            this.contents := if next == null then [data] else [data]+next.contents;
            this.footprint := if next == null then {this} else {this}+next.footprint;
        }
        
        function Length(node: Node?): nat
            reads set x | node != null && x in node.footprint
            decreases if node == null then {} else node.footprint
            requires node != null ==> node.valid()
        {
            if node == null then 0 else if node.next == null then 1 else 
            assert node.valid();
            assert node.next != null;
            1 + Length(node.next)
        }

        lemma LengthContent(node: Node)
            requires node.valid()
            decreases node.footprint
            ensures |node.contents| == Length(node)
        {
            if node.next == null {

            }else{
                LengthContent(node.next);
            }
        }
        
        method enqueueMid(d: int, pos: int)
            requires valid()
            requires 0 <= pos < |contents|
            modifies footprint
            ensures valid()
            // ensures valid() && fresh(footprint - old(footprint))
        {
            var i: int := 0;
            var curr := this;
            ghost var until := contents[..i];
            assert until == [];
            assert contents == [] + contents[i..];
            ghost var after := contents[i..];
            assert curr.next != null ==> curr.contents == contents[i..];
            assert curr.next == null ==> after == contents[i..];
            ghost var revList: seq<Node> := [];
            
            while(i < pos && curr.next != null)
                invariant i <= |contents|
                invariant curr != null
                invariant curr != null ==> curr.valid()
                invariant i == 0 ==> curr == this
                invariant until == contents[..i]
                invariant after == contents[i..]
                invariant after == curr.contents
                invariant |revList| == i
                invariant |revList| > 0 ==> revList[0].next == curr && revList[|revList|-1] == this
                invariant forall n :: n in revList ==> n in footprint-curr.footprint
                invariant forall k :: 1 <= k < |revList| ==> revList[k-1] == revList[k].next
                invariant forall k :: 0 <= k < |revList| ==> revList[k] in footprint
                invariant curr !in revList
                invariant distinct(revList)
                decreases if curr != null then curr.footprint else {}
            {
                assert contents == contents[..i]+contents[i..];
                until := until+[curr.data];
                after := curr.next.contents;
                ghost var oldcurr := curr;
                assert oldcurr !in curr.next.footprint;
                revList := [curr]+revList;
                curr := curr.next;
                i := i + 1;
                
            }
            assert until == contents[..i]; 
            assert after == contents[i..];
            if i > 0 {

            assert revList[0].next == curr;
            }else{
                assert curr == this;
            }

            var n := new Node(d, null);
            assert curr != null;
            // // n.data := d;
            
            if(curr.next == null) {
                assert n.valid();
                assert n.contents == [d];
                assert curr.contents == [curr.data];
                curr.next := n;
                assert curr.next.contents == n.contents;
                curr.footprint := {curr}+n.footprint;
                curr.contents := [curr.data]+[d];
                label ready:
                assert curr.valid();
                if |revList| == 0 {
                    assert this.valid();
                }else{
                    // for j:=0 to |revList|
                    //     invariant unchanged@ready(curr)
                    //     invariant forall k :: 0 <= k < j ==> revList[k].valid()
                    // {
                    //     if j == 0 {
                    //         revList[0].contents := [revList[0].data]+curr.contents;
                    //         revList[0].footprint := {revList[0]}+curr.footprint;
                    //         assert revList[0].next == curr;
                    //         assert curr.valid();
                    //         assert revList[0].valid();

                    //     }else{

                    //     }
                    // }
                }
                // contents := contents + [d]; 
                // assert this.valid();
                // ghost var gcurr := this;
                // while gcurr != null && gcurr != curr 
                //     decreases gcurr.footprint
                // {
                //     gcurr := gcurr.next;
                // }
                
            } else {
            //     assert contents[pos..] == curr.contents;
            //     n.next := curr.next;
            //     n.footprint := n.footprint + curr.footprint - {curr}; // acyclicity!
            //     curr.footprint := curr.footprint + n.footprint;
            //     curr.next := n;
            //     contents := contents[ .. pos] + [d] + contents[pos ..];
            }
            
            // footprint := footprint + n.footprint;
            // assert valid(); // error: could not prove: next in footprint. could not prove: next.valid()
        }
    }
}