Documentation

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho

The reply to a new member #

What an introducer seals into a contact voucher's reply, as katzenqt's GroupChatReplyWho: its roster in order, each member as a display name and a read cap starting where the new member is to start reading, then the rest of a JoinReply, each member written as its place in that list.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.maxNameChars :

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.maxNameChars = 30

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.readCapSize :

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.readCapSize = 136

Instances For

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.PleaseAdd :

name : String
readCap : ByteArray

Instances For

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqPleaseAdd :

DecidableEq PleaseAdd

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqPleaseAdd = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqPleaseAdd.decEq

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqPleaseAdd.decEq (x✝ x✝¹ : PleaseAdd) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instInhabitedPleaseAdd :

Inhabited PleaseAdd

Equations

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

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.ReplyWho :

pleaseAdds : List (Option PleaseAdd)
rosters : Option (List (Option (List (Nat × Option Nat))))
introductions : Option (List (Nat × Index × Nat))
introducer : Option Nat
newcomer : Option Nat

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqReplyWho.decEq (x✝ x✝¹ : ReplyWho) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqReplyWho :

DecidableEq ReplyWho

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqReplyWho = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instDecidableEqReplyWho.decEq

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instInhabitedReplyWho :

Inhabited ReplyWho

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instInhabitedReplyWho = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.instInhabitedReplyWho.default }

Between a reply and a `JoinReply` #

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.ofJoinReply (r : JoinReply) (name : Key → Option String) :

The reply for r, naming each member by name; a member with no name takes no place, as katzenqt leaves out a member it does not know.

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.toJoinReply (w : ReplyWho) :

Option JoinReply

The JoinReply a reply carries, or none when it carries no rosters or cannot be read.

Equations

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

Instances For

CBOR #

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.nat (n : Nat) :

Cborg.Term

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.nat n = Cborg.Term.TInt n.toInt64

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.optNat :

Option Nat → Cborg.Term

Equations

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.pleaseAddTerm (p : PleaseAdd) :

Cborg.Term

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.rosterTerm (r : List (Nat × Option Nat)) :

Cborg.Term

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.toTerm (w : ReplyWho) :

Cborg.Term

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.encode (w : ReplyWho) :

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.encode w = Cborg.toByteArray (Cborg.encodeTerm (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.toTerm w))

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termNat? :

Cborg.Term → Option Nat

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termNat? (Cborg.Term.TInt n) = if 0 ≤ n then some n.toInt.toNat else none
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termNat? (Cborg.Term.TInteger n) = if 0 ≤ n then some n.toNat else none
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termNat? x✝ = none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termList? :

Cborg.Term → Option (List Cborg.Term)

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termList? (Cborg.Term.TList ts) = some ts.toList
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termList? (Cborg.Term.TListI ts) = some ts.toList
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termList? x✝ = none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termMap? :

Cborg.Term → Option (List (Cborg.Term × Cborg.Term))

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termMap? (Cborg.Term.TMap kvs) = some kvs.toList
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termMap? (Cborg.Term.TMapI kvs) = some kvs.toList
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termMap? x✝ = none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termString? :

Cborg.Term → Option String

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termString? (Cborg.Term.TString s) = some s
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termString? (Cborg.Term.TStringI ss) = some (String.join ss.toList)
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termString? x✝ = none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termBytes? :

Cborg.Term → Option ByteArray

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termBytes? (Cborg.Term.TBytes b) = some b
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termBytes? (Cborg.Term.TBytesI bs) = some (Array.foldl (fun (x1 x2 : ByteArray) => x1 ++ x2) ByteArray.empty bs)
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.termBytes? x✝ = none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.isNull :

Cborg.Term → Bool

Equations

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.isNull Cborg.Term.TNull = true
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.isNull x✝ = false

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.field? (kvs : List (Cborg.Term × Cborg.Term)) (key : String) :

Option Cborg.Term

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.optional {α : Type} (t : Option Cborg.Term) (read : Cborg.Term → Option α) :

Option (Option α)

A value that may be absent or null; none when it is present and cannot be read.

Equations

One or more equations did not get rendered due to their size.
Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.optional none read = some none

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.nullableList {α : Type} (read : Cborg.Term → Option α) (t : Cborg.Term) :

Option (List (Option α))

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.readPleaseAdd (t : Cborg.Term) :

Option PleaseAdd

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.readRoster (t : Cborg.Term) :

Option (List (Nat × Option Nat))

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.readIntroduction (t : Cborg.Term) :

Option (Nat × Index × Nat)

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.ofTerm (t : Cborg.Term) :

Option ReplyWho

Equations

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

Instances For

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho.decode (b : ByteArray) :

Option ReplyWho

Equations

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

Instances For