stelliferous
Releases (2)
Definitions (2,086)
proofs/traversal_visit_witness.bend
proofs/traversal_witness.bend
- type Sample
- type StateEvidence
- def store
- def step
- def run
- type ResultEvidence
- def finish
- def array_evidence
- def array_sample
- def offset_read
- def first
- def second
- def source_unchanged
- def output_witness
- def update_sample
- def update_current
- def update_step
- def update
- type MapEvidence
- def mapped_value
- def map_step
- def map_run
- def mapped_output
- def map_in_place
- type FoldEvidence
- def fold_value
- def fold_step
- def fold_run
- def fold_finished
- def fold
proofs/u32_comparison.bend
proofs/u32_division.bend
- def decode
- def nat_lt_native
- def nat_le_native
- def native_ge_nat
- def fin
- def shifted_bound
- law step
- def transfer_bound
- law go
- def quotient
- def quotient_decode
- def remainder_decode
- def quotient_pair
- def remainder_pair
- def natural_quotient
- def natural_remainder
- def nat_nonzero
- def nonzero
- def divide
- def modulo
proofs/u32_shift.bend
- law out_pad
- def Goal
- def parts
- def no_carry
- def put_inc
- def encoded_shift
- def encoded_put
- def bounded_put
- def put_pad
- def DoubleGoal
- def double_parts
- def double_word
- def double
proofs/u32_successor.bend
- law pad_nat
- law inc_nat
- law adc_zero
- law adc_one
- law add_one
- law concat_pad
- def padded_successor
- def Goal
- def parts
- def word
- law successor
proofs/word_arithmetic.bend
- law carry
- law inc_left
- def encode
- law encode_add
- law double_carry
- def shift_put
- def double_word
- def encode_double
- law native_encoding
- def native_add
proofs/word_encoding.bend
- def concat
- def shift
- law double_add
- law zero_nat
- law finish_lt_zero
- law compare_high_only