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

Nat.lt in Init.Prelude

action join_round (n:node) (r:round) = {
    
    require r ≠ none;
    require one_a r;
    require ¬(∃ (r':round) (rMAX:round) (v:value), one_b_max_vote n r' rMAX v ∧ ¬ tot.le r' r);
    let maxr : round ← fresh
    let v : value ← fresh
      
    require ((maxr = none ∧ ∀ (mAXR:round) (v':value), ¬ (¬ tot.le r mAXR ∧ vote n mAXR v')) ∨
                    (maxr ≠ none ∧ ¬ tot.le r maxr ∧ vote n maxr v ∧
                    (∀ (mAXR:round) (v':value), (¬ tot.le r mAXR ∧ vote n mAXR v') -> tot.le mAXR maxr)
                   ));
    
    one_b_max_vote n r maxr v := True
}

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

action send_1a = {
  
  let r : round ← fresh
  require r ≠ none;
  one_a r := True
}

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

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]

instance : ToString Declaration where
  toString
    | Declaration.Constant c => toString c
    | Declaration.Relation r => toString r
    | Declaration.Function f => toString f

action empty = { pure () }

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

@[actSimp] def Wp.pure (r : ρ) : Wp m σ ρ := fun s post => 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 -/
          )

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

def uvPath := buildDir / "uv"

Prod.snd in Init.Prelude

Lake.logInfo in Lake.Util.Log

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

structure TheoremIdentifier where
  invName : Name
   
  actName : Option Name
  theoremName : Name
deriving Inhabited, BEq, ToJson, FromJson, Hashable

Auto.LamReif.printValuation in Auto.Translation.LamReif

Lean.Exception in Lean.Exception

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

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

unsat trace {
  enter
  enter
  any 2 actions
} by bmc

def cvc5.version := "1.3.1"

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 toSpecName (n : Name) : Name := n ++ `spec

Classical.choice in Init.Prelude

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

Lean.SimpleScopedEnvExtension in Lean.ScopedEnvExtension

IO.CancelToken in Init.System.IO

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

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 Wp.assume (asm : Prop) : Wp m σ PUnit := fun s post => asm → post () s

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₂

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

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

Lean.throwError in Lean.Exception

invariant [receive_self_msg_only_if_greatest] pending L L → le N L

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

Bool in Init.Prelude

Lean.TSyntaxArray.mk in Init.Prelude

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

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

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

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

System.FilePath.mk in Init.System.FilePath

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

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'

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

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

Lean.LocalContext in Lean.LocalContext

structure Vars where
  name : Ident
  type : Term

BaseIO in Init.System.IO

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)

invariant [manual_3] reach org

invariant [manual_3] ¬((¬(abort_flag) ∧ go_abort N))

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

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

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)

structure FirstOrderStructure where
  isMinimized : Bool

#guard_msgs(drop info) in

Lean.Parser.Term.implicitBinder in Lean.Parser.Term.Basic

#gen_spec

#guard_msgs in

Lean.Meta.Simp.defaultMaxSteps in Init.MetaTypes

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

invariant True

Ordering.gt in Init.Data.Ord.Basic

BaseIO.asTask in Init.System.IO

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

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

Lean.Parser.mkIdent in Lean.Parser.Types

relation a : node → Prop
relation s1 : node → node → Prop
relation in_s1 : node → Prop
relation s2 : node → node → Prop
relation in_s2 : node → Prop
relation p : node → node → Prop

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

liftM in Init.Prelude

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

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

invariant [all] state = a

abbrev Context := Lean.Elab.Tactic.Context

semiOutParam in Init.Prelude

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

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

Lean.Expr.sort in Lean.Expr

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
}

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

UInt32 in Init.Prelude

Auto.LamReif.reifMutInds in Auto.Translation.LamReif

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

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

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

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

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

Auto.LamReif.getLamEVarTy in Auto.Translation.LamReif

def whnfIsAppOf (typ : Expr) (n : Name) : MetaM Bool := do
  let norm ← Meta.whnf typ
  return norm.isAppOf n

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

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

isSome in Smt.Reconstruct.Certified.Utils

#time #check_invariants

action double_quant = {
  r N N := *
}

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

action decide_bc_decide_full_noval = {
  let n : node ← fresh
  let p : phase ← fresh
  assume decision_bc n p v0
  decision_full_noval n p := True
}

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

private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
    match (← isClassQuick? type) with
    | .none   => return none
    | .some c => return (some c)
    | .undef  => isClassExpensive? type

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

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

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

ST in Init.System.ST

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

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

instance : LE (Wp m σ ρ) where
  le := refines

Int in Init.Data.Int.Basic

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

Array.toList in Init.Prelude

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

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

crit N := False
}

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

MonadLift in Init.Prelude

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

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

num in Test.Playground.WHNFExamples

Lean.TSyntaxArray in Init.Prelude

def assembleInvariant : CommandElabM Unit := do
  let vd ← getAssertionParameters
  elabCommand $ <- Command.runTermElabM fun vs => do
    let stateTp <- getStateTpStx
    let allClauses := (<- localSpecCtx.get).spec.invariants
    let exprs := allClauses.toList.map (fun p => p.expr)
    let _ ← allClauses.mapM (fun t => do trace[veil.debug] s!"{t}")
    let invs ← if allClauses.isEmpty then `(fun _ => True) else PrettyPrinter.delab $ ← combineLemmas ``And exprs vs "invariants"
    `(@[invSimp, invSimpTopLevel] def $(mkIdent `Invariant) $[$vd]* : $stateTp -> Prop := $invs)
  trace[veil.info] "Invariant assembled"

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

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

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

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

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

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

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

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

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

