structure VerifiedIO.Prog : Type

• run : List Bit → Bit

theorem VerifiedIO.Prog.ext_iff {x y : Prog} : x = y ↔ x.run = y.run

theorem VerifiedIO.Prog.ext {x y : Prog} (run : x.run = y.run) : x = y

@[reducible, inline]

abbrev VerifiedIO.ProgM : Type → Type

Equations

• VerifiedIO.ProgM = StateT (List Bit) (Sum Bit)

def VerifiedIO.ioBit (b : Bit) : ProgM Bit

Equations

• VerifiedIO.ioBit b = do let __do_lift ← get match __do_lift with | [] => StateT.lift (Sum.inl b) | b₀ :: bs => do set bs pure b₀

class VerifiedIO.ProgM.WF {α : Type} (m : ProgM α) : Prop

• inr ⦃xs zs : List Bit⦄ ⦃r : α⦄ : StateT.run m xs = Sum.inr (r, zs) → zs <:+ xs ∧ ∀ ⦃ys : List Bit⦄, StateT.run m (xs ++ ys) = Sum.inr (r, zs ++ ys)
• inl ⦃xs : List Bit⦄ ⦃b : Bit⦄ : StateT.run m xs = Sum.inl b → ∀ ⦃ys zs : List Bit⦄ ⦃r : α⦄, StateT.run m (xs ++ ys) = Sum.inr (r, zs) → zs <:+ ys ∧ zs ≠ ys

def VerifiedIO.ProgM.toProg (m : ProgM Unit) : Prog

Equations

• m.toProg = { run := fun (bs : List Bit) => match StateT.run m bs with | Sum.inl b => b | Sum.inr val => 0 }

def VerifiedIO.Prog.toProgM (p : Prog) : ProgM Unit

Equations

• p.toProgM = do let bs ← get StateT.lift (Sum.inl (p.run bs))

def VerifiedIO.readBit : ProgM Bit

Equations

• VerifiedIO.readBit = VerifiedIO.ioBit 0

def VerifiedIO.writeBit (b : Bit) : ProgM Unit

Equations

• VerifiedIO.writeBit b = do let _ ← VerifiedIO.ioBit b pure ()

def VerifiedIO.readBitsUntil (p : List Bit → Bool) : ProgM (List Bit)

Equations

• VerifiedIO.readBitsUntil p = do let bs ← get match List.find? p bs.inits with | some bs₁ => do StateT.set (List.drop bs₁.length bs) pure bs₁ | none => StateT.lift (Sum.inl 0)

def VerifiedIO.readNat : ProgM ℕ

Equations

• VerifiedIO.readNat = do let bs ← VerifiedIO.readBitsUntil fun (x : List Bit) => decide (0 ∈ x) pure (bs.length - 1)

def VerifiedIO.writeNat (n : ℕ) : ProgM Unit

Equations

• VerifiedIO.writeNat n = do replicateM' n (VerifiedIO.writeBit 1) VerifiedIO.writeBit 0