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>
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

Lean.Core.Context in Lean.CoreM

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

open_isolate wrapper5 with protocol

def cvc5.version := "1.3.1"

open_isolate wrapper3 with wrapper2

instance : ToString ConstantDecl where
  toString c := s!"constant {c.name} : {c.sort}"

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

MonadExceptOf in Init.Prelude

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

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

def uvPath := buildDir / "uv"

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]

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

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

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

ST in Init.System.ST

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

ghost relation good (p : phase) :=
  started p ∧
  (∀ P0, lt P0 p → started P0) ∧
  (∀ P0 V0, lt P0 p ∧ started P0 ∧
    ((∃ N, decision_bc N P0 V0) ∨ state_value_locked P0 V0) →
      state_value_locked p V0)

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

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

def BigStep.fresh (τ : Type) : BigStep σ τ := fun s _r s' => s' = s

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 := *;
}

System.mkFilePath in Init.System.FilePath

STWorld in Init.System.ST

Lean.getConstInfo in Lean.MonadEnv

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₂)

Auto.Parser.SMTSexp.LexVal in Auto.Parser.SMTSexp

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

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

action retval = {
  return 42
}

abbrev Context := Lean.Elab.Tactic.Context

abbrev InputOutputPair := (Array FirstOrderValue) × FirstOrderValue

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

@[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)

Array.filter in Init.Data.Array.Basic

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

@[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)

Auto.runAuto in Auto.Tactic

def registerModuleSpecification : AttrM Unit := do
  let lctx := <- localSpecCtx.get
  let n := lctx.spec.name
  if (← globalSpecCtx.get).contains n then
    throwError "Specification {n} has already been declared"
  trace[veil] "Globally declaring specification {n}"
  globalSpecCtx.add (n, lctx)

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

Lean.Core.transform in Lean.Meta.Transform

| .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)

#gen_spec

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
}

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

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)"
}

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

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 FirstOrderSort.name : FirstOrderSort → SortName
  | FirstOrderSort.Interpreted s => s.name
  | FirstOrderSort.Uninterpreted s => s.name

Lean.trace in Lean.Util.Trace

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}"

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

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

Lake.LogIO in Lake.Util.Log

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

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

Lean.checkCache in Lean.Util.MonadCache

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 => ""

action recv (sender n next : node) = {
  require ∀ Z, n ≠ next ∧ ((Z ≠ n ∧ Z ≠ next) → btw n next Z)
  require pending sender n
  pending sender n := *
  if (sender = n) then
    leader n := True
  else
    if (le n sender) then
      pending sender next := True
}

invariant True

deriving instance Repr for LexVal
deriving instance Repr for Auto.Parser.SMTSexp.Sexp

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

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 := "")

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}"

#guard_msgs in

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 ...`"

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

structure SmtState where
  binderIds : Std.HashMap Name UInt64 := {}
deriving Inhabited

action foo2 (k : Nat) = {
  let mut y := 0
  y := k
  if y > 0 then
    return True
  else return False
}

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

Lean.Parser.Tactic.simpLemma in Init.Tactics

#gen_spec

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

invariant [one_b_max_vote_properties3] (one_b_max_vote N R RMAX V ∧ RMAX ≠ none ∧ ¬ tot.le R ROTHER ∧ ¬ tot.le ROTHER RMAX) → ¬ vote N ROTHER VOTHER

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

invariant [manual_13] a Y ∨ in_s2 X ∨ ¬ a X ∨ ¬ s1 X Y

#time #check_invariants

action phase_rnd1 = {
  let n : node ← fresh
  let p : phase ← fresh
  let q : set_majority ← fresh
  assume in_phase n p
  assume ¬ ∃ V : state_value, vote_rnd2 n p V
  assume ∀ (N : node), member_maj N q → ∃ V, vote_rnd1 N p V

crit N := False
}

#gen_spec

action foo (x : node) = {
  pure ()
}

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 -/
          )

def defineInitialActionFromGenerators (act : TSyntax `ident) (genIName genEName : Name) : CommandElabM Unit := do
    Command.runTermElabM fun _ => do
      
      let baseName := (← getCurrNamespace) ++ act.getId
      let _actIName ← genInitialAction baseName .internal genIName
      let _actEName ← genInitialAction baseName .external genEName
