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)

gfm.bend

• def Gfm.xtime
• def gfm.mul.gothe product, over the m bits of b from the bottom: p += a * bit; a *= x
• def gfm.mul.rawthe product of a and b, both below 2^m (matching both first, so that the product of unknown values stays a small term for the proof checkers)
• def Gfm.mul
• def gfm.pow.goa^e by squaring, over the 32 bits of e from the top
• def gfm.pow.start
• def Gfm.powa^e (a^0 = 1)
• def Gfm.inva^-1 = a^(2^m - 2); the inverse of 0 is 0
• def Gfm.div
• def Gfm.expx^i
• def Gfm.log.gothe least i with x^i = a, searching i below 2^m - 1 (0 for a = 0)
• def Gfm.log

proof_tab.bend

• def gt.bt
• def gt.ft
• def gt.tf
• def gt.wcon2
• def gt.u32_cong
• def gt.adc_zero
• def gt.adc_inca + (b + 1) = a + b with a carry in
• def gt.adc_carrya + b with a carry in is (a + b) + 1
• def gt.add_zero
• def gt.add_inc
• def gt.add_onethe fills' counter: i + 1 is the increment
• def gt.add_natthe sum of two counts, as U32, is the U32 of their sum
• def gt.lt_succ_r
• def gt.lt_self
• def gt.lt_self_addx < 1 + (n + x)
• def gt.lt_add_leftb < n, so b < m + n
• def gt.lt_suma < m and b < n, so a + b < m + n
• def gt.sum_lttwo logarithms (each below 255) sum below the exp table's 2^9 slots
• def gt.log_go_lt
• def gt.log_lt
• def gt.hd9
• def gt.hd8
• def gt.hl_set
• def gt.fethe exp fill's model: slot i (from slot k) holds gen^i
• def gt.fill_exp
• def gt.flthe log fill's model: slot gen^i holds i, from i = k
• def gt.fill_log
• def gt.elist
• def gt.elist_model
• def gt.rep_len
• def gt.hl_rep
• def gt.hl_elist
• def gt.f0
• def gt.e0
• def gt.exp_tablethe exp table of a field f, given that it is its fill (for a named field that is computation, proof_tab_cases.bend; it is stated per field because --verdict's kernel compares the two sides by running them)
• def gt.elist_nthentry j of the exp table's list is gen^j, for j < 510
• def gt.log_table
• def gt.fl_splitthe log fill splits: n + m writes are n writes, then m more
• def gt.tab
• def gt.new

proof_tab_cases.bend

• def gc.elt_bitsa byte, from its bits
• def gc.isz.bits.s111the table's zero test on a byte is Gf8.is_zero
• def gc.isz.bits.s011
• def gc.isz.bits.s101
• def gc.isz.bits.s001
• def gc.isz.bits.s110
• def gc.isz.bits.s010
• def gc.isz.bits.s100
• def gc.isz.bits.s000
• def gc.isz.bits
• def gc.isz
• def gc.elt0.s111a byte whose zero test is true is 0
• def gc.elt0.s011
• def gc.elt0.s101
• def gc.elt0.s001
• def gc.elt0.s110
• def gc.elt0.s010
• def gc.elt0.s100
• def gc.elt0.s000
• def gc.elt0.bits
• def gc.elt0
• def gc.aes.ex0
• def gc.aes.el0
• def gc.aes.llist
• def gc.aes.lmodel
• def gc.aes.new
• def gc.aes.log.bits.s111the aes log table's entry at a byte
• def gc.aes.log.bits.s011
• def gc.aes.log.bits.s101
• def gc.aes.log.bits.s001
• def gc.aes.log.bits.s110
• def gc.aes.log.bits.s010
• def gc.aes.log.bits.s100
• def gc.aes.log.bits.s000
• def gc.aes.log.bits
• def gc.aes.log
• def gc.rs.ex0
• def gc.rs.el0
• def gc.rs.llist
• def gc.rs.lmodel
• def gc.rs.new
• def gc.rs.log.bits.s111the rs log table's entry at a byte
• def gc.rs.log.bits.s011
• def gc.rs.log.bits.s101
• def gc.rs.log.bits.s001
• def gc.rs.log.bits.s110
• def gc.rs.log.bits.s010
• def gc.rs.log.bits.s100