val pcm : FStar.PCM.pcm (Steel.PCMMap.map Zeta.Steel.ApplicationTypes.tid
      (Steel.FractionalAnchoredPreorder.knowledge Zeta.Steel.ThreadLogMap.anchors))
let pcm = PM.pointwise tid fap
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
/
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
FStar.PCM.pcm (Steel.PCMMap.map Zeta.Steel.ApplicationTypes.tid
      (Steel.FractionalAnchoredPreorder.knowledge Zeta.Steel.ThreadLogMap.anchors))
Steel.PCMMap.pointwise Steel.FractionalAnchoredPreorder.knowledge Zeta.Steel.ThreadLogMap.log Zeta.Steel.ThreadLogMap.log_grows Zeta.Steel.ThreadLogMap.anchors Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadLogMap.fap
let pcm =
  
PM.pointwise tid fap