where

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

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

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

def isElaboratedCorrectly (n : Name) : MetaM Bool :=
  return !Expr.hasSyntheticSorry (← Meta.reduceAll $ ← Meta.mkConstWithFreshMVarLevels n)

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

elab (name := VeilDo) "do'" mode:term "in" stx:doSeq : term => do
   
  let mut preludeAssn : Array doSeqItem := #[]
  let doS <- match stx with
  | `(doSeq| $doE*) => pure doE
  | `(doSeq| { $doE* }) => pure doE
  | _ => throwErrorAt stx "unexpected syntax of Veil `do`-notation sequence {stx}"
  let (doS, vars) <- (expandDoSeqVeil (<- `(doSeq| $doS*))).run #[]
  \n→\n{doS}"
  elabTerm (<- `(term| ((do $doS*) : Wp $mode [State] _))) none

Auto.Parser.SMTSexp.Sexp in Auto.Parser.SMTSexp

instance : Inhabited StateAssertionKind where
  default := StateAssertionKind.invariant

def prepareLeanAutoQuery (mv : MVarId) (hints : TSyntax `Auto.hints) : TacticM String := do
  withTraceNode `veil.smt.perf.translate (fun _ => return "prepareAutoQuery") do
  \n" (commands.toList.map toString)
    return queryStr

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

abbrev BigStep := σ -> ρ -> σ -> Prop

def constructCommands (thms : Array (TSyntax `command)) : CoreM (TSyntax `commands) := `(commands| $[$thms]*)

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

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

Monad in Init.Prelude

Lean.ConstantInfo in Lean.Declaration

open_isolate protocol

invariant [echoed_requires_initial]
  ∀ (n originator : address) (r : round) (v : value),
    ¬ is_byz n → (echoed n originator r v → initial_msg originator n r v)

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

invariant [manual_3] ¬ (S ≠ T ∧ msg Y S ∧ msg Y T ∧ ¬ le T (epoch Y) ∧ ¬ le S (epoch Y))

IO.monoMsNow in Init.System.IO

def toActionKind (stx : TSyntax `actionKind) : ActionKind :=
  match stx with
  | `(actionKind|input) => ActionKind.input
  | `(actionKind|internal) => ActionKind.internal
  | `(actionKind|output) => ActionKind.output
  | _ => unreachable!

Exists in Init.Core

#guard_msgs(drop info) in

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

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

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

action bar =
  requires True
  ensures True
{
  require n = n
}

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

Set in Mathlib.Data.Set.Defs

ghost relation strong_state_value_locked (p : phase) (v : state_value) :=
  ∃ N : node, vote_rnd1 N p v ∧ (∀ N Valt, vote_rnd1 N p Valt → Valt = v)

#time #check_invariants

Id.run in Init.Control.Id

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}"

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

#gen_spec

def assembleLabelType (name : Name) : CommandElabM Unit := do
  let labelTypeName := mkIdent `Label
  elabCommand $ ← Command.runTermElabM fun _ => do
    let ctors ← (<- localSpecCtx.get).spec.actions.mapM (fun s => do
      let .some decl := s.actionDecl | throwError "[assembleLabelType] {s} is not an action"
      match decl.ctor with
      | none => throwError "DSL: missing label constructor for action {s.name}"
      | some ctor => pure ctor)
    trace[veil.info] "storing constructors for {name}"
    `(inductive $labelTypeName where $[$ctors]*)
  trace[veil.info] "Label {labelTypeName} type is defined"

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

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

action f (n : Nat)  = {
  pure n
}

invariant [curr_priv1] ((n_have_privilege N) ∧ N ≠ M) → (n_token_seq M) < (n_token_seq N)

invariant ∀ N B V, well_behaved N ∧ accepted_committed N B V → confirmed_prepared N B V

private def solverStr (solver : Option SmtSolver := none) : String :=
  match solver with
  | some solver => s!"{solver}: "
  | none => ""

num in Test.Playground.WHNFExamples

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

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

Lake.inputTextFile in Lake.Build.Common

liftM in Init.Prelude

Lean.MVarId in Lean.Expr

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

Lean.withTraceNode in Lean.Util.Trace

reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

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
}

Lean.explicitBinders in Init.NotationExtra

action fresh_with_lhs_type_ok = {
  let b : block ← (fresh)
  let q : queue ← fresh
}

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

outParam in Init.Prelude

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"

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

| .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)

Auto.Reif.ReifM in Auto.Translation.ReifM

#gen_spec

}

def repeatedOr  [Monad m] [MonadQuotation m] (operands : Array (TSyntax `term)) : m (TSyntax `term) := do
  repeatedOp `Or (default := ← `(term|$(mkIdent `False))) operands

