Theory Shallow_Micro_Rust.Core_Expression

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Core_Expression
  imports
    ― ‹This needs to come before the theories below for some reason otherwise Isabelle goes berserk
        with ▩‹SIMPLIFIER› exceptions raised about congruences.›
    "Misc.Debug_Logging"
    "HOL-Library.Word"
    "HOL-Eisbach.Eisbach"
    Basic_Case_Expression
begin
(*>*)

section‹Core Micro Rust›

named_theorems micro_rust_simps

subsection‹Runtime aborts›

text‹This describes the different ways that a runtime abort may have come about.  We have:
\begin{enumerate*}
\item A runtime panic, caused by the programmer making an explicit call to the ▩‹panic!› macro, or a
similar construct in Rust.
\item A programmer-facing assertion failed dynamically at runtime.
\item A dangling pointer.
\end{enumerate*}›
datatype 'abort abort
  = Panic ‹String.literal›
  | Unimplemented ‹String.literal›
  | AssertionFailed
  | DanglingPointer
  | TypeError
  | ResumedFromFatal
  | UnexpectedYield
  | CustomAbort 'abort

subsection‹Continuations›

text‹When working towards embedding ▩‹μRust› in Isabelle, we define all of the different ways that
a computation can end, using a dedicated ❙‹continuation› type.  In particular, in Rust, we can:
\begin{enumerate*}
\item Compute a value successfully,
\item Panic at runtime, raising a runtime exception,
\item Return early, with a value, from a computation.
\end{enumerate*}
These are captured below:›

datatype ('s, 'v, 'r, 'abort, 'i, 'o) continuation
  = Success ‹'v› ‹'s› ― ‹A successful, state-modifying computation, producing a value›
  | Return ‹'r› ‹'s›  ― ‹Return from the command early with a value, and the current state.›
  | Abort ‹'abort abort› ‹'s›
  | Yield ‹'i› ‹'s› ‹'o ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression›
  and ('s, 'v, 'r, 'abort, 'i, 'o) expression
  = Expression ‹'s ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation›

text‹Explicitly define a well-founded relation on continuations which makes continuations wrapped
in a \<^term>‹Yield› larger than any of the values of the continuations.›

subsection‹The type of shallow-embedded Micro Rust expressions›

text‹Rust is an expression-oriented language, and expressions can have side-effects, with function
calls modifying the global state, and otherwise-imperative features like variable assignment also
treated as unit-valued expressions.  Moreover, expressions can fail for a variety of reasons, most
notably a call to the ▩‹panic!› macro, or some other similar macro that induces a runtime abort.  As
a result of this, we model expressions as maps from some abstract ∗‹state› type, \<^typ>‹'s›, to values
of \<^typ>‹('s, 'v, 'r, 'abort, 'i, 'o) continuation›.  Moreover, note that our embedding of Rust expressions
is typed, piggy-backing off the HOL type system:›

