val map_map
      (m: PM.map tid aval)
      (f: (tid: tid -> a: FAP.avalue anchors {Map.sel m tid == FAP.Owns a} -> FAP.avalue anchors))
    : GTot (PM.map tid aval)
val map_map
      (m: PM.map tid aval)
      (f: (tid: tid -> a: FAP.avalue anchors {Map.sel m tid == FAP.Owns a} -> FAP.avalue anchors))
    : GTot (PM.map tid aval)
let map_map (m:PM.map tid aval)
            (f:(tid:tid -> a:FAP.avalue anchors{ Map.sel m tid == FAP.Owns a } -> FAP.avalue anchors))
  : GTot (PM.map tid aval)
  = Map.map_literal (fun tid ->
       match Map.sel m tid with
       | FAP.Owns m -> FAP.Owns (f tid m)
       | FAP.Nothing -> FAP.Nothing)
module Zeta.Steel.ThreadLogMap
open FStar.Ghost
open FStar.Seq
open Zeta.Steel.FormatsManual
open Zeta.Steel.ApplicationTypes
open Steel.ST.Util
module FAP = Steel.FractionalAnchoredPreorder
module PM = Steel.PCMMap
module M = Zeta.Steel.ThreadStateModel
module SA = Zeta.SeqAux

let committed_log_entries_split (l0 l1 l2: log)
  : Lemma
    (requires
      l0 == M.committed_log_entries l2 /\
      log_grows l0 l1 /\
      log_grows l1 l2)
    (ensures
      l0 == M.committed_log_entries l1)
  = let is_verify_epoch = function VerifyEpoch -> true | _ -> false in
    if SA.exists_sat_elems is_verify_epoch l2
    then (
      let i = SA.last_index is_verify_epoch l2 in
      assert (i < Seq.length l1);
      introduce forall j. i < j /\ j < Seq.length l1 ==>
                     not (is_verify_epoch (Seq.index l1 j))
      with introduce _ ==> _
      with _ . SA.lemma_last_index_correct1 is_verify_epoch l2 j;
      SA.last_index_opt_elim is_verify_epoch l1;
      assert (SA.prefix l1 (i + 1) `Seq.equal` SA.prefix l2 (i + 1));
      assert (SA.prefix l2 (i + 1) == l0)
    )
    else (
      assert (l0 == Seq.empty);
      assert (l1 `Seq.equal` SA.prefix l2 (Seq.length l1));
      assert (SA.is_prefix l2 l1);
      SA.lemma_not_exists_prefix is_verify_epoch l2 (Seq.length l1)
    )

let anchor : log -> log -> prop
  = fun l0 l1 ->
      log_grows l0 l1 /\
      l0 == M.committed_log_entries l1

let anchor_pre : squash (forall l0 l1. anchor l0 l1 ==> log_grows l0 l1) = ()

let anchor_split
  : squash (forall x z. x `anchor` z  ==> (forall y. log_grows x y /\ log_grows y z ==> x `anchor` y))
  = introduce forall x. _
    with introduce forall z. x `anchor` z  ==> (forall y. log_grows x y /\ log_grows y z ==> x `anchor` y)
    with introduce _ ==> _
    with _. introduce forall y. _
    with introduce _ ==> _
    with _. committed_log_entries_split x y z
let anchors : FAP.anchor_rel log_grows = anchor

let fap = FAP.pcm #log #log_grows #anchors
let pcm = PM.pointwise tid fap
let aval = FAP.knowledge anchors
let has_key  (m:PM.map tid aval) (tid:tid) = FAP.Owns? (Map.sel m tid)
let owns_key (m:PM.map tid aval) (tid:tid) =
  has_key m tid /\
  FAP.avalue_owns (FAP.Owns?._0 (Map.sel m tid))
let avalue_of (m:PM.map tid aval) (tid:tid { has_key m tid }) =
  (FAP.Owns?._0 (Map.sel m tid))
let get (m:PM.map tid aval) (tid:tid { has_key m tid }) =
  Steel.Preorder.curval (FAP.avalue_val (avalue_of m tid))
let put (m:PM.map tid aval)
        (tid:tid { has_key m tid })
        (l:log {get m tid `log_grows` l /\ anchors l l})
  = Map.upd m tid (FAP.Owns (FAP.avalue_update_value (FAP.Owns?._0 (Map.sel m tid)) l))

let update_value (l:log)
                 (m:PM.map tid aval)
                 (tid:tid {
                   owns_key m tid /\ //if you have full ownership of key
                   get m tid `log_grows` l /\ //you can update it wrt the preorder only
                   anchors l l
                 })
  : PCM.frame_preserving_upd pcm m (put m tid l)
  = PM.lift_frame_preserving_upd _ _ (FAP.update_value (FAP.Owns?._0 (Map.sel m tid)) l) m tid