Ordering.lt in Init.Data.Ord.Basic

action rcv_request (n : node) (m : node) (r : seq_t) = {
  require reqs n m r;
  n_RN n m := if seq.le r (n_RN n m) then n_RN n m else r;
  if (n_have_privilege n ∧ ¬ n_requesting n ∧ seq.next (t_LN (n_token_seq n) m) (n_RN n m)) then
    n_have_privilege n := False;
    let k : seq_t ← succ (n_token_seq n)
    t_for k m := True;
    t_LN k N := t_LN (n_token_seq n) N;
    t_q k N := t_q (n_token_seq n) N
}

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)

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

StateT in Init.Control.State

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

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

open_isolate wrapper3 with wrapper2

Lean.throwUnknownConstant in Lean.Exception

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

action retval = {
  return 42
}

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

Lean.Expr.forallE in Lean.Expr

abbrev Sexpr := Auto.Parser.SMTSexp.Sexp

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

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 Wp.alwaysSuccessfullyTerminates {σ } (req : SProp σ) (act : Wp m σ ρ)  : Prop :=
  ∀ s, req s -> act s (fun _ _ => True)

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

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}

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

#gen_spec

Lean.mkIdent in Init.Meta.Defs

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

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

| .app #[(.atom (.symb "relation")), (.atom (.symb relName)), (.app doms)] => do
    let relName := relName.toSanitizedName
    let doms ← findSortsArray doms struct
    let decl: RelationDecl := { name := relName, domain := doms }
    trace[veil.smt.debug] s!"{decl}"
    struct := { struct with signature := { struct.signature with relations := struct.signature.relations.push decl } }

def getStateDestructorPattern [Monad m] [MonadEnv m] [MonadQuotation m]: m (TSyntax `term) := do
  
  let fields ← (<- getFields).mapM (fun f => return ← `(term|$(mkIdent f)@_)) 
  `(term|⟨$fields:term,*⟩)

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

#gen_spec

Lemma.ofConst in Auto.Translation.Assumptions

Std.HashSet in Std.Data.HashSet.Basic

invariant [manual_2] s2 X Y → in_s2 X

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

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

le in Test.SmtTranslation.Names

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

Lean.AttrM in Lean.Attributes

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

Lean.isClass in Lean.Class

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

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

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

Lean.isReducible in Lean.ReducibilityAttrs

def getStateName : AttrM Name := getPrefixedName `State

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
}

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

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

