You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
class Queue (α : Type) (queue : outParam Type) where
  member (x : α) (q : queue) : Prop

action random_switch = {
  let s ← fresh one_elem
  state := s
}

invariant [honest_non_conflicting_echoes]
  ∀ (src originator dst₁ dst₂ : address) (r : round) (v₁ v₂ : value),
    (¬ is_byz src) → (echo_msg src dst₁ originator r v₁ ∧ echo_msg src dst₂ originator r v₂ → v₁ = v₂)

def checkCorrectInstantiation (id : Name) (ts : Array Term) [Monad m] [MonadEnv m] [MonadError m] : m Unit := do
  checkModuleExists id
  let module := (<- globalSpecCtx.get)[id]!.spec
  let vd := module.parameters
  let vs := ts
  if vd.size != vs.size then
    let vdStr := "\n".intercalate (Array.toList $ vd.map (fun x => s!"{x}"))
    throwError s!"Module {id} has {vd.size} parameters, but {vs.size} were provided\nrequired parameters: {vdStr}"

IO.monoMsNow in Init.System.IO

#guard_msgs(drop info, drop warning) in
#check_invariants

def getActCheckResultMessages' [Monad m] [MonadOptions m] (res: List (Name × Name × SmtResult × Option TimeInMs)) : m (Array String) := do
  let mut msgs := #[]
  if !res.isEmpty then
    msgs := msgs.push "The following set of actions must preserve the invariant:"
    for (actName, invResults) in group res do
      msgs := msgs.push s!"  {getBaseNameForDisplay actName}"
      for (invName, (r, time)) in invResults do
        msgs := msgs.push s!"    {getBaseNameForDisplay invName} ... {emoji r}{← getTimeForDisplay time}"
  pure msgs
