Computational Inductive Relations

Here we define the notion of Computational Relations as relations that have functions realizing/computing them. In other words, functions computing the same related states.

References

See [Ledger.FMBC2024] for a formal presentation of the idea?

inductive ComputationResult (Err R : Type) : Type

We represent computations using failing computations. A computation succeeds, returning a value, or fails, returning an error.

• Success {Err R : Type} : R → ComputationResult Err R
• Failure {Err R : Type} : Err → ComputationResult Err R

instance instReprComputationResult {Err✝ R✝ : Type} [Repr Err✝] [Repr R✝] : Repr (ComputationResult Err✝ R✝)

Equations

• instReprComputationResult = { reprPrec := instReprComputationResult.repr }

def instReprComputationResult.repr {Err✝ R✝ : Type} [Repr Err✝] [Repr R✝] : ComputationResult Err✝ R✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def ComputationResult.forgetErr {e r : Type} : ComputationResult e r → ComputationResult Unit r

We can just forget what error computations return.

Equations

• (ComputationResult.Failure a).forgetErr = ComputationResult.Failure ()
• (ComputationResult.Success r_1).forgetErr = ComputationResult.Success r_1

instance instToStringComputationResult {Err R : Type} [ToString Err] [ToString R] : ToString (ComputationResult Err R)

Because we use Plausible to quickcheck some properties, we need to have a way to show computation results in the screen.

Equations

• One or more equations did not get rendered due to their size.

def fail {R : Type} : ComputationResult Unit R

Failing computation with no error.

Equations

• fail = ComputationResult.Failure ()

def success {Err R : Type} (s : R) : ComputationResult Err R

Succeeding computation.

Equations

• success s = ComputationResult.Success s

def failWith {Err R : Type} (e : Err) : ComputationResult Err R

Failing computation with a given error.

Equations

• failWith e = ComputationResult.Failure e

def runOption {Err A : Type} (c : ComputationResult Err A) : Option A

Forgeting computation errors and mapping results into the Option type.

Equations

• runOption (ComputationResult.Success a) = some a
• runOption (ComputationResult.Failure a) = none

def fromOption {A : Type} (c : Option A) : ComputationResult Unit A

Comming back from Option without any specific error.

Equations

• fromOption (some r) = ComputationResult.Success r
• fromOption none = ComputationResult.Failure ()

def fromOptionWith {Err A : Type} (c : Option A) (e : Err) : ComputationResult Err A

Comming from Option but marking none values with a given error.

Equations

• fromOptionWith none e = ComputationResult.Failure e
• fromOptionWith (some t) e = ComputationResult.Success t

theorem fromOpt_Success {Err A : Type} {c : Option A} {e : Err} {t : A} : fromOptionWith c e = ComputationResult.Success t ↔ c = some t

def fromOptionWith' {Err A : Type} (e : Err) (c : Option A) : ComputationResult Err A

Equations

• fromOptionWith' e c = fromOptionWith c e

theorem from_option_success {A : Type} {ma : Option A} {a : A} : fromOption ma = ComputationResult.Success a ↔ ma = some a

def ComputationResult.isSuccess {Err R : Type} (s : ComputationResult Err R) : Bool

Checking if a result is successful.

Equations

• (ComputationResult.Success a).isSuccess = true
• (ComputationResult.Failure a).isSuccess = false

def ComputationResult.getErr {Err R : Type} (s : ComputationResult Err R) : Option Err

Getting errors if computation fails.

Equations

• (ComputationResult.Failure a).getErr = some a
• (ComputationResult.Success r).getErr = none

instance instFunctorComputationResult {Err : Type} : Functor (ComputationResult Err)

Computation Result is a functor

Equations

• One or more equations did not get rendered due to their size.

instance instFunctorFlipComputationResult {R : Type} : Functor (flip ComputationResult R)

Equations

• One or more equations did not get rendered due to their size.

def bimap {Err Err' R R' : Type} (em : Err → Err') (rm : R → R') (cm : ComputationResult Err R) : ComputationResult Err' R'

Equations

• bimap em rm (ComputationResult.Success a) = ComputationResult.Success (rm a)
• bimap em rm (ComputationResult.Failure a) = ComputationResult.Failure (em a)

def ComputationResult.merr {Err Err' R : Type} (f : Err → Err') (c : ComputationResult Err R) : ComputationResult Err' R

Equations

• ComputationResult.merr f (ComputationResult.Success a) = ComputationResult.Success a
• ComputationResult.merr f (ComputationResult.Failure a) = ComputationResult.Failure (f a)

instance instLawfulFunctorComputationResult {Err : Type} : LawfulFunctor (ComputationResult Err)

instance instApplicativeComputationResult {Err : Type} : Applicative (ComputationResult Err)

