# Computational proofs for every executable Hex law.
# Base normalization is sufficient; no termination escape is used.
import Base
import ./LAWS.bend as Laws

def Laws.encode_empty():
  {==}
def Laws.encode_zero():
  {==}
def Laws.encode_one():
  {==}
def Laws.encode_ten():
  {==}
def Laws.encode_fifteen():
  {==}
def Laws.encode_sixteen():
  {==}
def Laws.encode_sevenf():
  {==}
def Laws.encode_ff():
  {==}
def Laws.encode_masks_u32():
  {==}
def Laws.encode_multiple():
  {==}
def Laws.decode_empty():
  {==}
def Laws.decode_zero():
  {==}
def Laws.decode_lowercase():
  {==}
def Laws.decode_uppercase():
  {==}
def Laws.decode_mixed_case():
  {==}
def Laws.decode_multiple():
  {==}
def Laws.roundtrip_empty():
  {==}
def Laws.roundtrip_one():
  {==}
def Laws.roundtrip_multiple():
  {==}
def Laws.reject_odd_length():
  {==}
def Laws.reject_three_chars():
  {==}
def Laws.reject_invalid_g():
  {==}
def Laws.reject_invalid_prefix():
  {==}
def Laws.reject_whitespace():
  {==}
def Laws.reject_prefix():
  {==}
def Laws.reject_bad_tail():
  {==}