text‹We can ∗‹evaluate› an expression by simply "feeding it" a state, getting a continuation back:›
definition evaluate :: ‹('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒ ― ‹Micro Rust expression to evaluate›
                        's ⇒                      ― ‹State to evaluate expression in›
                        ('s, 'v, 'r, 'abort, 'i, 'o) continuation› where
  ‹evaluate e s ≡ case e of Expression f ⇒ f s›

text‹The definitions of \<^typ>‹('s, 'v, 'r, 'abort, 'i, 'o) expression› and \<^typ>‹('s, 'v, 'r, 'abort, 'i, 'o) continuation› are
mutually recursive, with recursion under a binder. As a consequence, inductive constructions on
continuations and expressions require a non-trivial termination proof. The following definition
captures the (soon proved to be) well-founded termination relation for those proofs.›

definition expression_wf_base :: ‹(('s, 'v, 'r, 'abort, 'i, 'o) expression × ('s, 'v, 'r, 'abort, 'i, 'o) expression) set› where
  ‹expression_wf_base = {(f, e). ∃σ σ' e' π ρ. evaluate e σ = Yield π σ' e' ∧ f = e' ρ}›

text‹The reflexive-transitive closure of \<^term>‹expression_wf_base›:›
definition expression_wf :: ‹(('s, 'v, 'r, 'abort, 'i, 'o) expression × ('s, 'v, 'r, 'abort, 'i, 'o) expression) set› where
  ‹expression_wf ≡ expression_wf_base⇧⁺›

definition lift_prop_to_cont :: ‹(('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒ bool) ⇒
      ('s, 'v, 'r, 'abort, 'i, 'o) continuation ⇒ bool› where
  ‹lift_prop_to_cont P c ≡ ∀π σ c'. c = Yield π σ c' ⟶ (∀e∈range c'. P e)›

lemma expression_wf_base_is_wf:
  shows ‹wf expression_wf_base› (is ?wf_base)
proof(unfold wf_def, safe)
     fix P :: ‹('a, 'b, 'c, 'd, 'e, 'f) expression ⇒ bool›
     and x :: ‹('a, 'b, 'c, 'd, 'e, 'f) expression›
  assume *: ‹∀x. (∀y. (y, x) ∈ expression_wf_base ⟶ P y) ⟶ P x›
  {
    fix x y
    have ‹P x ∧ (lift_prop_to_cont P) y›
    using * proof(induct_tac x and y)
      fix x1 x2
      show ‹lift_prop_to_cont P (Success x1 x2)›
        by (clarsimp simp add: lift_prop_to_cont_def)
    next
      fix x1 x2
      show ‹lift_prop_to_cont P (Return x1 x2)›
        by (clarsimp simp add: lift_prop_to_cont_def)
    next
      fix a σ
      show ‹lift_prop_to_cont P (Abort a σ)›
        by (clarsimp simp add: lift_prop_to_cont_def)
    next
      fix x y x1 x2 and x3 :: ‹'f ⇒ ('a, 'b, 'c, 'd, 'e, 'f) expression›
      assume ‹∀x. (∀y. (y, x) ∈ expression_wf_base ⟶ P y) ⟶ P x›
         and ‹⋀x4. x4 ∈ range x3 ⟹ P x4›
      from this show ‹lift_prop_to_cont P (Yield x1 x2 x3)›
        by (clarsimp simp add: lift_prop_to_cont_def)
    next
         fix x :: ‹'a ⇒ ('a, 'b, 'c, 'd, 'e, 'f) continuation›
      assume ‹∀x. (∀y. (y, x) ∈ expression_wf_base ⟶ P y) ⟶ P x›
         and ‹(⋀x4. x4 ∈ range x ⟹ lift_prop_to_cont P x4)›
      from this show ‹P (Expression x)›
        by (clarsimp simp add: lift_prop_to_cont_def expression_wf_base_def)
          (metis evaluate_def expression.case rangeI)
    qed
  }
  from this show ‹P x›
    by auto
qed

lemma expression_wf_is_wf[intro]:
  shows ‹wf expression_wf›
by (auto simp add: expression_wf_def intro: wf_trancl[OF expression_wf_base_is_wf])

subsection‹Deep evaluation of Micro Rust expressions›

text‹Evaluation via \<^term>‹evaluate› need not produce a result (▩‹Literal›,\<^term>‹Return› or
 ▩‹Abort›), but can also ▩‹Yield›. In this section, we define various 'deep' evaluation 
functions for ▩‹μRust› expressions, resolving yields by means of 'yield handlers'.›

subsubsection‹Yield handlers›

text‹A ∗‹yield handler› is a means to continue evaluation of a uRust program when its evaluation
via ▩‹evaluate› produces a \<^term>‹Yield›. It receives the yield prompt, the current state, and the
continuation of the program, and makes a decision on how to continue evaluation.

We consider multiple definitions trading simplicity and generality -- their equivalence is proved 
in 🗏‹Core_Expression_Lemmas.thy›› 

text‹First, a ∗‹deterministic› yield handler takes a prompt input as well as a continuation parametrized
by a prompt output, and deterministically return a continuation expression. Note, however, that 
non-determinism may still be modelled by incorporating the necessary random coins in the state
itself.›

type_synonym ('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_det = 
  ‹'i ⇒ ('o ⇒ 's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation) ⇒
     's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation›

text‹The following is the deep evaluation function for deterministic yield handlers:›

function deep_evaluate_det :: ‹('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_det ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒
    's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation› where
  ‹deep_evaluate_det y e σ = (case evaluate e σ of
      Success v σ' ⇒ Success v σ'
    | Return r σ' ⇒ Return r σ'
    | Abort a σ' ⇒ Abort a σ'
    | Yield π σ' e' ⇒ y π (λω. deep_evaluate_det y (e' ω)) σ')›
by pat_completeness auto

termination
  deep_evaluate_det
proof(relation ‹inv_image expression_wf (λc. fst (snd c))›)
  show ‹wf (inv_image expression_wf (λc. fst (snd c)))›
    by force
next
  fix y :: ‹'a ⇒ ('b ⇒ 'c ⇒ ('c, 'd, 'e, 'abort, 'a, 'b) continuation) ⇒ 'c ⇒
      ('c, 'd, 'e, 'abort, 'a, 'b) continuation› and e :: ‹('c, 'd, 'e, 'abort, 'a, 'b) expression› and σ x1 x2 x3 x a
  assume ‹evaluate e σ = Yield x1 x2 x3›
  from this show ‹((y, x3 x, a), y, e, σ) ∈ inv_image expression_wf (λc. fst (snd c))›
    by (force simp add: expression_wf_def expression_wf_base_def)
qed

declare deep_evaluate_det.simps[simp del]

text‹The most basic non-deterministic yield handler is one which takes a prompt input as well as
the current system state, and returns a set of ∗‹yield continuations›: A yield continuation is either
an ▩‹Abort›, or the decision to continue evaluation with a prompt return value and a potentially
modified new state.›

datatype ('s, 'abort, 'o) yield_handler_nondet_basic_result
  = YieldContinue ‹'o × 's›
  | YieldAbort    ‹'abort abort› ‹'s›

type_synonym ('s, 'abort, 'i, 'o) yield_handler_nondet_basic =
  ‹'i ⇒ 's ⇒ ('s, 'abort, 'o) yield_handler_nondet_basic_result set›

function deep_evaluates_nondet_basic :: ‹('i ⇒ 's ⇒ ('s, 'abort, 'o) yield_handler_nondet_basic_result set)
     ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒ 's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation set› where
  ‹deep_evaluates_nondet_basic y e σ = (case evaluate e σ of
      Success v σ'  ⇒ {Success v σ'}
    | Return r σ'   ⇒ {Return r σ'}
    | Abort a σ'     ⇒ {Abort a σ'}
    | Yield π σ' e' ⇒ (
        let handle_yield_result = λyield_result.
          case yield_result of 
            YieldContinue (ω, σ'') ⇒ deep_evaluates_nondet_basic y (e' ω) σ''
          | YieldAbort a σ'        ⇒ {Abort a σ'}
        in ⋃ (handle_yield_result ` (y π σ'))))›
by pat_completeness auto

termination
  deep_evaluates_nondet_basic
proof (relation ‹inv_image expression_wf (λc. fst (snd c))›)
  show ‹wf (inv_image expression_wf (λc. fst (snd c)))›
    by force
next
     fix y :: ‹'a ⇒ 'b ⇒ ('b, 'c, 'd) yield_handler_nondet_basic_result set›
     and e :: ‹('b, 'e, 'f, 'c, 'a, 'd) expression›
     and σ x1 x2 x3 x a
  assume ‹evaluate e σ = Yield x1 x2 x3›
  from this show ‹((y, x3 x, a), y, e, σ) ∈ inv_image expression_wf (λc. fst (snd c))›
    by (force simp add: expression_wf_def expression_wf_base_def)
qed

declare deep_evaluates_nondet_basic.simps [simp del]

text‹The most general notion of a yield handler takes a prompt input, a system state, as well as
∗‹sets› of possible continuations parametrized by prompt outputs and new states, and itself returns
a set of possible continuations.›

type_synonym ('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_nondet =  ‹'i ⇒
    ('o ⇒ 's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation set) ⇒ 's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation set›

function deep_evaluates_nondet :: ‹('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_nondet ⇒
      ('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒ 's ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) continuation set› where
  ‹deep_evaluates_nondet y e σ = (case evaluate e σ of
      Success v σ' ⇒ {Success v σ'}
    | Return r σ' ⇒ {Return r σ'}
    | Abort a σ' ⇒ {Abort a σ'}
    | Yield π σ' e' ⇒ y π (λω σ'. deep_evaluates_nondet y (e' ω) σ') σ')›
by pat_completeness auto

termination
  deep_evaluates_nondet
proof(relation ‹inv_image expression_wf (λc. fst (snd c))›)
  show ‹wf (inv_image expression_wf (λc. fst (snd c)))›
    by force
next
     fix y :: ‹'a ⇒ ('b ⇒ 'c ⇒ ('c, 'd, 'e, 'f, 'a,
                       'b) continuation set)
         ⇒ 'c ⇒ ('c, 'd, 'e, 'f, 'a, 'b) continuation set›
     and e :: ‹('c, 'd, 'e, 'f, 'a, 'b) expression›
     and σ x1 x2 x3 x a
  assume ‹evaluate e σ = Yield x1 x2 x3›
  from this show ‹((y, x3 x, a), y, e, σ) ∈ inv_image expression_wf (λc. fst (snd c))›
    by (force simp add: expression_wf_def expression_wf_base_def)
qed

text‹Next, we connect restricted and general yield handlers.

First, a basic non-deterministic yield handler gives a general one as follows:›

definition yield_handler_nondet_basic_to_nondet :: ‹('s, 'abort, 'i, 'o) yield_handler_nondet_basic ⇒
      ('s, 'b, 'c, 'abort, 'i, 'o) yield_handler_nondet› where
  ‹yield_handler_nondet_basic_to_nondet y π e σ ≡ ⋃ ( 
     let handle_yield_result = λres.
       case res of
         YieldContinue (ω, σ') ⇒ e ω σ'
       | YieldAbort a σ' ⇒ {Abort a σ'}
      in handle_yield_result ` (y π σ))›

text‹Second, every deterministic yield handler gives rise to a general non-deterministic 
yield handler:›

definition yield_handler_det_to_nondet :: ‹('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_det ⇒
    ('s, 'v, 'r, 'abort, 'i, 'o) yield_handler_nondet› where
  ‹yield_handler_det_to_nondet y π e σ ≡
     (λe_choice. y π e_choice σ) ` ({e'. ∀ω σ. e' ω σ ∈ e ω σ})›

text‹We will prove in 🗏‹Core_Expression_Lemmas.thy› that the conversions between the different 
yield handlers intertwine the various deep evaluation functions.›

paragraph‹Some examples and properties of non-deterministic basic yield handlers:›

text‹A ∗‹non-empty› yield handler is one which always returns at least one continuation.
We will show below that deep evaluatin for non-empty yield handlers always produces at least
one result:›

definition is_nonempty_yield_handler :: ‹('s, 'abort, 'i, 'o) yield_handler_nondet_basic ⇒ bool› where
  ‹is_nonempty_yield_handler y ≡ (∀a b. y a b ≠ {})›
  
subsection‹More basic material›

text‹A \<^text>‹function_body› represents a callable function which has already had all arguments
applied and returns \<^typ>‹'b›, while operating on machine state typ‹'s›.›
datatype ('s, 'b, 'abort, 'i, 'o) function_body
  = FunctionBody (function_body: ‹('s, 'b, 'b, 'abort, 'i, 'o) expression›)

lemma function_body_simp [simp, micro_rust_simps]:
  shows ‹function_body (FunctionBody f) = f›
by (simp add: function_body_def)

text‹A ❙‹literal› value does not depend on the state at all.  Note that the type of the literal is
reflected in the type of the expression:›
definition literal :: ‹'v ⇒ ― ‹HOL value to lift into an expression›
                       ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹literal v ≡ Expression (Success v)›

definition deep_compose1 :: ‹('b ⇒ 'c) ⇒ ('t0 ⇒ 'b) ⇒ ('t0 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose1 g f ≡ λt0. (g (f t0))›
definition deep_compose2 :: ‹('b ⇒ 'c) ⇒ ('t0 ⇒ 't1 ⇒ 'b) ⇒ ('t0 ⇒ 't1 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose2 g f ≡ λt0 t1. (g (f t0 t1))›
definition deep_compose3 :: ‹('b ⇒ 'c) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ 'b) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose3 g f ≡ λt0 t1 t2. (g (f t0 t1 t2))›
definition deep_compose4 :: ‹('b ⇒ 'c) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 'b) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose4 g f ≡ λt0 t1 t2 t3. (g (f t0 t1 t2 t3))›
definition deep_compose5 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose5 g f ≡ λt0 t1 t2 t3 t4. (g (f t0 t1 t2 t3 t4))›
definition deep_compose6 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose6 g f ≡ λt0 t1 t2 t3 t4 t5. (g (f t0 t1 t2 t3 t4 t5))›
definition deep_compose7 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose7 g f ≡ λt0 t1 t2 t3 t4 t5 t6. (g (f t0 t1 t2 t3 t4 t5 t6))›
definition deep_compose8 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose8 g f ≡ λt0 t1 t2 t3 t4 t5 t6 t7. (g (f t0 t1 t2 t3 t4 t5 t6 t7))›
definition deep_compose9 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose9 g f ≡ λt0 t1 t2 t3 t4 t5 t6 t7 t8. (g (f t0 t1 t2 t3 t4 t5 t6 t7 t8))›
definition deep_compose10 :: ‹('b ⇒ 'c) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ 'b) ⇒
                             ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ 'c)›
  where [micro_rust_simps]: ‹deep_compose10 g f ≡ λt0 t1 t2 t3 t4 t5 t6 t7 t8 t9. (g (f t0 t1 t2 t3 t4 t5 t6 t7 t8 t9))›

text‹A bunch of convenience functions for lifting pure functions to Micro Rust expressions:›

abbreviation (input) lift_exp0 :: ‹'v ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression›
  where ‹lift_exp0 ≡ literal›
definition lift_exp1 :: ‹('a ⇒ 'b) ⇒
                         ('a ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp1 ≡ deep_compose1 literal›
definition lift_exp2 :: ‹('a ⇒ 'b ⇒ 'c) ⇒
                         ('a ⇒ 'b ⇒ ('s, 'c, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp2 ≡ deep_compose2 literal›
definition lift_exp3 :: ‹('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒
                         ('a ⇒ 'b ⇒ 'c ⇒ ('s, 'd, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp3 ≡ deep_compose3 literal›
definition lift_exp4 :: ‹('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e) ⇒
                         ('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ ('s, 'e, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp4 ≡ deep_compose4 literal›
definition lift_exp5 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp5 ≡ deep_compose5 literal›
definition lift_exp6 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp6 ≡ deep_compose6 literal›
definition lift_exp7 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp7 ≡ deep_compose7 literal›
definition lift_exp8 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression)›
  where [micro_rust_simps]: ‹lift_exp8 ≡ deep_compose8 literal›

text‹A ❙‹function literal› lifts a value as a Micro Rust \<^typ>‹('s, 'v, 'abort, 'i, 'o) function_body›.›
definition fun_literal :: ‹'v ⇒ ('s, 'v, 'abort, 'i, 'o) function_body› where
  ‹fun_literal v ≡ FunctionBody (literal v)›

text‹More convenience functions for lifting pure functions to Micro Rust functions, i.e. values
of type \<^typ>‹('s, 'v, 'abort, 'i, 'o) function_body›.›

definition lift_fun0 :: ‹'v ⇒ ('s, 'v, 'abort, 'i, 'o) function_body›
  where [micro_rust_simps]: ‹lift_fun0 ≡ fun_literal›
definition lift_fun1 :: ‹('a ⇒ 'b) ⇒
                         ('a ⇒ ('s, 'b, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun1 ≡ deep_compose1 fun_literal›
definition lift_fun2 :: ‹('a ⇒ 'b ⇒ 'c) ⇒
                         ('a ⇒ 'b ⇒ ('s, 'c, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun2 ≡ deep_compose2 fun_literal›
definition lift_fun3 :: ‹('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒
                         ('a ⇒ 'b ⇒ 'c ⇒ ('s, 'd, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun3 ≡ deep_compose3 fun_literal›
definition lift_fun4 :: ‹('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e) ⇒
                         ('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ ('s, 'e, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun4 ≡ deep_compose4 fun_literal›
definition lift_fun5 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun5 ≡ deep_compose5 fun_literal›
definition lift_fun6 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun6 ≡ deep_compose6 fun_literal›
definition lift_fun7 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun7 ≡ deep_compose7 fun_literal›
definition lift_fun8 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun8 ≡ deep_compose8 fun_literal›
definition lift_fun9 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun9 ≡ deep_compose9 fun_literal›
definition lift_fun10 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ 'v) ⇒
                         ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body)›
  where [micro_rust_simps]: ‹lift_fun10 ≡ deep_compose10 fun_literal›

text‹As an example of a \<^term>‹fun_literal› Micro Rust expression, we introduce the ∗‹skip› command:
This is just an abbreviation for the unit literal, though with a more suggestive name for when we
use it later.  Though this looks useless, it will prove useful later when we come to ∗‹derive› new
expressions from old:›
abbreviation (input) skip :: ‹('s, unit, 'r, 'abort, 'i, 'o) expression› where
  ‹skip ≡ literal ()›

text‹An ∗‹abort› expression aborts computation at runtime with the given abort type.›
definition abort :: ‹'abort abort ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹abort a ≡ Expression (Abort a)›

text‹A ∗‹panic› expression aborts computation at runtime with a defined error message.  Note that
the panic message must be a string literal:›
abbreviation panic :: ‹String.literal ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹panic msg ≡ abort (Panic msg)›

text ‹An ∗‹unimplemented› expression aborts a computation at runtime, indicating that some
function is not implemented. The given string should indicate the name of the unimplemented function.
This is the same as a ∗‹panic› in most ways, but conformance testing will end early with a warning,
instead of an error, if it encounters an unimplemented abort.›
abbreviation unimplemented :: ‹String.literal ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹unimplemented nm ≡ abort (Unimplemented nm)›

text‹This will sometimes prove useful to help disambiguate complex expressions, making it look like
we are introducing a new stack scope:›
abbreviation (input) scoped :: ‹('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹scoped e ≡ e›

subsection‹Monadic computation›

text‹We now develop some infrastructure related to the type of expressions, which will be
generally useful all over the place.  This is the ∗‹monadic bind› construct: note that it is
essentially a generalized form of ∗‹let›, and in fact this is the syntax which we will assign it in
Micro Rust, rather than working in the ∗‹do-block› style familiar from Haskell (though we will often
use this style when providing ∗‹definitions› of Micro Rust expressions).  Note that sequencing
(i.e., the semicolon from Rust) is also a degenerate form of this construct where the unit-valued
result of the first expression in the sequence is bound to a variable name which is never used in
the second expression:›
function bind :: ‹('s, 'v, 'r, 'abort, 'i, 'o) expression ⇒         ― ‹Expression to bind to variable›
                    ('v ⇒ ('s, 'a, 'r, 'abort, 'i, 'o) expression) ⇒ ― ‹Body of let construct, with new binding›
                    ('s, 'a, 'r, 'abort, 'i, 'o) expression› where
  ‹bind e f = Expression (λσ. case evaluate e σ of
      Success v σ' ⇒ evaluate (f v) σ'
    | Return r σ' ⇒ Return r σ'
    | Abort a σ' ⇒ Abort a σ'
    | Yield π σ' e' ⇒ Yield π σ' (λρ. bind (e' ρ) f))›
by pat_completeness auto

termination
  bind
proof (relation ‹inv_image expression_wf fst›)
  show ‹wf (inv_image expression_wf fst)›
    by force
next
     fix e :: ‹('a, 'b, 'c, 'd, 'e, 'f) expression›
     and f :: ‹'b ⇒ ('a, 'g, 'c, 'd, 'e, 'f) expression›
     and x x1 x2 x3 a
  assume ‹evaluate e x = Yield x1 x2 x3›
  from this show ‹((x3 a, f), e, f) ∈ inv_image expression_wf fst›
    by (force simp add: expression_wf_def expression_wf_base_def)
qed

lemma bind_evaluate:
  shows ‹evaluate (bind e f) σ = 
     (case evaluate e σ of
      Success v σ' ⇒ evaluate (f v) σ'
    | Return r σ' ⇒ Return r σ'
    | Abort a σ' ⇒ Abort a σ'
    | Yield π σ' e' ⇒ Yield π σ' (λρ. bind (e' ρ) f))›
by (simp add: evaluate_def)

text‹Contrary to definitions by ▩‹Definition›, the definition of \<^term>‹bind› is marked as ▩‹simp› 
by default. Removing it to keep the default behaviour of ▩‹definitions› of not being unfolded 
automatically.›
declare Core_Expression.bind.simps[simp del]

text‹The following is the sequencing operator (the semicolon), familiar from C-language family
programming languages.  Note that it is again well-typed: both expressions being sequenced must be
unit-valued.  It is also a degenerate form of the monadic bind operator, as previously mentioned:›
definition sequence :: ‹('s, 'a, 'r, 'abort, 'i, 'o) expression ⇒ ― ‹First expression to execute›
                        ('s, 'b, 'r, 'abort, 'i, 'o) expression ⇒ ― ‹Second expression to execute›
                        ('s, 'b, 'r, 'abort, 'i, 'o) expression› where
  ‹sequence e f ≡ bind e (λ_. f)›

subsection‹Extracting and modifying state›

text‹The following functions are utility functions, or basic building blocks, that we will use when
defining the semantics of larger, more complex expressions.  Note that the
\<^typ>‹('s, 'v, 'r, 'abort, 'i, 'o) expression› is a form of ∗‹state monad›, which "bundles" along an implicit machine
state (of type \<^typ>‹'s›).  We will frequently need to observe some aspect of the machine during the
course of a computation: for example reading from a register file, or checking whether a page is
mapped within the address space of a principal, or similar.  The following definition provides a
generic method for querying such elements:›
definition get :: ‹('a ⇒ 'b) ⇒ ('a, 'b, 'r, 'abort, 'i, 'o) expression› where
  ‹get f ≡ Expression (λσ. Success (f σ) σ)›

text‹Moreover, the following function provides a generic method for ∗‹modifying› elements of the
underlying machine state, for example writing to a file, or moving pages between principals, or
similar:›
definition put :: ‹('a ⇒ 'a) ⇒ ('a, unit, 'r, 'abort, 'i, 'o) expression› where
  ‹put f ≡ Expression (λσ. Success () (f σ))›

definition put_assert :: ‹('a ⇒ 'a option) ⇒ 'abort abort ⇒ ('a, unit, 'r, 'abort, 'i, 'o) expression› where
  ‹put_assert f a ≡ Expression (λσ. case f σ of None ⇒ Abort a σ | Some σ' ⇒ Success () σ')›

subsection‹Evaluation of lists of expressions›

text‹Given a list of expressions, evaluate them each in order and return
a list of the resulting values.›

fun list_sequence :: ‹('s, 'v, 'r, 'abort, 'i, 'o) expression list ⇒ ('s, 'v list, 'r, 'abort, 'i, 'o) expression› where
  ‹list_sequence []     = literal []› |
  ‹list_sequence (x#xs) =
     bind x (λv.
     bind (list_sequence xs) (λvs.
       literal (v#vs)))›

subsection‹Return expressions›

text‹The ▩‹return_func› command returns a value from a function early, capturing the current state
in doing so.  Note that the ∗‹return› command can appear in lots of unexpected places in Rust.
Partly, this is why our \<^typ>‹('s, 'v, 'r, 'abort, 'i, 'o) continuation› type is so complex, accepting an extra type
parameter, \<^typ>‹'r›, compared to what one may normally expect from a state monad.  This is because
there is a distinction between the type of ▩‹return_func›, which can be used at type ▩‹bool› when it
appears as the "test" expression in a conditional, and the type of the value that it returns, namely
the expected return type of the enclosing function.›

definition return_val :: ‹'r ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹return_val r ≡ Expression (λσ. Return r σ)›

definition return_func :: ‹('s, 'r, 'r, 'abort, 'i, 'o) expression ⇒ ('s, 'v, 'r, 'abort, 'i, 'o) expression› where
  ‹return_func v ≡ bind v return_val›

text‹Note that \<^term>‹return_func› is not the ∗‹unit› of the expression monad, as one may expect from
the name if you are coming from Haskell!  That is \<^term>‹literal›.›

subsection ‹Calling functions›

text ‹Execute a Rust function.›
function call_function_body :: ‹('s, 'b, 'b, 'abort, 'i, 'o) expression ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression› where
  ‹call_function_body e =
    Expression (λσ.
          (case evaluate e σ of
             Success x σ' ⇒ Success x σ'
           | Return x σ'  ⇒ Success x σ'
           | Yield π σ' e' ⇒ Yield π σ' (λω. call_function_body (e' ω))
           | Abort abt σ'  ⇒ Abort abt σ'))›
by pat_completeness auto

termination
  call_function_body
proof(relation ‹expression_wf›)
  show ‹wf expression_wf›
    by force
next
     fix e :: ‹('a, 'b, 'b, 'c, 'd, 'e) expression›
     and x x1 x2 x3 a
  assume ‹evaluate e x = Yield x1 x2 x3›
  from this show ‹(x3 a, e) ∈ expression_wf›
    by (force simp add: expression_wf_def expression_wf_base_def)
qed

declare Core_Expression.call_function_body.simps[simp del]

text ‹Execute a Rust function.›
definition call :: ‹('s, 'b, 'abort, 'i, 'o) function_body ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression› where
  ‹call fn ≡ case fn of FunctionBody body ⇒ call_function_body body›

subsection‹Binary operations›

text‹A bit of sugar to reduce the typing burden for binary operations on expressions.›

type_synonym ('s, 'a, 'b, 'c, 'r, 'abort, 'i, 'o) urust_binop3 =
  ‹('s, 'a, 'r, 'abort, 'i, 'o) expression ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression ⇒ ('s, 'c, 'r, 'abort, 'i, 'o) expression›
type_synonym ('s, 'a,         'r, 'abort, 'i, 'o) urust_binop  =
  ‹('s, 'a, 'a, 'a, 'r, 'abort, 'i, 'o) urust_binop3›
type_synonym ('s, 'a,     'c, 'r, 'abort, 'i, 'o) urust_binop2 =
  ‹('s, 'a, 'a, 'c, 'r, 'abort, 'i, 'o) urust_binop3›

subsection ‹Derived constructions›

definition bind1
   :: ‹('arg0 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind1 f e0 ≡ bind e0 (λv0. f v0)›

definition bind2
   :: ‹('arg0 ⇒ 'arg1 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind2 f e0 e1 ≡ bind e0 (λv0. bind e1 (λv1. (f v0 v1)))›

definition bind3
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind3 f e0 ≡ λe1 e2. bind e0 (λv0. bind2 (f v0) e1 e2)›

definition bind4
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind4 f e0 ≡ λe1 e2 e3. bind e0 (λv0. bind3 (f v0) e1 e2 e3)›

definition bind5
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind5 f e0 ≡ λe1 e2 e3 e4. bind e0 (λv0. bind4 (f v0) e1 e2 e3 e4)›

definition bind6
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind6 f e0 ≡ λe1 e2 e3 e4 e5. bind e0 (λv0. bind5 (f v0) e1 e2 e3 e4 e5)›

definition bind7
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind7 f e0 ≡ λe1 e2 e3 e4 e5 e6. bind e0 (λv0. bind6 (f v0) e1 e2 e3 e4 e5 e6)›

definition bind8
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7  ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind8 f e0 ≡ λe1 e2 e3 e4 e5 e6 e7. bind e0 (λv0. bind7 (f v0) e1 e2 e3 e4 e5 e6 e7)›

definition bind9
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ 'arg8 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg8, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind9 f e0 ≡ λe1 e2 e3 e4 e5 e6 e7 e8. bind e0 (λv0. bind8 (f v0) e1 e2 e3 e4 e5 e6 e7 e8)›

definition bind10
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ 'arg8 ⇒ 'arg9 ⇒ ('s, 'v, 'c, 'abort, 'i, 'o) expression) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg8, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg9, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bind10 f e0 ≡ λe1 e2 e3 e4 e5 e6 e7 e8 e9. bind e0 (λv0. bind9 (f v0) e1 e2 e3 e4 e5 e6 e7 e8 e9)›

definition bindlift1
   :: ‹('arg0 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift1 ≡ bind1 ∘ lift_exp1›

definition bindlift2
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift2 ≡ bind2 ∘ lift_exp2›

definition bindlift3
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift3 ≡ bind3 ∘ lift_exp3›

definition bindlift4
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift4 ≡ bind4 ∘ lift_exp4›

definition bindlift5
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift5 ≡ bind5 ∘ lift_exp5›

definition bindlift6
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift6 ≡ bind6 ∘ lift_exp6›

definition bindlift7
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift7 ≡ bind7 ∘ lift_exp7›

definition bindlift8
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ 'v) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹bindlift8 ≡ bind8 ∘ lift_exp8›

abbreviation call_deep1 :: ‹('t0 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒ ('t0 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep1 ≡ deep_compose1 call›
abbreviation call_deep2 :: ‹('t0 ⇒ 't1 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒ ('t0 ⇒ 't1 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep2 ≡ deep_compose2 call›
abbreviation call_deep3 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep3 ≡ deep_compose3 call›
abbreviation call_deep4 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒ ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep4 ≡ deep_compose4 call›
abbreviation call_deep5 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep5 ≡ deep_compose5 call›
abbreviation call_deep6 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep6 ≡ deep_compose6 call›
abbreviation call_deep7 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep7 ≡ deep_compose7 call›
abbreviation call_deep8 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep8 ≡ deep_compose8 call›
abbreviation call_deep9 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep9 ≡ deep_compose9 call›
abbreviation call_deep10 :: ‹('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ ('s, 'b, 'abort, 'i, 'o) function_body) ⇒
                            ('t0 ⇒ 't1 ⇒ 't2 ⇒ 't3 ⇒ 't4 ⇒ 't5 ⇒ 't6 ⇒ 't7 ⇒ 't8 ⇒ 't9 ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression)› where
  ‹call_deep10 ≡ deep_compose10 call›

definition funcall0
   :: ‹('s, 'b, 'abort, 'i, 'o) function_body ⇒ ('s, 'b, 'r, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹funcall0 f ≡ call f›

definition funcall1
   :: ‹('arg0 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall1 f e0 ≡ bind1 (call_deep1 f) e0›

definition funcall2
   :: ‹('arg0 ⇒ 'arg1 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall2 f e0 e1 ≡ bind2 (call_deep2 f) e0 e1›

definition funcall3
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall3 f e0 e1 e2 ≡ bind3 (call_deep3 f) e0 e1 e2›

definition funcall4
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall4 f e0 e1 e2 e3 ≡ bind4 (call_deep4 f) e0 e1 e2 e3›

definition funcall5
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall5 f e0 e1 e2 e3 e4 ≡ bind5 (call_deep5 f) e0 e1 e2 e3 e4›

definition funcall6
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall6 f e0 e1 e2 e3 e4 e5 ≡ bind6 (call_deep6 f) e0 e1 e2 e3 e4 e5›

definition funcall7
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
‹funcall7 f e0 e1 e2 e3 e4 e5 e6 ≡ bind7 (call_deep7 f) e0 e1 e2 e3 e4 e5 e6›

definition funcall8
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹funcall8 f e0 e1 e2 e3 e4 e5 e6 e7 ≡ bind8 (call_deep8 f) e0 e1 e2 e3 e4 e5 e6 e7›

definition funcall9
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ 'arg8 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg8, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹funcall9 f e0 e1 e2 e3 e4 e5 e6 e7 e8 ≡ bind9 (call_deep9 f) e0 e1 e2 e3 e4 e5 e6 e7 e8›

definition funcall10
   :: ‹('arg0 ⇒ 'arg1 ⇒ 'arg2 ⇒ 'arg3 ⇒ 'arg4 ⇒ 'arg5 ⇒ 'arg6 ⇒ 'arg7 ⇒ 'arg8 ⇒ 'arg9 ⇒ ('s, 'v, 'abort, 'i, 'o) function_body) ⇒
      ('s, 'arg0, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg1, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg2, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg3, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg4, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg5, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg6, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg7, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg8, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'arg9, 'c, 'abort, 'i, 'o) expression ⇒
      ('s, 'v, 'c, 'abort, 'i, 'o) expression› where [micro_rust_simps]:
   ‹funcall10 f e0 e1 e2 e3 e4 e5 e6 e7 e8 e9 ≡ bind10 (call_deep10 f) e0 e1 e2 e3 e4 e5 e6 e7 e8 e9›

(*<*)
end
(*>*)