bend-osdev-array

Releases (2)

• 0.1.0.1 indexed
• 0.1.0.0 unindexed

Definitions (227)

LAWS.bend

• law get_same_array
• law get_set_same
• law set_keeps_size
• law get_new
• law new_perfect
• law set_perfect
• law size_perfect
• law new_leaves
• law model_length
• law model_get
• law model_set
• law get_set_other
• law index_below
• law index_of_nat
• law index_wrap
• law index_of_u32
• law of_list_perfect
• law of_list_leaves
• law of_list_size
• law of_list_get
• law of_list_set
• law of_list_new
• law reflect
• law set_length
• law nth_set_same
• law nth_set_other
• law nth_replicate
• law witness_perfect
• law witness_other
• law witness_index
• law witness_index_wrap
• law witness_list
• law vector_wrap
• law vector_leaves
• law vector_index
• law vector_of_list
• law vector_index_wrap
• law vector_not_perfect

PROOF.bend

• def AP.bool_t
• def AP.ft
• def AP.tf
• def AP.nat_t
• def AP.sz1 + k is never 0
• def AP.succ_cong
• def AP.double_cong
• def AP.double_add
• def AP.lt_cancel
• def AP.le_succ
• def AP.not_lt_le
• def AP.lt_one
• def AP.double_zero
• def AP.bv
• def AP.nc
• def AP.cb
• def AP.fin_le_ff
• def AP.fin_le_tf
• def AP.fin_le_ft
• def AP.fin_lt_xf
• def AP.le_bits
• def AP.lt_bits
• def AP.ha
• def AP.hb
• def AP.hc
• def AP.alg2
• def AP.alg4
• def AP.alg6
• def AP.adcfor b <= a (b < a when the carry in c is False): a = adc(a, b, True, c) + (1 - c) + b
• def AP.wcon_cong
• def AP.u32_cong
• def AP.pw
• def AP.lm
• def AP.spzz
• def AP.spz
• def AP.sp
• def AP.shl_put
• def AP.shln_pwshln(1, d) is 2^d
• def AP.padz
• def AP.padp
• def AP.shr_pw
• def AP.pw_shln
• def AP.shr_shlnhalving 2^(d+1) gives 2^d (below 2^32)
• def AP.val_pw
• def AP.val_shln
• def AP.z1
• def AP.z2
• def AP.sub_one
• def AP.mask_lm
• type AP.Tree
• def AP.build
• def AP.reflect.node
• def AP.reflect.join
• def AP.reflect
• def AP.and_l
• def AP.and_r
• def AP.size
• def AP.swap_t
• def AP.swap_v
• def AP.get_v
• def AP.mask
• def AP.z