where group {T : Type} (xs : List (Name × T)) : List (Name × List T) :=
  xs.foldl (fun acc (key, val) =>
    match acc.find? (fun (k, _) => k = key) with
    | some (k, vs) =>
          acc.filter (fun (k', _) => k' ≠ key) ++ [(k, vs ++ [val])]
    | none =>
      acc ++ [(key, [val])]) []

IO.Process.Child in Init.System.IO

le in Test.SmtTranslation.Names

def ProofResult.isProven (res : ProofResult) : Bool := match res with
  | .proven _ => true
  | .notProven => false

action with_if = {
  if (x) then
    pure ()
    
}

@[command_elab Veil.declareStateComponent]
def elabStateComponentNamed : CommandElab := fun stx => do
  match stx with
  | `(command|$mutab:stateMutability ? $kind:stateComponentKind $name:ident $br:bracketedBinder* : $dom:term) => do
    defineIt mutab kind name br dom
  | `(command|$mutab:stateMutability ? relation $name:ident $br:bracketedBinder*) => do
    let kind ← `(stateComponentKind|relation)
    let dom ← `(Prop)
    defineIt mutab kind name br dom
  
  | _ => throwUnsupportedSyntax
where
  defineIt (mutab : Option (TSyntax `stateMutability)) (kind : TSyntax `stateComponentKind) (name : Ident) (br : TSyntaxArray ``Term.bracketedBinder) (dom : TSyntax `term) := do
    if !br.isEmpty then
      defineStateComponent mutab kind name.getId (.complex br dom)
    else
      let sig ← `(Command.structSimpleBinder|$name:ident : $dom)
      defineStateComponent mutab kind name.getId (.simple sig)

inductive ActionLabel (ℓ : Type) [Label ℓ] where
  | internal (label : ℓ)
  | input (label : ℓ)
  | output (label : ℓ)
deriving BEq, Inhabited

invariant True

invariant [token_relation] ((t_for I N) ∧ (t_for J M) ∧ seq.lt I J) → seq.le I (n_token_seq N)

invariant propose N V1 ∧ propose N V2 → V1 = V2

| .atom (.symb "unknown") =>
    trace[veil.smt.result] "{solverName} says Unknown"
      if retryOnUnknown then
        let newSolver := solverToTryOnUnknown solverName
        trace[veil.smt.debug] "Retrying with {newSolver}"
        querySolver goalQuery withTimeout (forceSolver := .some newSolver) (retryOnUnknown := false)
      else
        let (_, solver) ← solver.takeStdin
        let stdout ← solver.stdout.readToEnd
        let stderr ← solver.stderr.readToEnd
        trace[veil.smt.debug] "stdout: {stdout}"
        trace[veil.smt.debug] "stderr: {stderr}"
        solver.kill
        return (SmtResult.Unknown .none, solverName)

def StateComponentType.stx (sct : StateComponentType) : CoreM (TSyntax `term) := do
  match sct with
  | .simple t => getSimpleBinderType t
  | .complex b d => getSimpleBinderType $ ← complexBinderToSimpleBinder (mkIdent Name.anonymous) b d

def toActionAttribute (type : ActionKind) : AttrM (TSyntax `Lean.Parser.Term.attrInstance) :=
  match type with
  | .internal => `(attrInstance|internalActDef)
  | .input => `(attrInstance|inputActDef)
  | .output => `(attrInstance|outputActDef)

safety [cancelled_after_deadline] cancelled N K V D → expired D

supermajorities_intersect_in_honest :
    ∀ (s1 s2 : nset), ∃ (a : node), member a s1 ∧ member a s2 ∧ ¬ is_byz a

invariant [manual_14] p A B → a A

ax1 : v0 ≠ v1
  ax2 : v0 ≠ vquestion
  ax3 : v1 ≠ vquestion
  ax4 : ∀ (x : t), x = v0 ∨ x = v1 ∨ x = vquestion

def elabSautoAll (stx : Syntax) (trace : Bool := false) : TacticM Unit := withMainContext do
  let idents ← getPropsInContext
  let auto_tac ← `(tactic| sauto [$[$idents:ident],*])
  if trace then
    addSuggestion stx auto_tac
  evalTactic auto_tac

invariant [oneb_leftrnd] one_b N R2 ∧ ¬tot.le R2 R1 -> left_rnd N R1

inductive Mode where
  | internal : Mode
  | external : Mode
deriving BEq

BaseIO.mapTasks in Init.System.IO

invariant True

invariant [vote_proposal] (vote N R V) → proposal R V

def runUnfold (e : Expr) (defs : List Name) : TermElabM Expr := do
  let mut eu := e
  for name in defs do eu := (<- unfold eu name).expr
  return eu

def uvPath := buildDir / "uv"

#time #check_invariants

register_option veil.smt.seed : Nat := {
  defValue := 0xcafe
  descr := "SMT seed to use"
}

def getInitCheckResultMessages [Monad m] [MonadOptions m] (res : List (TheoremIdentifier × SmtResult × Option TimeInMs)) : m (Array String) := getInitCheckResultMessages' (res.map (fun (id, r) => (id.invName, r)))

after_init {
  a X := X = org ∨ X = other;
  s1 X Y := (X = org ∧ Y = other) ∨ (X = other ∧ Y = org);
  in_s1 X := X = org ∨ X = other;
  s2 X Y := False;
  in_s2 X := False;
  p X Y := (X = org ∧ Y = other) ∨ (X = other ∧ Y = org);
  reach X := X = org;
  error X := False
}

action set_X = {
  X := True
}

instance : Hashable InterpretedSort where
  hash s := (`InterpretedSort ++ s.name).hash

abbrev doSeqItem := TSyntax ``Term.doSeqItem

@[actSimp]
abbrev Wp.toWlp {σ ρ : Type} {m : Mode} (wp : Wp m σ ρ) : Wlp m σ ρ :=
  
  fun (s : σ) (post : RProp σ ρ) => ¬ wp s (fun r s' => ¬ post r s')

elab "prove_inv_safe" proof:term : command => do
  liftCoreM errorIfStateNotDefined
  elabCommand $ <- Command.runTermElabM fun _ => do
    let stateTp <- getStateTpStx
    let invSafe := mkIdent ``RelationalTransitionSystem.invSafe
    `(theorem $(mkIdent `safety_init) : $invSafe (σ := $stateTp) :=
       by admit /- proof elided -/
          )

private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=
    withReducible do 
      existsTelescopeReducingAux type (cleanupAnnotations := false) fun _ type => isClassApp? type

action empty = { pure () }

#gen_spec

def Interpretation.toString (interp : Interpretation) (decl : Declaration) : Id String := do
  let mut out := ""
  match interp with
  | .Enumeration iopairs =>
    if interp.isAlwaysFalse then
      return s!"{decl.alwaysFalseMessage}\n"
    for (args, val) in iopairs.qsortOrd do
      match decl with
      | Declaration.Constant c => out := out ++ s!"{c.name} = {val}\n"
      | Declaration.Relation r =>
          \n"
          if val.isTrue then out := out ++ s!"{r.name}{Array.funcArgsString args} = true\n"
      | Declaration.Function f => out := out ++ s!"{f.name}{Array.funcArgsString args} = {val}\n"
  | .Symbolic str => out := out ++ s!"{decl.name} = {str}\n"
  return out

def theoremSuggestionsForIndicators (generateInitThms : Bool) (actIndicators invIndicators : List (Name × Expr)) (vcStyle : VCGenStyle) (sorry_body: Bool := false): CommandElabM (Array (TheoremIdentifier × TSyntax `command)) := do
  let (initIndicators, acts) ← Command.runTermElabM fun _ => do
    
    let initIndicators ← invIndicators.mapM (fun (invName, _) => resolveGlobalConstNoOverloadCore invName)
    let actIndicators ← actIndicators.mapM (fun (actName, _) => resolveGlobalConstNoOverloadCore actName)
    let mut acts := #[]
    for actName in actIndicators do
      for invName in initIndicators do
        acts := acts.push (actName, invName)
    return (initIndicators, acts)
  theoremSuggestionsForChecks (if generateInitThms then initIndicators else []) acts.toList vcStyle sorry_body

class ThreeValuedType (t : Type) where
  v0 : t
  v1 : t
  vquestion : t

Lean.pp.funBinderTypes in Lean.PrettyPrinter.Delaborator.Options

elab "[State]" : term => do
    let stateTp := (← localSpecCtx.get).spec.stateStx
    elabTerm (<- `(term| $stateTp)) none

def createForallBinders [Monad m] [MonadQuotation m] (vars : Array (Ident × Option Name)) : m (Array (TSyntax `Lean.Parser.Term.bracketedBinder)) := do
  let binders ← vars.mapM fun (var, sort) => do
    match sort with
    | none => return ← `(bracketedBinder|($var))
    | some sort => return ← `(bracketedBinder|($var : $(mkIdent sort)))
  return binders

#time #check_invariants

action capital_assign = {
  let one : seq_t ← succ seq.zero
  
  n_token_seq N := if N = init_node then one else seq.zero

Lean.Expr.letE in Lean.Expr

def started_good (s : State' node set_majority set_f_plus_1 proposal_value) : Prop :=
  ∀ (p : phase), started p s → good p s

IO.RealWorld in Init.System.IO

action stabilize (x : node) (y : node) (z : node) = {
  require a x;
  require s1 x y;
  require a y;
  require p y z;
  require ring.btw x z y;
  s1 x Z := Z = z;
  in_s1 x := True;
  s2 x Y := Y = y;
  in_s2 x := True
}

def ModuleSpecification.mutableComponents (spec : ModuleSpecification) : Array StateComponent :=
  spec.signature.filter (fun sc => sc.isMutable)

instance : ToString StateAssertionKind where
  toString
    | StateAssertionKind.assumption => "assumption"
    | StateAssertionKind.invariant => "invariant"
    | StateAssertionKind.trustedInvariant => "trusted invariant"
    | StateAssertionKind.safety => "safety"

Lean.Level in Lean.Level

Lean.setEnv in Lean.MonadEnv

Lean.Meta.Simp.Result in Lean.Meta.Tactic.Simp.Types

instance : GenBigStep σ ρ (Wp.modifyGet act) (BigStep.modifyGet act) where
  lawful := inferInstance
  equiv := by admit /- proof elided -/

invariant [manual_8] a X ∨ ¬ p Y X ∨ ¬ s1 X Y

invariant ∀ (R:round) (V:value), (∃ n:node, decision n R V)
       -> ∃ (q:quorum), ∀ N:node, member N q -> vote N R V

def existsBinderName (typ : Expr) : MetaM Name := do
  let norm ← Meta.whnf typ
  match_expr norm with
  | Exists _ body => return body.bindingName!
  | _ => throwError "Expected an existential quantifier, got {norm}"

Lean.checkCache in Lean.Util.MonadCache

Nonempty in Init.Prelude

Lean.Meta.whnf in Lean.Meta.Basic

Classical.choice in Init.Prelude

target downloadDependencies pkg : Array FilePath := do
  let uv ← downloadDependency pkg (pkg.buildDir / "uv") downloadPythonUv
  let z3 ← downloadDependency pkg (pkg.buildDir / "z3") (downloadSolver Solver.z3)
  let cvc5 ← downloadDependency pkg (pkg.buildDir / "cvc5") (downloadSolver Solver.cvc5)
  return Job.collectArray #[uv, z3, cvc5]

action double_quant = {
  r N N := *
}

def toBracketedBinderArray (stx : TSyntax `Lean.explicitBinders) : MetaM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do
  let mut binders := #[]
  match stx with
  | `(explicitBinders|$bs*) => do
    binders := binders.append (← bs.mapM helper)
  | _ => throwError "unexpected syntax in explicit binder: {stx}"
  return binders.flatten
  where
  helper (stx : TSyntax `Lean.bracketedExplicitBinders) : MetaM (TSyntaxArray `Lean.Parser.Term.bracketedBinder) := do
    let mut binders := #[]
    match stx with
    | `(bracketedExplicitBinders|($bis* : $tp)) => do
      for bi in bis do
        let id := toIdent bi
        let fb ← `(bracketedBinder| ($id : $tp:term))
        binders := binders.push fb
      pure ()
    | _ => throwError "unexpected syntax in explicit binder: {stx}"
    return binders

abbrev Sexpr := Auto.Parser.SMTSexp.Sexp

Lean.Exception in Lean.Exception

invariant [voted_requires_echo_quorum_or_vote_quorum]
  ∀ (n originator : address) (r : round) (v : value),
    ¬ is_byz n → (voted n originator r v →
      (∃ (q : nodeset), nset.supermajority q ∧
        ∀ (src : address), member src q → echo_msg src n originator r v) ∨
      (∃ (q : nodeset), nset.greater_than_third q ∧
        ∀ (src : address), member src q → vote_msg src n originator r v))

def simpleAddDefn (n : Name) (e : Expr)
  (red := Lean.ReducibilityHints.regular 0)
  (attr : Array Attribute := #[])
  (type : Option Expr := none) : TermElabM Unit := do
  addDecl <|
    Declaration.defnDecl <|
      mkDefinitionValEx n [] (type.getD <| ← Meta.inferType e) e red
      (DefinitionSafety.safe) []
  enableRealizationsForConst n
  Elab.Term.applyAttributes n attr

invariant [allowed_crit] (crit N) → (n_have_privilege N ∧ n_requesting N)

Array.mapM in Init.Data.Array.Basic

Lean.MonadResolveName in Lean.ResolveName

action decide_bc_decide_full_val = {
  let n : node ← fresh
  let p : phase ← fresh
  let q : set_majority ← fresh
  assume decision_bc n p v1
  if v : (∀ (N : node), member_maj N q → propose N v) then
    decision_full_val n p v := True
}

action send (n next : node) = {
  require ∀ Z, n ≠ next ∧ ((Z ≠ n ∧ Z ≠ next) → btw n next Z)
  pending n next := True
}

private partial def isClassApp? (type : Expr) (instantiated := false) : MetaM (Option Name) := do
    match type.getAppFn with
    | .const c _ =>
      let env ← getEnv
      if isClass env c then
        return some c
      else
        
        match (← whnf type).getAppFn with
        | .const c _ => if isClass env c then return some c else return none
        | _ => return none
    | .mvar .. =>
      if instantiated then return none
      isClassApp? (← instantiateMVars type) true
    | _ => return none

def InterpretedSort.valToString {s : InterpretedSort} (val : s.interpretation) : String :=

def _root_.Lean.EnvExtension.get [Inhabited σ] (ext : EnvExtension σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

def blocks_slices (S : Set Node) (p : Node) : Prop :=
  ∀ Sl ∈ slices p, Sl ∩ S ≠ ∅

def toIOActionDeclIdent (id : Ident) : Ident := mkIdent $ toIOActionDeclName id.getId

Auto.Embedding.Lam.MutualIndInfo in Auto.Embedding.LamInductive

action remove (x : node) (y : node) (z : node) = {
  require a x;
  require s1 x y;
  require ¬ a y;
  require s2 x z;
  s1 x Z := Z = z;
  in_s1 x := True;
  s2 x Y := False;
  in_s2 x := False
}

Lean.Syntax in Init.Prelude

def invInit [RelationalTransitionSystem σ] :=
  ∀ (s : σ), assumptions s -> init s -> inv s

instance assert_lawful : LawfulAction (Wp.assert (m := m) (σ := σ) rq) where
  inter := by admit /- proof elided -/

invariant in_phase N P1 ∧ in_phase N P2 → P1 = P2
invariant vote_rnd1 N P1 V ∧ in_phase N P2 → le P1 P2
invariant vote_rnd2 N P1 V ∧ in_phase N P2 → le P1 P2
invariant vote_rnd2 N P V2 → ∃ V1, vote_rnd1 N P V1
invariant in_phase N P1 → ∃ V1, vote_rnd1 N P1 V1
invariant in_phase N P1 ∧ le P1 P2 ∧ P1 ≠ P2 → ¬ ∃ V1, vote_rnd1 N P2 V1
invariant in_phase N P1 ∧ le P1 P2 ∧ P1 ≠ P2 → ¬ ∃ V1, vote_rnd2 N P2 V1

def funcasesM (t : Term) (vs : Array Expr) : TermElabM Term := do
  let stateTpExpr := (<- localSpecCtx.get).spec.stateType
  let .some sn := stateTpExpr.getAppFn.constName?
    | throwError "{stateTpExpr} is not a constant"
  let .some _sinfo := getStructureInfo? (<- getEnv) sn
    | throwError "{stateTpExpr} is not a structure"
  let fns := _sinfo.fieldNames.map Lean.mkIdent
  let moduleName <- getCurrNamespace
  let stateName := `State
  let casesOn <- mkConst $ (moduleName ++ stateName ++ `casesOn)
  let casesOn <- PrettyPrinter.delab casesOn
  let stateTp <- getStateTpStx
  let term ← `(term| (fun $(mkIdent `st) : $stateTp =>
      $(casesOn) $(← getSectionArgumentsStx vs)* (motive := fun _ => Prop) $(mkIdent `st) <| (fun $[$fns]* => ($t : Prop))))
  trace[veil.debug] "funcasesM: {term}"
  return term

instance [Label ℓ]: ToString (ActionLabel ℓ) where
  toString
    | ActionLabel.internal l => "internal " ++ toString l
    | ActionLabel.input l => "input " ++ toString l
    | ActionLabel.output l => "output " ++ toString l

def toSpecName (n : Name) : Name := n ++ `spec

type node
instantiate ring : RingTopology node

def ActionLabel.type {ℓ : Type} [Label ℓ] : ActionLabel ℓ → ActionKind
  | .internal _ => .internal
  | .input _ => .input
  | .output _ => .output

Classical.inhabited_of_nonempty in Init.Classical

def toExtIdent (id : Ident) : Ident := mkIdent $ toExtName id.getId

Auto.UMonoFact in Auto.Translation.Assumptions

Lean.Elab.Term.TermElabM.run in Lean.Elab.Term.TermElabM

IO.FS.removeDirAll in Init.System.IO

action foo (k : Nat) =
  requires ∀ x, r x k
  ensures True
{
  let x <- fresh node
  require r x k
}

action send (n next : node) = {
  require ∀ Z, n ≠ next ∧ ((Z ≠ n ∧ Z ≠ next) → btw n next Z)
  pending n next := True
}

instance get_lawful : LawfulAction (Wp.get (m := m) (σ := σ)) where
  inter := by admit /- proof elided -/

#split_invariants

invariant [receive_self_msg_only_if_greatest] pending L L → le N L

invariant [manual_3] reach org

def cvc5.version := "1.3.1"

| _ => throwError s!"(parseInstruction) malformed instruction: {inst} ({repr inst})"
  return struct

invariant [unique_tokens] ((t_for I N) ∧ (t_for I M)) → N = M
invariant ((n_token_seq N) ≠ 0) → t_for (n_token_seq N) N

def throwIfRefersToMutable (t : Term) : TermElabM Unit :=
  withAutoBoundCont
    (do let _ ← elabTerm t .none)
    
    
    (fun n => do
      let immutable := (← localSpecCtx.get).spec.immutableComponents.map (fun sc => sc.name)
      return immutable.contains n || isCapital (mkIdent n))
    (fun ex n => do
      let mutable := (← localSpecCtx.get).spec.mutableComponents.map (fun sc => sc.name)
      if mutable.contains n then
        throwErrorAt ex.getRef "The assumption refers to mutable state component `{n}`!"
      else
        throwErrorAt ex.getRef "The assumption refers to unbound variable `{n}`!")

action sabotage (n: node) = {
    require ¬ honest n;
    block_confirmed n B T := *;
    transaction_confirmed TR n := *
}

def parseStrAsJson [Monad m] [MonadError m] (str : String) : m Json := do
  match Json.parse str with
  | .ok json => return json
  | .error err => throwError s!"could not parse {str} as Json: {err}"

Lean.Parser.Command.structSimpleBinder in Lean.Parser.Command

Lean.nullKind in Init.Prelude

structure intertwined (S : Set Node) where
  well_behaved : S ⊆ W
   
  q_inter : (∀ Q Q',
    quorum (inst := inst.project S) Q →
    quorum (inst := inst.project S) Q' →
    Q ∩ S ≠ ∅ → Q' ∩ S ≠ ∅ → Q ∩ Q' ∩ S ≠ ∅)

instance [Ord α] : Ord (Array α) where
  compare a b :=
    a.zip b |>.foldl (init := Ordering.eq) fun c (a, b) => match c with
      | Ordering.eq => compare a b
      | c => c

invariant [decision_bc_started] decision_bc N P V2 → started P
close_isolate

@[inline] abbrev TwoState := σ -> σ -> Prop

Lake.download in Lake.Build.Actions

MonadExceptOf in Init.Prelude

axiom_0 : ∀ (n : node), intact n → intertwined n
  axiom_1 : ∀ (n : node), intertwined n → well_behaved n
  qi_intertwined : ∀ (q1 q2 : nset),
    (∃ (n1 : node), intertwined n1 ∧ is_quorum q1 ∧ member n1 q1) ∧
    (∃ (n2 : node), intertwined n2 ∧ is_quorum q2 ∧ member n2 q2) →
    ∃ (n3 : node), well_behaved n3 ∧ member n3 q1 ∧ member n3 q2

instance : GenBigStep σ τ (Wp.fresh τ) (BigStep.fresh τ) where
  lawful := inferInstance
  equiv := by admit /- proof elided -/

#guard_msgs(drop warning, drop info) in
sat trace {
  set_flag
  set_flag
} by bmc_sat

safety [mutual_exclusion] (holds N1 ∧ holds N2) → N1 = N2
invariant N1 ≠ N2 → ¬(replied N1 N2 ∧ replied N2 N1)
invariant (N1 ≠ N2 ∧  holds N1) → replied N1 N2

instance : Inhabited StateAssertionKind where
  default := StateAssertionKind.invariant

Lean.MonadEnv in Lean.Environment

List.range in Init.Data.List.Basic

MonadLiftT in Init.Prelude

def toFunBinderArray (stx : TSyntax `Lean.explicitBinders) : MetaM (TSyntaxArray `Lean.Parser.Term.funBinder) := do
  let mut binders := #[]
  match stx with
  | `(explicitBinders|$bs*) => do
    binders := binders.append (← bs.mapM helper)
  | _ => throwError "unexpected syntax in explicit binder: {stx}"
  return binders.flatten
  where
  helper (stx : TSyntax `Lean.bracketedExplicitBinders) : MetaM (TSyntaxArray `Lean.Parser.Term.funBinder) := do
    let mut binders := #[]
    match stx with
    | `(bracketedExplicitBinders|($bis* : $tp)) => do
      for bi in bis do
        let id := toIdent bi
        let fb ← `(Lean.Parser.Term.funBinder| ($id : $tp:term))
        binders := binders.push fb
      pure ()
    | _ => throwError "unexpected syntax in explicit binder: {stx}"
    return binders

abbrev UninterpretedValue := Lean.Name

def Declaration.arity : Declaration → Nat
  | Declaration.Constant _ => 0
  | Declaration.Relation r => r.domain.size
  | Declaration.Function f => f.domain.size

invariant [indv_true] indv

abbrev Wp.alwaysSuccessfullyTerminates {σ } (req : SProp σ) (act : Wp m σ ρ)  : Prop :=
  ∀ s, req s -> act s (fun _ _ => True)

register_option veil.smt.retryOnUnknown : Bool := {
  defValue := true
  descr := "Should the query be retried with a different SMT solver if it the first check returns `unknown`? (default: true)"
}

def mkStateTpStx (vd : Array (TSyntax `Lean.Parser.Term.bracketedBinder)) (vs : Array Expr) : TermElabM Term := do
  let stateTpExpr := (<- localSpecCtx.get).spec.stateType
  unless stateTpExpr != default do throwError "State has not been declared so far"
  let stateTp ← PrettyPrinter.delab stateTpExpr
  let stx ← `(term|@$stateTp $(← getStateArgumentsStx vd vs)*)
  return stx

instance : Ord SortName where
  compare a b := a.cmp b

instance modifyGet_lawful : LawfulAction (Wp.modifyGet f (m := m) (σ := σ) (ρ := ρ)) where
  inter := by admit /- proof elided -/

Lean.Parser.Tactic.tacticSeq in Lean.Parser.Term.Basic

readThe in Init.Prelude

| .atom (.symb "unsat") =>
    trace[veil.smt.result] "{solverName} says Unsat"
    let (_, solver) ← solver.takeStdin
    let stdout ← solver.stdout.readToEnd
    let stderr ← solver.stderr.readToEnd
    trace[veil.smt.debug] "stdout: {stdout}"
    trace[veil.smt.debug] "stderr: {stderr}"
    solver.kill
    return (SmtResult.Unsat, solverName)

#gen_spec

IO.CancelToken.new in Init.System.IO

def isHypToCollect (typ : Expr) : MetaM Bool := do
  
  
  
  let isInhabitationFact ← whnfIsAppOf typ ``Nonempty
  return (← Meta.isProp typ) && !isInhabitationFact

Lean.getStructureInfo? in Lean.Structure

instance {σ σ'} [IsSubStateOf σ σ'] (act : Wp .external σ ρ) (actTr : BigStep σ ρ) [inst:GenBigStep σ ρ act actTr]
  : GenBigStep σ' ρ (Wp.lift (σ' := σ') act) (BigStep.lift (σ := σ) actTr) where
  lawful := inferInstance
  equiv pre := by admit /- proof elided -/

open_isolate wrapper5 with protocol

def hypIsClass (hyp : LocalDecl) : TacticM Bool := do
  let env ← getEnv
  match hyp.type.getAppFn.constName? with
  | some name => return name ≠ ``And ∧ isStructure env name
  | none => return false

Ring in Mathlib.Algebra.Ring.Defs

#guard_msgs in

def FirstOrderStructure.findDecl (s : FirstOrderStructure) (name : Lean.Name) : MetaM Declaration :=
  match s.signature.constants.find? (fun c => c.name == name) with
  | some c => return Declaration.Constant c
  | none => match s.signature.relations.find? (fun r => r.name == name) with
    | some r => return Declaration.Relation r
    | none => match s.signature.functions.find? (fun f => f.name == name) with
      | some f => return Declaration.Function f
      | none => throwError s!"{name} provided an interpretation for, but not previously declared!"

invariant [decision_full_val_agree] decision_full_val N1 P1 V1 ∧ decision_full_val N2 P2 V2 → V1 = V2

safety [paid] paid N K V D → proposed N K V D

invariant [echoed_iff_echo]
  ∀ (n dst originator : address) (r : round) (v : value),
    ¬ is_byz n → (echoed n originator r v ↔ echo_msg n dst originator r v)

Lean.Syntax.TSepArray.ofElems in Init.Meta.Defs

#gen_spec

private def createAux (path : String) (args : Array String) : MetaM SolverProc := do
    trace[veil.smt.debug] "invoking {path} {args}"
    IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped,
                      cmd := path, args := args}

Lean.Meta.mkSimpContext in Mathlib.Tactic.Simps.Basic

safety [paid_if_enough_sigs] paid N K V D → (∀ s, sig N K V D s ∧ sig_auth s)

def declareProcedure [Monad m] [MonadEnv m] [MonadError m] (actT : Option ActionKind)  (declName : Name) : m Unit := do
  let procedureExists := (← localSpecCtx.get).spec.procedures.any fun t => t.name == declName
  if procedureExists then
    throwError "A procedure or action named {declName} has already been declared!"
  let spec := match actT with
    | some actT => ActionSpecification.mkPlain actT declName (mkConst declName)
    | none => ProcedureSpecification.mkPlain declName (mkConst declName)
  localSpecCtx.modify (fun s => { s with spec := {s.spec with procedures := s.spec.procedures.push spec }})

action initial_vote1 = {
  let n : node ← fresh
  let q : set_majority ← fresh
  assume ∃ V : proposal_value, propose n V
  assume ∀ P, ¬ ∃ V : state_value, vote_rnd1 n P V
  assume ∀ P, ¬ ∃ V : state_value, vote_rnd2 n P V
  assume ∀ P, ¬ ∃ V : state_value, decision_bc n P V
  assume ∀ P, ¬ in_phase n P

def getPrePost (spec : doSeq) [Monad m] [MonadError m] [MonadQuotation m] :
  m (Term × TSyntax `rcasesPat × Term) := do
  match spec with
  | `(doSeq| requires $pre ensures $id, $post:term $_:unchanged_decl ?) => pure (pre, id, post)
  | `(doSeq| requires $pre ensures $post:term $_:unchanged_decl ?) => pure (pre, <- `(rcasesPat|(_ : Unit)), post)
  | _ => throwErrorAt spec "Invalid specification: expected `requires ... ensures ...`"

#gen_spec

structure StateSpecification where
  name : Name
   
  lang : Option (TSyntax ``Term.doSeq)
   
  expr : Expr
deriving Inhabited, BEq

def parseActionKindStx (stx : Option (TSyntax `actionKind)) : CommandElabM (TSyntax `actionKind) := do
  return stx.getD $ ← `(actionKind|internal)

def toGenIdent (id : Ident) (mode : Mode): Ident := mkIdent $ toGenName id.getId mode

Inhabited.mk in Init.Prelude

Lake.env in Lake.CLI.Actions

structure Signature where
  constants : Array ConstantDecl
  relations : Array RelationDecl
  functions : Array FunctionDecl
deriving BEq, Hashable, Ord

Std.HashSet.insertMany in Std.Data.HashSet.Basic

def toBindersWithMappedTypes [Monad m] [MonadQuotation m] [MonadError m] (stx : TSyntax `Lean.explicitBinders) (mapping : Array (Term × Term)) : m (TSyntax `Lean.explicitBinders) := do
  let mut newBinders := #[]
  match stx with
  | `(explicitBinders|$bs*) => do
    for b in bs do
      match b with
      | `(bracketedExplicitBinders|($bis* : $tp)) => do
        let newTp := match mapping.find? (fun (paramType, _argType) => paramType == tp) with
          | some (_, newTp) => newTp
          | none => tp
        newBinders := newBinders.push $ ← `(bracketedExplicitBinders|($bis* : $newTp))
      | _ => throwError "unexpected syntax in explicit binder: {b}"
  | _ => throwError "unexpected syntax in explicit binder: {stx}"
  let newStx ← `(explicitBinders|$newBinders*)
  return newStx

instance : Lean.KVMap.Value SmtTranslator where
  toDataValue n := toString n
  ofDataValue?
  | "lean-smt"  => some .leanSmt
  | "lean-auto" => some .leanAuto
  | _           => none

def CheckInvariantsBehaviour.exclamation [Monad m] [MonadOptions m] : m CheckInvariantsBehaviour := do
  let vcGen := veil.vc_gen.get (← getOptions)
  return (vcGen, .checkTheoremsIndividually, .printUnverifiedTheorems)

def getStateArguments [ToMessageData α] (vd : Array (TSyntax `Lean.Parser.Term.bracketedBinder)) (vs : Array α) [Monad m] [MonadError m]: m (Array α) := do
  if vd.size != vs.size then throwError "Mismatch in number of arguments between {vd} and {vs}"
  let vs' := (vd.zip vs).filter (fun (b, _) => !isTypeClassBinder b) |> .map Prod.snd
  return vs'

def declareSpecParameters (vd : Array (TSyntax `Lean.Parser.Term.bracketedBinder)) : CommandElabM Unit := do
  localSpecCtx.modify (fun s => { s with spec.parameters := vd })

@[actSimp] def Wp.bind (wp : Wp m σ ρ) (wp_cont : ρ -> Wp m σ ρ') : Wp m σ ρ' :=
  fun s post => wp s (fun r s' => wp_cont r s' post)

Lean.Level.zero in Lean.Level

def runSimp (e : Expr) (stx : TermElabM (TSyntax `tactic)) : TermElabM Simp.Result := do
  let stx ← stx
  let mv := (← mkFreshExprMVar e)
  let (res, [_l]) ← Tactic.run mv.mvarId! (do
    let sc <- mkSimpContext stx false
    let cfg := { sc.ctx.config with maxSteps := veilSimpMaxSteps }
    let ctx ← sc.ctx.setConfig cfg
    let res <- simp e ctx (simprocs := sc.simprocs) (discharge? := none)
    return res
  ) | throwError "[runSimp] expected exactly one goal after simplification"
  return res.1

#guard_msgs in

invariant [current_privilege_latest_token_2] ((n_have_privilege N) ∧ (t_for I M)) → seq.le I (n_token_seq N)

register_option veil.smt.finiteModelFind : Bool := {
  defValue := true
  descr := "Should the `
}

action send (n next : node) = {
  require ∀ Z, n ≠ next ∧ ((Z ≠ n ∧ Z ≠ next) → btw n next Z)
  pending n next := True
}

instance : ToString FirstOrderSort where
  toString
    | FirstOrderSort.Interpreted s => toString s
    | FirstOrderSort.Uninterpreted s => toString s

#gen_spec

safety
      ((honest N1 ∧ honest N2) → (block_confirmed N1 B T ∧ block_confirmed N2 B T) ∨ (¬ block_confirmed N1 B T ∧ ¬ block_confirmed N2 B T))
    ∧ ((honest N1 ∧ honest N2) → (transaction_confirmed TR N1 ∧ transaction_confirmed TR N2) ∨ (¬ transaction_confirmed TR N1 ∧ ¬ transaction_confirmed TR N2))
    ∧ ((honest N ∧ leader N T2 ∧ transaction_time TR T1 ∧ tot.le T1 T2 ∧ broadcasted N ∧ honest N1) → transaction_confirmed TR N1)

elab "#split_invariants" : command => do
  let allClauses := (← localSpecCtx.get).spec.invariants
  if allClauses.isEmpty then return

action call_in_capital_assign = {
  n_token_seq N := if N = init_node then ← succ seq.zero else seq.zero
}

def one_such_Background (node : Type) [fba : FBA.System node]
    (I : Set node) (hI : FBA.intact (inst := fba) I)
    (S : Set node) (hS : FBA.intertwined (inst := fba) S)
    (hIS : I ⊆ S) : SCP.Background node (Set node) where
  well_behaved n := n ∈ fba.W
  intertwined n := n ∈ S
  intact n := n ∈ I
  member n s := n ∈ s
  is_quorum := FBA.quorum (inst := fba)
  blocks_slices := FBA.blocks_slices (inst := fba)

invariant [propose_if_lower_configured] proposal R2 V ∧ tot.le R1 R2 → ∃ c, configure_round_msg R1 c

#guard_msgs in

def elabBindersAndCapitals
  (br : Array Syntax)
  (vs : Array Expr)
  (e : Syntax)
  (k : Array Expr -> Expr -> TermElabM α)
   : TermElabM α := do
  withAutoBoundCapitals $ Term.elabBinders br fun brs => do
    let vars := (← getLCtx).getFVars.filter (fun x => not $ vs.elem x || brs.elem x)
    trace[veil.debug] "[elabBindersAndCapitals] {e}"
    let e <- elabTermAndSynthesize e none
    lambdaTelescope e fun _ e => do
        let e <- mkForallFVars vars e
        k vars e

def checkInvariants (stx : Syntax) (behaviour : CheckInvariantsBehaviour)
  (isolate : NameHashSet := ∅) : CommandElabM Unit := do
  liftCoreM (do errorIfStateNotDefined; warnIfNoInvariantsDefined; warnIfNoActionsDefined)
  let (initChecks, actChecks) ← getAllChecks isolate
  checkTheorems stx initChecks actChecks behaviour

Lean.mkTheoremValEx in Lean.Declaration

isSome in Smt.Reconstruct.Certified.Utils

@[actSimp] def Wp.require (rq : Prop) : Wp m σ PUnit :=
  match m with
  | Mode.internal => Wp.assert rq
  | Mode.external => Wp.assume rq

action call_nondet_assgn' = {
  let m ← fresh node;
  if x then
    nondet_assgn m;
    call_nondet_assgn
  else
    let n ← fresh node;
    nondet_assgn n
    r N M := *;
}

Auto.LamReif.reifMutInds in Auto.Translation.LamReif

#guard_msgs(drop warning) in
procedure foobar (k : Nat) =
  requires ∀ x, r x k
  ensures True
{
  let x <- fresh node
  require r x k
}

register_simp_attr quantifierSimp

def getTimeForDisplay [Monad m] [MonadOptions m] (time : Option TimeInMs) : m String := do
  if !veil.showVerificationTime.get (← getOptions) then
    return ""
  return match time with
  | .some time => s!" ({time} ms)"
  | .none => ""

Std.HashSet in Std.Data.HashSet.Basic

def checkIndividualTheorem (thmId : TheoremIdentifier) (cmd : TSyntax `command) : CommandElabM ProofResult := do
  let env ← getEnv
  
  
  if (← resolveGlobalName thmId.theoremName).isEmpty then
    trace[veil.debug] "Checking theorem {thmId.theoremName} for the first time"
    elabCommand (← `(#guard_msgs(drop warning) in $(cmd)))
  else
    trace[veil.debug] "Theorem {thmId.theoremName} has been checked before; reusing result"
  
  let thFullName ← resolveGlobalConstNoOverloadCore thmId.theoremName
  let th ← getConstInfo thFullName
  let (isProven, proofKind) ← match th with
    | ConstantInfo.thmInfo attempt =>
      
      
      let isProven := !attempt.value.hasSyntheticSorry
      let proofKind := if attempt.value.hasSorry then ProofKind.trustingSolver else ProofKind.checkedByLean
      pure (isProven, proofKind)
    | _ => throwError s!"checkTheorem: expected {thmId.theoremName} to be a theorem"
  
  
  if !isProven then
    setEnv env
  let result := if isProven then .proven proofKind else .notProven
  return result

def z3Path := buildDir / "z3"

@[command_elab Veil.transitionDefinition]
def elabTransition : CommandElab := fun stx => do
  match stx with
  | `(command|$actT:actionKind ? transition $nm:ident $br:explicitBinders ? = { $t:term }) => do
    let fields : Array Name ← getFields
    let mut unchangedFields := #[]
    for f in fields do
      unless t.raw.find? (·.getId.toString == f.toString ++ "'") |>.isSome do
        unchangedFields := unchangedFields.push $ mkIdent f
    let stx ← `($actT:actionKind ? transition $nm $br ? = by admit /- proof elided -/
      )
    elabCommand stx
  | _ => throwUnsupportedSyntax

partial def expandDoElemVeil (stx : doSeqItem) : VeilM (Array doSeqItem) := do
  trace[veil.debug] "[expand doElem] {stx}"
  match stx with
  
  | `(Term.doSeqItem| $stx ;) => expandDoElemVeil $ <- `(Term.doSeqItem| $stx:doElem)
  
  
  | `(Term.doSeqItem| return $t:term) | `(Term.doSeqItem| pure $t:term)
  | `(Term.doSeqItem| require $t) | `(Term.doSeqItem| assert $t) | `(Term.doSeqItem| assume $t) => return #[stx]
  
  | `(Term.doSeqItem|let $_ : $_ ← fresh $_) | `(Term.doSeqItem|let $_ : $_ ← fresh)
  | `(Term.doSeqItem|let $_ ← fresh $_) | `(Term.doSeqItem|let $_ ← fresh) => return #[stx]
  
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn:doSeqItem* else $els:doSeq) =>
    let fs <- `(Term.doSeqItem| let $h:ident <- fresh)
    let t' <- `(Term.doSeqItem| assume $t)
    let thn := fs :: t' :: thn.toList |>.toArray
    expandDoElemVeil $ <-
      `(Term.doSeqItem| if (∃ $h:ident, $t) then $thn* else $els)
  | `(Term.doSeqItem| if $t:term then $thn:doSeq) =>
    expandDoElemVeil $ <- `(Term.doSeqItem| if $t then $thn:doSeq else pure ())
  
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn) =>
    expandDoElemVeil $ <- `(Term.doSeqItem| if $h:ident : $t:term then $thn else pure ())
  | `(Term.doSeqItem| if $t:term then $thn:doSeq else $els:doSeq) =>
    let thn <- expandDoSeqVeil thn
    let els <- expandDoSeqVeil els
    let ret ← `(Term.doSeqItem| if $t then $thn* else $els*)
    return #[ret]
  
  | `(Term.doSeqItem| $id:ident := *) =>
    let typeStx ← (<- localSpecCtx.get) |>.spec.getStateComponentTypeStx (id.getId)
    let fr := mkIdent <| <- mkFreshUserName `fresh
    modify (·.push ⟨fr, typeStx.getD (<- `(_))⟩)
    expandDoElemVeil $ <- `(Term.doSeqItem|$id:ident := $fr)
  | `(Term.doSeqItem| $idts:term := *) =>
    let some (id, ts) := TSyntax.isApp? idts | throwErrorAt stx "wrong syntax for non-deterministic assignment {stx}"
    let typeStx ← (<- localSpecCtx.get) |>.spec.getStateComponentTypeStx (id.getId)
    let fr := mkIdent <| <- mkFreshUserName `fresh
    modify (·.push ⟨fr, typeStx.getD (<- `(_))⟩)
    expandDoElemVeil $ <- `(Term.doSeqItem|$idts:term := $fr:ident $ts*)
  
  | `(Term.doSeqItem| $id:ident := $t:term) =>
    trace[veil.debug] "[expand assignment with args] {stx}"
    let name := id.getId
    if name.isAtomic then
      let id' <- `(Term.structInstLVal| $id:ident)
      let fields <- getFields
      if id.getId ∈ fields then
        throwIfImmutable id'
        
        
        let res ← withRef stx `(Term.doSeqItem| $id:ident ← modifyGet
            (fun st => (($t, {st with $id:ident := $t}))))
        return #[res]
      else
        let res ← `(Term.doSeqItem| $id:ident := $t:term)
        return #[res]
    else
      let base := mkIdent name.getPrefix
      let suff := mkIdent $ name.updatePrefix default
      expandDoElemVeil $ <- withRef stx `(Term.doSeqItem| $base:ident := { $base with $suff:ident := $t })
  | `(Term.doSeqItem| $idts:term := $t:term) =>
    trace[veil.debug] "[expand assignment with args] {stx}"
    let some (id, ts) := TSyntax.isApp? idts | return #[stx]
    let stx' <- withRef t `(term| $id[ $[$ts],* ↦ $t:term ])
    let stx <- withRef stx `(Term.doSeqItem| $id:ident := $stx')
    expandDoElemVeil stx
   
  
  
  | `(Term.doSeqItem|$t:term) =>
    let b := mkIdent <| <- mkFreshUserName `_b
    let bind <- `(Term.doSeqItem| let $b:ident ← $t:term)
    return #[bind] ++ (← refreshState) ++ #[← `(Term.doSeqItem| pure $b:ident)]
  
  
  | doE =>
    trace[veil.debug] "[expand just a doElem] {stx}"
    return #[doE] ++ (← refreshState)
where
refreshState : VeilM (Array doSeqItem) := do
  let pattern ← getStateAccessorPattern
  let refresh ← `(Term.doSeqItem| $pattern:term := ← get)
  return #[refresh]

| .Sat (some m) => Json.arr #["sat", m]
    | .Unknown (some r) => Json.arr #["unknown", r]
    | .Failure (some r) => Json.arr #["failure", r]

structure ActionDeclaration where
  kind: ActionKind
  name: Lean.Name
  ctor : Option (TSyntax `Lean.Parser.Command.ctor)
deriving BEq, Inhabited

private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
  if isClass (← getEnv) constName then
    return .some constName
  else
    match (← getConstTemp? constName) with
    | some (.defnInfo ..) => return .undef 
    | _ => return .none

Lean.liftCommandElabM in Lean.Elab.Command

let (tempvars, thmType, subThmTypes) ← Command.runTermElabM fun vs => do
    let allClauses := (← localSpecCtx.get).spec.invariants
    let allClauses := allClauses.toList
    let invExprs := allClauses.map (fun x => mkAppN x.expr vs)
    let invNames := allClauses.map StateAssertion.name
    
    let invExprs := invExprs.reverse
    let invNames := invNames.reverse
    let invExprs ← invExprs.mapM (fun x => mkAppM ``RelationalTransitionSystem.isInvariant #[x])
    let invConj := mkAndN invExprs
    let thmType ← mkForallFVars vs invConj
    let subThmTypes ← invExprs.mapM (fun x => mkForallFVars vs x)
    
    let thmType ← instantiateMVars thmType
    let subThmTypes ← subThmTypes.mapM instantiateMVars
    let tempvars ← vs.mapM (fun x => x.fvarId!.getUserName)
    pure (tempvars, thmType, invNames.zip subThmTypes)

#guard_msgs in

def BigStep.bind (act : BigStep σ ρ) (act' : ρ -> BigStep σ ρ') : BigStep σ ρ' :=
  fun s r' s' => ∃ r s'', act s r s'' ∧ act' r s'' r' s'

def displaySuggestion (stx : Syntax) (theorems : Array (TSyntax `command)) (preMsg : Option String := none) := do
    Command.liftTermElabM do
    let cmd ← constructCommands theorems
    let suggestion : Suggestion := {
      suggestion := cmd
      preInfo? := preMsg
      toCodeActionTitle? := .some (fun _ => "Replace with explicit proofs.")
    }
    addSuggestion stx suggestion (header := "")

action empty = {
  pure ()
}

def isTypeClassBinder : TSyntax `Lean.Parser.Term.bracketedBinder → Bool
  | `(bracketedBinder| $_:instBinder) => true
  | _ => false

def toIdent (bi : TSyntax ``binderIdent) : Ident :=
  match bi with
  | `(binderIdent|$i:ident) => i
  | _ => unreachable!

member in Test.SmtTranslation.Names

abbrev Context := Lean.Elab.Tactic.Context

instance (priority := high) : Ord Declaration where
  compare x y := compare x.name y.name |>.then (compare x y)

def toTrIdent (id : Ident) : Ident := mkIdent $ toTrName id.getId

node in Test.SmtTranslation.Inductive

invariant [none_property2] ¬vote N R none

instance : ToString RelationDecl where
  toString r := s!"relation {r.name} : {r.domain}"

def failureGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}solver invocation failed"

Lean.PersistentArray.toArray in Lean.Data.PersistentArray

def boolSortI : InterpretedSort := { name := `Bool }

def toGenInstName (n : Name) (mode : Mode) : Name :=
  n ++ (match mode with
  | Mode.internal => `genIInst
  | Mode.external => `genEInst)

def BigStep.assert (ast : Prop) : BigStep σ PUnit := fun s _ s' => ast ∧ s' = s

inductive Declaration where
  | Constant (c : ConstantDecl)
  | Relation (r : RelationDecl)
  | Function (f : FunctionDecl)
deriving BEq, Hashable, Ord

@[inline] abbrev RProp (ρ : Type u) := ρ → SProp σ

#time #check_invariants

def getLeanAutoNameFor (name : String) : CoreM String := do
    let mut preName := name.map (fun c => if allowed c then c else '_')
    if preName.all (fun c => c == '_') then
      preName := "pl_" ++ preName
    if preName.back.isDigit then
      preName := preName ++ "_"
    
    
    return "_" ++ preName
  where
    allowed (c : Char) :=
      let allowedStr : String :=
        "~!@$%^&*_-+=<>.?/" ++
        "ΑαΒβΓγΔδΕεΖζΗηΘθΙιΚκΛλΜμΝνΞξΟοΠπΡρΣσςΤτΥυΦφΧχΨψΩω" ++
        "₀₁₂₃₄₅₆₇₈₉"
      let allowedSet : Std.HashSet UInt32 := Std.HashSet.insertMany Std.HashSet.emptyWithCapacity (List.map Char.val allowedStr.toList)
      c.isAlphanum || allowedSet.contains c.val

safety [agreement]
  ∀ (src dst₁ dst₂ : address) (r : round) (v₁ v₂ : value),
    ¬ is_byz dst₁ ∧ ¬ is_byz dst₂ ∧ delivered dst₁ src r v₁ ∧ delivered dst₂ src r v₂ → v₁ = v₂

kind in Auto.Parser.TPTP

Lean.NameHashSet in Lean.Data.NameMap.Basic

action g = {
  let n <- fresh node'
  test.r' N n := True
  r'' := test.r
  r'' := test'.r
  let _ <- test.f 1
  test'.f 1
}

partial def expandDoSeqVeil (stx : doSeq) : VeilM (Array doSeqItem) :=
  match stx with
  | `(doSeq| $doS:doSeqItem*) => return Array.flatten $ ← doS.mapM expandDoElemVeil
  | _ => throwErrorAt stx s!"unexpected syntax of Veil `do`-notation sequence {stx}"

safety [vote_integrity]
  ∀ (src dst : node) (r : round) (v : value),
     ¬ is_byz src ∧ ¬ is_byz dst ∧ voted dst src r v → (sent src r ∧ initial_value src r v)

def Declaration.alwaysFalseMessage (decl : Declaration) : String :=
  match decl with
  | Declaration.Constant c => s!"{c.name} = false"
  | Declaration.Relation r => s!"{r.name} = ∅"
  | Declaration.Function f => s!"{f.name} = λ _ → false"

invariant [vote_rnd2_vote_rnd1] vote_rnd2 N P V ∧ V ≠ vquestion → ∃ N2, vote_rnd1 N2 P V

instance : ToString VCGenStyle where
  toString
    | .wp => "wp"
    | .transition => "transition"

ghost relation members_voted_rnd2 (q : set_majority) (p : phase) :=
  ∀ N, member_maj N q → ∃ V, vote_rnd2 N p V

unsat trace {
  enter
  enter
  any 2 actions
} by bmc

def _root_.Lean.SimpleScopedEnvExtension.modify
  (ext : SimpleScopedEnvExtension α σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

def quantMetaTelescopeReducing (e : Expr) (mode : checkMode) (k : Array Expr → Expr → n α) : n α :=
  match mode with
  | .goal => forallTelescopeReducing e k
  | .hypothesis => existsTelescopeReducing e k

Lean.FromJson in Lean.Data.Json.FromToJson.Basic

instance : BEq InterpretedSort where
  beq s₁ s₂ := s₁.name == s₂.name

def toExplicitBinders [Monad m] [MonadError m] [MonadQuotation m] (stx : TSyntax `Lean.Parser.Term.bracketedBinder) : m (TSyntax `Lean.bracketedExplicitBinders) := do
  match stx with
  | `(bracketedBinder| ($id:ident : $tp:term))
  | `(bracketedBinder| [$id:ident : $tp:term])
  | `(bracketedBinder| {$id:ident : $tp:term}) =>
    return ← `(bracketedExplicitBinders|($(toBinderIdent id) : $tp))
  | _ => throwError "unexpected syntax in explicit binder: {stx}"

Lean.Meta.SplitIf.mkDischarge? in Lean.Meta.Tactic.SplitIf

invariant [decision_bc_same_round_agree] decision_bc N1 P V1 ∧ decision_bc N2 P V2 → V1 = V2

def toGenName (n : Name) (mode : Mode) : Name :=
  n ++ (match mode with
  | Mode.internal => `genI
  | Mode.external => `genE)

def simpWp (e : Expr) : TermElabM Simp.Result := do
  let stx := `(tactic| simp only [wpSimp])
  runSimp e stx

invariant state_value_locked P V → ∀ Q : set_majority, members_voted_rnd2 Q P →
  ∃ N : node, member_maj N Q ∧ vote_rnd2 N P V
invariant state_value_locked P V → ∀ Q : set_majority, members_voted_rnd2 Q P → ¬ coin P V2
invariant state_value_locked P V ∧ next P P2 → state_value_locked P2 V

def toInstName (n : Name) (mode : Mode) : Name :=
  n ++ (match mode with
  | Mode.internal => `inst
  | Mode.external => `instExt)

ghost relation state_value_locked (p : phase) (v : state_value) :=
  ∀ N Valt, vote_rnd1 N p Valt → Valt = v

def getSubInitializers [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m]: m (Array (Ident × Term)) := do
  let mut names := #[]
  let ourSpec := (← localSpecCtx.get).spec
  for (modAlias, _) in ourSpec.dependencies do
    let initName := mkIdent <| modAlias ++ `initializer
    let initTerm <- `(@$initName $(← ourSpec.arguments)*)
    names := names.push (initName, initTerm)
  return names

invariant [manual_1] s1 X Y → in_s1 X

action fresh_with_lhs_type_2 = {
  let b : block ← fresh
  let q : queue ← fresh
}

def assertProcedureDeclared [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] (nm : Name) (op : String) : m Unit := do
  let procedureExists := (← localSpecCtx.get).spec.procedures.any fun t => t.name == nm
  if !procedureExists then
    throwError "Procedure {nm} has not been declared (trying to {op})"

Lean.Elab.Tactic.evalTactic in Lean.Elab.Tactic.Basic

abbrev CheckTheoremResultStringMarker := "[VEIL_CHECK_RESULT]\n"

action foo (k : Nat) =
  requires ∀ x, r x k
  ensures True
{
  let x <- fresh node
  
  require r x k
}

@[actSimp]
def _root_.Function.toWp (m : Mode) (r : TwoState σ) : Wp m σ Unit :=
  fun s post => ∀ s', r s s' -> post () s'

Lean.Syntax.ident in Init.Prelude

register_option veil.smt.reconstructProofs : Bool := {
  defValue := false
  descr := "Whether to use Lean SMT's proof reconstruction"
}

def bracketedBindersToTerms [Monad m] [MonadError m] [MonadQuotation m] (stx : Array (TSyntax `Lean.Parser.Term.bracketedBinder)) : m (Array Term) := do
  let idents : Array (Option Ident) ← stx.mapM bracketedBinderIdent
  let terms ← idents.mapM (fun mid => do
    match mid with
    | some id => `(term|$id)
    | none => `(term|_))
  return terms

def repeatedForall  [Monad m] [MonadQuotation m] (vars : Array (Ident × Option Name)) (body : TSyntax `term) : m (TSyntax `term) := do
  let binders ← createForallBinders vars
  if binders.size == 0 then return body
  else `(term|∀ $binders*, $body)

Lean.mkFreshFVarId in Lean.Expr

def ProcedureSpecification.actionDecl (proc : ProcedureSpecification) : Option ActionDeclaration :=
  match proc.kind with
  | .action decl => some decl
  | .procedure _ => none

invariant block_found N1 B1 TI1  ∨ ¬ honest N1  ∨ ¬ broadcastable N1 B1 TI1
invariant leader N1 TI1  ∨ ¬ honest N1  ∨ ¬ broadcastable N1 B1 TI1
invariant leader N1 TI1  ∨ ¬ block_found N1 B1 TI1
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ honest N1  ∨ ¬ broadcastable N1 B1 TI2  ∨ ¬ block_found N1 B1 TI1)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ honest N1  ∨ ¬ broadcastable N1 B1 TI1  ∨ ¬ block_found N1 B1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ honest N1  ∨ ¬ broadcastable N1 B1 TI1  ∨ ¬ broadcastable N1 B1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ leader N1 TI2  ∨ ¬ honest N1  ∨ ¬ broadcastable N1 B1 TI1)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ leader N1 TI1  ∨ ¬ block_found N1 B1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ leader N1 TI2  ∨ ¬ block_found N1 B1 TI1)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ block_found N1 B1 TI1  ∨ ¬ block_found N1 B1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ leader N1 TI1  ∨ ¬ honest N1  ∨ ¬ broadcastable N1 B1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ leader N1 TI1  ∨ ¬ leader N1 TI2)
invariant (tot.le TI1 TI2  ∧ TI1 ≠ TI2) -> (¬ transaction_time TR1 TI1  ∨ ¬ transaction_time TR1 TI2)

safety [deliver_integrity]
  ∀ (src dst : address) (r : round) (v : value),
     ¬ is_byz src ∧ ¬ is_byz dst ∧ delivered dst src r v → (sent src r ∧ initial_value src r v)

structure ConstantDecl where
  name : SortName
  sort : FirstOrderSort
deriving BEq, Hashable, Ord

#guard_msgs in

def defineProcedureFromGenerator (proc : TSyntax `ident) (br : Option (TSyntax `Lean.explicitBinders)) (genIName : Name) : CommandElabM Unit := do
    declareProcedure .none proc.getId
    registerProcedureBinders proc.getId br
    Command.runTermElabM fun _ => do
      let baseName := (← getCurrNamespace) ++ proc.getId
      let _ ← genProcedure baseName genIName
where

Lean.Meta.MetaM in Lean.Meta.Basic

macro "exists?" br:explicitBinders ? "," t:term : term =>
  match br with
  | some br => `(exists $br, $t)
  | none => `($t)

invariant [master_complete_zero_or_holds] (R2 = master_complete ∨ (configure_round_msg R3 C ∧ complete_of C = R2)) ∧ ¬ tot.le R2 R1 → complete_msg R2

def _root_.Lean.EnvExtension.modify (ext : EnvExtension σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

safety [single_leader] leader L → le N L
invariant pending S D ∧ btw S N D → le N S
invariant pending L L → le N L

Lean.Language.SnapshotTree in Lean.Language.Basic

Lean.Meta.mkFreshExprMVar in Lean.Meta.Basic

Lean.DefinitionSafety.safe in Lean.Declaration

elab "prove_inv_inductive" proof:term : command => do
  liftCoreM errorIfStateNotDefined
  elabCommand $ <- Command.runTermElabM fun _ => do
    let stateTp <- getStateTpStx
    let invInductive := mkIdent ``RelationalTransitionSystem.invInductive
    `(theorem $(mkIdent `inv_inductive) : $invInductive (σ := $stateTp) :=
      by admit /- proof elided -/
         )

def satGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}the goal is false"

instance : GenBigStep σ PUnit (Wp.assume asm) (BigStep.assume asm) where
  lawful := inferInstance
  equiv := by admit /- proof elided -/

Lean.Elab.Attribute in Lean.Elab.Attributes

safety [paid] paid N K V D → proposed N K V D

instance : FromJson SmtResult where
  fromJson? s := match s with
    | Json.arr #["sat"] => .ok (.Sat none)
    | Json.arr #["unsat"] => .ok .Unsat
    | Json.arr #["unknown"] => .ok (.Unknown none)
    | Json.arr #["failure"] => .ok (.Failure none)
    | Json.arr #["sat", m] => fromJsonStr? m >>= fun m => .ok (.Sat (some m))
    | Json.arr #["unknown", r] => fromJsonStr? r >>= fun r => .ok (.Unknown (some r))
    | Json.arr #["failure", r] => fromJsonStr? r >>= fun r => .ok (.Failure (some r))
    | _ => .error s!"invalid SMT result: {s}"
    where
      fromJsonStr? : Json → Except String String
        | Json.str s => .ok s
        | s => .error s!"expected string, got {s}"

zero : t
  zero_le (x : t) : le zero x

action retval = {
  return 42
}

Bool in Init.Prelude

def emoji (res : SmtResult) : String :=
  match res with
  | .Unsat => "✅"
  | .Sat _ => "❌"
  | .Unknown _ => s!"❓"
  | .Failure reason => s!"💥 {reason}"

#gen_spec

if v : (∀ (N : node), member_maj N q → vote_rnd1 N p v) then
    vote_rnd2 n p v := True
  else
    vote_rnd2 n p vquestion := True
}

Lean.Name in Init.Prelude

#gen_state

}
</all_available_defs>

<all_available_lemmas>
theorem lift_transition {σ σ'} [IsSubStateOf σ σ'] (m : Mode) (tr : TwoState σ) :
  (@Wp.lift _  m σ σ' _ (tr.toWp m)).toTwoState =
  fun st st' =>
    tr (getFrom st) (getFrom st') ∧
    st' = (setIn (@getFrom σ σ' _ st') st)

theorem agreement_bc.is_inv : RelationalTransitionSystem.isInvariant
  (σ := State' node set_majority set_f_plus_1 proposal_value) agreement_bc

theorem bind_terminates m (act : Wp m σ ρ) (act' : ρ -> Wp m σ ρ') s [LawfulAction act] :
  pre s ->
  act.alwaysSuccessfullyTerminates pre →
  (act.bind act').alwaysSuccessfullyTerminates pre ->
  act.toBigStep s r' s' ->
  (act' r').alwaysSuccessfullyTerminates (· = s')

theorem TwoState_sound'_ret_unit' [LawfulAction act] {st : σ} (ens : RProp σ PUnit) :
  act st ens → (∀ st', act.toTwoState st st' → ens () st')

theorem not_forall' {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x

theorem reachable_inclusion (sys sys' : RelationalTransitionSystem σ)
  (hinit_implies : ∀ (st : σ), sys.init st → sys'.init st)
  (hnext_implies : ∀ (st st' : σ), sys.next st st' → sys'.next st st') :
  ∀ (st : σ), reachable (sys := sys) st → reachable (sys := sys') st

theorem quorum_after_proj (Q S : Set Node) : quorum (inst := inst) Q → quorum (inst := inst.project S) Q

theorem ite_then_forall_push_out [IsHigherOrder α] [ne : Nonempty α] (c r : Prop) (q : α → Prop) : (if c then ∀ t, q t else r) = (∀ t, if c then q t else r)
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Set.Basic

namespace FBA

def project {α β : Type} (slices : β → Set (Set α)) (S : Set α) : β → Set (Set α) :=
  fun n => { Sl ∩ S | Sl ∈ slices n }

class System (Node : Type) where
   
  W : Set Node
  slices : Node → Set (Set Node)
   
  slices_ne : ∀ p ∈ W, slices p ≠ ∅

variable {Node : Type}

def System.project (sys : System Node) (I : Set Node) : System Node :=
  { W := sys.W
    slices := FBA.project sys.slices I
    slices_ne := by admit /- proof elided -/

variable [inst : System Node]

open System

def quorum (Q : Set Node) : Prop := ∀ p ∈ Q ∩ W, ∃ Sl ∈ slices p, Sl ⊆ Q

def blocks_slices (S : Set Node) (p : Node) : Prop :=
  ∀ Sl ∈ slices p, Sl ∩ S ≠ ∅

structure intertwined (S : Set Node) where
  well_behaved : S ⊆ W
   
  q_inter : (∀ Q Q',
    quorum (inst := inst.project S) Q →
    quorum (inst := inst.project S) Q' →
    Q ∩ S ≠ ∅ → Q' ∩ S ≠ ∅ → Q ∩ Q' ∩ S ≠ ∅)

structure intact (I : Set Node) extends intertwined I where
   
  q_avail : quorum (inst := inst) I
</local_ctx>

<target_theorem>
theorem slice_blocks_ne : ∀ n S I, intact (inst := inst) I → n ∈ I → blocks_slices S n →
    S ∩ I ≠ ∅ :=
</target_theorem>