Equations

• One or more equations did not get rendered due to their size.

instance instLawfulApplicativeComputationResult {Err : Type} : LawfulApplicative (ComputationResult Err)

instance instBindComputationResult {Err : Type} : Bind (ComputationResult Err)

Equations

• One or more equations did not get rendered due to their size.

instance instMonadComputationResult {Err : Type} : Monad (ComputationResult Err)

Equations

• instMonadComputationResult = { toApplicative := instApplicativeComputationResult, toBind := instBindComputationResult }

def ComputationResult.isFailure {Err R : Type} (s : ComputationResult Err R) : Bool

Equations

• (ComputationResult.Failure a).isFailure = true
• (ComputationResult.Success r).isFailure = false

theorem bind_success {Err R R' : Type} {s : ComputationResult Err R} {res : R'} {s' : R → ComputationResult Err R'} (H : s >>= s' = ComputationResult.Success res) : ∃ (r : R), s = ComputationResult.Success r ∧ s' r = ComputationResult.Success res

theorem match_success {Err R : Type} {s' : R} {s : Option R} {f : R → ComputationResult Err R} {e : Err} (H : (match fromOptionWith s e with | ComputationResult.Success a => f a | ComputationResult.Failure x => ComputationResult.Failure x) = ComputationResult.Success s') : ∃ (a : R), s = some a ∧ f a = ComputationResult.Success s'

theorem match_success_success {Err Err' R : Type} {c : ComputationResult Err R} {r' : R} {f : Err → Err'} (H : (match c with | ComputationResult.Success r => ComputationResult.Success r | ComputationResult.Failure e => ComputationResult.Failure (f e)) = ComputationResult.Success r') : c = ComputationResult.Success r'

structure ComputationalRel {Env In State : Type} (Err : Type) (Rel : Env → In → State → State → Prop) : Type

• compute : Env → In → State → ComputationResult Err State
• correct (e : Env) (i : In) (s s' : State) : self.compute e i s = ComputationResult.Success s' ↔ Rel e i s s'

theorem failure_nostep {Env In State Err : Type} {Rel : Env → In → State → State → Prop} {e : Env} {i : In} {s : State} (CRel : ComputationalRel Err Rel) (HFail : (CRel.compute e i s).isFailure = true) (s' : State) : ¬Rel e i s s'

theorem option_match_success {α β : Type} {o : Option α} {e : β} {t : α} (H : (match o, t with | none, t => ComputationResult.Failure e | some u, t => ComputationResult.Success u) = ComputationResult.Success t) : o = some t

Composition of State Machines

This is not very sophisticated composition, it just matches our needs in this project. If we eventually detect this is a good pattern, we can write a library around this. In IOG, Andre Knispel is writing a framework Categorical Crytpo taking ideas like this to the next level.

To keep composition clean, we assume there is a parameter global shared set of parameters GP. Ideally, users may choose shared parameters and put them in this GP type, but it is not mandatory. Each machine has their own set of parameters, states and actions. For flexibility, we may assume that they may compute something different than their states.

def CompositionAndOps.product_comp {GP P₁ P₂ S₁ S₂ A₁ A₂ O₁ O₂ Err₁ Err₂ : Type} (m1 : GP → P₁ → S₁ → A₁ → ComputationResult Err₁ O₁) (m2 : GP → P₂ → S₂ → A₂ → ComputationResult Err₂ O₂) : GP → P₁ × P₂ → S₁ × S₂ → A₁ × A₂ → ComputationResult (Err₁ ⊕ Err₂) (O₁ × O₂)

Product Composition. Tensor Product.

Equations

• One or more equations did not get rendered due to their size.

def CompositionAndOps.product_sharing_comp {GP P₁ P₂ S₁ S₂ A₁ A₂ O₁ O₂ Err₁ Err₂ : Type} (m1 : GP → P₁ × S₂ → S₁ → A₁ → ComputationResult Err₁ O₁) (m2 : GP → P₂ × S₁ → S₂ → A₂ → ComputationResult Err₂ O₂) : GP → P₁ × P₂ → S₁ × S₂ → A₁ × A₂ → ComputationResult (Err₁ ⊕ Err₂) (O₁ × O₂)

Equations

• One or more equations did not get rendered due to their size.

def CompositionAndOps.computational_product {GP P₁ P₂ S₁ S₂ A₁ A₂ Err₁ Err₂ : Type} {rel1 : GP × P₁ → A₁ → S₁ → S₁ → Prop} {rel2 : GP × P₂ → A₂ → S₂ → S₂ → Prop} (c1 : ComputationalRel Err₁ rel1) (c2 : ComputationalRel Err₂ rel2) : ComputationalRel (Err₁ ⊕ Err₂) fun (x : GP × P₁ × P₂) => match (motive := GP × P₁ × P₂ → A₁ × A₂ → S₁ × S₂ → S₁ × S₂ → Prop) x with | (gp, p) => Products.Joint (fun (gp : GP) (p : P₁) => rel1 (gp, p)) (fun (gp : GP) (p : P₂) => rel2 (gp, p)) gp p

Equations

• One or more equations did not get rendered due to their size.

def CompositionAndOps.parallel_comp {GP P₁ P₂ S₁ S₂ A₁ A₂ Err₁ Err₂ : Type} (m1 : GP → P₁ → S₁ → A₁ → ComputationResult Err₁ S₁) (m2 : GP → P₂ → S₂ → A₂ → ComputationResult Err₂ S₂) : GP → P₁ × P₂ → S₁ × S₂ → A₁ ⊕ A₂ → ComputationResult (Err₁ ⊕ Err₂) (S₁ × S₂)

Equations

• CompositionAndOps.parallel_comp m1 m2 gp pp ss (Sum.inl a) = bimap Sum.inl (fun (x : S₁) => (x, ss.snd)) (m1 gp pp.fst ss.fst a)
• CompositionAndOps.parallel_comp m1 m2 gp pp ss (Sum.inr a) = bimap Sum.inr (fun (x : S₂) => (ss.fst, x)) (m2 gp pp.snd ss.snd a)

def CompositionAndOps.computational_parallel {GP P₁ P₂ S₁ S₂ A₁ A₂ Err₁ Err₂ : Type} {rel1 : GP × P₁ → A₁ → S₁ → S₁ → Prop} {rel2 : GP × P₂ → A₂ → S₂ → S₂ → Prop} (c1 : ComputationalRel Err₁ rel1) (c2 : ComputationalRel Err₂ rel2) : ComputationalRel (Err₁ ⊕ Err₂) fun (gpp : GP × P₁ × P₂) (oa : A₁ ⊕ A₂) (ss ss' : S₁ × S₂) => match oa with | Sum.inl a => rel1 (gpp.fst, gpp.snd.fst) a ss.fst ss'.fst ∧ ss.snd = ss'.snd | Sum.inr a => rel2 (gpp.fst, gpp.snd.snd) a ss.snd ss'.snd ∧ ss.fst = ss'.fst

Equations

• One or more equations did not get rendered due to their size.

def CompositionAndOps.parallel_comp_sharing_state {GP P₁ P₂ S₁ S₂ A₁ A₂ Err₁ Err₂ : Type} (m1 : GP → P₁ → S₂ → S₁ → A₁ → ComputationResult Err₁ S₁) (m2 : GP → P₂ → S₁ → S₂ → A₂ → ComputationResult Err₂ S₂) : GP → P₁ × P₂ → S₁ × S₂ → A₁ ⊕ A₂ → ComputationResult (Err₁ ⊕ Err₂) (S₁ × S₂)

Equations

• CompositionAndOps.parallel_comp_sharing_state m1 m2 gp pp ss (Sum.inl a) = bimap Sum.inl (fun (x : S₁) => (x, ss.snd)) (m1 gp pp.fst ss.snd ss.fst a)
• CompositionAndOps.parallel_comp_sharing_state m1 m2 gp pp ss (Sum.inr a) = bimap Sum.inr (fun (x : S₂) => (ss.fst, x)) (m2 gp pp.snd ss.fst ss.snd a)

def CompositionAndOps.conditional_sub {GP P₁ S₁ A₁ A₂ O₁ Err₁ : Type} (m : GP → P₁ → S₁ → A₁ → ComputationResult Err₁ O₁) (lift : S₁ → A₂ → Option A₁) : GP → P₁ → S₁ → A₂ → ComputationResult (Option Err₁) O₁

Equations

• CompositionAndOps.conditional_sub m lift gp p s a = match lift s a with | some na => ComputationResult.merr some (m gp p s na) | none => failWith none

def CompositionAndOps.computational_conditional {GP P₁ S₁ A₁ A₂ Err₁ : Type} {rel1 : GP × P₁ → S₁ → A₁ → S₁ → Prop} (c1 : ComputationalRel Err₁ fun (e : GP × P₁) (i : A₁) (s : S₁) => rel1 e s i) (lift : S₁ → A₂ → Option A₁) : ComputationalRel (Option Err₁) fun (x : GP × P₁) (i : A₂) (s : S₁) => match (motive := GP × P₁ → S₁ → Prop) x with | (g, p) => InterfaceRestrictions.ConditionalSub (fun (gp : GP) (p : P₁) => rel1 (gp, p)) lift g p s i

Equations

• One or more equations did not get rendered due to their size.