Documentation

Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill

Backfill against epoch-keyed replica storage #

A stream owner rewrites every box once per replica epoch so every position stays populated. See "Backfill" in the group chat spec. A replica keeps the current and previous epochs; a data write matching what is stored stores nothing, so a rewrite does not move a box into the current epoch.

source
inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.Kind :
Type
Instances For
    source
    @[instance_reducible]
    instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.instDecidableEqKind :
    DecidableEq Kind
    Equations
    source
    @[reducible, inline]
    abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.Box :
    Type

    One box at one replica: what is stored, by the epoch it was stored in. At most one entry per epoch; storing again in the same epoch replaces it.

    Equations
    Instances For
      source
      def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.kept (now e : ℕ) :
      Bool

      The epochs a replica keeps at epoch now: now and the one before.

      Equations
      Instances For
        source
        def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.look (now : ℕ) (b : Box) :
        Option Kind

        What a read at epoch now returns: the newest kept entry, if any.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.put (now : ℕ) (k : Kind) (b : Box) :
          Box
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.write (refresh : Bool) (now : ℕ) (k : Kind) (b : Box) :
            Box

            A write of kind k at epoch now. With refresh, a matching data write is stored again.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.Settled (now : ℕ) (b : Box) :
              Prop

              Nothing stored in an epoch that has not begun.

              Equations
              Instances For
                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.look_put_now (now : ℕ) (k : Kind) (b : Box) :
                look now (put now k b) = some k
                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.look_put_next {now : ℕ} {k : Kind} {b : Box} (hb : Settled now b) :
                look (now + 1) (put now k b) = some k

                An entry stored at now is what a read in the next epoch returns, if nothing is newer.

                As deployed, a rewrite does not keep a box #

                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.deployed_rewrite_lost (e : ℕ) :
                have first := write false e Kind.data []; have rewritten := write false (e + 1) Kind.data first; look (e + 1) first = some Kind.data ∧ rewritten = first ∧ look (e + 2) rewritten = none

                Without refresh, a box written in epoch e and rewritten in e + 1 is gone in e + 2.

                Storing a matching write again would keep it #

                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.refresh_rewrite_kept {now : ℕ} {b : Box} (hb : Settled now b) (hnt : look now b ≠ some Kind.tomb) :
                look now (write true now Kind.data b) = some Kind.data ∧ look (now + 1) (write true now Kind.data b) = some Kind.data

                With refresh, a data rewrite in epoch now is readable through now + 1, from any settled state not holding a tombstone.

                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.deployed_rewrite_noop {now : ℕ} {b : Box} (h : look now b = some Kind.data) :
                write false now Kind.data b = b

                Without refresh, rewriting a readable data box changes nothing.

                Tombstones #

                source
                theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Backfill.tomb_kept (refresh : Bool) {now : ℕ} {b : Box} (hb : Settled now b) :
                look now (write refresh now Kind.tomb b) = some Kind.tomb ∧ look (now + 1) (write refresh now Kind.tomb b) = some Kind.tomb

                A tombstone is stored at the current epoch and read through the next.