expr in Smt.Data.Sexp

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

Lean.Syntax.ident in Init.Prelude

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.pp.motives.all in Lean.PrettyPrinter.Delaborator.Options

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

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

def defineTransition (actT : TSyntax `actionKind) (nm : TSyntax `ident) (br : Option (TSyntax `Lean.explicitBinders)) (tr : Term) : CommandElabM Unit := do
  let vd ← getImplicitProcedureParameters
  let baseName := (← getCurrNamespace) ++ nm.getId
  let (origName, trName) := (toOriginalIdent nm, toTrIdent nm)
  let (originalDef, trDef) ← Command.runTermElabM fun vs => do
    let stateTpT ← getStateTpStx
    let trType <- `($stateTpT -> $stateTpT -> Prop)
    let sectionArgs ← getSectionArgumentsStx vs
    let (univBinders, args) ← match br with
    | some br => pure (← toBracketedBinderArray br, ← explicitBindersIdents br)
    | none => pure (#[], #[])
    
    let originalDef ← `(@[actSimp] def $origName $[$vd]* $univBinders* : $trType := $tr)
    
    
    
    let trDef ← do
      let (st, st') := (mkIdent `st, mkIdent `st')
      let rhs ← match br with
      | some br => `(fun ($st $st' : $stateTpT) => ∃ $br, @$origName $sectionArgs* $args* $st $st')
      | none => `(fun ($st $st' : $stateTpT) => @$origName $sectionArgs* $args* $st $st')
      `(@[actSimp] def $trName $[$vd]* : $trType := $(← unfoldWp rhs))
    return (originalDef, trDef)
  trace[veil.info] "{originalDef}"
  elabCommand originalDef
  trace[veil.info] "{trDef}"
  elabCommand trDef
  let (genIName, genEName) ← Command.runTermElabM fun vs => do
    let (genIName, _genExpI) ← genGeneratorFromTransition vs origName baseName .internal
    let (genEName, _genExpE) ← genGeneratorFromTransition vs origName baseName .external
    return (genIName, genEName)
  
  defineActionFromGenerators actT nm br genIName genEName (generateTransition := false)
where
  genGeneratorFromTransition (vs : Array Expr) (origName : Ident) (baseName : Name) (mode : Mode) := do
    let genName := toGenName baseName mode
    let sectionArgs ← getSectionArgumentsStx vs
    let (funBinders, args) ← match br with
    | some br => pure (← toFunBinderArray br, ← explicitBindersIdents br)
    | none => pure (#[], #[])
    let term ← match mode with
    | Mode.internal => `((@$origName $sectionArgs* $args*).toWp .internal)
    | Mode.external => `((@$origName $sectionArgs* $args*).toWp .external)
    let genl ← `(fun $funBinders* => $term)
    let genExp <- withDeclName genName do elabTermAndSynthesize genl none
    let genExp <- instantiateMVars <| <- mkLambdaFVarsImplicit vs genExp
    simpleAddDefn genName genExp (attr := #[{name := `generatorSimp}, {name := `actSimp}, {name := `reducible}]) («type» := ← inferType genExp)
    return (genName, genExp)

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

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

register_simp_attr quantifierSimp

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)

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

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

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

PUnit in Init.Prelude

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

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

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

#guard_msgs in

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)

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 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 notify (x : node) (y : node) (z : node) = {
  require a x;
  require s1 x y;
  require a y;
  require ∀ X, p y z ∨ ¬ p y X;
  require ring.btw z x y;
  p y X := X = x
}

absurd in Init.Prelude

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

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)

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

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

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

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

Array in Init.Prelude

invariant [none_property2] ¬vote N R none

Lean.Meta.SplitIf.getSimpContext in Lean.Meta.Tactic.SplitIf

