bend-osdev-aes Releases (1): 0.1.0.0 0xd84f91a0afea422022cbb4f397ca1abb indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-aes@0.1.0.0 Definitions (138, 1 to 100 shown): LAWS.aes_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/LAWS.bend&name=aes_round_trip) # AES (aes.bend): decryption undoes encryption, for every key (every value # of CmAesKey, whatever its number of rounds and round keys: AES-128, AES-192 # and AES-256 among them) and every block law aes_round_trip: for k: X.CmAesKey for +b: M.CmBlock {X.CmAes.decrypt(k, X.CmAes.encrypt(k, b)) == b : M.CmBlock} LAWS.aes128_fips197_c1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/LAWS.bend&name=aes128_fips197_c1) # FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block law aes128_fips197_c1: {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key128(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, M.CmError, B.Octets>} PROOF.sp.blk16g (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=sp.blk16g) def sp.blk16g(z0: U32, z1: U32, z2: U32, z3: U32, z4: U32, z5: U32, z6: U32, z7: U32, z8: U32, z9: U32, z10: U32, z11: U32, z12: U32, z13: U32, z14: U32, z15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}: PROOF.bx.ru32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=bx.ru32) def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}: PROOF.ap.nth (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.nth) def ap.nth(xs: List<&2, U32>, n: Nat) -> U32: PROOF.ap.pick (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.pick) def ap.pick(+n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, e: {xs == ys : List<&2, U32>}) -> {ap.nth(xs, n) == ap.nth(ys, n) : U32}: PROOF.ap.bridge (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.bridge) def ap.bridge(+c0: Bool, +c1: Bool, +c2: Bool, +c3: Bool, +c4: Bool, +c5: Bool, +c6: Bool, +c7: Bool, +c8: Bool, +c9: Bool, +c10: Bool, +c11: Bool, +c12: Bool, +c13: Bool, +c14: Bool, +c15: Bool, +c16: Bool, +c17: Bool, +c18: Bool, +c19: Bool, +c20: Bool, +c21: Bool, +c22: Bool, +c23: Bool, +c24: Bool, +c25: Bool, +c26: Bool, +c27: Bool, +c28: Bool, +c29: Bool, +c30: Bool, +c31: Bool) -> {U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}} == U32.and(255, U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}: PROOF.ap.e_sbl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.e_sbl) def ap.e_sbl(c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool) -> {SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}}) == U32.and(255, SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}})) : U32}: PROOF.ap.sbl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.sbl) def ap.sbl(+x: U32) -> {SB.sbox(U32.and(255, x)) == U32.and(255, SB.sbox(U32.and(255, x))) : U32}: PROOF.ap.e_sbi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.e_sbi) def ap.e_sbi(c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool) -> {X.aes.isbox(SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}})) == U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}} : U32}: PROOF.ap.sbi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.sbi) def ap.sbi(+x: U32) -> {X.aes.isbox(SB.sbox(U32.and(255, x))) == U32.and(255, x) : U32}: PROOF.ap.ex2.l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ex2.l) def ap.ex2.l(+x: U32) -> List<&2, U32>: PROOF.ap.ex2.r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ex2.r) def ap.ex2.r(+x: U32) -> List<&2, U32>: PROOF.ap.ex2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ex2) def ap.ex2(c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool) -> {ap.ex2.l(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}}) == ap.ex2.r(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}}) : List<&2, U32>}: PROOF.ap.xtb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xtb) def ap.xtb(+x: U32) -> {SB.xtime(U32.and(255, x)) == U32.and(255, SB.xtime(U32.and(255, x))) : U32}: PROOF.ap.m3b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m3b) def ap.m3b(+x: U32) -> {SB.mul3(U32.and(255, x)) == U32.and(255, SB.mul3(U32.and(255, x))) : U32}: PROOF.ap.m9b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m9b) def ap.m9b(+x: U32) -> {X.aes.m9(U32.and(255, x)) == G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)) : U32}: PROOF.ap.m11b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m11b) def ap.m11b(+x: U32) -> {X.aes.m11(U32.and(255, x)) == G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x)) : U32}: PROOF.ap.m13b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m13b) def ap.m13b(+x: U32) -> {X.aes.m13(U32.and(255, x)) == G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)) : U32}: PROOF.ap.m14b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m14b) def ap.m14b(+x: U32) -> {X.aes.m14(U32.and(255, x)) == G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)) : U32}: PROOF.ap.col00 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col00) def ap.col00(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, x))))) == U32.and(255, x) : U32}: PROOF.ap.col01 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col01) def ap.col01(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col02 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col02) def ap.col02(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col03 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col03) def ap.col03(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, x))))) == 0 : U32}: PROOF.ap.col10 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col10) def ap.col10(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, x))))) == 0 : U32}: PROOF.ap.col11 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col11) def ap.col11(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, x))))) == U32.and(255, x) : U32}: PROOF.ap.col12 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col12) def ap.col12(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col13 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col13) def ap.col13(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col20 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col20) def ap.col20(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col21 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col21) def ap.col21(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, x))))) == 0 : U32}: PROOF.ap.col22 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col22) def ap.col22(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, x))))) == U32.and(255, x) : U32}: PROOF.ap.col23 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col23) def ap.col23(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col30 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col30) def ap.col30(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col31 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col31) def ap.col31(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, x)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, x)))) == 0 : U32}: PROOF.ap.col32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col32) def ap.col32(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, x))))) == 0 : U32}: PROOF.ap.col33 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col33) def ap.col33(+x: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, x))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, x))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, x)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, x))))) == U32.and(255, x) : U32}: PROOF.ap.fin0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.fin0) def ap.fin0(+x: U32) -> {G.Gf8.add(G.Gf8.add(U32.and(255, x), 0), G.Gf8.add(0, 0)) == U32.and(255, x) : U32}: PROOF.ap.fin1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.fin1) def ap.fin1(+x: U32) -> {G.Gf8.add(G.Gf8.add(0, U32.and(255, x)), G.Gf8.add(0, 0)) == U32.and(255, x) : U32}: PROOF.ap.fin2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.fin2) def ap.fin2(+x: U32) -> {G.Gf8.add(G.Gf8.add(0, 0), G.Gf8.add(U32.and(255, x), 0)) == U32.and(255, x) : U32}: PROOF.ap.fin3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.fin3) def ap.fin3(+x: U32) -> {G.Gf8.add(G.Gf8.add(0, 0), G.Gf8.add(0, U32.and(255, x))) == U32.and(255, x) : U32}: PROOF.ap.bb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.bb) def ap.bb(+x: U32) -> {U32.and(255, U32.and(255, x)) == U32.and(255, x) : U32}: PROOF.ap.xorb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xorb) def ap.xorb(+a: U32, +b: U32) -> {U32.xor(U32.and(255, a), U32.and(255, b)) == U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))) : U32}: PROOF.ap.bylo (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.bylo) def ap.bylo(+x: U32) -> {B.byte(x) == U32.and(255, x) : U32}: PROOF.ap.isb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.isb) def ap.isb(+x: U32, +y: U32, +e: {x == U32.and(255, y) : U32}) -> {x == U32.and(255, x) : U32}: PROOF.ap.gx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.gx) def ap.gx(+k: U32, +u: U32, +v: U32) -> {G.Gf8.mul(G.Gf8.aes(), k, U32.xor(u, v)) == G.Gf8.mul(G.Gf8.aes(), k, G.Gf8.add(u, v)) : U32}: PROOF.ap.mx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mx) def ap.mx(+k: U32, +u: U32, +v: U32) -> {G.Gf8.mul(G.Gf8.aes(), k, U32.xor(u, v)) == G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, u), G.Gf8.mul(G.Gf8.aes(), k, v)) : U32}: PROOF.ap.glo (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.glo) def ap.glo(+k: U32, +x: U32) -> {G.Gf8.mul(G.Gf8.aes(), k, U32.and(255, x)) == G.Gf8.mul(G.Gf8.aes(), k, x) : U32}: PROOF.ap.m9 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m9) def ap.m9(+x: U32) -> {X.aes.m9(x) == G.Gf8.mul(G.Gf8.aes(), 9, x) : U32}: PROOF.ap.m11 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m11) def ap.m11(+x: U32) -> {X.aes.m11(x) == G.Gf8.mul(G.Gf8.aes(), 11, x) : U32}: PROOF.ap.m13 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m13) def ap.m13(+x: U32) -> {X.aes.m13(x) == G.Gf8.mul(G.Gf8.aes(), 13, x) : U32}: PROOF.ap.m14 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m14) def ap.m14(+x: U32) -> {X.aes.m14(x) == G.Gf8.mul(G.Gf8.aes(), 14, x) : U32}: PROOF.ap.xg0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xg0) def ap.xg0(m1: G.Gf8Bits, m2: G.Gf8Bits) -> {U32.xor(G.Gf8Bits.to(m1), G.Gf8Bits.to(m2)) == G.Gf8.add(G.Gf8Bits.to(m1), G.Gf8Bits.to(m2)) : U32}: PROOF.ap.xg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xg) def ap.xg(+k1: U32, +k2: U32, +u: U32, +v: U32) -> {U32.xor(G.Gf8.mul(G.Gf8.aes(), k1, u), G.Gf8.mul(G.Gf8.aes(), k2, v)) == G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k1, u), G.Gf8.mul(G.Gf8.aes(), k2, v)) : U32}: PROOF.ap.imixg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.imixg) def ap.imixg(+p: U32, +q: U32, +r: U32, +s: U32) -> {X.aes.imix0(p, q, r, s) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}: PROOF.ap.swap4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.swap4) def ap.swap4(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(a, b), G.Gf8.add(c, d)) == G.Gf8.add(G.Gf8.add(a, c), G.Gf8.add(b, d)) : U32}: PROOF.ap.trans (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.trans) def ap.trans(+t00: U32, +t01: U32, +t02: U32, +t03: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03)), G.Gf8.add(G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}: PROOF.ap.row (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.row) def ap.row(+k: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32) -> {G.Gf8.mul(G.Gf8.aes(), k, U32.xor(U32.xor(U32.xor(x1, x2), x3), x4)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))) : U32}: PROOF.ap.out0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out0) def ap.out0(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 11, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 9, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))))) == U32.and(255, a) : U32}: PROOF.ap.out1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out1) def ap.out1(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 11, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 9, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))))) == U32.and(255, b) : U32}: PROOF.ap.out2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out2) def ap.out2(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 11, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d))))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))))) == U32.and(255, c) : U32}: PROOF.ap.out3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out3) def ap.out3(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 11, U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d)))))) == U32.and(255, d) : U32}: PROOF.ap.mixc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mixc) def ap.mixc(+a: U32, +b: U32, +c: U32, +d: U32) -> {X.aes.imix_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) == TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)} : TT.Quad}: PROOF.ap.rowb0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rowb0) def ap.rowb0(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}: PROOF.ap.rowb1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rowb1) def ap.rowb1(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(U32.and(255, c))), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}: PROOF.ap.rowb2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rowb2) def ap.rowb2(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}: PROOF.ap.rowb3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rowb3) def ap.rowb3(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.mul3(U32.and(255, a))), U32.and(255, b))), U32.and(255, c))), U32.and(255, SB.xtime(U32.and(255, d))))) : U32}: PROOF.ap.mixcb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mixcb) def ap.mixcb(+a: U32, +b: U32, +c: U32, +d: U32) -> {A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)}) == X.aes.mask_w(A.mix_column(TT.W{U32.and(255, a), U32.and(255, b), U32.and(255, c), U32.and(255, d)})) : TT.Quad}: PROOF.ap.ark2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ark2) def ap.ark2(+m: TT.State, +k: TT.State) -> {A.add_round_key(A.add_round_key(m, k), k) == m : TT.State}: PROOF.ap.shift (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.shift) def ap.shift(+s: TT.State) -> {X.aes.inv_shift(A.shift_rows(s)) == s : TT.State}: PROOF.ap.shm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.shm) def ap.shm(+s: TT.State) -> {A.shift_rows(X.aes.mask(s)) == X.aes.mask(A.shift_rows(s)) : TT.State}: PROOF.ap.mm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mm) def ap.mm(+s: TT.State) -> {X.aes.mask(X.aes.mask(s)) == X.aes.mask(s) : TT.State}: PROOF.ap.subl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.subl) def ap.subl(+s: TT.State) -> {A.sub_bytes(X.aes.mask(s)) == X.aes.mask(A.sub_bytes(X.aes.mask(s))) : TT.State}: PROOF.ap.subi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.subi) def ap.subi(+s: TT.State) -> {X.aes.inv_sub(A.sub_bytes(X.aes.mask(s))) == X.aes.mask(s) : TT.State}: PROOF.ap.mixl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mixl) def ap.mixl(+s: TT.State) -> {A.mix_columns(X.aes.mask(s)) == X.aes.mask(A.mix_columns(X.aes.mask(s))) : TT.State}: PROOF.ap.mixi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.mixi) def ap.mixi(+s: TT.State) -> {X.aes.inv_mix(A.mix_columns(X.aes.mask(s))) == X.aes.mask(s) : TT.State}: PROOF.ap.arkl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.arkl) def ap.arkl(+m: TT.State, +k: TT.State) -> {A.add_round_key(X.aes.mask(m), X.aes.mask(k)) == X.aes.mask(A.add_round_key(X.aes.mask(m), X.aes.mask(k))) : TT.State}: PROOF.ap.ismask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.ismask) def ap.ismask(+x: TT.State, +v: TT.State, +e: {x == X.aes.mask(v) : TT.State}) -> {x == X.aes.mask(x) : TT.State}: PROOF.ap.round_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.round_inv) def ap.round_inv(+z: TT.State, +k: TT.State) -> {X.aes.inv_round(A.round(X.aes.mask(z), X.aes.mask(k)), X.aes.mask(k)) == X.aes.mask(z) : TT.State}: PROOF.ap.round_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.round_eq) def ap.round_eq(+z: TT.State, +k: TT.State) -> {A.round(X.aes.mask(z), X.aes.mask(k)) == X.aes.mask(A.add_round_key(X.aes.mask(A.mix_columns(X.aes.mask(A.shift_rows(A.sub_bytes(X.aes.mask(z)))))), X.aes.mask(k))) : TT.State}: PROOF.ap.round_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.round_out) def ap.round_out(+z: TT.State, +k: TT.State) -> {A.round(X.aes.mask(z), X.aes.mask(k)) == X.aes.mask(A.round(X.aes.mask(z), X.aes.mask(k))) : TT.State}: PROOF.ap.last_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.last_inv) def ap.last_inv(+z: TT.State, +k: TT.State) -> {X.aes.inv_last(A.last_round(X.aes.mask(z), X.aes.mask(k)), X.aes.mask(k)) == X.aes.mask(z) : TT.State}: PROOF.ap.last_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.last_eq) def ap.last_eq(+z: TT.State, +k: TT.State) -> {A.last_round(X.aes.mask(z), X.aes.mask(k)) == X.aes.mask(A.add_round_key(X.aes.mask(A.shift_rows(A.sub_bytes(X.aes.mask(z)))), X.aes.mask(k))) : TT.State}: PROOF.ap.last_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.last_out) def ap.last_out(+z: TT.State, +k: TT.State) -> {A.last_round(X.aes.mask(z), X.aes.mask(k)) == X.aes.mask(A.last_round(X.aes.mask(z), X.aes.mask(k))) : TT.State}: PROOF.ap.rounds_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rounds_out) def ap.rounds_out(n: Nat, ks: List<&2, TT.State>, +z: TT.State) -> {A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks)) == X.aes.mask(A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks))) : TT.State}: PROOF.ap.rounds_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.rounds_inv) def ap.rounds_inv(n: Nat, ks: List<&2, TT.State>, +z: TT.State) -> {X.aes.inv_rounds(n, X.aes.mask_keys(ks), A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks))) == X.aes.mask(z) : TT.State}: PROOF.ap.cipher_out (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.cipher_out) def ap.cipher_out(+nr: Nat, ks: List<&2, TT.State>, +s: TT.State) -> {A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks)) == X.aes.mask(A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks))) : TT.State}: PROOF.ap.cipher_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.cipher_inv) def ap.cipher_inv(+nr: Nat, ks: List<&2, TT.State>, +s: TT.State) -> {X.aes.inv_cipher(nr, X.aes.mask_keys(ks), A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks))) == X.aes.mask(s) : TT.State}: PROOF.ap.state_back (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.state_back) def ap.state_back(+e: TT.State) -> {X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(e)))) == X.aes.mask(e) : TT.State}: PROOF.ap.in_mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.in_mask) def ap.in_mask(+b: M.CmBlock) -> {X.aes.state_in(b) == X.aes.mask(X.aes.state_in(b)) : TT.State}: PROOF.ap.out_in (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out_in) def ap.out_in(+b: M.CmBlock) -> {X.aes.out(X.aes.mask(X.aes.state_in(b))) == b : M.CmBlock}: PROOF.ap.top (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.top) def ap.top(+nr: Nat, +ks: List<&2, TT.State>, +b: M.CmBlock) -> {X.aes.out(X.aes.inv_cipher(nr, X.aes.mask_keys(ks), X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(A.cipher(nr, X.aes.state_in(b), X.aes.mask_keys(ks)))))))) == b : M.CmBlock}: Aes.aes.xt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.xt) def aes.xt(+x: U32) -> U32: Aes.aes.gmul.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.gmul.go) def aes.gmul.go(n: Nat, +a: U32, +b: U32, p: U32) -> U32: Aes.aes.gmul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.gmul) def aes.gmul(+a: U32, +b: U32) -> U32: Aes.aes.inv.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv.go) # a := a^2 * x, n times: from a = x, six times gives x^127 def aes.inv.go(n: Nat, a: U32, +x: U32) -> U32: Aes.aes.inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv) # the multiplicative inverse, x^254 (0 for 0) def aes.inv(+x: U32) -> U32: Aes.aes.rotl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.rotl) def aes.rotl(+b: U32, +n: Nat) -> U32: Aes.aes.isbox (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.isbox) # the inverse S-box: the inverse affine map, then the inverse def aes.isbox(x: U32) -> U32: Aes.aes.mask_w (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask_w) # each byte's low 8 bits def aes.mask_w(w: T.Quad) -> T.Quad: Aes.aes.mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask) def aes.mask(s: T.State) -> T.State: More: https://jend.leeeet.dev/packages/bend-osdev-aes.txt?definitions_offset=100