anchor.diff:          (ensures (fun m0 vv m1->
               (isNonEmpty (st m0)) /\ (isNonEmpty (st m1))
               /\ allocatedInRegion (reveal (asRef vv)) (topRegion m0) (topRegion m1) init
  -            /\ refLoc (reveal (asRef vv)) = InStack (topRegionId m0) /\ (topRegionId m0 = topRegionId m1)
  +            /\ regionOf (reveal (asRef vv)) = InStack (topRegionId m0) /\ (topRegionId m0 = topRegionId m1)
               /\ tail m0 = tail m1))
           (hide empty)
   
  
positive.code:         (ensures (fun m0 vv m1->
              (isNonEmpty (st m0)) /\ (isNonEmpty (st m1))
              /\ allocatedInRegion (reveal (asRef vv)) (topRegion m0) (topRegion m1) (Seq.create len init)
              /\ refLoc (reveal (asRef vv)) = InStack (topRegionId m0) /\ (topRegionId m0 = topRegionId m1)
              /\ tail m0 = tail m1))
          (hide empty)
  
  
negative.code: val readIndex :  #a:Type  -> r:(sstarray a)
    -> index:nat
    -> PureMem a
          (requires (fun m ->  (refIsLive (reveal (asRef r)) m) /\ index < Seq.length (lookupRef (reveal (asRef r)) m) ) )
          (ensures (fun m v->
            (refIsLive (reveal (asRef r)) m) /\ index < Seq.length (lookupRef (reveal (asRef r)) m)
            /\ v = Seq.index (lookupRef (reveal (asRef r)) m) index ))
  
  val writeIndex :  #a:Type -> r:((sstarray a))
    -> index:nat -> newV:a ->
   Mem unit
      (requires (fun m ->  (refIsLive (reveal (asRef r)) m) /\ index < Seq.length (lookupRef (reveal (asRef r)) m) ) )
      (ensures ( fun m0 _ m1 ->
          (refIsLive (reveal (asRef r)) m0) /\ index < Seq.length (lookupRef (reveal (asRef r)) m0) /\
            (m1 = (writeMemAux (reveal (asRef r)) m0 (Seq.upd (lookupRef (reveal (asRef r)) m0) index newV)))))
        (only (reveal (asRef r)))
  
  