val lemma_consistent_log_prefix_consistent (#vcfg:_)
  (init_map: slot_state_map vcfg)
  (l:logS vcfg) (i:nat{i <= length l})
  : Lemma (requires (consistent_log init_map l))
        (ensures (consistent_log init_map (prefix l i)))
val lemma_consistent_log_prefix_consistent (#vcfg:_)
  (init_map: slot_state_map vcfg)
  (l:logS vcfg) (i:nat{i <= length l})
  : Lemma (requires (consistent_log init_map l))
        (ensures (consistent_log init_map (prefix l i)))
let rec lemma_consistent_log_prefix_consistent (#vcfg:_)
  (init_map: slot_state_map vcfg)
  (l:logS vcfg) (i:nat{i <= length l})
  : Lemma (requires (consistent_log init_map l))
          (ensures (consistent_log init_map (prefix l i)))
          (decreases (length l))
  = if i < length l then (
      let n' = length l - 1 in
      let l' = prefix l n' in
      consistent_log_implies_hprefix_consistent init_map l;
      lemma_consistent_log_prefix_consistent init_map l' i
    )
module Zeta.Intermediate.Logs

open FStar.Classical
open Zeta.SeqIdx

let all_slots_assoc_comp (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg))
  : b:bool{b <==> all_slots_assoc ssm ss}
  = not (exists_elems_with_prop_comp (fun s -> not (is_assoc ssm s)) ss)

#push-options "--fuel 1 --ifuel 1 --query_stats"

let consistent_log_implies_hprefix_consistent (#vcfg:_) (init_map: slot_state_map vcfg) (l: logS vcfg {length l > 0})
  : Lemma (requires (consistent_log init_map l))
          (ensures (let i = length l - 1 in
                    let l' = prefix l i in
                    consistent_log init_map l'))
          [SMTPat (consistent_log init_map l)]
  = let i = length l - 1 in
    let l' = prefix l i in
    let aux(s:_)
      : Lemma (ensures (slot_state_trans_closure s l' (init_map s) <> None))
      = eliminate forall (s:slot_id vcfg). slot_state_trans_closure s l (init_map s) <> None
        with s
    in
    forall_intro aux

#pop-options
/
Zeta.SeqIdx.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Logs.fst

    init_map: Zeta.Intermediate.SlotKeyRel.slot_state_map vcfg ->
    l: Zeta.Intermediate.Logs.logS vcfg ->
    i: Prims.nat{i <= FStar.Seq.Base.length l}
  -> FStar.Pervasives.Lemma (requires Zeta.Intermediate.Logs.consistent_log init_map l)
      (ensures Zeta.Intermediate.Logs.consistent_log init_map (Zeta.SeqAux.prefix l i))
      (decreases FStar.Seq.Base.length l)
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.Logs.logS Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Intermediate.Verifier.logS_entry Prims.op_LessThan Zeta.Intermediate.Logs.lemma_consistent_log_prefix_consistent Prims.unit Zeta.Intermediate.Logs.consistent_log_implies_hprefix_consistent FStar.Seq.Base.seq Prims.op_Equality Zeta.SeqAux.prefix Prims.int Prims.op_Subtraction Prims.bool Zeta.Intermediate.Logs.consistent_log Prims.squash Prims.Nil FStar.Pervasives.pattern
let rec lemma_consistent_log_prefix_consistent
      (#vcfg: _)
      (init_map: slot_state_map vcfg)
      (l: logS vcfg)
      (i: nat{i <= length l})
    : Lemma (requires (consistent_log init_map l))
      (ensures (consistent_log init_map (prefix l i)))
      (decreases (length l)) =
  
if i < length l
then
  (let n' = length l - 1 in
    let l' = prefix l n' in
    consistent_log_implies_hprefix_consistent init_map l;
    lemma_consistent_log_prefix_consistent init_map l' i)