bend-osdev-aead Releases (1): 0.1.0.0 0x7fac88c9586171e58e205ceb355ebac1 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-aead@0.1.0.0 Definitions (226, 1 to 100 shown): LAWS.aegis128_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=aegis128_round_trip) law aegis128_round_trip: for +k: G.AdAegisKey for +n: B.Octets for +a: B.Octets for +p: B.Octets {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(k, n, a, p), c => G.AdAegis128.open(k, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(k, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>} LAWS.aegis128_tamper (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=aegis128_tamper) # a tag of 16 bytes other than the one AEGIS-128 computes for the ciphertext # is refused, under a 16-byte nonce law aegis128_tamper: for +k: G.AdAegisKey for +n: B.Octets for +a: B.Octets for +c: B.Octets for +t: B.Octets for hn: {B.Octets.len(n) == 16n : Nat} for hl: {B.Octets.len(t) == 16n : Nat} for ht: {Ad.AdTag.is_eq(G.AdAegis128.tag_of(k, n, a, c), t) == False{} : Bool} {G.AdAegis128.open(k, n, a, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>} LAWS.aesround_rfc10032 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=aesround_rfc10032) # RFC 10032, Appendix A.1: AESRound(000102..0f, 101112..1f) = # 7a7b4e5638782546a8c0477a3b813f43 law aesround_rfc10032: {R.AdAes.round(R.AdAes.sbox(), R.AdBlk{66051, 67438087, 134810123, 202182159}, R.AdBlk{269554195, 336926231, 404298267, 471670303}) == R.AdBlk{2054901334, 947397958, 2831173498, 998326083} : R.AdBlk} LAWS.authenc_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=authenc_round_trip_if) law authenc_round_trip_if: for ~KE: Data for ~KM: Data for ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~mac: KM -> B.Octets -> B.Octets for ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets for ~tlen: Nat for +ke: KE for +km: KM for +iv: B.Octets … LAWS.authenc_tamper (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=authenc_tamper) # a tag of tlen bytes other than the computed one is refused, and the # cipher never runs law authenc_tamper: for ~KE: Data for ~KM: Data for ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~mac: KM -> B.Octets -> B.Octets for ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets for ~tlen: Nat for +k: Au.AdAuthencKey for +iv: B.Octets … LAWS.essiv_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=essiv_round_trip_if) law essiv_round_trip_if: for ~KD: Data for ~KS: Data for ~Blk: Data for ~enc: KS -> Blk -> Blk for ~blk_of: B.Octets -> Maybe<&2, Blk> for ~blk_to: Blk -> B.Octets for ~cenc: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~cdec: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for +kd: KD for +ks: KS … LAWS.essiv_aead_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=essiv_aead_round_trip_if) law essiv_aead_round_trip_if: for ~KD: Data for ~KS: Data for ~Blk: Data for ~enc: KS -> Blk -> Blk for ~blk_of: B.Octets -> Maybe<&2, Blk> for ~blk_to: Blk -> B.Octets for ~seal: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~open: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for +kd: KD for +ks: KS … LAWS.seqiv_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=seqiv_round_trip_if) law seqiv_round_trip_if: for ~KA: Data for ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~ivlen: Nat for +ka: KA for +salt: B.Octets for +seq: B.Octets for +aad: B.Octets for +p: B.Octets for hl: {B.Octets.len(Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)) == ivlen : Nat} … LAWS.echainiv_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&name=echainiv_round_trip_if) law echainiv_round_trip_if: for ~KA: Data for ~KC: Data for ~Blk: Data for ~enc: KC -> Blk -> Blk for ~blk_of: B.Octets -> Maybe<&2, Blk> for ~blk_to: Blk -> B.Octets for ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> for ~ivlen: Nat for +ka: KA … PROOF.byte_xor_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=byte_xor_byte) # BEGIN GENERATED by gen/proof.py: bits # the low byte of a XOR depends only on the low byte of its first operand def byte_xor_byte(z: U32, k: U32) -> {B.byte(U32.xor(z, k)) == B.byte(U32.xor(B.byte(z), k)) : U32}: PROOF.be32_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=be32_len) # a word's big-endian bytes are four def be32_len(v: U32) -> {4n == B.len(B.be32(v)) : Nat}: PROOF.byte_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=byte_byte) # a byte masked again is itself def byte_byte(h: U32) -> {B.byte(h) == B.byte(B.byte(h)) : U32}: PROOF.bool_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=bool_xx) def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}: PROOF.word_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=word_xx) def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}: PROOF.u32_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=u32_xx) def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}: PROOF.byte_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=byte_xx) def byte_xx(+h: U32, +k: U32) -> {B.byte(h) == B.byte(U32.xor(B.byte(U32.xor(h, k)), k)) : U32}: PROOF.nat_add_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_add_zero) def nat_add_zero(x: Nat) -> {x == Nat.add(x, 0n) : Nat}: PROOF.nat_add_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_add_succ) def nat_add_succ(x: Nat, +t: Nat) -> {1n+Nat.add(x, t) == Nat.add(x, 1n+t) : Nat}: PROOF.nat_sub_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_sub_zero) def nat_sub_zero(x: Nat) -> {x == Nat.sub(x, 0n) : Nat}: PROOF.nat_sub_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_sub_add) def nat_sub_add(+x: Nat, t: Nat) -> {x == Nat.sub(Nat.add(x, t), t) : Nat}: PROOF.nat_lt_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_lt_zero) def nat_lt_zero(x: Nat) -> {False{} == Nat.is_lt(x, 0n) : Bool}: PROOF.nat_lt_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_lt_add) def nat_lt_add(+x: Nat, t: Nat) -> {False{} == Nat.is_lt(Nat.add(x, t), t) : Bool}: PROOF.len_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=len_append) def len_append(xs: List<&2, U32>, +ys: List<&2, U32>) -> {Nat.add(B.len(xs), B.len(ys)) == B.len(B.append(xs, ys)) : Nat}: PROOF.mask_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=mask_len) def mask_len(xs: List<&2, U32>) -> {B.len(xs) == B.len(B.mask(xs)) : Nat}: PROOF.olen_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=olen_of) # the length of a list made Octets def olen_of(+xs: List<&2, U32>) -> {B.len(xs) == B.Octets.len(B.Octets.of_list(xs)) : Nat}: PROOF.olen_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=olen_append) # the length of a joined string def olen_append(+a: B.Octets, +b: B.Octets) -> {Nat.add(B.Octets.len(a), B.Octets.len(b)) == B.Octets.len(B.Octets.append(a, b)) : Nat}: PROOF.split_join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=split_join) # A ciphertext joined with its tag splits back into the two def split_join(+c: B.Octets, +t: B.Octets) -> {Done{Ad.AdSplit{c, t}} == Ad.AdTag.split(B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}: PROOF.is_eq_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=is_eq_refl) def is_eq_refl(+o: B.Octets) -> {True{} == Ad.AdTag.is_eq(o, o) : Bool}: PROOF.seqiv_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seqiv_r) def seqiv_r(~KA: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +ka: KA, +salt: B.Octets, +seq: B.Octets, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, hl: {B.Octets.len(iv) == ivlen : Nat}, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => open(ka, iv, B.Octets.append(aad, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r), c => Sq.AdSeqiv.open(~KA, ~open, ~ivlen, Sq.AdSeqivKey{ka, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.echainiv_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=echainiv_r) def echainiv_r(~KA: Data, ~KC: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +ka: KA, +kc: KC, +salt: B.Octets, +seq: B.Octets, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, hl: {B.Octets.len(iv) == ivlen : Nat}, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => open(ka, iv, B.Octets.append(aad, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r), c => Ec.AdEchainiv.open(~KA, ~KC, ~open, ~ivlen, Ec.AdEchainivKey{ka, kc, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.fit_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=fit_len) def fit_len(n: Nat, xs: List<&2, U32>) -> {B.len(Au.ad.au.fit(n, xs)) == n : Nat}: PROOF.au_tag_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=au_tag_len) # every tag has tlen bytes def au_tag_len(~KE: Data, ~KM: Data, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: Au.AdAuthencKey, +aad: B.Octets, +iv: B.Octets, +c: B.Octets) -> {B.Octets.len(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c)) == tlen : Nat}: PROOF.authenc_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=authenc_r) def authenc_r(~KE: Data, ~KM: Data, ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +ke: KE, +km: KM, +iv: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, Cr.CrError, B.Octets>, h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, r, c => dec(ke, iv, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, r) : Result<&2, &2, Cr.CrError, B.Octets>}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => Au.ad.au.sealed(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c), r), c => Au.AdAuthenc.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => Au.ad.au.sealed(~KE, ~KM, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, aad, iv, c), r)) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.ego_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=ego_ref) def ego_ref(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.eafter(xs, sb, r), G.ad.ae.rev(acc, G.ad.ae.eout(xs, sb, r))} == G.ad.ae.ego(xs, sb, r, acc) : G.AdAegisOut}: PROOF.dgo_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=dgo_ref) def dgo_ref(ys: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.dafter(ys, sb, r), G.ad.ae.rev(acc, G.ad.ae.dout(ys, sb, r))} == G.ad.ae.dgo(ys, sb, r, acc) : G.AdAegisOut}: PROOF.dec_enc_after (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=dec_enc_after) # decryption runs through the states encryption ran through, and gives the # message's bytes back def dec_enc_after(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eafter(xs, sb, r) == G.ad.ae.dafter(G.ad.ae.eout(xs, sb, r), sb, r) : G.AdAegisRun}: PROOF.dec_enc_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=dec_enc_out) def dec_enc_out(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {B.mask(xs) == G.ad.ae.dout(G.ad.ae.eout(xs, sb, r), sb, r) : List<&2, U32>}: PROOF.mask_eout (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=mask_eout) # the ciphertext's bytes are bytes, and as many as the message's def mask_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eout(xs, sb, r) == B.mask(G.ad.ae.eout(xs, sb, r)) : List<&2, U32>}: PROOF.len_eout (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=len_eout) def len_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {B.len(xs) == B.len(G.ad.ae.eout(xs, sb, r)) : Nat}: PROOF.blk_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=blk_len) # every tag has 16 bytes def blk_len(b: R.AdBlk) -> {16n == B.Octets.len(R.AdBlk.to_octets(b)) : Nat}: PROOF.tag_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=tag_len) def tag_len(st: G.AdAegisSt) -> {16n == B.Octets.len(G.ad.ae.tag(st)) : Nat}: PROOF.fin_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=fin_len) def fin_len(+sb: R.AdSbox, +st: G.AdAegisSt, +al: Nat, +ml: Nat) -> {16n == B.Octets.len(G.ad.ae.final(sb, st, al, ml)) : Nat}: PROOF.seal_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_ok) def seal_ok(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}) -> {Done{G.ad.ae.seal.go(kk, n, a, p)} == G.AdAegis128.seal(kk, n, a, p) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.seal_bad (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_bad) def seal_bad(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == False{} : Bool}) -> {Fail{Cr.CrBadNonceLength{B.Octets.len(n)}} == G.AdAegis128.seal(kk, n, a, p) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.open_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=open_ok) def open_ok(+kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +c: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}) -> {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, c), s => G.ad.ae.open.go(kk, n, a, s)) == G.AdAegis128.open(kk, n, a, c) : Result<&2, &2, Cr.CrError, B.Octets>}: PROOF.nonce_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nonce_ok) def nonce_ok(+n: B.Octets, hn: {B.Octets.len(n) == 16n : Nat}) -> {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}: PROOF.seal_go_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_go_eq) def seal_go_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {B.Octets.append(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) == G.ad.ae.seal.go(G.AdAegisKey{k, sb}, n, a, p) : B.Octets}: PROOF.tag_of_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=tag_of_eq) def tag_of_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)) == G.AdAegis128.tag_of(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : B.Octets}: PROOF.plain_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=plain_eq) def plain_eq(+k: R.AdBlk, +sb: R.AdSbox, +n: B.Octets, +a: B.Octets, +p: B.Octets) -> {p == G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a)))) : B.Octets}: PROOF.aegis_rt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=aegis_rt) def aegis_rt(b: Bool, +kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}, e2: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(kk, n, a, p), c => G.AdAegis128.open(kk, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(kk, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>}: Aead.AdSplit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdSplit) # A ciphertext and its tag, split from the bytes of both (the tag the last # tlen bytes; CrTooShort for fewer than tlen bytes) type AdSplit is Data: AdSplit{c: B.Octets, t: B.Octets} Aead.ad.split.pick (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=ad.split.pick) def ad.split.pick(short: Bool, +tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>: Aead.AdTag.split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.split) def AdTag.split(+tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>: Aead.AdTag.join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.join) # the ciphertext with its tag appended def AdTag.join(c: B.Octets, t: B.Octets) -> B.Octets: Aead.AdTag.is_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.is_eq) # Whether two tags are equal, every byte compared (no early exit) def AdTag.is_eq(a: B.Octets, b: B.Octets) -> Bool: Aegis128.AdAegisSt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegisSt) # The state (internal) type AdAegisSt is Data: AdAegisSt{s0: R.AdBlk, s1: R.AdBlk, s2: R.AdBlk, s3: R.AdBlk, s4: R.AdBlk} Aegis128.ad.ae.update (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.update) def ad.ae.update(+sb: R.AdSbox, st: AdAegisSt, +m: R.AdBlk) -> AdAegisSt: Aegis128.ad.ae.z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.z) # the keystream block S1 xor S4 xor (S2 and S3) def ad.ae.z(st: AdAegisSt) -> R.AdBlk: Aegis128.ad.ae.c0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.c0) # const0 and const1 (the Fibonacci sequence mod 256) def ad.ae.c0() -> R.AdBlk: Aegis128.ad.ae.c1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.c1) def ad.ae.c1() -> R.AdBlk: Aegis128.ad.ae.init.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.init.go) def ad.ae.init.go(n: Nat, +sb: R.AdSbox, +k: R.AdBlk, +kiv: R.AdBlk, st: AdAegisSt) -> AdAegisSt: Aegis128.ad.ae.init (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.init) def ad.ae.init(+sb: R.AdSbox, +k: R.AdBlk, +iv: R.AdBlk) -> AdAegisSt: Aegis128.ad.ae.absorb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.absorb) # the state after the associated data's 16-byte pieces (the last # zero-padded) def ad.ae.absorb(+sb: R.AdSbox, ps: List<&2, List<&2, U32>>, st: AdAegisSt) -> AdAegisSt: Aegis128.AdAegisRun (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegisRun) # The message, a byte at a time (internal): the state, the keystream bytes # left of the current block, the current block's plaintext bytes so far # (last first) and how many type AdAegisRun is Data: AdAegisRun{st: AdAegisSt, zs: List<&2, U32>, buf: List<&2, U32>, n: Nat} Aegis128.ad.ae.run0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.run0) def ad.ae.run0(+st: AdAegisSt) -> AdAegisRun: Aegis128.ad.ae.rev (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.rev) def ad.ae.rev(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>: Aegis128.ad.ae.tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.tail) def ad.ae.tail(xs: List<&2, U32>) -> List<&2, U32>: Aegis128.ad.ae.head (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.head) def ad.ae.head(xs: List<&2, U32>) -> U32: Aegis128.ad.ae.step.pick (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.step.pick) def ad.ae.step.pick(full: Bool, +sb: R.AdSbox, st: AdAegisSt, zs: List<&2, U32>, +buf: List<&2, U32>, +n: Nat) -> AdAegisRun: Aegis128.ad.ae.step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.step) # the run after the plaintext byte x def ad.ae.step(+sb: R.AdSbox, r: AdAegisRun, x: U32) -> AdAegisRun: Aegis128.ad.ae.zhead (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.zhead) # the next keystream byte def ad.ae.zhead(r: AdAegisRun) -> U32: Aegis128.ad.ae.flush.pick (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.flush.pick) def ad.ae.flush.pick(empty: Bool, +sb: R.AdSbox, st: AdAegisSt, buf: List<&2, U32>) -> AdAegisSt: Aegis128.ad.ae.flush (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.flush) # the state after the last, short block (zero-padded) def ad.ae.flush(+sb: R.AdSbox, r: AdAegisRun) -> AdAegisSt: Aegis128.ad.ae.eout (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.eout) def ad.ae.eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun) -> List<&2, U32>: Aegis128.ad.ae.eafter (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.eafter) def ad.ae.eafter(xs: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun) -> AdAegisRun: Aegis128.ad.ae.dout (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.dout) def ad.ae.dout(ys: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun) -> List<&2, U32>: Aegis128.ad.ae.dafter (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.dafter) def ad.ae.dafter(ys: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun) -> AdAegisRun: Aegis128.AdAegisOut (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegisOut) # The loops that run (tail calls): the run after the bytes, and the output type AdAegisOut is Data: AdAegisOut{r: AdAegisRun, out: List<&2, U32>} Aegis128.ad.ae.ego (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.ego) def ad.ae.ego(xs: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun, acc: List<&2, U32>) -> AdAegisOut: Aegis128.ad.ae.dgo (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.dgo) def ad.ae.dgo(ys: List<&2, U32>, +sb: R.AdSbox, +r: AdAegisRun, acc: List<&2, U32>) -> AdAegisOut: Aegis128.ad.ae.fin.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.fin.go) # Finalization: the tag from the state after the message, and the lengths def ad.ae.fin.go(n: Nat, +sb: R.AdSbox, +tmp: R.AdBlk, st: AdAegisSt) -> AdAegisSt: Aegis128.ad.ae.tag (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.tag) def ad.ae.tag(st: AdAegisSt) -> B.Octets: Aegis128.ad.ae.w64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.w64) # n as a 64-bit word, counted up (W64.from_nat divides by 2^32, a literal # the checker would expand when a proof meets it) def ad.ae.w64(n: Nat, acc: W.W64) -> W.W64: Aegis128.ad.ae.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.bits) # the bit length of n bytes as 8 little-endian bytes def ad.ae.bits(n: Nat) -> List<&2, U32>: Aegis128.ad.ae.s3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.s3) def ad.ae.s3(st: AdAegisSt) -> R.AdBlk: Aegis128.ad.ae.final (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.final) def ad.ae.final(+sb: R.AdSbox, +st: AdAegisSt, +alen: Nat, +mlen: Nat) -> B.Octets: Aegis128.AdAegisKey (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegisKey) # An AEGIS-128 key: the key block and the AES S-box (opaque) type AdAegisKey is Data: AdAegisKey{k: R.AdBlk, sb: R.AdSbox} Aegis128.ad.ae.key.pick (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.key.pick) def ad.ae.key.pick(ok: Bool, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdAegisKey>: Aegis128.ad.ae.key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.key) def ad.ae.key(+o: B.Octets) -> Result<&2, &2, Cr.CrError, AdAegisKey>: Aegis128.AdAegis128.key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegis128.key) # a 16-byte key def AdAegis128.key(o: B.Octets) -> Result<&2, &2, Cr.CrError, AdAegisKey>: Aegis128.ad.ae.start (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.start) # the run before the message: the state after the key, nonce and associated # data def ad.ae.start(+sb: R.AdSbox, +k: R.AdBlk, +nonce: B.Octets, +aad: B.Octets) -> AdAegisRun: Aegis128.ad.ae.sealed (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.sealed) def ad.ae.sealed(+sb: R.AdSbox, +aad: B.Octets, +p: B.Octets, o: AdAegisOut) -> B.Octets: Aegis128.ad.ae.seal.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.seal.go) def ad.ae.seal.go(kk: AdAegisKey, +nonce: B.Octets, +aad: B.Octets, +p: B.Octets) -> B.Octets: Aegis128.ad.ae.nonce (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.nonce) def ad.ae.nonce(+nonce: B.Octets) -> Result<&2, &2, Cr.CrError, Unit>: Aegis128.ad.ae.seal (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.seal) def ad.ae.seal(+kk: AdAegisKey, +nonce: B.Octets, +aad: B.Octets, +p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: Aegis128.AdAegis128.seal (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegis128.seal) # p sealed under a 16-byte nonce: the ciphertext and the 16-byte tag def AdAegis128.seal(kk: AdAegisKey, nonce: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: Aegis128.ad.ae.tag_of.of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.tag_of.of) def ad.ae.tag_of.of(+sb: R.AdSbox, +aad: B.Octets, +c: B.Octets, o: AdAegisOut) -> B.Octets: Aegis128.ad.ae.tag_of.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.tag_of.go) def ad.ae.tag_of.go(kk: AdAegisKey, +nonce: B.Octets, +aad: B.Octets, +c: B.Octets) -> B.Octets: Aegis128.AdAegis128.tag_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegis128.tag_of) # The tag open expects for the ciphertext c (without its tag) def AdAegis128.tag_of(kk: AdAegisKey, +nonce: B.Octets, +aad: B.Octets, +c: B.Octets) -> B.Octets: Aegis128.ad.ae.plain.of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.plain.of) def ad.ae.plain.of(o: AdAegisOut) -> B.Octets: More: https://jend.leeeet.dev/packages/bend-osdev-aead.txt?definitions_offset=100