Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
880 B · 33 lines
12345678910111213141516171819202122232425262728293031323334# eukhe: the proof of LAW tiny_elect_spec## PROOF: a case per probe; on a pong the code's comparison is the spec's# (LA.te.same), and both pick Join on True and Replace on False.
import Baseimport ../../bend/tiny.bend as Tnimport ../../laws/base.bend as LawsBaseimport ../../laws/tiny.bend as Tinyimport ./base.bend as LA
def te.elect_pong(b: Bool) -> {Tn.elect.pong(b) == Tiny.sp_pong(b, Tn.Join{}, Tn.Replace{}) : Tn.Act}: match b: case True{}: {==} case False{}: {==}
def Tiny.tiny_elect_spec(p, m): match p: case Tn.Missing{}: {==} case Tn.Unreachable{}: {==} case Tn.Pong{+t}: %LA.te.same(t, m) : {Tn.elect.pong(Tn.same(t, m)) == Tiny.sp_pong(_, Tn.Join{}, Tn.Replace{}) : Tn.Act} te.elect_pong(Tn.same(t, m)) case Tn.Odd{}: {==} case Tn.Garbled{}: {==} case Tn.Hung{}: {==}