HList usage question

Stream: lean4

[David Stainton 🦡]

Hi. I'm relatively new to Lean and I'm writing a cryptography library in Lean, called CryptWalker.
I'm a little hesitant to post his question because there's a lot of code involved and I don't
want to write too much or take up too much of anyone's time.

I have a HList of KEMs, key encapsulation mechanisms. And my goal here is to write a unit test which
iterates over the HList of KEMs and tests each KEM by using it to generate a key pair and then
encapsulate a secret with the public key and decapsulate it with the private key:

def testKEM {α : Type} [kemInstance : KEM α] (kem : α) : IO Unit := do
  let (alicePublicKey, alicePrivateKey) ← kemInstance.generateKeyPair
  let (ciphertext, bobSharedSecret) ← kemInstance.encapsulate kem alicePublicKey
  let aliceSharedSecret := kemInstance.decapsulate kem alicePrivateKey ciphertext
  if bobSharedSecret == aliceSharedSecret then
    IO.println "Shared secrets match!"
  else
    panic! "KEM test failed!"

def testAllKEMs : ∀ {ts : List Type}, HList ts → IO Unit
| [], HList.nil => IO.println "All KEM tests passed!"
| (α :: ts), HList.cons kem rest => do
  @testKEM kem
  testAllKEMs rest

def main : IO Unit := do
  testAllKEMs Schemes

Currently the test doesn't compile because the HList i'm passing in has a type mismatch:

application type mismatch
  testAllKEMs Schemes
argument
  Schemes
has type
  HList
    [KEM CryptWalker.nike.x25519.X25519Scheme, KEM CryptWalker.nike.x448.X448Scheme,
      KEM CryptWalker.nike.x41417.X41417Scheme] : Type 1
but is expected to have type
  HList (?m.14139 x✝⁸ x✝⁷ x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝) : Type

application type mismatch
  @testKEM kem
argument
  kem
has type
  α : Type
but is expected to have type
  Type : Type 1

Here's my KEM type class which is polymorphic over the specific KEM "scheme":

class Key (key : Type) where
  encode : key → ByteArray
  decode : ByteArray → Option key

class PrivateKey (privkey : Type) extends Key privkey

class PublicKey (pubkey : Type) extends Key pubkey

class KEM (scheme : Type) where
  PublicKeyType : Type
  PrivateKeyType : Type

  generateKeyPair : IO (PublicKeyType × PrivateKeyType)
  encapsulate : scheme → PublicKeyType → IO (ByteArray × ByteArray)
  decapsulate : scheme → PrivateKeyType → ByteArray → ByteArray
  privateKeySize : Nat
  publicKeySize : Nat
  encodePrivateKey : PrivateKeyType → ByteArray
  decodePrivateKey : ByteArray → Option PrivateKeyType
  encodePublicKey : PublicKeyType → ByteArray
  decodePublicKey : ByteArray → Option PublicKeyType

HList I got from community discussion threads:

universe u
inductive HList : List (Type u) → Type (u+1)
  | nil  : HList []
  | cons : α → HList αs → HList (α::αs)

But I saw various other definitions of HList that might work for this use case.

and here's how I generate my list of KEM schemes:

def defaultHash := fun x => Sha256.hash x

instance : Adapter X25519Scheme where
  hash := defaultHash

instance : Adapter X448Scheme where
  hash := defaultHash

instance : Adapter X41417Scheme where
  hash := defaultHash

def X25519AsKEM : KEM X25519Scheme := inferInstance
def X448AsKEM : KEM X448Scheme := inferInstance
def X41417AsKEM : KEM X41417Scheme := inferInstance

def Schemes : HList [KEM X25519Scheme, KEM X448Scheme, KEM X41417Scheme] :=
  HList.cons (X25519AsKEM) $
  HList.cons (X448AsKEM) $
  HList.cons (X41417AsKEM) $
  HList.nil

[Daniel Weber]

Something general to note is that in Lean types don't have computational content, and are erased in compilation.
Specifically here, there are a few problems:

• In testKEM, there are two things with computational content - the kemInstance, and the kem. However, testAllKEMs only gets the kemInstance as input - it doesn't have the kem itself.
• testAllKEMs doesn't know that the types in ts are KEMs, so it can't actually call testKEM.
  I think this should work:

def testAllKEMs : List (Σ α : Type, KEM α × α) → IO Unit
| [] => IO.println "All KEM tests passed!"
| ⟨_, _, kem⟩ :: rest => do
  testKEM kem
  testAllKEMs rest

[David Stainton 🦡]

Thanks! That helps. Turns out I had to change the NIKE scheme types to be a structure instead of a class.
I ended up constructing my list of KEMs like this:

def defaultHash := fun x => Sha256.hash x

instance : Adapter X25519Scheme where
  hash := defaultHash

instance : Adapter X448Scheme where
  hash := defaultHash

instance : Adapter X41417Scheme where
  hash := defaultHash

def X25519AsKEM : KEM X25519Scheme := inferInstance
def X448AsKEM : KEM X448Scheme := inferInstance
def X41417AsKEM : KEM X41417Scheme := inferInstance

def X25519Instance : X25519Scheme := {}
def X448Instance : X448Scheme := {}
def X41417Instance : X41417Scheme := {}

def Schemes : List (Σ α : Type, KEM α × α) :=
  [
    ⟨X25519Scheme, (X25519AsKEM, X25519Instance)⟩,
    ⟨X448Scheme, (X448AsKEM, X448Instance)⟩,
    ⟨X41417Scheme, (X41417AsKEM, X41417Instance)⟩,
  ]