let liveness_inv = i:hinv {
  forall l h0 h1. {:pattern (i h1); (modifies l h0 h1)}  i h0 /\ modifies l h0 h1 /\ address_liveness_insensitive_locs `loc_includes` l ==> i h1
}
let liveness_inv =
i:
hinv
  { forall l h0 h1. {:pattern (i h1); (modifies l h0 h1)}
      i h0 /\ modifies l h0 h1 /\ address_liveness_insensitive_locs `loc_includes` l ==> i h1 }
EverParse3d.Actions.Base.fst.checked
prims.fst.checked LowStar.Comment.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.List.fsti.checked LowParse.Spec.FLData.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked LowParse.Low.ListUpTo.fst.checked LowParse.Low.Int.fsti.checked LowParse.Low.FLData.fst.checked LowParse.Low.BoundedInt.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked EverParse3d.Prelude.fst.checked EverParse3d.Kinds.fst.checked EverParse3d.InputStream.Base.fst.checked EverParse3d.InputStream.All.fsti.checked EverParse3d.ErrorCode.fst.checked C.Loops.fst.checked
EverParse3d.Actions.Base.fst
EverParse3d.Actions.Base.hinv Prims.l_Forall LowStar.Monotonic.Buffer.loc FStar.Monotonic.HyperStack.mem Prims.l_imp Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.address_liveness_insensitive_locs
module EverParse3d.Actions.Base
friend EverParse3d.Kinds
friend EverParse3d.Prelude
open FStar.HyperStack.ST
open LowStar.Buffer
open LowStar.BufferOps
module B = LowStar.Buffer
module I = EverParse3d.InputStream.Base
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

module LPE = EverParse3d.ErrorCode
open FStar.Tactics.Typeclasses

module B = LowStar.Buffer
module U8 = FStar.UInt8
module P = EverParse3d.Prelude
val liveness_inv : Type
Type