give-up.rav

include "./flows_ra.rav"
include "./ccm_instances.rav"
include "./keyset_ra.rav"

import Library.Type
import Library.CancellativeResourceAlgebra

interface Keyspace {
  rep type T

  val ks: Set[T]
}

module IntKeyspace : Keyspace {
  rep type T = Int

  val ks: Set[T] = {| k: Int :: true |}
}

interface SearchStructureSpec {
  type K
  val keyspace: Set[K]

  type Op = data { case searchOp ; case insertOp ; case deleteOp }

	func opSpec(op: Op, k: K, c_in: Set[K]) returns (c_out_res: (Set[K], Bool)) {
    op == searchOp() ? 
      ((c_in, (k in c_in))) :
    (op == insertOp() ?
      ((c_in ++ {| k |}, (k !in c_in))) :
      ((c_in -- {| k |}, (k in c_in))))
	}
}

interface NodeImpl {

  module Spec : SearchStructureSpec
  import Spec._

  module K_Type : Library.Type {
    rep type T = K
  }

  module Multiset_K = Multiset[K_Type]
  module Flow_K = FlowsRA[Multiset_K]

  import Flow_K._
  import Multiset_K.elem

  pred node(n: Ref; c: Set[K], flow_int: Flow_K)

  // func outsets(outset: Map[Ref, Set[K]]) returns (ret: Set[K])
  // {
  //   {| k: K :: exists r: Ref :: k in outset[r] |}
  // }

  // func keyset(inset: Set[K], outset: Map[Ref, Set[K]]) returns (ret: Set[K])
  // {
  //   inset -- outsets(outset)
  // }

  func inset(i: Flow_K.T, n: Ref) returns (ret: Set[K])
  {
    {| k : K :: (i.inf[n])[k] > 0 |}
  }

  func insets(i: Flow_K.T) returns (ret: Set[K])
  {
    {| k : K :: exists n: Ref :: n in i.dom && k in inset(i, n) |}
  }

  func outset(i: Flow_K.T, n: Ref) returns (ret: Set[K])
  {
    {| k : K :: (i.out[n])[k] > 0 |}
  }

  func outsets(i: Flow_K.T) returns (ret: Set[K])
  {
    {| k: K :: exists n: Ref :: {outset(i,n)} n !in i.dom && k in outset(i,n) |}
  }

  func keyset(i: Flow_K.T) returns (ret: Set[K])
  {
    insets(i) -- outsets(i)
  }

  proc createRoot()
    returns (r: Ref)
    ensures node(r, {||}, 
    Flow_K.int({| l:Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |}))

