Pigeonhole replica

A replica stores, per box ID (a public key), a payload and a signature over it under that key. Requests are handled by the state machine step:

• Write: the payload must be boxSize bytes, verify under the box ID, and the box must be free.
• Tombstone (empty payload): must verify over the empty payload; replaces the box.
• Read: returns the stored entry, with a distinct code for a tombstone.

Not modelled: storage failures, read repair, epochs.

structure Cryptlib.Protocols.Pigeonhole.Replica.Entry (Sg : Primitives.Sign.Sign.Signature) : Type

A stored payload and its signature. An empty payload is a tombstone.

• payload : ByteArray
• sig : Sg.Sig

@[reducible, inline]

abbrev Cryptlib.Protocols.Pigeonhole.Replica.Store (Sg : Primitives.Sign.Sign.Signature) : Type

Equations

• Cryptlib.Protocols.Pigeonhole.Replica.Store Sg = (Sg.PublicKey → Option (Cryptlib.Protocols.Pigeonhole.Replica.Entry Sg))

def Cryptlib.Protocols.Pigeonhole.Replica.Store.empty {Sg : Primitives.Sign.Sign.Signature} : Store Sg

Equations

• Cryptlib.Protocols.Pigeonhole.Replica.Store.empty x✝ = none

def Cryptlib.Protocols.Pigeonhole.Replica.Store.put {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (s : Store Sg) (id : Sg.PublicKey) (e : Entry Sg) : Store Sg

Equations

• s.put id e x = if x = id then some e else s x

@[simp]

theorem Cryptlib.Protocols.Pigeonhole.Replica.Store.put_same {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (s : Store Sg) (id : Sg.PublicKey) (e : Entry Sg) : s.put id e id = some e

theorem Cryptlib.Protocols.Pigeonhole.Replica.Store.put_other {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (s : Store Sg) {id x : Sg.PublicKey} (e : Entry Sg) (h : x ≠ id) : s.put id e x = s x

inductive Cryptlib.Protocols.Pigeonhole.Replica.Request (Sg : Primitives.Sign.Sign.Signature) : Type

A request as the replica receives it, after MKEM decryption.

• write {Sg : Primitives.Sign.Sign.Signature} (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) : Request Sg
• read {Sg : Primitives.Sign.Sign.Signature} (id : Sg.PublicKey) : Request Sg

inductive Cryptlib.Protocols.Pigeonhole.Replica.Code : Type

Reply result codes.

• success : Code
• invalidPayload : Code
• invalidSignature : Code
• boxAlreadyExists : Code
• boxIDNotFound : Code
• tombstone : Code

@[instance_reducible]

instance Cryptlib.Protocols.Pigeonhole.Replica.instDecidableEqCode : DecidableEq Code

Equations

• Cryptlib.Protocols.Pigeonhole.Replica.instDecidableEqCode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Cryptlib.Protocols.Pigeonhole.Replica.Reply (Sg : Primitives.Sign.Sign.Signature) : Type

• writeReply {Sg : Primitives.Sign.Sign.Signature} (code : Code) : Reply Sg
• readReply {Sg : Primitives.Sign.Sign.Signature} (code : Code) (entry : Option (Entry Sg)) : Reply Sg

def Cryptlib.Protocols.Pigeonhole.Replica.step {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) : Request Sg → Store Sg × Reply Sg

Handle one request. boxSize is the required payload length.

Equations

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

def Cryptlib.Protocols.Pigeonhole.Replica.Valid {Sg : Primitives.Sign.Sign.Signature} (s : Store Sg) : Prop

Every stored box verifies under its own ID.

Equations

• Cryptlib.Protocols.Pigeonhole.Replica.Valid s = ∀ (id : Sg.PublicKey) (e : Cryptlib.Protocols.Pigeonhole.Replica.Entry Sg), s id = some e → Sg.verify id e.payload e.sig = true

theorem Cryptlib.Protocols.Pigeonhole.Replica.valid_empty {Sg : Primitives.Sign.Sign.Signature} : Valid Store.empty

theorem Cryptlib.Protocols.Pigeonhole.Replica.valid_put {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] {s : Store Sg} (hs : Valid s) (id : Sg.PublicKey) (e : Entry Sg) (h : Sg.verify id e.payload e.sig = true) : Valid (s.put id e)

theorem Cryptlib.Protocols.Pigeonhole.Replica.step_valid {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (hs : Valid s) (r : Request Sg) : Valid (step boxSize s r).fst

Every request preserves Valid.

def Cryptlib.Protocols.Pigeonhole.Replica.run {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) : Store Sg → List (Request Sg) → Store Sg

Run a list of requests in order.

Equations

• Cryptlib.Protocols.Pigeonhole.Replica.run boxSize x✝ [] = x✝
• Cryptlib.Protocols.Pigeonhole.Replica.run boxSize x✝ (r :: rs) = Cryptlib.Protocols.Pigeonhole.Replica.run boxSize (Cryptlib.Protocols.Pigeonhole.Replica.step boxSize x✝ r).fst rs

theorem Cryptlib.Protocols.Pigeonhole.Replica.run_valid {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (rs : List (Request Sg)) (s : Store Sg) : Valid s → Valid (run boxSize s rs)

theorem Cryptlib.Protocols.Pigeonhole.Replica.write_success_verifies {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) (h : (step boxSize s (Request.write id payload sig)).snd = Reply.writeReply Code.success) : Sg.verify id (if payload.size = 0 then ByteArray.empty else payload) sig = true

An accepted write's signature verifies under the box ID.

theorem Cryptlib.Protocols.Pigeonhole.Replica.step_write_cases {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) : (step boxSize s (Request.write id payload sig)).fst = s ∨ ∃ (e : Entry Sg), (step boxSize s (Request.write id payload sig)).fst = s.put id e ∧ Sg.verify id (if payload.size = 0 then ByteArray.empty else payload) sig = true

A write leaves the store unchanged, or stores a verified entry under its box ID.

theorem Cryptlib.Protocols.Pigeonhole.Replica.write_fresh {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) (hne : payload.size ≠ 0) (hsz : payload.size = boxSize) (hv : Sg.verify id payload sig = true) (hfree : s id = none) : step boxSize s (Request.write id payload sig) = (s.put id { payload := payload, sig := sig }, Reply.writeReply Code.success)

A well-formed, correctly signed write to a free box is accepted and stores the box.

theorem Cryptlib.Protocols.Pigeonhole.Replica.write_existing {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) (hne : payload.size ≠ 0) (hsz : payload.size = boxSize) (hv : Sg.verify id payload sig = true) (e : Entry Sg) (hex : s id = some e) : step boxSize s (Request.write id payload sig) = (s, Reply.writeReply Code.boxAlreadyExists)

A non-empty write to an existing box is refused and changes nothing.

theorem Cryptlib.Protocols.Pigeonhole.Replica.step_read_put {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (e : Entry Sg) : step boxSize (s.put id e) (Request.read id) = (s.put id e, Reply.readReply (if e.payload.size = 0 then Code.tombstone else Code.success) (some e))

A read leaves the store unchanged and returns the stored entry.

theorem Cryptlib.Protocols.Pigeonhole.Replica.read_after_write {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (payload : ByteArray) (sig : Sg.Sig) (hne : payload.size ≠ 0) : (step boxSize (s.put id { payload := payload, sig := sig }) (Request.read id)).snd = Reply.readReply Code.success (some { payload := payload, sig := sig })

Reading a box just written returns what was written.

theorem Cryptlib.Protocols.Pigeonhole.Replica.tombstone_then_read {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (id : Sg.PublicKey) (sig : Sg.Sig) (hv : Sg.verify id ByteArray.empty sig = true) : step boxSize s (Request.write id ByteArray.empty sig) = (s.put id { payload := ByteArray.empty, sig := sig }, Reply.writeReply Code.success) ∧ (step boxSize (s.put id { payload := ByteArray.empty, sig := sig }) (Request.read id)).snd = Reply.readReply Code.tombstone (some { payload := ByteArray.empty, sig := sig })

A signed tombstone replaces the box; a read then reports a tombstone.

theorem Cryptlib.Protocols.Pigeonhole.Replica.step_frame {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : Nat) (s : Store Sg) (r : Request Sg) (x : Sg.PublicKey) (h : (step boxSize s r).fst x ≠ s x) : ∃ (payload : ByteArray), ∃ (sig : Sg.Sig), r = Request.write x payload sig ∧ Sg.verify x (if payload.size = 0 then ByteArray.empty else payload) sig = true

A request that changes the entry at x is a write to x whose signature verifies.