let owns_anchored_key (m:PM.map tid aval) (tid:tid) =
  has_key m tid /\
  FAP.avalue_owns_anchored (FAP.Owns?._0 (Map.sel m tid))

let put_anchored (m:PM.map tid aval)
                 (tid:tid { has_key m tid })
                 (l:log {
                   get m tid `log_grows` l /\
                   l `FAP.compat_with_any_anchor_of` (avalue_of m tid)
                 }) =
  Map.upd m tid (FAP.Owns (FAP.avalue_update_anchored_value (FAP.Owns?._0 (Map.sel m tid)) l))

let update_anchored_value (l:log)
                          (m:PM.map tid aval)
                          (tid:tid {
                            owns_anchored_key m tid /\ //if you own an anchored key, you can update if you respect
                            get m tid `log_grows` l /\ //the preorder
                            l `FAP.compat_with_any_anchor_of` (avalue_of m tid) //and respect any anchor of the current value
                          })
  : PCM.frame_preserving_upd pcm m (put_anchored m tid l)
  = PM.lift_frame_preserving_upd _ _ (FAP.update_anchored_value (FAP.Owns?._0 (Map.sel m tid)) l) m tid

module G = Steel.ST.GhostPCMReference

let t = G.ref _ pcm

let no_ownership (m:PM.map tid aval) (tid:tid) =
  not (has_key m tid) \/
  (let (p, _) = FAP.Owns?._0 (Map.sel m tid) in
   None? (fst p) /\
   None? (snd p))

let has_anchor (m:PM.map tid aval) (tid:tid) =
  has_key m tid /\
  (let p, _ = FAP.Owns?._0 (Map.sel m tid) in
   Some? (snd p))

let perm_of (m:PM.map tid aval) (tid:tid { has_key m tid }) =
  let p, _ = FAP.Owns?._0 (Map.sel m tid) in
  fst p

let perm_ok (m:PM.map tid aval) (tid:tid { has_key m tid }) =
  let av = FAP.Owns?._0 (Map.sel m tid) in
  FAP.perm_ok av

let anchor_of (m:PM.map tid aval) (t:tid{ has_anchor m t }) =
  let p, _ = FAP.Owns?._0 (Map.sel m t) in
  Some?.v (snd p)

let owns_anchor_only (m:PM.map tid aval) (tid:tid) =
  has_anchor m tid /\
  None? (perm_of m tid)


(*** Ownership predicates ***)
let related_domains (m:repr) (m':PM.map tid aval) =
    forall tid. has_key m' tid <==> Some? (Map.sel m tid)

let global_anchor_pred (x:t) (m:repr) (m':PM.map tid aval)
  : prop
  = related_domains m m' /\
    (forall (tid:tid). {:pattern (Map.sel m tid) \/ has_key m' tid}
       (has_key m' tid ==>
         owns_anchor_only m' tid /\
         get m' tid == Some?.v (Map.sel m tid) /\
         anchor_of m' tid == get m' tid))

