anchor.diff:     For short arrays, such as the MD5 checksum (4 words), it might not be too inefficient*)
   val to_seq :  #a:Type  -> r:(sstarray a)
     -> PureMem (seq a)
  -        (requires (fun m -> b2t (liveRef (reveal (asRef r)) m)))
  -        (ensures (fun m v-> (liveRef (reveal (asRef r)) m) /\ v = (lookupRef (reveal (asRef r)) m)))
  +        (requires (fun m -> b2t (refIsLive (reveal (asRef r)) m)))
  +        (ensures (fun m v-> (refIsLive (reveal (asRef r)) m) /\ v = (lookupRef (reveal (asRef r)) m)))
  
positive.code:         (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)
              /\ tail m0 = tail m1))
          (hide empty)
  
  
negative.code:         (ensures (fun m0 vv m1->
              (isNonEmpty (st m0)) /\ (isNonEmpty (st m1))
              /\ allocatedInRegion (reveal (asRef vv)) (topRegion m0) (topRegion m1) (Seq.create len init)
              /\ regionOf (reveal (asRef vv)) = InStack (topRegionId m0) /\ (topRegionId m0 = topRegionId m1)
              /\ tail m0 = tail m1))
          (hide empty)
  
  