Documentation

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox

The boxes a member wrote to its own stream #

What a member may still rewrite, and what retention lets it forget. See "Sent-box records" and "Disappearing messages" in the group chat spec.

source
structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Retention :
Type
  • window : Option Nat

    Epochs a Sent-box record is kept and backfilled; none keeps it for good.

  • discardAcked : Bool

    Drop plaintext every member still read has acknowledged.

  • keepSent : Option Nat

    Epochs the policy keeps sent content.

  • keepReceived : Option Nat

    Epochs the policy keeps received content.

Instances For
    source
    @[instance_reducible]
    instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqRetention :
    DecidableEq Retention
    Equations
    source
    def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqRetention.decEq (x✝ x✝¹ : Retention) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedRetention :
      Inhabited Retention
      Equations
      source
      structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Record :
      Type
      • index : Index

        The box's whole MessageBoxIndex.

      • plaintext : Option Payload

        none once the plaintext is gone, or if it was never handed over.

      • control : Bool
      • written : Nat
      • settled : Bool

        Written as a tombstone once every member acknowledged it.

      Instances For
        source
        def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqRecord.decEq (x✝ x✝¹ : Record) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqRecord :
          DecidableEq Record
          Equations
          source
          @[instance_reducible]
          instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedRecord :
          Inhabited Record
          Equations
          source
          structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox :
          Type
          • records : Common.Dict Nat Record

            By the box's Idx64, which orders the boxes of the member's stream as it wrote them.

          • backfilled : Option Nat

            The epoch last backfilled.

          Instances For
            source
            @[instance_reducible]
            instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqSentBox :
            DecidableEq SentBox
            Equations
            source
            def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqSentBox.decEq (x✝ x✝¹ : SentBox) :
            Decidable (x✝ = x✝¹)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedSentBox :
              Inhabited SentBox
              Equations
              source
              def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.record (s : SentBox) (index : Index) (plaintext : Option Payload) (control : Bool) (epoch : Nat) :
              SentBox
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.check (s : SentBox) (index : Index) :
                Option Nat

                The Sent-box check: the Idx64 of the box index names, or none if the member never wrote it.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.checkAt (s : SentBox) (idx64 : Nat) :
                  Bool

                  The Sent-box check for an acknowledgement, which names the box by its Idx64.

                  Equations
                  Instances For
                    source
                    def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.retain (s : SentBox) (epoch : Nat) (policy : Retention) (everyoneAcked : Nat → Bool) :
                    SentBox
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.SentBox.backfill (s : SentBox) (epoch : Nat) (everyoneAcked : Nat → Bool) :
                      SentBox × List Effect

                      Rewrite every record a member has yet to acknowledge, at most once per epoch, and write a record every member has acknowledged as a tombstone once its plaintext is gone. Nothing when nobody is behind.

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