bend-osdev-gf
Releases (3)
Definitions (522)
LAWS.bend
- law mul_comm
- law mul_assoc
- law mul_distrib
- law mul_one
- law mul_zero
- law xtime_mul_x
- law add_comm
- law add_assoc
- law add_zero
- law add_self
- law pow_add
- law mul_inv_aes
- law mul_inv_rs
- law exp_log_aes
- law exp_log_rs
- law inv_zero
- law v_aes_mul
- law v_aes_mul13
- law v_aes_xtime
- law v_aes_invthe inverse of {53} is {ca} (the AES S-box's first step)
- law v_rs_x8in 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_order
- law v_div
- law tab_mul_aes
- law tab_mul_rs
- law tab_log_aes
- law tab_log_rs
- law tab_exp_aes
- law tab_exp_rs
- law witness_tab_expa witness for tab_exp's hypothesis: the last entry, 509
- law v_tab_mul_aes
- law v_tab_inv_aes
- law v_tab_mul_rs
- law v_tab_zero
- law v_gcm_x15e2ec746917062882c85b0685353deb7
- law v_gcm_ghashf38cbb1ad69223dcc3457ae5b6b0f885 (one block of C, then the lengths: 0 bits of A, 128 of C)
- law v_cmac_k1L = 7df76b0c1ab899b33e42f047b91b546f, K1 = fbeed618357133667c85e08f7236a8de, K2 = f7ddac306ae266ccf90bc11ee46d513b
- law v_cmac_k2
- law v_gcm_mul_xGCM's x is the block 0x40 00 ..
- law v_gcm_mul_x_value
- law v_be_mul_xin big-endian order x is the number 2: double_be is multiplication by it
- law v_be_mul
- law v_xts_wrapXTS: the top bit of byte 15 wraps round as 0x87 into byte 0
- law v_xts_double
- law v_gf128_octets
- law v_gf128_short
- law gfm_add_comm
- law gfm_mul_comm_gf16
- law gfm_mul_inv_gf16
- law gfm_mul_inv_gf32
- law v_bch13_x13
- law v_bch13_order
- law v_bch13_mul
- law v_bch13_inv
- law v_bch13_log
- law v_bch14_mul
PROOF.bend
- def bx_comm
- def bx_assoc
- def bx_zr
- def bx_self
- def bx_swap
- def band_xor
- def blin
- def rb_eq
- def rx_comm
- def rx_assoc
- def rx_zr
- def rx_self
- def rx_swap
- def rx_zl
- def x_lin
- def x_zero
- def sel_xor
- def sel_txor
- def x_sel
- def step_lin_b
- def horner_lin_b
- def m_lin_r
- type GfPbpairs of bits, for the product's linearity in its first factor
- def pl.x
- def pl.l
- def pl.r
- def step_lin_a
- def horner_lin_a
- def m_lin_l
- def step_zero
- def horner_zero
- def m_zero_r
- def m_zero_l
- def m_sel_l
- def m_sel_r
- def ssthe sum of t_i * v_i
- def ml
- def mr
- def xl
- def basis
- def bl
- def xk
- def xs
- def fs