#time #check_invariants

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

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

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

Auto.LamReif.reifInhabitations in Auto.Translation.LamReif

node in Test.SmtTranslation.Inductive

structure InterpretedSort where
  name : SortName
  
deriving BEq, Hashable, Inhabited, Ord

#time #check_invariants

action succ (n : seq_t) = {
  let k : seq_t ← fresh
  assume seq.next n k;
  return k
}

DecidableEq in Init.Prelude

def mkSimpName (n : Ident) :=
     mkNode `Lean.Parser.Tactic.simpLemma #[Syntax.node default nullKind #[], Syntax.node default nullKind #[], Syntax.ident SourceInfo.none default n.getId []]

impl in Mathlib.Deprecated.MLList.BestFirst

#guard_msgs in

Char.val in Init.Prelude

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

parse in Auto.Parser.TPTP

macro "funcases" t:term : term => `(term| by admit /- proof elided -/
)

Lake.LogIO in Lake.Util.Log

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

invariant ∀ Q, coin P V → ∃ N : node, member_fp1 N Q ∧ vote_rnd2 N P vquestion
invariant decision_bc N P V → ¬ coin P V2

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

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

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

invariant (∃ N, intertwined N ∧ confirmed_committed N B V) →
  ∃ Q, is_quorum Q ∧ (∃ N, intertwined N ∧ member N Q) ∧ (∀ N, well_behaved N ∧ member N Q → accepted_committed N B V)
invariant (∃ N, intertwined N ∧ confirmed_prepared N B V) →
  ∃ Q, is_quorum Q ∧ (∃ N, intertwined N ∧ member N Q) ∧ (∀ N, well_behaved N ∧ member N Q → accepted_prepared N B V)

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

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)

invariant [indv_true] indv

def agreement_bc (s : State' node set_majority set_f_plus_1 proposal_value) : Prop :=
  ∀ N1 P1 V1 N2 P2 V2,
    s.decision_bc N1 P1 V1 →
    s.decision_bc N2 P2 V2 →
    V1 = V2

Lean.trace in Lean.Util.Trace

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

abbrev doSeq := TSyntax ``Term.doSeq

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

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

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

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

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 }

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

def closeCapitals (s : Term) : MacroM Term :=
  let caps := getCapitals s
  `(forall $[$caps]*, $s)

Lean.Meta.mkFreshExprMVar in Lean.Meta.Basic

abbrev CheckTheoremResultStringMarker := "[VEIL_CHECK_RESULT]\n"

def HO_exists_push_left_impl : Simp.Simproc := fun e => do
  let_expr Exists t eBody := e | return .continue
  
  let step : Simp.Step ← lambdaBoundedTelescope eBody (maxFVars := 1) (fun ks lBody => do
      let_expr Exists t' eBody' := lBody | return .continue
      
      
      
      if (← isHigherOrder t') && !(← isHigherOrder t) && !(dependsOn t' ks)  then
        let step : Simp.Step ← lambdaBoundedTelescope eBody' (maxFVars := 1) (fun ks' lBody' => do
          
          let innerExists := mkAppN e.getAppFn #[t, ← mkLambdaFVars ks lBody']
          let outerExists := mkAppN lBody.getAppFn #[t', ← mkLambdaFVars ks' innerExists]
          let body ← mkLambdaFVars (ks ++ ks') lBody'
          let proof ← mkAppOptM ``exists_comm_eq #[t, t', body]
          return .visit { expr := outerExists, proof? := proof })
        return step
      else
        return .continue
  )
  return step
where
  dependsOn (child : Expr) (deps : Array Expr) : Bool :=
    child.find? (fun e => deps.contains e) != none

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

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

invariant [inv] True

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

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

def mkSimpLemmas (simpIds : Array Ident) : Syntax.TSepArray `Lean.Parser.Tactic.simpLemma "," := namesToLemmas (simpIds.map mkSimpName)

