bend-osdev-gf

Releases (3)

• 0.1.2.0 invalid

  expected a package named bend-osdev-word64@0.1.1.1 on https://hub.bend-lang.com

  at bend-osdev-bytes@0.1.1.1/bytes.bend:12

  5 files do not load

  • LAWS.bend
  • PROOF.bend
  • check.bend
  • gf128.bend
  • package.bend
• 0.1.1.0 indexed
• 0.1.0.0 unindexed

Definitions (522)

PROOF.bend

• def lin_l
• def lin_r
• def lin_x
• def decevery byte is the sum of its bits times the basis (by cases)
• def hf
• def me0
• def me1
• def me2
• def me3
• def me4
• def me5
• def me6
• def me7
• def comm_e0
• def comm_e1
• def comm_e2
• def comm_e3
• def comm_e4
• def comm_e5
• def comm_e6
• def comm_e7
• def mlr
• def comm
• def ml_x
• def ax
• def ak
• def mlx_c
• def assoc
• def ot
• def bdisc
• def bt_absurd
• def elt_pow
• def mul_elt_l
• def pow_elt
• def log_elt
• def elt_bits
• def fixza nonzero byte as itself, and 0 as 1, so that the per-byte facts hold for every byte and need no hypothesis while they are split into cases
• def fix_nz
• def mul_inv_aes.s11111
• def mul_inv_aes.s11110
• def mul_inv_aes.s11101
• def mul_inv_aes.s11100
• def mul_inv_aes.s11011
• def mul_inv_aes.s11010
• def mul_inv_aes.s11001
• def mul_inv_aes.s11000
• def mul_inv_aes.s10111
• def mul_inv_aes.s10110
• def mul_inv_aes.s10101
• def mul_inv_aes.s10100
• def mul_inv_aes.s10011
• def mul_inv_aes.s10010
• def mul_inv_aes.s10001
• def mul_inv_aes.s10000
• def mul_inv_aes.s01111
• def mul_inv_aes.s01110
• def mul_inv_aes.s01101
• def mul_inv_aes.s01100
• def mul_inv_aes.s01011
• def mul_inv_aes.s01010
• def mul_inv_aes.s01001
• def mul_inv_aes.s01000
• def mul_inv_aes.s00111
• def mul_inv_aes.s00110
• def mul_inv_aes.s00101
• def mul_inv_aes.s00100
• def mul_inv_aes.s00011
• def mul_inv_aes.s00010
• def mul_inv_aes.s00001
• def mul_inv_aes.s00000
• def mul_inv_aes.bits
• def mul_inv_aes.core
• def mul_inv_aes.lift
• def exp_log_aes.s11111
• def exp_log_aes.s11110
• def exp_log_aes.s11101
• def exp_log_aes.s11100
• def exp_log_aes.s11011
• def exp_log_aes.s11010
• def exp_log_aes.s11001
• def exp_log_aes.s11000
• def exp_log_aes.s10111
• def exp_log_aes.s10110
• def exp_log_aes.s10101
• def exp_log_aes.s10100
• def exp_log_aes.s10011
• def exp_log_aes.s10010
• def exp_log_aes.s10001
• def exp_log_aes.s10000
• def exp_log_aes.s01111
• def exp_log_aes.s01110
• def exp_log_aes.s01101
• def exp_log_aes.s01100
• def exp_log_aes.s01011
• def exp_log_aes.s01010
• def exp_log_aes.s01001
• def exp_log_aes.s01000
• def exp_log_aes.s00111
• def exp_log_aes.s00110
• def exp_log_aes.s00101