val max_valid_all_prefix_aux (psm: pseq_machine) (s: seq (elem_type_p psm))
    : Tot
      (i:
        nat
          { i <= length s /\ valid_all psm (prefix s i) /\
            (i < length s ==> ~(valid_all psm (prefix s (i + 1)))) }) (decreases (length s))
val max_valid_all_prefix_aux (psm: pseq_machine) (s: seq (elem_type_p psm))
    : Tot
      (i:
        nat
          { i <= length s /\ valid_all psm (prefix s i) /\
            (i < length s ==> ~(valid_all psm (prefix s (i + 1)))) }) (decreases (length s))
let rec max_valid_all_prefix_aux (psm: pseq_machine) (s: seq (elem_type_p psm))
  : Tot (i: nat{i <= length s /\
               valid_all psm (prefix s i) /\
               (i < length s ==>
                ~ (valid_all psm (prefix s (i + 1))))})
    (decreases (length s)) =
  let n = length s in
  let sm = seq_machine_of psm in
  let pf = partn_fn psm in
  if n = 0 then (
    lemma_prefix0_empty s;
    lemma_empty_seq_valid_all psm;
    0
  )
  else 
    let s' = prefix s (n - 1) in
    let i = max_valid_all_prefix_aux psm s' in
    if i = n - 1 then
      let e = index s (n - 1) in
      let k = pf e in
      let sk = partn psm k s in
      if valid sm sk then (
        lemma_valid_all_extend psm s;
        n
      )      
      else i
    else i
module Zeta.SeqMachine

let lemma_empty_seq_init (sm: seq_machine) (s: seq (elem_type sm){length s = 0})
  : Lemma (ensures (seq_machine_run sm s = (init_state sm)))
  = lemma_reduce_empty (init_state sm) (trans_fn sm);
    lemma_empty s

let lemma_empty_seq_valid (sm: seq_machine):
  Lemma (valid sm (empty #(elem_type sm))) =
  lemma_reduce_empty (init_state sm) (trans_fn sm)

let lemma_valid_prefix (sm: seq_machine) (s: (seq (elem_type sm)){valid sm s}) (i:nat{i <= length s}):
  Lemma (valid sm (prefix s i)) =
  let si = prefix s i in
  if valid sm si then ()
  else (
    lemma_reduce_prefix (init_state sm) (trans_fn sm) s i;
    lemma_reduce_identity (fail_state sm) (trans_fn sm) (suffix s (length s - i))
  )

let rec max_valid_prefix_aux (sm: seq_machine) (s: seq (elem_type sm))
  : Tot (i:nat{i <= length s /\
              valid sm (prefix s i) /\
              (i < length s ==> not (valid sm (prefix s (i + 1))))
              })
    (decreases (length s)) =
  lemma_empty_seq_valid sm;
  lemma_prefix0_empty s;
  let n = length s in
  if valid sm s then n
  else max_valid_prefix_aux sm (prefix s (n - 1))

let max_valid_prefix = max_valid_prefix_aux

let lemma_empty_seq_valid_all (psm: pseq_machine):
  Lemma (valid_all psm (empty #(elem_type_p psm))) =
  let s = empty #(elem_type_p psm) in
  let key = key_type psm in
  let sm = seq_machine_of psm in
  let pf = partn_fn psm in
  let aux(k: key):
    Lemma (requires True)
          (ensures (valid sm (partn psm k s)))
          [SMTPat (valid sm (partn psm k s))]
          =
    lemma_filter_empty (iskey pf k);
    lemma_empty_seq_valid sm
  in
  ()

let lemma_valid_all_prefix (psm: pseq_machine)
                           (s: (seq (elem_type_p psm)){valid_all psm s}) (i:nat{i <= length s}):
  Lemma (requires True)
        (ensures (valid_all psm (prefix s i)))
        (decreases (length s)) =
  let si = prefix s i in
  let key = key_type psm in
  let sm = seq_machine_of psm in
  let pf = partn_fn psm in
  let aux(k: key):
    Lemma (requires True)
          (ensures (valid sm (partn psm k si)))
          [SMTPat (valid sm (partn psm k si))]
    =
    lemma_filter_prefix (iskey pf k) s si;
    lemma_valid_prefix sm (partn psm k s) (length (partn psm k si))
  in
  ()

let lemma_valid_all_extend (psm: pseq_machine) (s: seq (elem_type_p psm)):
  Lemma (requires (length s > 0 /\
                   valid_all psm (prefix s (length s - 1)) /\
                   valid (seq_machine_of psm)
                         (partn psm (partn_fn psm (index s (length s - 1))) s)))
        (ensures (valid_all psm s)) =
  let n = length s in
  let sm = seq_machine_of psm in
  let pf = partn_fn psm in
  let key = key_type psm in
  let k' = pf (index s (n - 1)) in
  let aux(k: key):
    Lemma (requires True)
          (ensures (valid sm (partn psm k s)))
          [SMTPat (valid sm (partn psm k s))] =
    if k' = k then ()
    else lemma_filter_extend1 (iskey pf k) s    
  in
  ()
/
prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqMachine.fst
psm: Zeta.SeqMachine.pseq_machine -> s: FStar.Seq.Base.seq (Zeta.SeqMachine.elem_type_p psm)
  -> Prims.Tot
    (i:
      Prims.nat
        { i <= FStar.Seq.Base.length s /\ Zeta.SeqMachine.valid_all psm (Zeta.SeqAux.prefix s i) /\
          (i < FStar.Seq.Base.length s ==>
            ~(Zeta.SeqMachine.valid_all psm (Zeta.SeqAux.prefix s (i + 1)))) })
Zeta.SeqMachine.pseq_machine FStar.Seq.Base.seq Zeta.SeqMachine.elem_type_p Prims.op_Equality Prims.int Prims.unit Zeta.SeqMachine.lemma_empty_seq_valid_all Zeta.SeqAux.lemma_prefix0_empty Prims.bool Prims.op_Subtraction Zeta.SeqMachine.valid Zeta.SeqMachine.lemma_valid_all_extend Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.SeqMachine.valid_all Zeta.SeqAux.prefix Prims.l_imp Prims.op_LessThan Prims.l_not Prims.op_Addition Zeta.SeqMachine.partn Zeta.SeqMachine.key_type FStar.Seq.Base.index Zeta.SeqMachine.max_valid_all_prefix_aux Zeta.SeqMachine.partn_fn Zeta.SeqMachine.seq_machine Zeta.SeqMachine.seq_machine_of
let rec max_valid_all_prefix_aux (psm: pseq_machine) (s: seq (elem_type_p psm))
    : Tot
      (i:
        nat
          { i <= length s /\ valid_all psm (prefix s i) /\
            (i < length s ==> ~(valid_all psm (prefix s (i + 1)))) }) (decreases (length s)) =
  
let n = length s in
let sm = seq_machine_of psm in
let pf = partn_fn psm in
if n = 0
then
  (lemma_prefix0_empty s;
    lemma_empty_seq_valid_all psm;
    0)
else
  let s' = prefix s (n - 1) in
  let i = max_valid_all_prefix_aux psm s' in
  if i = n - 1
  then
    let e = index s (n - 1) in
    let k = pf e in
    let sk = partn psm k s in
    if valid sm sk
    then
      (lemma_valid_all_extend psm s;
        n)
    else i
  else i