crypto.bend
1# bend-osdev-crypto: one set of typed interfaces for the cryptographic
2# algorithms of bend-osdev, the Bend counterpart of Linux's crypto API.
3#
4# An interface is a signature of template arguments: an algorithm satisfies it
5# by supplying a def of each type, and a generic algorithm (HMAC over a hash,
6# a mode over a block cipher) takes the signature as its own template
7# arguments, so it is specialised at compile time for each algorithm it runs
8# over. The interfaces, one file each:
9#
10# block.bend block cipher: key schedule, encrypt and decrypt a block
11# stream.bend stream cipher: a state that encrypts the next piece of data
12# hash.bend hash: streaming init / update / final, and one-shot
13# mac.bend message authentication code: compute and verify
14# aead.bend authenticated encryption with associated data: seal, open
15# kdf.bend key derivation
16# sign.bend signature: sign and verify
17# kex.bend key agreement
18#
19# Each interface has laws that every instance must satisfy; README.md states
20# them and gen/instances.py writes one law per instance into LAWS.bend. This
21# file holds what every interface shares: the error type.
22import Base
23import bend-osdev-bytes@0.1.0.0/bytes.bend as B
24
25# Every failure an interface reports. An instance whose algorithm has its own
26# error type maps it onto these (inst_lc.bend, inst_cm.bend).
27type CrError is Data:
28 CrBadKeyLength{got: Nat}
29 CrBadIvLength{got: Nat}
30 CrBadNonceLength{got: Nat}
31 CrBadTagLength{got: Nat}
32 CrBadBlockSize{got: Nat}
33 CrNotBlockMultiple{len: Nat}
34 CrTooShort{len: Nat}
35 CrTooLong{len: Nat}
36 CrBadPadding{}
37 CrTagMismatch{}
38 CrBadOutputLength{got: Nat}
39 CrBadKey{}
40 CrBadPublicKey{}
41
42# A check, as a step of a Result block
43def CrError.check(ok: Bool, e: CrError) -> Result<&2, &2, CrError, Unit>:
44 match ok:
45 case True{}:
46 Done{Unit{}}
47 case False{}:
48 Fail{e}
49
50# A result with an algorithm's own error type, its error mapped onto CrError
51def CrError.lift(~E: Data, ~A: Data, ~f: E -> CrError, r: Result<&2, &2, E, A>) -> Result<&2, &2, CrError, A>:
52 match r:
53 case Fail{e}:
54 Fail{f(e)}
55 case Done{x}:
56 Done{x}