  proc decisiveOp(dop: Op, n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
    returns (succ: Bool, res: Bool, implicit ghost c1: Set[K])
    requires k in keyset(i_n)
    requires node(n, c, i_n)
    ensures node(n, c1, i_n)
    ensures succ ==> opSpec(dop, k, c) == ((c1, res)) 
    ensures !succ ==> c == c1

  proc findNext(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
    returns (ret: Bool, n1: Ref)
    requires k in inset(i_n, n)
    requires node(n, c, i_n)
    ensures node(n, c, i_n) && 
      (ret ?   
        k in outset(i_n, n1) :
        k !in outsets(i_n))

  proc inRange(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
    returns (ret: Bool)
    requires node(n, c, i_n)
    ensures node(n, c, i_n) && (ret ==> k in inset(i_n, n))


  lemma nodeSepStar(n: Ref, c1: Set[K], c2: Set[K], i_n1: Flow_K, i_n2: Flow_K)
    requires node(n, c1, i_n1) && node(n, c2, i_n2)
    ensures false
}

// interface SearchStructure {
//   module Spec: SearchStructureSpec
//   import Spec._

//   pred css(r: Ref, c: Set[K])

//   // inv cssInv(r: Ref)

//   proc create()
//     returns (r: Ref)
//     ensures css(r, {||})

//   // proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K])
//   //   returns (res: Bool, implicit ghost c1: Set[K])
//   //   requires k in keyset
//   //   // requires cssInv(r)
//   //   atomic requires cssR(r, c)
//   //   atomic ensures cssR(r, c1) && opSpec(dop, k, c, c1, res)
// }


interface GiveUpTemplate[Node: NodeImpl] {
  module Spec: SearchStructureSpec = Node.Spec
  import Node.Spec._
  import Node._
  import Node.Flow_K._
  import Node.Multiset_K.elem
  import Node.Multiset_K.fromSet

  module Ref_Type : Library.Type {
    rep type T = Ref
  }

  module SetRefRA = Library.SetRA[Ref_Type]

  module AuthSetRef = Library.Auth[SetRefRA]
    
  module Keyset_K = KeysetRA[K_Type]
  module AuthKeyset_K = Library.Auth[Keyset_K]
  module AuthFlow_K = Library.Auth[Flow_K]

  ghost field authSet: AuthSetRef
  ghost field authKS: AuthKeyset_K
  ghost field authFlow: AuthFlow_K
  field lock: Int

  proc lockNode(n: Ref, implicit ghost b: Int)
    atomic requires own(n.lock, b, 1.0)
    atomic ensures own(n.lock, 1, 1.0) && b == 0

  proc unlockNode(n: Ref)
    atomic requires own(n.lock, 1, 1.0)
    atomic ensures own(n.lock, 0, 1.0)

  proc lockNodeHigh(r: Ref, n: Ref, implicit ghost c: Set[K])
    returns (ghost c_n : Set[K], ghost i_n: Flow_K)
    requires inFP(r, n)
    atomic requires css(r, c)
    atomic ensures css(r, c) && nodePred(r, n, c_n, i_n) && inFP(r, n)
  {
    ghost var phi := bindAU();

    ghost var g_i0: Flow_K;
    ghost var lockval0: Map[Ref, Int];
    ghost var contents0: Map[Ref, Set[K]];
    ghost var intf0: Map[Ref, Flow_K];
    
    ghost val c0: Set[K] := openAU(phi);
    unfold css(r, c0);
    g_i0, lockval0, contents0, intf0 :| cssR(r, c0, g_i0, lockval0, contents0, intf0);
    cssInFp(r, n, c0, g_i0, lockval0, contents0, intf0);

    unfold cssR(r, c0, g_i0, lockval0, contents0, intf0);

    lockNode(n, lockval0[n]);
    ghost var lockval00: Map[Ref, Int] := lockval0[n := 1];
    fold cssR(r, c0, g_i0, lockval00, contents0, intf0);
    assert cssR(r, c0, g_i0, lockval00, contents0, intf0);
    fold css(r, c0);

    commitAU(phi, contents0[n], intf0[n]);
    return contents0[n], intf0[n];
  }

  proc unlockNodeHigh(r: Ref, n: Ref, ghost c_n: Set[K], ghost i_n: Flow_K, implicit ghost c: Set[K])
    requires inFP(r, n)
    requires nodePred(r, n, c_n, i_n)
    atomic requires css(r, c)
    atomic ensures css(r, c) && inFP(r, n)
  {
    ghost var phi := bindAU();

    ghost var g_i1: Flow_K;
    ghost var lockval1: Map[Ref, Int];
    ghost var contents1: Map[Ref, Set[K]];
    ghost var intf1: Map[Ref, Flow_K];
    
    ghost val c1: Set[K] := openAU(phi);
    unfold css(r, c1);
    g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1);
    cssInFp(r, n, c1, g_i1, lockval1, contents1, intf1);
    
    unfold cssR(r, c1, g_i1, lockval1, contents1, intf1);
    
    {!
      if (lockval1[n] != 1) {
        unfold nodePred(r, n, contents1[n], intf1[n]);
        unfold nodePred(r, n, c_n, i_n);
        Node.nodeSepStar(n, c_n, contents1[n], i_n, intf1[n]);
      }
    !}

    unlockNode(n);
    ghost var lockval2: Map[Ref, Int] := lockval1[n := 0];
    ghost var contents2: Map[Ref, Set[K]] := contents1[n := c_n];
    ghost var intf2: Map[Ref, Flow_K] := intf1[n := i_n];
    
    fold cssR(r, c1, g_i1, lockval2, contents2, intf2);
    assert cssR(r, c1, g_i1, lockval2, contents2, intf2);
    fold css(r, c1);

    commitAU(phi);
  }
  

  pred globalinv(g_i: Flow_K, r: Ref) {
      Flow_K.valid(g_i) &&
      r in g_i.dom &&
      outsets(g_i) == {||} &&
      inset(g_i, r) == keyspace  
  }

  pred globalRes(r: Ref, c: Set[K], g_i: Flow_K) {
    own(r.authKS, AuthKeyset_K.auth( Keyset_K.prodKS( keyspace, c ))) &&
    own(r.authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom))) && 
    own(r.authFlow, AuthFlow_K.auth(g_i)) &&
    globalinv(g_i, r)
  }

  pred nodePred(r: Ref, n: Ref; c: Set[K], i_n: Flow_K) {
    own(r.authKS, AuthKeyset_K.frag( Keyset_K.prodKS( keyset(i_n), c ) )) &&
    own(r.authFlow, AuthFlow_K.frag(i_n)) &&
    i_n.dom == {|n|} && 
    node(n, c, i_n)
  }

