bend-osdev-gf Releases (3): 0.1.2.0 0x7a66255b2e354c73838e88d45f7d1593 invalid https://jend.leeeet.dev/files.txt?path=bend-osdev-gf@0.1.2.0 expected a package named bend-osdev-word64@0.1.1.1 on https://hub.bend-lang.com At https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&start_line=12. Files that do not load: LAWS.bend, PROOF.bend, check.bend, gf128.bend, package.bend. 0.1.1.0 0x783d0fad62351acb750d929ab748bb90 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-gf@0.1.1.0 0.1.0.0 0xeaa58f996c50eb57673f63c368c1de92 unindexed https://jend.leeeet.dev/files.txt?path=bend-osdev-gf@0.1.0.0 Definitions (522, 1 to 100 shown): LAWS.mul_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_comm) law mul_comm: for +f: G.Gf8Field for +a: U32 for +b: U32 {G.Gf8.mul(f, a, b) == G.Gf8.mul(f, b, a) : U32} LAWS.mul_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_assoc) law mul_assoc: for +f: G.Gf8Field for +a: U32 for +b: U32 for +c: U32 {G.Gf8.mul(f, G.Gf8.mul(f, a, b), c) == G.Gf8.mul(f, a, G.Gf8.mul(f, b, c)) : U32} LAWS.mul_distrib (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_distrib) law mul_distrib: for +f: G.Gf8Field for +a: U32 for +b: U32 for +c: U32 {G.Gf8.mul(f, a, G.Gf8.add(b, c)) == G.Gf8.add(G.Gf8.mul(f, a, b), G.Gf8.mul(f, a, c)) : U32} LAWS.mul_one (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_one) law mul_one: for +f: G.Gf8Field for +a: U32 {G.Gf8.mul(f, 1, a) == G.Gf8.elt(a) : U32} LAWS.mul_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_zero) law mul_zero: for +f: G.Gf8Field for +a: U32 {G.Gf8.mul(f, 0, a) == 0 : U32} LAWS.xtime_mul_x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=xtime_mul_x) law xtime_mul_x: for +f: G.Gf8Field for +a: U32 {G.Gf8.xtime(f, a) == G.Gf8.mul(f, 2, a) : U32} LAWS.add_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=add_comm) law add_comm: for +a: U32 for +b: U32 {G.Gf8.add(a, b) == G.Gf8.add(b, a) : U32} LAWS.add_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=add_assoc) law add_assoc: for +a: U32 for +b: U32 for +c: U32 {G.Gf8.add(G.Gf8.add(a, b), c) == G.Gf8.add(a, G.Gf8.add(b, c)) : U32} LAWS.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=add_zero) law add_zero: for +a: U32 {G.Gf8.add(a, 0) == G.Gf8.elt(a) : U32} LAWS.add_self (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=add_self) law add_self: for +a: U32 {G.Gf8.add(a, a) == 0 : U32} LAWS.pow_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=pow_add) law pow_add: for +f: G.Gf8Field for +a: U32 for +m: Nat for +n: Nat {G.Gf8.pow(f, a, Nat.add(m, n)) == G.Gf8.mul(f, G.Gf8.pow(f, a, m), G.Gf8.pow(f, a, n)) : U32} LAWS.mul_inv_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_inv_aes) law mul_inv_aes: for +a: U32 for nz: {G.Gf8.is_zero(a) == False{} : Bool} {G.Gf8.mul(G.Gf8.aes(), a, G.Gf8.inv(G.Gf8.aes(), a)) == 1 : U32} LAWS.mul_inv_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=mul_inv_rs) law mul_inv_rs: for +a: U32 for nz: {G.Gf8.is_zero(a) == False{} : Bool} {G.Gf8.mul(G.Gf8.rs(), a, G.Gf8.inv(G.Gf8.rs(), a)) == 1 : U32} LAWS.exp_log_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=exp_log_aes) law exp_log_aes: for +a: U32 for nz: {G.Gf8.is_zero(a) == False{} : Bool} {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), a)) == G.Gf8.elt(a) : U32} LAWS.exp_log_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=exp_log_rs) law exp_log_rs: for +a: U32 for nz: {G.Gf8.is_zero(a) == False{} : Bool} {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), a)) == G.Gf8.elt(a) : U32} LAWS.inv_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=inv_zero) law inv_zero: for +f: G.Gf8Field {G.Gf8.inv(f, 0) == 0 : U32} LAWS.v_aes_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_aes_mul) law v_aes_mul: {G.Gf8.mul(G.Gf8.aes(), 87, 131) == 193 : U32} LAWS.v_aes_mul13 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_aes_mul13) law v_aes_mul13: {G.Gf8.mul(G.Gf8.aes(), 87, 19) == 254 : U32} LAWS.v_aes_xtime (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_aes_xtime) law v_aes_xtime: {[G.Gf8.xtime(G.Gf8.aes(), 87), G.Gf8.mul(G.Gf8.aes(), 87, 4), G.Gf8.mul(G.Gf8.aes(), 87, 8), G.Gf8.mul(G.Gf8.aes(), 87, 16)] == [174, 71, 142, 7] : List<&2, U32>} LAWS.v_aes_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_aes_inv) # the inverse of {53} is {ca} (the AES S-box's first step) law v_aes_inv: {G.Gf8.inv(G.Gf8.aes(), 83) == 202 : U32} LAWS.v_rs_x8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_rs_x8) # in the Reed-Solomon field x^8 = x^4 + x^3 + x^2 + 1 = 0x1D, and x has # order 255 (x^255 = 1): x generates the field law v_rs_x8: {G.Gf8.exp(G.Gf8.rs(), 8n) == 29 : U32} LAWS.v_rs_order (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_rs_order) law v_rs_order: {G.Gf8.exp(G.Gf8.rs(), 255n) == 1 : U32} LAWS.v_div (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_div) law v_div: {G.Gf8.mul(G.Gf8.aes(), G.Gf8.div(G.Gf8.aes(), 87, 131), 131) == 87 : U32} LAWS.tab_mul_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_mul_aes) law tab_mul_aes: for +a: U32 for +b: U32 {T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), a, b) == (T.Gf8Tab.new(G.Gf8.aes()), G.Gf8.mul(G.Gf8.aes(), a, b)) : T.Gf8Tab & U32} LAWS.tab_mul_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_mul_rs) law tab_mul_rs: for +a: U32 for +b: U32 {T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), a, b) == (T.Gf8Tab.new(G.Gf8.rs()), G.Gf8.mul(G.Gf8.rs(), a, b)) : T.Gf8Tab & U32} LAWS.tab_log_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_log_aes) law tab_log_aes: for +a: U32 {T.Gf8Tab.log(T.Gf8Tab.new(G.Gf8.aes()), a) == (T.Gf8Tab.new(G.Gf8.aes()), U32.from_nat(G.Gf8.log(G.Gf8.aes(), a))) : T.Gf8Tab & U32} LAWS.tab_log_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_log_rs) law tab_log_rs: for +a: U32 {T.Gf8Tab.log(T.Gf8Tab.new(G.Gf8.rs()), a) == (T.Gf8Tab.new(G.Gf8.rs()), U32.from_nat(G.Gf8.log(G.Gf8.rs(), a))) : T.Gf8Tab & U32} LAWS.tab_exp_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_exp_aes) law tab_exp_aes: for +i: U32 for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool} {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.aes()), i) == (T.Gf8Tab.new(G.Gf8.aes()), G.Gf8.exp(G.Gf8.aes(), U32.to_nat(i))) : T.Gf8Tab & U32} LAWS.tab_exp_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=tab_exp_rs) law tab_exp_rs: for +i: U32 for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool} {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.rs()), i) == (T.Gf8Tab.new(G.Gf8.rs()), G.Gf8.exp(G.Gf8.rs(), U32.to_nat(i))) : T.Gf8Tab & U32} LAWS.witness_tab_exp (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=witness_tab_exp) # a witness for tab_exp's hypothesis: the last entry, 509 law witness_tab_exp: {Nat.is_lt(U32.to_nat(509), 510n) == True{} : Bool} LAWS.v_tab_mul_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_tab_mul_aes) law v_tab_mul_aes: {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.aes()), 87, 131)) == 193 : U32} LAWS.v_tab_inv_aes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_tab_inv_aes) law v_tab_inv_aes: {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.inv(T.Gf8Tab.new(G.Gf8.aes()), 83)) == 202 : U32} LAWS.v_tab_mul_rs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_tab_mul_rs) law v_tab_mul_rs: {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 200, 77)) == G.Gf8.mul(G.Gf8.rs(), 200, 77) : U32} LAWS.v_tab_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_tab_zero) law v_tab_zero: {Pair.snd(T.Gf8Tab, U32, T.Gf8Tab.mul(T.Gf8Tab.new(G.Gf8.rs()), 0, 77)) == 0 : U32} LAWS.v_gcm_x1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gcm_x1) # 5e2ec746917062882c85b0685353deb7 law v_gcm_x1: {H.Gf128.mul_gcm(H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(1580123974, 2440061576, 746958952, 1398005431) : H.Gf128} LAWS.v_gcm_ghash (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gcm_ghash) # f38cbb1ad69223dcc3457ae5b6b0f885 (one block of C, then the lengths: 0 bits # of A, 128 of C) law v_gcm_ghash: {H.Gf128.ghash(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558), [H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960), H.Gf128.of_words(0, 0, 0, 128)]) == H.Gf128.of_words(4086086426, 3599901660, 3276110565, 3065051269) : H.Gf128} LAWS.v_cmac_k1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_cmac_k1) # L = 7df76b0c1ab899b33e42f047b91b546f, K1 = fbeed618357133667c85e08f7236a8de, # K2 = f7ddac306ae266ccf90bc11ee46d513b law v_cmac_k1: {H.Gf128.double_be(H.Gf128.of_words(2113366796, 448305587, 1044574279, 3105576047)) == H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798) : H.Gf128} LAWS.v_cmac_k2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_cmac_k2) law v_cmac_k2: {H.Gf128.double_be(H.Gf128.of_words(4226733592, 896611174, 2089148559, 1916184798)) == H.Gf128.of_words(4158499888, 1793222348, 4178297118, 3832369467) : H.Gf128} LAWS.v_gcm_mul_x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gcm_mul_x) # GCM's x is the block 0x40 00 .. 00: mul_x_gcm is multiplication by it law v_gcm_mul_x: {H.Gf128.mul_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1073741824, 0, 0, 0)) == H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128} LAWS.v_gcm_mul_x_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gcm_mul_x_value) law v_gcm_mul_x_value: {H.Gf128.mul_x_gcm(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(9544371, 3302352631, 4285422924, 992614664) : H.Gf128} LAWS.v_be_mul_x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_be_mul_x) # in big-endian order x is the number 2: double_be is multiplication by it law v_be_mul_x: {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(0, 0, 0, 2)) == H.Gf128.double_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) : H.Gf128} LAWS.v_be_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_be_mul) law v_be_mul: {H.Gf128.mul_be(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328), H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)) == H.Gf128.of_words(780021721, 1580971822, 2568813327, 4049188832) : H.Gf128} LAWS.v_xts_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_xts_wrap) # XTS: the top bit of byte 15 wraps round as 0x87 into byte 0 law v_xts_wrap: {H.Gf128.double_le(H.Gf128.of_words(0, 0, 0, 255)) == H.Gf128.of_words(2264924160, 0, 0, 254) : H.Gf128} LAWS.v_xts_double (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_xts_double) law v_xts_double: {H.Gf128.double_le(H.Gf128.of_words(19088743, 2309737967, 4275878552, 1985229328)) == H.Gf128.of_words(38177486, 307731423, 4256789809, 3987235872) : H.Gf128} LAWS.v_gf128_octets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gf128_octets) law v_gf128_octets: {H.Gf128.of_octets(H.Gf128.to_octets(H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558))) == Done{H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)} : Result<&2, &2, H.Gf128Error, H.Gf128>} LAWS.v_gf128_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_gf128_short) law v_gf128_short: {H.Gf128.of_octets(B.Octets.zeros(15n)) == Fail{H.Gf128BadLength{15n}} : Result<&2, &2, H.Gf128Error, H.Gf128>} LAWS.gfm_add_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=gfm_add_comm) law gfm_add_comm: for +f: M.GfmField for +a: U32 for +b: U32 {M.Gfm.add(f, a, b) == M.Gfm.add(f, b, a) : U32} LAWS.gfm_mul_comm_gf16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=gfm_mul_comm_gf16) law gfm_mul_comm_gf16: for +a: U32 for +b: U32 {M.Gfm.mul(M.Gfm.gf16(), a, b) == M.Gfm.mul(M.Gfm.gf16(), b, a) : U32} LAWS.gfm_mul_inv_gf16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=gfm_mul_inv_gf16) law gfm_mul_inv_gf16: for +a: U32 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf16(), a), 0) == False{} : Bool} {M.Gfm.mul(M.Gfm.gf16(), a, M.Gfm.inv(M.Gfm.gf16(), a)) == 1 : U32} LAWS.gfm_mul_inv_gf32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=gfm_mul_inv_gf32) law gfm_mul_inv_gf32: for +a: U32 for nz: {U32.is_eq(M.Gfm.elt(M.Gfm.gf32(), a), 0) == False{} : Bool} {M.Gfm.mul(M.Gfm.gf32(), a, M.Gfm.inv(M.Gfm.gf32(), a)) == 1 : U32} LAWS.v_bch13_x13 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch13_x13) law v_bch13_x13: {M.Gfm.exp(M.Gfm.bch13(), 13) == 27 : U32} LAWS.v_bch13_order (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch13_order) law v_bch13_order: {M.Gfm.exp(M.Gfm.bch13(), 8191) == 1 : U32} LAWS.v_bch13_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch13_mul) law v_bch13_mul: {M.Gfm.mul(M.Gfm.bch13(), 1234, 5678) == 4994 : U32} LAWS.v_bch13_inv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch13_inv) law v_bch13_inv: {M.Gfm.inv(M.Gfm.bch13(), 1234) == 2297 : U32} LAWS.v_bch13_log (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch13_log) law v_bch13_log: {M.Gfm.log(M.Gfm.bch13(), 1664) == 100 : U32} LAWS.v_bch14_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/LAWS.bend&name=v_bch14_mul) law v_bch14_mul: {M.Gfm.mul(M.Gfm.bch14(), 12345, 6789) == 6882 : U32} PROOF.bx_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bx_comm) def bx_comm(+a: Bool, +b: Bool) -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}: PROOF.bx_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bx_assoc) def bx_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}: PROOF.bx_zr (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bx_zr) def bx_zr(+a: Bool) -> {Bool.xor(a, False{}) == a : Bool}: PROOF.bx_self (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bx_self) def bx_self(+a: Bool) -> {Bool.xor(a, a) == False{} : Bool}: PROOF.bx_swap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bx_swap) def bx_swap(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> {Bool.xor(Bool.xor(a, b), Bool.xor(c, d)) == Bool.xor(Bool.xor(a, c), Bool.xor(b, d)) : Bool}: PROOF.band_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=band_xor) def band_xor(+a: Bool, +b: Bool, +q: Bool) -> {Bool.and(Bool.xor(a, b), q) == Bool.xor(Bool.and(a, q), Bool.and(b, q)) : Bool}: PROOF.blin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=blin) def blin(+a: Bool, +b: Bool, +u: Bool, +v: Bool, +q: Bool) -> {Bool.xor(Bool.xor(a, b), Bool.and(Bool.xor(u, v), q)) == Bool.xor(Bool.xor(a, Bool.and(u, q)), Bool.xor(b, Bool.and(v, q))) : Bool}: PROOF.rb_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rb_eq) def rb_eq(-a0: Bool, -a1: Bool, -a2: Bool, -a3: Bool, -a4: Bool, -a5: Bool, -a6: Bool, -a7: Bool, -c0: Bool, -c1: Bool, -c2: Bool, -c3: Bool, -c4: Bool, -c5: Bool, -c6: Bool, -c7: Bool, e0: {a0 == c0 : Bool}, e1: {a1 == c1 : Bool}, e2: {a2 == c2 : Bool}, e3: {a3 == c3 : Bool}, e4: {a4 == c4 : Bool}, e5: {a5 == c5 : Bool}, e6: {a6 == c6 : Bool}, e7: {a7 == c7 : Bool}) -> {G.Gf8Bits{a0, a1, a2, a3, a4, a5, a6, a7} == G.Gf8Bits{c0, c1, c2, c3, c4, c5, c6, c7} : G.Gf8Bits}: PROOF.rx_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_comm) def rx_comm(+a: G.Gf8Bits, +b: G.Gf8Bits) -> {G.Gf8Bits.xor(a, b) == G.Gf8Bits.xor(b, a) : G.Gf8Bits}: PROOF.rx_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_assoc) def rx_assoc(+a: G.Gf8Bits, +b: G.Gf8Bits, +c: G.Gf8Bits) -> {G.Gf8Bits.xor(G.Gf8Bits.xor(a, b), c) == G.Gf8Bits.xor(a, G.Gf8Bits.xor(b, c)) : G.Gf8Bits}: PROOF.rx_zr (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_zr) def rx_zr(+a: G.Gf8Bits) -> {G.Gf8Bits.xor(a, G.Gf8Bits.zero()) == a : G.Gf8Bits}: PROOF.rx_self (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_self) def rx_self(+a: G.Gf8Bits) -> {G.Gf8Bits.xor(a, a) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.rx_swap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_swap) def rx_swap(+a: G.Gf8Bits, +b: G.Gf8Bits, +c: G.Gf8Bits, +d: G.Gf8Bits) -> {G.Gf8Bits.xor(G.Gf8Bits.xor(a, b), G.Gf8Bits.xor(c, d)) == G.Gf8Bits.xor(G.Gf8Bits.xor(a, c), G.Gf8Bits.xor(b, d)) : G.Gf8Bits}: PROOF.rx_zl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=rx_zl) def rx_zl(+a: G.Gf8Bits) -> {G.Gf8Bits.xor(G.Gf8Bits.zero(), a) == a : G.Gf8Bits}: PROOF.x_lin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=x_lin) def x_lin(+u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.x(G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.x(u, p), G.Gf8Bits.x(v, p)) : G.Gf8Bits}: PROOF.x_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=x_zero) def x_zero(+p: G.Gf8Bits) -> {G.Gf8Bits.x(G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.sel_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=sel_xor) def sel_xor(+t: Bool, +u: G.Gf8Bits, +v: G.Gf8Bits) -> {G.Gf8Bits.sel(t, G.Gf8Bits.xor(u, v)) == G.Gf8Bits.xor(G.Gf8Bits.sel(t, u), G.Gf8Bits.sel(t, v)) : G.Gf8Bits}: PROOF.sel_txor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=sel_txor) def sel_txor(+s: Bool, +t: Bool, +b: G.Gf8Bits) -> {G.Gf8Bits.sel(Bool.xor(s, t), b) == G.Gf8Bits.xor(G.Gf8Bits.sel(s, b), G.Gf8Bits.sel(t, b)) : G.Gf8Bits}: PROOF.x_sel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=x_sel) def x_sel(+t: Bool, +u: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.x(G.Gf8Bits.sel(t, u), p) == G.Gf8Bits.sel(t, G.Gf8Bits.x(u, p)) : G.Gf8Bits}: PROOF.step_lin_b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=step_lin_b) def step_lin_b(+t: Bool, +A: G.Gf8Bits, +C: G.Gf8Bits, +u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.step(t, G.Gf8Bits.xor(A, C), G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.step(t, A, u, p), G.Gf8Bits.step(t, C, v, p)) : G.Gf8Bits}: PROOF.horner_lin_b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=horner_lin_b) def horner_lin_b(ts: List<&2, Bool>, +A: G.Gf8Bits, +C: G.Gf8Bits, +u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(ts, G.Gf8Bits.xor(A, C), G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.horner(ts, A, u, p), G.Gf8Bits.horner(ts, C, v, p)) : G.Gf8Bits}: PROOF.m_lin_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_lin_r) def m_lin_r(+a: G.Gf8Bits, +u: G.Gf8Bits, +v: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(a, G.Gf8Bits.xor(u, v), p) == G.Gf8Bits.xor(G.Gf8Bits.mul(a, u, p), G.Gf8Bits.mul(a, v, p)) : G.Gf8Bits}: PROOF.GfPb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=GfPb) # pairs of bits, for the product's linearity in its first factor type GfPb is Data: GfPb{s: Bool, t: Bool} PROOF.pl.x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=pl.x) def pl.x(ps: List<&2, GfPb>) -> List<&2, Bool>: PROOF.pl.l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=pl.l) def pl.l(ps: List<&2, GfPb>) -> List<&2, Bool>: PROOF.pl.r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=pl.r) def pl.r(ps: List<&2, GfPb>) -> List<&2, Bool>: PROOF.step_lin_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=step_lin_a) def step_lin_a(+s: Bool, +t: Bool, +A: G.Gf8Bits, +C: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.step(Bool.xor(s, t), G.Gf8Bits.xor(A, C), b, p) == G.Gf8Bits.xor(G.Gf8Bits.step(s, A, b, p), G.Gf8Bits.step(t, C, b, p)) : G.Gf8Bits}: PROOF.horner_lin_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=horner_lin_a) def horner_lin_a(ps: List<&2, GfPb>, +A: G.Gf8Bits, +C: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(pl.x(ps), G.Gf8Bits.xor(A, C), b, p) == G.Gf8Bits.xor(G.Gf8Bits.horner(pl.l(ps), A, b, p), G.Gf8Bits.horner(pl.r(ps), C, b, p)) : G.Gf8Bits}: PROOF.m_lin_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_lin_l) def m_lin_l(+s: G.Gf8Bits, +t: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.xor(s, t), b, p) == G.Gf8Bits.xor(G.Gf8Bits.mul(s, b, p), G.Gf8Bits.mul(t, b, p)) : G.Gf8Bits}: PROOF.step_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=step_zero) def step_zero(+t: Bool, +p: G.Gf8Bits) -> {G.Gf8Bits.step(t, G.Gf8Bits.zero(), G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.horner_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=horner_zero) def horner_zero(ts: List<&2, Bool>, +p: G.Gf8Bits) -> {G.Gf8Bits.horner(ts, G.Gf8Bits.zero(), G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.m_zero_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_zero_r) def m_zero_r(+a: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(a, G.Gf8Bits.zero(), p) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.m_zero_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_zero_l) def m_zero_l(+b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.zero(), b, p) == G.Gf8Bits.zero() : G.Gf8Bits}: PROOF.m_sel_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_sel_l) def m_sel_l(+t: Bool, +a: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(G.Gf8Bits.sel(t, a), b, p) == G.Gf8Bits.sel(t, G.Gf8Bits.mul(a, b, p)) : G.Gf8Bits}: PROOF.m_sel_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=m_sel_r) def m_sel_r(+t: Bool, +a: G.Gf8Bits, +b: G.Gf8Bits, +p: G.Gf8Bits) -> {G.Gf8Bits.mul(a, G.Gf8Bits.sel(t, b), p) == G.Gf8Bits.sel(t, G.Gf8Bits.mul(a, b, p)) : G.Gf8Bits}: PROOF.ss (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=ss) # the sum of t_i * v_i def ss(ts: List<&2, Bool>, vs: List<&2, G.Gf8Bits>) -> G.Gf8Bits: PROOF.ml (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=ml) def ml(vs: List<&2, G.Gf8Bits>, +b: G.Gf8Bits, +p: G.Gf8Bits) -> List<&2, G.Gf8Bits>: PROOF.mr (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=mr) def mr(vs: List<&2, G.Gf8Bits>, +b: G.Gf8Bits, +p: G.Gf8Bits) -> List<&2, G.Gf8Bits>: PROOF.xl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=xl) def xl(vs: List<&2, G.Gf8Bits>, +p: G.Gf8Bits) -> List<&2, G.Gf8Bits>: PROOF.basis (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=basis) def basis() -> List<&2, G.Gf8Bits>: PROOF.bl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bl) def bl(a: G.Gf8Bits) -> List<&2, Bool>: PROOF.xk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=xk) def xk(n: Nat, b: G.Gf8Bits, +p: G.Gf8Bits) -> G.Gf8Bits: PROOF.xs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=xs) def xs(+b: G.Gf8Bits, +p: G.Gf8Bits) -> List<&2, G.Gf8Bits>: PROOF.fs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=fs) def fs(n: Nat) -> List<&2, Bool>: More: https://jend.leeeet.dev/packages/bend-osdev-gf.txt?definitions_offset=100