invariant [manual_14] p A B → a A

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

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}`!")

def declareSpecName (n : Name) : CommandElabM Unit := do
  let ctx ← localSpecCtx.get
  let existingName := ctx.spec.name
  if existingName != Name.anonymous && existingName != n then
    throwError s!"Specification already named ({existingName}); cannot rename to {n}!"
  trace[veil.info] "declaring module {n}"
  localSpecCtx.modify (fun s => { s with spec.name := n })

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

next (x y : t) : Prop
  next_def (x y : t) : next x y ↔ (lt x y ∧ ∀ z, lt x z → le y z)

def extractStructure (model : Sexpr) : MetaM FirstOrderStructure := do
  let mut struct : FirstOrderStructure := default
  let instructions ← extractInstructions model
  trace[veil.smt.debug] "instructions: {instructions}"
  for inst in instructions do
    struct := (← parseInstruction inst struct)
  return struct

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!"

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

#gen_spec

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

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

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}

action return_two (n : seq_t) = {
  let m ← fresh seq_t
  return (n, m)
}

action set_X = {
  X := True
}

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

action phase_rnd2 = {
  let n : node ← fresh
  let p : phase ← fresh
  let psucc : phase ← fresh
  let q : set_majority ← fresh
  assume in_phase n p
  assume ∃ V : state_value, vote_rnd2 n p V
  assume ∀ (N : node), member_maj N q → ∃ V, vote_rnd2 N p V
  assume next p psucc

def FirstOrderStructure.isInterpretedByFiniteEnumeration (s : FirstOrderStructure) (decl : Declaration) : Bool :=
  match s.interp.get? decl with
  | some (Interpretation.Enumeration _) => true
  | _ => false

class TotalOrderWithNone (t : Type) where
  
  le (x y : t) : Prop
  none : t
  
  le_refl       (x : t) : le x x
  le_trans  (x y z : t) : le x y → le y z → le x z
  le_antisymm (x y : t) : le x y → le y x → x = y
  le_total    (x y : t) : le x y ∨ le y x

Lean.Expr.forallE in Lean.Expr

#time #check_invariants

def liftProcedureGenerators (forAct : TSyntax `ident) (withBinders : Option (TSyntax `Lean.explicitBinders)) (stateTpT : TSyntax `term) (fromBaseGenerator : Name) (instatiatedWithArgs : Array Term) (isInitialAction : Bool := false) : CommandElabM (Name × Name) := do
  Command.runTermElabM fun vs => do
    let baseName := (← getCurrNamespace) ++ forAct.getId
    let (genIName, _genExpI) ← liftGenerator baseName vs withBinders fromBaseGenerator instatiatedWithArgs .internal isInitialAction
    let (genEName, _genExpE) ← liftGenerator baseName vs withBinders fromBaseGenerator instatiatedWithArgs .external isInitialAction
    return (genIName, genEName)
where
  liftGenerator (liftedActName : Name) (actVs : Array Expr) (actBinders :  Option (TSyntax `Lean.explicitBinders)) (baseNameToLift : Name) (depArgs : Array Term) (mode : Mode) (isInitialAction : Bool)  := do
    let baseGenName := toGenName baseNameToLift mode
    let (actParams, actArgs) ← match actBinders with
    | some br => pure (← toFunBinderArray br, ← explicitBindersIdents br)
    | none => pure (#[], #[])
    let infer ← `(term|_)
    let (srcWpType, typeClassInst, retType) := (infer, infer, infer)
    
    let dstWpType ← `(term|Wp $(← mode.stx) ($stateTpT))
    let liftedGenStx ← `(fun $actParams* => @monadLift $srcWpType $dstWpType $typeClassInst $retType <| @$(mkIdent baseGenName) $depArgs* $actArgs*)
    let liftedGenName := toGenName liftedActName mode
    trace[veil.info] "{liftedGenName} := {liftedGenStx}"
    let genExp <- withDeclName liftedGenName do elabTermAndSynthesize liftedGenStx .none
    let ⟨genExp, _, _⟩ <- simpWp genExp
    let genExp <- instantiateMVars <| <- mkLambdaFVarsImplicit actVs genExp
    let initAttr := if isInitialAction then #[{name := `initSimp}] else #[]
    simpleAddDefn liftedGenName genExp (attr := #[{name := `generatorSimp}, {name := `actSimp}, {name := `reducible}] ++ initAttr)
    return (liftedGenName, genExp)

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

inductive Interpretation
  | Enumeration (iopairs : Array InputOutputPair)
  | Symbolic    (expr : String)
deriving Ord, Inhabited

#guard_msgs(drop warning) in
#gen_spec

Repr in Init.Data.Repr

invariant True

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

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)

relation t_for : seq_t → node → Prop
function t_LN : seq_t → node → seq_t
relation t_q : seq_t → node → Prop

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

@[actSimp] def Wp.modifyGet (act : σ -> ρ × σ) : Wp m σ ρ := fun s post => let (ret, s') := act s ; post ret s'

Array.mapM in Init.Data.Array.Basic

trans : ∀ w x y z, btw w x y → btw w y z → btw w x z
  acyclic : ∀ w x y, btw w x y → ¬ btw w y x
  total : ∀ w x y, btw w x y ∨ btw w y x ∨ w = x ∨ x = y
  cyclic_perm : ∀ x y z, btw x y z ∧ x ≠ z → btw y z x

def defineDepsProcedures : CommandElabM Unit := do
  let stateTpT ← liftCoreM $ getStateTpStx
  for (modAlias, dependency) in (<- localSpecCtx.get).spec.dependencies do
    
    let depArgs := dependency.arguments
    let globalCtx <- globalSpecCtx.get
    let some depCtx := globalCtx[dependency.name]? | throwError "Module {dependency.name} is not declared"
    
    let initName := dependency.name ++ `initializer
    let liftedName := mkIdent <| modAlias ++ (stripFirstComponent initName)
    trace[veil.info] "lifting {initName} from module {dependency.name} to module {← specName} as {liftedName}"
    let (genIName, genEName) ← liftProcedureGenerators liftedName .none stateTpT initName depArgs (isInitialAction := true)
    defineInitialActionFromGenerators liftedName genIName genEName
    
    for procToLift in depCtx.spec.procedures do
      let procBaseName := dependency.name ++ procToLift.name
      
      
      
      
      let actBaseName := if procToLift.hasSpec then toSpecName procBaseName else procBaseName
      let liftedName := mkIdent <| modAlias ++ (stripFirstComponent actBaseName)
      
      
      
      
      
      
      let liftedBinders ← do match procToLift.br with
        | some br => pure (Option.some (← toBindersWithMappedTypes br (← dependency.typeMapping)))
        | none => pure .none
      trace[veil.info] "lifting {procToLift.kindString} {actBaseName} from module {dependency.name} to module {← specName} as {liftedName}"
      let (genIName, genEName) ← liftProcedureGenerators liftedName liftedBinders stateTpT actBaseName depArgs
      match procToLift.kind with
      | .action decl =>
        let actionKind ← Veil.ActionKind.stx decl.kind
        defineActionFromGenerators actionKind liftedName liftedBinders genIName genEName
      | .procedure _ => defineProcedureFromGenerator liftedName liftedBinders genIName

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

unsat trace {
  enter
  enter
  any 2 actions
} by bmc

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

@[actSimp] def Wp.pure (r : ρ) : Wp m σ ρ := fun s post => post r s

Lean.StructureInfo in Lean.Structure

action empty = { pure () }

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
}

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

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

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

#guard_msgs in

List.range in Init.Data.List.Basic

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

Hashable in Init.Prelude

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

Lean.mkTheoremValEx in Lean.Declaration

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

register_simp_attr quantifierSimp

Inhabited in Init.Prelude

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

invariant [indv_true] indv

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"

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

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

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

#gen_spec

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

Std.HashSet in Std.Data.HashSet.Basic

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)

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

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

Lean.logInfo in Lean.Log

def defineProcedureGenerators (act : TSyntax `ident) (br : Option (TSyntax `Lean.explicitBinders)) (l : doSeq) : CommandElabM (Name × Name) := do
  Command.runTermElabM fun vs => do
    let funBinders ← match br with
    | some br => toFunBinderArray br
    | none => pure #[]
    let baseName := (← getCurrNamespace) ++ act.getId
    let (genIName, _genExpI) ← genGenerator vs funBinders baseName .internal l
    let (genEName, _genExpE) ← genGenerator vs funBinders baseName .external l
    return (genIName, genEName)
where

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

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

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

simproc HO_forall_push_left (∀_ _, _) := HO_forall_push_left_impl

macro "forall?" br:bracketedBinder* "," t:term : term =>
  if br.size > 0 then
    `(∀ $br*, $t)
  else
    `($t)

args in Auto.Parser.TPTP

L in Archive.Hairer

invariant [none_property2] ¬vote N R none

structure FunctionDecl where
  name : SortName
  domain : Array FirstOrderSort
  range : FirstOrderSort
deriving BEq, Hashable, Ord

action fail(n: node) = {
  require alive n;
  alive n := False;
  abort_flag := True
}

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

def intSortI : InterpretedSort := { name := `Int }

readThe in Init.Prelude

Smt.Tactic.elabHints in Smt.Tactic.Smt

def assembleNext : CommandElabM Unit := do
  let vd ← getActionParameters
  elabCommand $ ← Command.runTermElabM fun vs => do
    let stateTp ← getStateTpStx
    let sectionArgs ← getSectionArgumentsStx vs
    let (st, st') := (mkIdent `st, mkIdent `st')
    let trs ← (<- localSpecCtx.get).spec.actions.mapM (fun s => do
      let nm := mkIdent $ toTrName s.name
      `(@$nm $sectionArgs* $st $st'))
    
    let next ← if trs.isEmpty then `(fun ($st $st' : $stateTp) => $st = $st') else
              `(fun ($st $st' : $stateTp) => $(← repeatedOr trs))
    trace[veil.debug] "[assembleActions] {next}"
    `(@[actSimp] def $(mkIdent $ `Next) $[$vd]* := $next)
  trace[veil.info] "Next transition assembled"

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

#time #check_invariants

def getInitCheckResultMessages' [Monad m] [MonadOptions m]  (res: List (Name × SmtResult × Option TimeInMs)) : m (Array String) := do
  let mut msgs := #[]
  if !res.isEmpty then
    msgs := msgs.push "Initialization must establish the invariant:"
    for (invName, (r, time)) in res do
      msgs := msgs.push s!"  {getBaseNameForDisplay invName} ... {emoji r}{← getTimeForDisplay time}"
  pure msgs

#guard_msgs in

invariant ∀ N B V1 V2, well_behaved N ∧ accepted_prepared N B V1 ∧ accepted_prepared N B V2 → V1 = V2

invariant [decision_full_noval_inv] decision_full_noval N P → decision_bc N P v0

Lean.Json in Lean.Data.Json.Basic

Lean.mkIdent in Init.Meta.Defs

def registerProcedureSyntax [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] (nm : Name) (lang : TSyntax `Lean.Parser.Term.doSeq) : m Unit := do
  assertProcedureDeclared nm "registerProcedureSyntax"
  localSpecCtx.modify fun s =>
    { s with spec.procedures := s.spec.procedures.map fun t =>
      if t.name == nm then
        { t with lang := lang }
      else t }

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

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

@[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

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

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

Lean.TSyntax in Init.Prelude

open_isolate wrapper2 with wrapper1

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

#gen_spec

def simpleAddThm (n : Name) (tp : Expr) (tac : TermElabM (TSyntax `Lean.Parser.Tactic.tacticSeq))
  (attr : Array Attribute := #[]) : TermElabM Unit := do
  addDecl <|
    Declaration.thmDecl <|
      mkTheoremValEx n [] tp (<- elabTermAndSynthesize (<- `(by admit /- proof elided -/
      )) tp) []
  enableRealizationsForConst n
  applyAttributes n attr

invariant coin P V →
  ∃ Q : set_majority, ∀ N : node, member_maj N Q → vote_rnd2 N P vquestion

abbrev ExplicitInterpretation := Std.HashMap Declaration Interpretation

def StateComponent.getSimpleBinder (sc : StateComponent) : CoreM (TSyntax ``Command.structSimpleBinder) := do
  match sc.type with
  | .simple t => return t
  | .complex b d => return ← complexBinderToSimpleBinder (mkIdent sc.name) b d

expr in Smt.Data.Sexp

def Array.funcArgsString (vals : Array FirstOrderValue) : String :=
  "(" ++ (String.intercalate ", " (vals.map toString).toList) ++ ")"

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 -/

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

instance [inst : GenBigStep σ ρ act actTr] : LawfulAction act := inst.lawful

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 toInstName (n : Name) (mode : Mode) : Name :=
  n ++ (match mode with
  | Mode.internal => `inst
  | Mode.external => `instExt)

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

#gen_spec

Lean.Elab.Tactic.getUnsolvedGoals in Lean.Elab.Tactic.Basic

abbrev CheckTheoremResultStringMarker := "[VEIL_CHECK_RESULT]\n"

invariant [manual_6] p X Y ∧ p X Z → Y = Z

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

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

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

if v : (v ≠ vquestion ∧
      (∃ N0 Q, member_fp1 N0 Q ∧ (∀ N, member_fp1 N Q → member_maj N q ∧ vote_rnd2 N p v)))
  then
    decision_bc n p v := True
    vote_rnd1 n psucc v := True
    in_phase n psucc := True
    in_phase n p := False
  else
    if v : (v ≠ vquestion ∧ (∃ N, member_maj N q ∧ vote_rnd2 N p v)) then
      vote_rnd1 n psucc v := True
      in_phase n psucc := True
      in_phase n p := False
    else
      if v : (v ≠ vquestion ∧ coin p v) then
        vote_rnd1 n psucc v := True
        in_phase n psucc := True
        in_phase n p := False
      else
        let v : state_value ← fresh
        assume v ≠ vquestion
        coin p v := True
        vote_rnd1 n psucc v := True
        in_phase n psucc := True
        in_phase n p := False
}

def mkOrN : List Expr → Expr
  | [] => mkConst ``True
  | [p] => p
  | p :: ps => mkOr p (mkOrN ps)

macro "unfold_wp" : conv =>
  `(conv| unfold
    
    Wp.pure
    Wp.bind
    Wp.assume
    Wp.assert
    Wp.require
    Wp.fresh
    Wp.get
    
    set
    modify
    modifyGet
    get
    instMonadStateOfMonadStateOf
    getThe
    MonadStateOf.modifyGet
    MonadStateOf.get
    MonadStateOf.set
    instMonadStateOfWp
    
    Wp.spec
    
    Wp.toWlp
    Wp.toBigStep
    Wp.toTwoState
    BigStep.toWp
    Function.toWp
    
    monadLift
    getFrom
    setIn
    instMonadLiftTOfMonadLift
    MonadLift.monadLift
    instMonadLiftWpOfIsSubStateOf
    instMonadLiftT)

def ProcedureSpecification.name (a : ProcedureSpecification) : Name :=
  match a.kind with
  | .action decl => decl.name
  | .procedure decl => decl.name

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

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

def getStateName : AttrM Name := getPrefixedName `State

#guard_msgs in

Lean.binderIdent in Init.Notation

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))

#gen_state

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

Lean.mkAppN in Lean.Expr

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

simproc HO_exists_push_left (∃ _ _, _) := HO_exists_push_left_impl

#guard_msgs in

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

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 -/
         )

Lean.Syntax.node in Init.Prelude

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

Lean.SimpleScopedEnvExtension in Lean.ScopedEnvExtension

LE in Init.Prelude

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}"

#guard_msgs in

@[wpSimp] def modifyGetE : modifyGet = Wp.modifyGet (σ := σ) (ρ := ρ) (m := m) := rfl

Lean.Name in Init.Prelude

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

let conjunctionThmName := moduleName ++ `inv_split_base
  Command.liftTermElabM do
    let thmName1 := ``RelationalTransitionSystem.invariant_merge
    let thmName2 := ``RelationalTransitionSystem.invInductive_to_isInvariant
    let thmName3 := `inv_inductive
    simpleAddThm conjunctionThmName thmType
      `(tacticSeq|
        intros ; repeat rw [@$(mkIdent thmName1):ident]
        apply $(mkIdent thmName2)
        next => intro _ _ ; simp [invSimp]
        next => apply $(mkIdent thmName3))

StateT in Init.Control.State

}
</all_available_defs>

<all_available_lemmas>
theorem lift_transition_big_step' {σ σ'} [IsSubStateOf σ σ'] (m : Mode) (r : Wp m σ ρ) [LawfulAction r] (st : σ') :
  r.alwaysSuccessfullyTerminates (· = getFrom st) →
  (@Wp.lift _  m σ σ' _ r).toBigStep st =
  fun r' st' =>
    r.toBigStep (getFrom st) r' (getFrom st') ∧
    st' = (setIn (@getFrom σ σ' _ st') st)

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

theorem foo : ∀ (p q : Prop), p → (p → q) → q

theorem intertwined_node_is_well_behaved : ∀ n S, intertwined (inst := inst) S → n ∈ S → n ∈ W

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

<local_ctx>
import Veil.DSL.Base

namespace Veil

section Veil

open Classical

section Types

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

variable (m : Mode) (σ ρ : Type)

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

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

abbrev Wp (m : Mode) (σ ρ : Type) := σ -> RProp σ ρ -> Prop

abbrev Wlp (m : Mode) (σ ρ : Type) := σ -> RProp σ ρ -> Prop

abbrev BigStep := σ -> ρ -> σ -> Prop

end Types

section Theory

variable {σ ρ : Type}

@[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)

@[actSimp] def Wp.get : Wp m σ σ := fun s post => post s s

@[actSimp] def Wp.set (s' : σ) : Wp m σ Unit := fun _ post => post () s'

@[actSimp] def Wp.modifyGet (act : σ -> ρ × σ) : Wp m σ ρ := fun s post => let (ret, s') := act s ; post ret s'

class IsSubStateOf (σ : semiOutParam Type) (σ' : Type) where
   
  setIn : σ -> σ' -> σ'
   
  getFrom : σ' -> σ

  setIn_getFrom_idempotent : ∀ σ', setIn (getFrom σ') σ' = σ'
  getFrom_setIn_idempotent : ∀ σ σ', getFrom (setIn σ σ') = σ

@[actSimp] def Wp.lift {σ σ'} [IsSubStateOf σ σ'] (act : Wp m σ ρ) : Wp m σ' ρ :=
  fun s' post => act (getFrom s') (fun r s => post r (setIn s s'))

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

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

@[actSimp]
def Wp.toBigStep {σ} (wp : Wp m σ ρ) : BigStep σ ρ :=
  fun s r' s' =>
    wp.toWlp s (fun r₀ s₀ => r' = r₀ ∧ s' = s₀)

abbrev Wp.triple {σ ρ} (req : SProp σ) (act : Wp m σ ρ) (ens : RProp σ ρ) : Prop :=
  ∀ s, req s -> act s ens

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

abbrev BigStep.triple {σ } (req : SProp σ) (act : BigStep σ ρ) (ens : RProp σ ρ) : Prop :=
  ∀ s r' s', req s -> act s r' s' -> ens r' s'

class LawfulAction {σ ρ : Type} (act : Wp m σ ρ) where
  inter {τ : Type} [Inhabited τ] (post : τ -> RProp σ ρ) :
    ∀ s : σ, (∀ t : τ, act s (post t)) -> act s (∀ t, post t · ·)

  impl (post post' : RProp σ ρ) : ∀ s,
    (∀ r s, post r s -> post' r s) -> act s post -> act s post'

section TwoStateSoundness

end TwoStateSoundness

section BigStepSoundness

end BigStepSoundness

section LawfulActionInstances

instance pure_lawful : LawfulAction (Wp.pure (σ := σ) (m := m) r) where
  inter := by admit /- proof elided -/

instance bind_lawful (act : Wp m' σ ρ) (act' : ρ -> Wp m σ ρ') [LawfulAction act] [∀ r, LawfulAction (act' r)] : LawfulAction (Wp.bind (m := m) act act') where
  inter := by admit /- proof elided -/

instance (priority := low) internal_sound (act : Wp m σ ρ) [inst : LawfulAction (m := .internal) act] : LawfulAction (m := .external) act where
  inter := inst.inter
  impl := inst.impl

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

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

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

instance fresh_lawful : LawfulAction (Wp.fresh (m := m) (σ := σ) τ) where
  inter := by admit /- proof elided -/

instance spec_lawful : LawfulAction (Wp.spec (m := m) req ens) where
  inter := by admit /- proof elided -/

instance (r : σ -> σ -> Prop) : LawfulAction (r.toWp (m := m)) where
  inter := by admit /- proof elided -/

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

instance set_lawful (s : σ) : LawfulAction (Wp.set s (m := m)) where
  inter := by admit /- proof elided -/

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

instance if_lawful [Decidable c] [instT: LawfulAction t] [instS : LawfulAction e] : LawfulAction (ite c t e) where
  inter := by admit /- proof elided -/

instance lift_lawful (act : Wp m σ ρ) [IsSubStateOf σ σ'] [LawfulAction act] :
  LawfulAction (act.lift (σ' := σ')) where
  inter := by admit /- proof elided -/

end LawfulActionInstances

section GenBigStepInstances

class GenBigStep (σ ρ : Type) (wp : Wp .external σ ρ) (tr : outParam (BigStep σ ρ)) where
  lawful : LawfulAction wp
  equiv pre  :
    wp.alwaysSuccessfullyTerminates pre -> ∀ s, pre s -> tr s = wp.toBigStep s

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

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

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

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

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

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

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

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

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

instance [inst : GenBigStep σ ρ act actTr] : LawfulAction act := inst.lawful
</local_ctx>

<target_theorem>
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') :=
</target_theorem>

