BACAP test vectors (from hpqc) and randomized round-trip tests

def hexField (j : Lean.Json) (k : String) : Except String ByteArray

Equations

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

def unwrap {α : Type} : Except String α → IO α

Equations

• unwrap (Except.ok v) = pure v
• unwrap (Except.error e) = throw (IO.userError e)

def parseMessageBoxIndexHex (s : String) : Option Cryptlib.Protocols.BACAP.Types.MessageBoxIndex

Equations

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

def parseWriteCap (data : ByteArray) : Except String Cryptlib.Protocols.BACAP.Types.WriteCap

Equations

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

def hexOfPubBytes (v : Cryptlib.Primitives.Sign.Ed25519Blinded.PubBytes) : String

Equations

• hexOfPubBytes v = Cryptlib.Util.newhex.byteArrayToHex { data := v.toArray }

def hexOfSigBytes (s : Cryptlib.Primitives.Sign.Ed25519Blinded.SigBytes) : String

Equations

• hexOfSigBytes s = Cryptlib.Util.newhex.byteArrayToHex { data := s.toArray }

def hexOfByteArray (b : ByteArray) : String

Equations

• hexOfByteArray b = Cryptlib.Util.newhex.byteArrayToHex b

def vecToByteArray {n : ℕ} (v : Vector UInt8 n) : ByteArray

Equations

• vecToByteArray v = { data := v.toArray }

structure MBIVec : Type

• name : String
• initial : ByteArray
• advanceTo : ℕ
• expected : ByteArray

def parseMBIVec (v : Lean.Json) : Except String MBIVec

Equations

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

structure BoxIDVec : Type

• name : String
• writeCapHex : ByteArray
• advanceBy : ℕ
• ctxHex : ByteArray
• useContext : Bool
• expected : ByteArray

def parseBoxIDVec (v : Lean.Json) : Except String BoxIDVec

Equations

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

structure EncryptVec : Type

• name : String
• writeCapHex : ByteArray
• advanceBy : ℕ
• ctxHex : ByteArray
• plaintext : ByteArray
• expectedBoxID : ByteArray
• expectedCiphertext : ByteArray
• expectedSignature : ByteArray

def parseEncryptVec (v : Lean.Json) : Except String EncryptVec

Equations

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

structure MutateVec : Type

• name : String
• writeCapHex : ByteArray
• advanceBy : ℕ
• saltHex : ByteArray
• readCtxHex : ByteArray
• expectedIndex : ByteArray
• expectedBoxID : ByteArray

def parseMutateVec (v : Lean.Json) : Except String MutateVec

Equations

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

def loadVectors {α : Type} (path primName : String) (parse : Lean.Json → Except String α) : IO (Array α)

Equations

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

def advancedIndex (wc : Cryptlib.Protocols.BACAP.Types.WriteCap) (n : ℕ) : Option Cryptlib.Protocols.BACAP.Types.MessageBoxIndex

The cap's index, advanced by n steps.

Equations

• advancedIndex wc n = if n > 0 then wc.messageBoxIndex.advanceIndexTo (wc.messageBoxIndex.idx64 + n.toUInt64) else some wc.messageBoxIndex

def testMessageBoxIndex : IO UInt32

Equations

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

def testBoxID : IO UInt32

Equations

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

def testEncrypt : IO UInt32

Equations

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

def testWriteCapRoundTrip : IO UInt32

Equations

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

def testMutateKDFState : IO UInt32

Equations

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

def testGenerate : IO UInt32

A freshly generated cap encrypts, verifies and decrypts.

Equations

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

def indexRun : Cryptlib.Protocols.BACAP.Types.MessageBoxIndex → ℕ → Option (Array Cryptlib.Protocols.BACAP.Types.MessageBoxIndex)

The next n indices of a ratchet, starting at start itself.

Equations

• indexRun x✝ 0 = some #[]
• indexRun x✝ n.succ = do let __do_lift ← x✝.nextIndex let __do_lift ← indexRun __do_lift n pure (#[x✝] ++ __do_lift)

def testAliceBob : IO UInt32

Alice writes three boxes; Bob, holding only the read cap, derives their IDs and reads them.

Equations

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

def toVec (n : ℕ) (b : ByteArray) : Option (Vector UInt8 n)

Equations

• toVec n b = if h : b.data.size = n then some (Vector.mk b.data h) else none

def readCapOfBytes (b : ByteArray) : Option Cryptlib.Protocols.BACAP.Types.ReadCap

A read cap from bytes, or none if the length or the root key is wrong.

Equations

• readCapOfBytes b = toVec Cryptlib.Protocols.BACAP.Types.ReadCapSize b >>= Cryptlib.Protocols.BACAP.Types.unmarshalReadCap

def writeCapOfBytes (b : ByteArray) : Option Cryptlib.Protocols.BACAP.Types.WriteCap

A write cap from bytes, or none if the length is wrong or the key halves disagree.

Equations

• writeCapOfBytes b = toVec Cryptlib.Protocols.BACAP.Types.WriteCapSize b >>= Cryptlib.Protocols.BACAP.Types.unmarshalWriteCap

def indexOfBytes (b : ByteArray) : Option Cryptlib.Protocols.BACAP.Types.MessageBoxIndex

Equations

• indexOfBytes b = Option.map Cryptlib.Protocols.BACAP.Types.unmarshalMessageBoxIndex (toVec Cryptlib.Protocols.BACAP.Types.MessageBoxIndexSize b)

def strField (j : Lean.Json) (k : String) : Except String String

Equations

• strField j k = do let __do_lift ← j.getObjVal? k __do_lift.getStr?

def optHexField (j : Lean.Json) (k : String) : Except String ByteArray

An optional hex field: absent reads as empty.

Equations

• optHexField j k = match j.getObjVal? k with | Except.ok a => hexField j k | Except.error a => pure ByteArray.empty

def report (ok : Bool) (name : String) (why : String := "") : IO Bool

Equations

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

def testLayout : IO UInt32

Equations

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

def testTombstone : IO UInt32

Equations

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

def reachable (rc : Cryptlib.Protocols.BACAP.Types.ReadCap) (idx : Cryptlib.Protocols.BACAP.Types.MessageBoxIndex) : Bool

Whether idx is on the cap's stream, by contains and by positionAt.

Equations

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

def testPosition : IO UInt32

Equations

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

def rejects (v : Lean.Json) : Except String Bool

Whether this implementation rejects the input a negative vector describes.

Equations

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

def testNegative : IO UInt32

Equations

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

def main : IO UInt32

Equations

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