let global_anchor (x:t) ([@@@smt_fallback] m:repr)
  : vprop
  = exists_ (fun m' ->
      G.pts_to x m' `star`
      pure (global_anchor_pred x m m'))


let intro_global_anchor (#o:_)
                        (x:t)
                        (m:repr) (m':PM.map tid aval)
  : STGhost unit o
       (G.pts_to x m')
       (fun _ -> global_anchor x m)
       (requires global_anchor_pred x m m')
       (ensures fun _ -> True)
  = intro_pure (global_anchor_pred x m m');
    intro_exists m' (fun m' ->
      G.pts_to x m' `star`
      pure (global_anchor_pred x m m'))


let elim_global_anchor (#o:_) (x:t) (m:repr)
  : STGhost (erased (PM.map tid aval)) o
       (global_anchor x m)
       (fun m' -> G.pts_to x m')
       (requires True)
       (ensures fun m' -> global_anchor_pred x m m')
  = let m' = elim_exists () in
    elim_pure _;
    m'

////////////////////////////////////////////////////////////////////////////////

let tids_pts_to_pred (x:t)
                     (frac:perm)
                     (m:repr)
                     (with_anchor:bool)
                     (m': PM.map tid aval)
  : prop
  = related_domains m m' /\
    (forall (tid:tid).{:pattern (Map.sel m tid) \/ (has_key m' tid)}
           (has_key m' tid ==>
             perm_ok m' tid /\
             perm_of m' tid == Some frac /\
             (with_anchor <==> has_anchor m' tid) /\
             get m' tid == Some?.v (Map.sel m tid)))

let tids_pts_to (x:t)
                ([@@@smt_fallback] frac:perm)
                ([@@@smt_fallback] m:repr)
                (with_anchor:bool)
  : vprop
  = exists_ (fun m' ->
    G.pts_to x m' `star`
    pure (tids_pts_to_pred x frac m with_anchor m'))

let intro_tids_pts_to (#o:_)
                      (x:t)
                      (frac:perm)
                      (m:repr)
                      (with_anchor:bool)
                      (m':PM.map tid aval)
  : STGhost unit o
       (G.pts_to x m')
       (fun _ -> tids_pts_to x frac m with_anchor)
       (requires tids_pts_to_pred x frac m with_anchor m')
       (ensures fun _ -> True)
  = intro_pure (tids_pts_to_pred x frac m with_anchor m');
    intro_exists m' (fun m' ->
      G.pts_to x m' `star`
      pure (tids_pts_to_pred x frac m with_anchor m'))

let elim_tids_pts_to (#o:_)
                     (x:t)
                     (frac:perm)
                     (m:repr)
                     (with_anchor:bool)
  : STGhost (erased (PM.map tid aval)) o
       (tids_pts_to x frac m with_anchor)
       (fun m' -> G.pts_to x m')
       (requires True)
       (ensures fun m' -> tids_pts_to_pred x frac m with_anchor m')
  = let m' = elim_exists () in
    elim_pure _;
    m'

////////////////////////////////////////////////////////////////////////////////
let singleton (t:tid) (l:log)
  : repr
  = Map.upd (Map.const None) t (Some l)

let tid_pts_to (x:t)
               (t:tid)
               ([@@@smt_fallback] frac:perm)
               ([@@@smt_fallback] l:log)
               (with_anchor:bool)
  : vprop
  = tids_pts_to x frac (singleton t l) with_anchor

////////////////////////////////////////////////////////////////////////////////

let snapshot_pred (x:t)
                  (m:repr)
                  (m':PM.map tid aval)
  : prop
  = related_domains m m' /\
    (forall tid. has_key m' tid ==>
            get m' tid == Some?.v (Map.sel m tid) /\
            no_ownership m' tid)

let global_snapshot (x:t)
                    ([@@@smt_fallback] m:repr)
  : vprop
  = exists_ (fun m' ->
      G.pts_to x m' `star`
      pure (snapshot_pred x m m'))


let intro_global_snapshot (#o:_)
                          (x:t)
                          (m:repr)
                          (m':PM.map tid aval)
  : STGhost unit o
    (G.pts_to x m')
    (fun _ -> global_snapshot x m)
    (requires snapshot_pred x m m')
    (ensures fun _ -> True)
  = intro_pure (snapshot_pred x m m');
    intro_exists m' (fun m' -> G.pts_to x m' `star` pure (snapshot_pred x m m'))


let elim_global_snapshot (#o:_)
                         (x:t)
                         (m:repr)
  : STGhost (PM.map tid aval) o
    (global_snapshot x m)
    (fun m' -> G.pts_to x m')
    (requires True)
    (ensures fun m' -> snapshot_pred x m m')
  = let m' = elim_exists () in
    elim_pure _;
    m'

////////////////////////////////////////////////////////////////////////////////
(*** Utilities ***)
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.SeqAux.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.GhostPCMReference.fsti.checked Steel.Preorder.fst.checked Steel.PCMMap.fst.checked Steel.FractionalAnchoredPreorder.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.Sugar.fsti.checked
Zeta.Steel.ThreadLogMap.fst

    m: Steel.PCMMap.map Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadLogMap.aval ->
    f:
      (
            tid: Zeta.Steel.ApplicationTypes.tid ->
            a:
              Steel.FractionalAnchoredPreorder.avalue Zeta.Steel.ThreadLogMap.anchors
                {FStar.Map.sel m tid == Steel.FractionalAnchoredPreorder.Owns a}
          -> Steel.FractionalAnchoredPreorder.avalue Zeta.Steel.ThreadLogMap.anchors)
  -> Prims.GTot (Steel.PCMMap.map Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadLogMap.aval)
Steel.PCMMap.map Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadLogMap.aval Steel.FractionalAnchoredPreorder.avalue Zeta.Steel.ThreadLogMap.log Zeta.Steel.ThreadLogMap.log_grows Zeta.Steel.ThreadLogMap.anchors Prims.eq2 Steel.FractionalAnchoredPreorder.knowledge FStar.Map.sel Steel.FractionalAnchoredPreorder.Owns FStar.Map.map_literal Steel.FractionalAnchoredPreorder.Nothing
let map_map
      (m: PM.map tid aval)
      (f: (tid: tid -> a: FAP.avalue anchors {Map.sel m tid == FAP.Owns a} -> FAP.avalue anchors))
    : GTot (PM.map tid aval) =
  
Map.map_literal (fun tid ->
      match Map.sel m tid with
      | FAP.Owns m -> FAP.Owns (f tid m)
      | FAP.Nothing -> FAP.Nothing)