Reading one member's stream

A reader reads in order, one box at a time. A scan rechecks boxes previously stepped past and may jump ahead to a box another member acknowledged, keeping the boxes it skips. A reader acknowledges the end of the unbroken run it has read (run). See "Rewrite and scan" in the group chat spec.

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Mode : Type

• idle : Mode
• reading : Mode
• scanning : Mode

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMode : DecidableEq Mode

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMode : Inhabited Mode

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMode = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMode.default }

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader : Type

• stream : Key
• readCap : ByteArray
• next : Index

  The index of the next box to read.

• last : Option Index

  The last box read in order, data or tombstone.

• passed : Nat

  How many boxes this reader has passed.

• kept : List (Index × Nat × Option Index)

  Boxes a scan stepped past without reading, oldest first: each with the count it was passed at and the box before it.

• lost : Option (Nat × Option Index)

  The first box passed unread and no longer kept; acknowledgements stop before it.

• mode : Mode
• tried : List Nat

  The Idx64 of each acknowledged box a scan has already looked for.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReader.decEq (x✝ x✝¹ : Reader) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReader : DecidableEq Reader

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReader = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqReader.decEq

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReader : Inhabited Reader

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReader = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedReader.default }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.read (r : Reader) : Reader × List Effect

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.ahead (r : Reader) (heard : List Nat) : List Nat

Acknowledged boxes a scan has not looked for yet.

Equations

• r.ahead heard = List.filter (fun (h : Nat) => decide (h ≠ Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.counter r.next) && !r.tried.contains h) heard

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.rechecks (r : Reader) : List Effect

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.scan (r : Reader) (heard : List Nat) (window : Nat) : Reader × List Effect

Recheck what was kept, then look for acknowledged boxes ahead, or probe forward from here.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.run (r : Reader) : Option Index

The end of the unbroken run read: how far this stream may be acknowledged.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.lose (r : Reader) (at_ : Nat) (before : Option Index) : Reader

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.loseAll (r : Reader) (dropped : List (Index × Nat × Option Index)) : Reader

Give up on each of dropped.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.forget (r : Reader) (window : Nat) : Reader

Drop kept boxes more than window behind, as lost.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.stepped (r : Reader) (skipped : List Index) (start : Nat) : List (Index × Nat × Option Index)

The boxes a walk kept, from position start, each with the box before it.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.jump (r : Reader) (t : Index) (skipped : List Index) (steps : Nat) : Reader

Jump to t past steps boxes, keeping the last skipped of them; any before those are given up on.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.walked (r : Reader) (target : Option Index) (skipped : List Index) (steps window : Nat) : Reader × List Effect

The result of a walk: jump to target, keeping the boxes passed.

Equations

• r.walked none skipped steps window = (r, [Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Effect.readBox r.stream r.readCap r.next false])
• r.walked (some t) skipped steps window = ((r.jump t skipped steps).forget window, [Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Effect.readBox r.stream r.readCap t false])

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.messageOf : ReadResult → Option Message

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.messageOf (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadResult.data m) = m
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.messageOf (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReadResult.missing why) = none

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.advance (r : Reader) (index next : Index) : Reader

Read the box expected next, in order.

Equations

• r.advance index next = { stream := r.stream, readCap := r.readCap, next := next, last := some index, passed := r.passed + 1, kept := r.kept, lost := r.lost, mode := r.mode, tried := r.tried }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Reader.found (r : Reader) (index : Index) (result : ReadResult) (next : Option Index) (window : Nat) : Option Message × Reader × List Effect

Take one box read: its message if it is new data to ingest, and what to read next.

Equations

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