def genStateExtInstances : CommandElabM Unit := do
  let currName <- getCurrNamespace
  let vd := (<- getScope).varDecls
  let insts <- Command.runTermElabM fun vs => do
    let mut insts := #[]
    for (modAlias, dep) in (<- localSpecCtx.get).spec.dependencies do
      let ts ← dep.stateArguments
      let currTs <- getStateArgumentsStx vd vs
      let alia := mkIdent modAlias
      let stateExtTypeclass := mkIdent ``IsSubStateOf
      let inst <-
        `(@[actSimp]

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

Lean.StructureInfo in Lean.Structure

Lake.inputTextFile in Lake.Build.Common

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
}

Lean.Name.anonymous in Init.Prelude

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

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

#guard_msgs(drop warning) in
#gen_spec

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

greater_than_third (s : nset) : Prop
   
  supermajority (s : nset) : Prop

#guard_msgs in

instance : Inhabited StateAssertionKind where
  default := StateAssertionKind.invariant

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

invariant [manual_17] ¬ (s1 V0 V1 ∧ V1 ≠ org ∧ s2 V0 V2 ∧ ring.btw V0 org V2)

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

Lean.resolveGlobalConstNoOverloadCore in Lean.ResolveName

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

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

instance : ToString FirstOrderValue where
  toString
    | FirstOrderValue.Interpreted s val => s.valToString val
    | FirstOrderValue.Uninterpreted _ val => toString val

error in Auto.Parser.TPTP

action remove_org (x : node) (y : node) (z : node) = {
  require x ≠ org;
  require s1 x y;
  require ¬ a y ∨ ¬ reach y;
  require ∀ Z, (¬ a y) → (¬ s2 x Z ∨ s2 x z);
  require (¬ a y ∧ s2 x z) → (¬ a z ∨ ¬ reach z);
  reach x := False
}

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

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

class Rabia.Background (node set_majority set_f_plus_1 : outParam Type) where
  member_maj : node → set_majority → Prop
  member_fp1 : node → set_f_plus_1 → Prop

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
}

action foo (z : node)= {
  let _qq ← f 5 z;
  pure 42
}

#gen_spec

open_isolate wrapper4 with protocol

relation n_have_privilege : node → Prop
relation n_requesting : node → Prop
function n_RN : node → node → seq_t

invariant [manual_12] a Y ∨ a Z ∨ ¬ s1 X Y ∨ ¬ s2 X Z

IO.Process.spawn in Init.System.IO

action set_X = {
  X := True
}

Lean.Meta.throwTacticEx in Lean.Meta.Tactic.Util

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

}
</all_available_defs>

<all_available_lemmas>
theorem forall_and_on_the_left : b ∧ (∀ x, p x) ↔ (∀ x, b ∧ p x)

theorem TwoState_sound [LawfulAction act] (req : SProp σ) (ens : SProp σ) :
  -- The post-condition is not trivial
  (¬ ∀ s, ens s) ->
  act.toTwoState.triple req ens -> act.triple req (fun _ => ens)

theorem Set.ne_empty_iff_exists_mem {α : Type u} {s : Set α} : s ≠ ∅ ↔ ∃ a, a ∈ s

theorem invariant_merge [sys : RelationalTransitionSystem σ] (p q : σ → Prop) :
  (isInvariant p ∧ isInvariant q) ↔ (isInvariant (fun s => p s ∧ q s))

theorem exists_and_right'_eq : ((∃ x, p x) ∧ b) = (∃ x, p x ∧ b)

theorem funextEq' {α β : Type} (f g : α → β) :
  (f = g) = ∀ x, f x = g x

@[smtSimp] theorem iff_eq_eq : (p ↔ q) = (p = q)

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

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

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

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

<target_theorem>
theorem TwoState_sound'_ret_unit [LawfulAction act] (req : SProp σ) (ens : RProp σ PUnit) :
  act.triple req ens → act.toTwoState.triple req (ens () ·) :=
</target_theorem>