  pred inFP(r: Ref, n: Ref) {
    own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) )
  }

  pred cssR(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K]) {
      (forall n: Ref :: n in g_i.dom ==> 
          own(n.lock, lockval[n], 1.0) && (lockval[n] == 1 ? true : nodePred(r, n, contents[n], intf[n])))
      && 
      globalRes(r, c, g_i)
  }

  pred css(r: Ref, c: Set[K]) {
    exists g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K] :: 
      cssR(r, c, g_i, lockval, contents, intf)
  }

  lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K])
    requires cssR(r, c, g_i, lockval, contents, intf)
    requires inFP(r, n)
    ensures n in g_i.dom
    ensures cssR(r, c, g_i, lockval, contents, intf)
    ensures inFP(r, n)
  {
    unfold cssR(r, c, g_i, lockval, contents, intf);
    unfold globalRes(r, c, g_i);
    unfold inFP(r, n);

    fold globalRes(r, c, g_i);
    fold inFP(r, n);
    fold cssR(r, c, g_i, lockval, contents, intf);
  }


  lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K])
    requires cssR(r, c, g_i, lockval, contents, intf)
    requires n in g_i.dom
    ensures inFP(r, n)
    ensures cssR(r, c, g_i, lockval, contents, intf)
  {
    unfold cssR(r, c, g_i, lockval, contents, intf);
    unfold globalRes(r, c, g_i);

    fpu(r, authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom)), AuthSetRef.auth_frag(SetRefRA.set_constr(g_i.dom), SetRefRA.set_constr(g_i.dom)));

    fold globalRes(r, c, g_i);
    fold inFP(r, n);
    fold cssR(r, c, g_i, lockval, contents, intf);
  }

  lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K])
    requires cssR(r, c, g_i, lockval, contents, intf)
    ensures cssR(r, c, g_i, lockval, contents, intf)
    ensures r in g_i.dom
  {
    unfold cssR(r, c, g_i, lockval, contents, intf);
    unfold globalRes(r, c, g_i);
    unfold globalinv(g_i, r);

    fold globalinv(g_i, r);
    fold globalRes(r, c, g_i);
    fold cssR(r, c, g_i, lockval, contents, intf);
  }

  proc create()
    returns (r: Ref)
    ensures css(r, {||})
  {
    r := Node.createRoot();

    var i_r: Flow_K := int(
        {| l:Ref :: l == r ? fromSet(keyspace) : fromSet({||})  |},
        zeroFlow(),
        {|r|}
      );
    var contents: Map[Ref, Set[K]] := {| l: Ref :: {||} |};
    var lockval: Map[Ref, Int] := {| l: Ref :: 0 |};
    var intf: Map[Ref, Flow_K] := {| l: Ref :: l == r ? i_r : Flow_K.id |};

    r := new(
      authKS: AuthKeyset_K.auth_frag(
        Keyset_K.prodKS(keyspace, {||}),
        Keyset_K.prodKS(keyspace, {||})
      ),
      authSet:AuthSetRef.auth(SetRefRA.set_constr({|r|})),
      authFlow: AuthFlow_K.auth_frag(
        i_r, i_r
      ),
      lock:0
    );

    fold nodePred(r, r, {||}, i_r);

    fold globalinv(i_r, r);
    fold globalRes(r, {||}, i_r);
    fold cssR(r, {||}, i_r, lockval, contents, intf);
    assert cssR(r, {||}, i_r, lockval, contents, intf);
    fold css(r, {||});
  }

  lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K], c_n: Set[K], i_n: Flow_K)
    requires cssR(r, c, g_i, lockval, contents, intf)
    requires nodePred(r, n, c_n, i_n)
    requires k in outset(i_n, n1)
    requires n in g_i.dom
    ensures cssR(r, c, g_i, lockval, contents, intf)
    ensures nodePred(r, n, c_n, i_n)
    ensures n1 in g_i.dom
  {
    if (n1 !in g_i.dom) {
      unfold cssR(r, c, g_i, lockval, contents, intf);
      unfold nodePred(r, n, c_n, i_n);

      unfold globalRes(r, c, g_i);
      unfold globalinv(g_i, r);

      ghost var i_o: Flow_K := Flow_K.frame(g_i, i_n);
      
      assert i_o.out[n1] == Multiset_K.frame(g_i.out[n1], i_n.out[n1]);
      assert k !in outset(g_i, n1);
      
      fold nodePred(r, n, c_n, i_n);
      fold globalinv(g_i, r);
      fold globalRes(r, c, g_i);
      fold cssR(r, c, g_i, lockval, contents, intf);
    }
  }

  proc traverse(r: Ref, n: Ref, k: K, implicit ghost c: Set[K])
    returns (nn: Ref, implicit ghost cnn: Set[K], implicit ghost i_nn: Flow_K)
    requires inFP(r, n)
    atomic requires css(r, c)
    atomic ensures css(r, c)
    ensures nodePred(r, nn, cnn, i_nn)
    ensures inFP(r, nn)
    ensures k in keyset(i_nn)
  {
    ghost val phi := bindAU();

    ghost var c_n: Set[K];
    ghost var i_n: Flow_K;
    
    ghost val c0: Set[K] := openAU(phi);
    c_n, i_n := lockNodeHigh(r, n, c0);
    abortAU(phi);
    
    unfold nodePred(r, n, c_n, i_n);
    
    var in_range: Bool := Node.inRange(n, k, c_n, i_n);

    if (in_range) {
      var succ: Bool;
      var n1: Ref;
      succ, n1 := Node.findNext(n, k, c_n, i_n);

      fold nodePred(r, n, c_n, i_n);

      if (succ) {
        ghost var g_i1: Flow_K;
        ghost var lockval1: Map[Ref, Int];
        ghost var contents1: Map[Ref, Set[K]];
        ghost var intf1: Map[Ref, Flow_K];
        
        ghost val c1: Set[K] := openAU(phi);
        unfold css(r, c1);
        g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1);

        cssInFp(r, n, c1, g_i1, lockval1, contents1, intf1);
        fpInStep(r, n, n1, k, c1, g_i1, lockval1, contents1, intf1, c_n, i_n);
        fpInCss(r, n1, c1, g_i1, lockval1, contents1, intf1);

        assert cssR(r, c1, g_i1, lockval1, contents1, intf1);
        fold css(r, c1);

        unlockNodeHigh(r, n, c_n, i_n, c1);

        abortAU(phi);

        ghost val c2: Set[K] := openAU(phi);

        nn, cnn, i_nn := traverse(r, n1, k, c2);

        commitAU(phi, nn, cnn, i_nn);
        return nn, cnn, i_nn;
      } else {
        ghost val c0: Set[K] := openAU(phi);
        unlockNodeHigh(r, n, c_n, i_n, c0);
        abortAU(phi);

        ghost var g_i1: Flow_K;
        ghost var lockval1: Map[Ref, Int];
        ghost var contents1: Map[Ref, Set[K]];
        ghost var intf1: Map[Ref, Flow_K];
        
        ghost val c1: Set[K] := openAU(phi);

        commitAU(phi, n, c_n, i_n);
        return n, c_n, i_n;
      }
    } else {

      fold nodePred(r, n, c_n, i_n);

      ghost val c0: Set[K] := openAU(phi);
      unlockNodeHigh(r, n, c_n, i_n, c0);
      abortAU(phi);

      ghost var g_i1: Flow_K;
      ghost var lockval1: Map[Ref, Int];
      ghost var contents1: Map[Ref, Set[K]];
      ghost var intf1: Map[Ref, Flow_K];
      
      ghost val c1: Set[K] := openAU(phi);

      unfold css(r, c1);
      g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1);

      unfold cssR(r, c1, g_i1, lockval1, contents1, intf1);
      unfold globalRes(r, c1, g_i1);
      unfold globalinv(g_i1, r);

      fold globalinv(g_i1, r);
      fold globalRes(r, c1, g_i1);
      fold cssR(r, c1, g_i1, lockval1, contents1, intf1);

      fpInCss(r, r, c1, g_i1, lockval1, contents1, intf1);
      
      assert cssR(r, c1, g_i1, lockval1, contents1, intf1);
      fold css(r, c1);
      nn, cnn, i_nn := traverse(r, r, k, c1);

      commitAU(phi, nn, cnn, i_nn);
    }
  }

  lemma keyset_theorem(r: Ref, dop: Op, k: K, c_n: Set[K], c_n1: Set[K], c: Set[K], res: Bool, k_n: Set[K])
    returns (c1: Set[K])
    requires opSpec(dop, k, c_n) == ((c_n1, res))
    requires own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c)))
    requires own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n)))
    // requires own(r.authFlow, AuthFlow_K.auth(g_i))requires own(r.authFlow, AuthFlow_K.frag(g_i))
    requires c_n1 subseteq k_n
    requires k in k_n
    requires k in keyspace

    ensures opSpec(dop, k, c) == ((c1, res))
    ensures own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c1)))
    ensures own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n1)))
  {
    //unfold opSpec(dop, k, c_n, c_n1, res);

    if (dop == searchOp || !res) {
      c1 := c;
      //fold opSpec(dop, k, c, c1, res);
    } else {
      if (dop == insertOp) {
        c1 := c ++ {| k |};
      } else {
        c1 := c -- {| k |};
      }
        
      {!
        //fold opSpec(dop, k, c, c1, res);

        /*assert AuthKeyset_K.fpuAllowed(
          AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)), 
          AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1))
        ) with {
          assert forall k: Keyset_K :: {Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n1))} {Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n))}
            Keyset_K.prodKS(keyspace, c) == Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n)) ==>
            Keyset_K.prodKS(keyspace, c1) == Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n1));

          //assert AuthKeyset_K.valid(AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)));
          //assert AuthKeyset_K.valid(AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1)));
        }*/
          
        fpu(r, authKS, 
          AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)),
          AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1)));
      !}
    }
  }

  proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K])
    returns (res: Bool, implicit ghost cc: Set[K])
    requires k in keyspace
    atomic requires css(r, c)
    atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res))
  {
    ghost val phi := bindAU();

    var n: Ref;
    ghost var c_n: Set[K];
    ghost var i_n: Flow_K;
    ghost var g_i0: Flow_K;
    ghost var lockval0: Map[Ref, Int];
    ghost var contents0: Map[Ref, Set[K]];
    ghost var intf0: Map[Ref, Flow_K];
    
    ghost val c0: Set[K] := openAU(phi);
    unfold css(r, c0);
    g_i0, lockval0, contents0, intf0 :| cssR(r, c0, g_i0, lockval0, contents0, intf0);

    root_fp(r, c0, g_i0, lockval0, contents0, intf0);
    fpInCss(r, r, c0, g_i0, lockval0, contents0, intf0);
    assert cssR(r, c0, g_i0, lockval0, contents0, intf0);
    fold css(r, c0);
    
    n, c_n, i_n := traverse(r, r, k, c0);

    abortAU(phi);

    var succ: Bool;
    ghost var c_n1: Set[K];

    unfold nodePred(r, n, c_n, i_n);
    //assert own(r.authFlow, AuthFlow_K.frag(i_n));
    
    succ, res, c_n1 := Node.decisiveOp(dop, n, k, c_n, i_n);
    if (succ) {

      ghost var g_i1: Flow_K;
      ghost var lockval1: Map[Ref, Int];
      ghost var contents1: Map[Ref, Set[K]];
      ghost var intf1: Map[Ref, Flow_K];
      
      ghost val c1: Set[K] := openAU(phi);
      unfold css(r, c1);
      g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1);
      cssInFp(r, n, c1, g_i1, lockval1, contents1, intf1);
      unfold cssR(r, c1, g_i1, lockval1, contents1, intf1);
      
      {!
        if (lockval1[n] != 1) {
          unfold nodePred(r, n, contents1[n], intf1[n]);
          Node.nodeSepStar(n, c_n1, contents1[n], i_n, intf1[n]);
        }
      !}

      unlockNode(n);

      unfold globalRes(r, c1, g_i1);
      //unfold opSpec(dop, k, c_n, c_n1, res);
      //fold opSpec(dop, k, c_n, c_n1, res);

      cc := keyset_theorem(r, dop, k, c_n, c_n1, c1, res, keyset(i_n));

      /*AuthFlow_K.compValid();
      AuthFlow_K.weak_frameCompInv();*/

      fold globalRes(r, cc, g_i1);
      ghost var lockval2: Map[Ref, Int] := lockval1[n := 0];
      ghost var contents2: Map[Ref, Set[K]] := contents1[n := c_n1];
      ghost var intf2: Map[Ref, Flow_K] := intf1[n := i_n];

      //Flow_K.compFrameInv();
      //Flow_K.frameCompInv();
      fold nodePred(r, n, contents2[n], intf2[n]);
      fold cssR(r, cc, g_i1, lockval2, contents2, intf2);
      assert cssR(r, cc, g_i1, lockval2, contents2, intf2);
      fold css(r, cc);

      commitAU(phi, res, cc);

      return res, cc;
    } else {
      fold nodePred(r, n, c_n, i_n);
      ghost val c0: Set[K] := openAU(phi);
      unlockNodeHigh(r, n, c_n, i_n, c0);
      abortAU(phi);
      
      ghost val c1: Set[K] := openAU(phi);
      res, cc := cssOp(dop, r, k, c1);
      commitAU(phi, res, cc);
      
      return res, cc;
    }
  }
}