JSON trace format

Reads call arguments and writes results and member state in katzenqt's trace format. Bytes are hex; a map is a list of pairs in order.

Writing

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.hex (b : ByteArray) : Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.hex b = Lean.Json.str (Cryptlib.Util.newhex.byteArrayToHex b)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.arr (l : List Lean.Json) : Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.arr l = Lean.Json.arr l.toArray

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.opt {α : Type} (f : α → Lean.Json) : Option α → Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.opt f (some a) = f a
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.opt f none = Lean.Json.null

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.nat (n : ℕ) : Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.nat n = Lean.toJson n

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.pairs {K V : Type} (fk : K → Lean.Json) (fv : V → Lean.Json) (d : Common.Dict K V) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.introRef (r : IntroRef) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.message (m : Message) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.payload : Payload → Lean.Json

A message decoded, or bytes the member never looks into, as {"bytes": hex}.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.joinReply (r : JoinReply) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.effect : Effect → Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.outgoing (o : Outgoing) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.mode : Mode → Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.mode Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Mode.idle = Lean.Json.str "idle"
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.mode Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Mode.reading = Lean.Json.str "reading"
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.mode Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Mode.scanning = Lean.Json.str "scanning"

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.induction : Induction → Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.induction Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Induction.idle = Lean.Json.str "idle"
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.induction Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Induction.catchingUp = Lean.Json.str "catching up"
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.induction Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Induction.inducting = Lean.Json.str "inducting"

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.at_ (a : At) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.reader (r : Reader) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.rosters (r : Rosters) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.retention (p : Retention) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.sentBox (s : SentBox) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.ledger (l : Ledger) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.pending (p : Pending) : Lean.Json

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.group (g : Group) : Lean.Json

Equations

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

Reading

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.Parse (α : Type u_1) : Type u_1

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.Parse = Except String

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.field (j : Lean.Json) (k : String) : Parse Lean.Json

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.field j k = j.getObjVal? k

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.bytes (j : Lean.Json) : Parse ByteArray

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.optional {α : Type} (f : Lean.Json → Parse α) : Lean.Json → Parse (Option α)

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.optional f Lean.Json.null = pure none
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.optional f x✝ = some <$> f x✝

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.list {α : Type} (f : Lean.Json → Parse α) (j : Lean.Json) : Parse (List α)

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.list f j = do let __do_lift ← j.getArr? List.mapM f __do_lift.toList

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.pair {α β : Type} (f : Lean.Json → Parse α) (g : Lean.Json → Parse β) (j : Lean.Json) : Parse (α × β)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.triple {α β γ : Type} (f : Lean.Json → Parse α) (g : Lean.Json → Parse β) (h : Lean.Json → Parse γ) (j : Lean.Json) : Parse (α × β × γ)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.num (j : Lean.Json) : Parse ℕ

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.num j = j.getNat?

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readIntroRef (j : Lean.Json) : Parse IntroRef

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readMessage (j : Lean.Json) : Parse Message

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readPayload (j : Lean.Json) : Parse Payload

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readJoinReply (j : Lean.Json) : Parse JoinReply

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readRetention (j : Lean.Json) : Parse Retention

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readResult : Lean.Json → Parse ReadResult

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace.readEvent (j : Lean.Json) : Parse Event

Equations

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