import Base
import ./lib.bend as By

# to_list(empty) is Nil.
law to_list_empty:
  { By.Bytes.to_list(By.Bytes.empty()) == Nil{} : List<&2, U32> }

# empty is B{Nil}.
law empty_is_b_nil:
  { By.Bytes.empty() == By.B{Nil{}} : By.Bytes }

# to_list undoes the B encoding.
law to_list_b:
  for xs: List<&2, U32>
  { By.Bytes.to_list(By.B{xs}) == xs : List<&2, U32> }

# from_list is the B constructor.
law from_list_b:
  for xs: List<&2, U32>
  { By.Bytes.from_list(xs) == By.B{xs} : By.Bytes }

# to_list ∘ from_list is identity on the underlying list.
law to_list_from_list:
  for xs: List<&2, U32>
  { By.Bytes.to_list(By.Bytes.from_list(xs)) == xs : List<&2, U32> }

# from_list ∘ to_list is identity on Bytes.
law from_list_to_list:
  for xs: List<&2, U32>
  { By.Bytes.from_list(By.Bytes.to_list(By.B{xs})) == By.B{xs} : By.Bytes }

# singleton packs a one-element list.
law to_list_singleton:
  for +x: U32
  { By.Bytes.to_list(By.Bytes.singleton(x)) == x <> Nil{} : List<&2, U32> }

# singleton is B{x <> Nil}.
law singleton_is_b:
  for +x: U32
  { By.Bytes.singleton(x) == By.B{x <> Nil{}} : By.Bytes }

# length(empty) is 0.
law length_empty:
  { By.Bytes.length(By.Bytes.empty()) == 0n : Nat }

# length(B{xs}) is List.length(xs).
law length_b:
  for xs: List<&2, U32>
  { By.Bytes.length(By.B{xs}) == List.length(&2, U32, xs) : Nat }

# length(singleton(x)) is 1.
law length_singleton:
  for +x: U32
  { By.Bytes.length(By.Bytes.singleton(x)) == 1n : Nat }

# get(empty, 0) is None.
law get_empty_zero:
  { By.Bytes.get(By.Bytes.empty(), 0n) == None{} : Maybe<&2, U32> }

# get(singleton(x), 0) recovers x.
law get_singleton_zero:
  for +x: U32
  { By.Bytes.get(By.Bytes.singleton(x), 0n) == Some{x} : Maybe<&2, U32> }

# get(singleton(x), 1) is None.
law get_singleton_one:
  for +x: U32
  { By.Bytes.get(By.Bytes.singleton(x), 1n) == None{} : Maybe<&2, U32> }

# append unwraps to List.append.
law to_list_append:
  for xs: List<&2, U32>
  for ys: List<&2, U32>
  {
    By.Bytes.to_list(By.Bytes.append(By.B{xs}, By.B{ys}))
      == List.append(&2, U32, xs, ys)
    : List<&2, U32>
  }

# append(empty, bs) leaves bs unchanged (via to_list).
law append_empty_left:
  for xs: List<&2, U32>
  {
    By.Bytes.to_list(By.Bytes.append(By.Bytes.empty(), By.B{xs}))
      == xs
    : List<&2, U32>
  }

# Definitional form of append(bs, empty) (needs List.append_nil for identity).
law append_empty_right_def:
  for xs: List<&2, U32>
  {
    By.Bytes.to_list(By.Bytes.append(By.B{xs}, By.Bytes.empty()))
      == List.append(&2, U32, xs, Nil{})
    : List<&2, U32>
  }

# append of two singletons.
law append_singletons:
  for +x: U32
  for +y: U32
  {
    By.Bytes.to_list(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y)))
      == x <> (y <> Nil{})
    : List<&2, U32>
  }

# length(append(empty, B{xs})) is List.length(xs).
law length_append_empty_left:
  for xs: List<&2, U32>
  {
    By.Bytes.length(By.Bytes.append(By.Bytes.empty(), By.B{xs}))
      == List.length(&2, U32, xs)
    : Nat
  }

# get on append of singletons.
law get_append_singletons_zero:
  for +x: U32
  for +y: U32
  {
    By.Bytes.get(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y)), 0n)
      == Some{x}
    : Maybe<&2, U32>
  }

law get_append_singletons_one:
  for +x: U32
  for +y: U32
  {
    By.Bytes.get(By.Bytes.append(By.Bytes.singleton(x), By.Bytes.singleton(y)), 1n)
      == Some{y}
    : Maybe<&2, U32>
  }

# reverse unwraps to List.reverse.
law to_list_reverse:
  for xs: List<&2, U32>
  {
    By.Bytes.to_list(By.Bytes.reverse(By.B{xs}))
      == List.reverse(&2, U32, xs)
    : List<&2, U32>
  }

# reverse(empty) is empty.
law reverse_empty:
  { By.Bytes.to_list(By.Bytes.reverse(By.Bytes.empty())) == Nil{} : List<&2, U32> }

# reverse(singleton(x)) is singleton(x).
law reverse_singleton:
  for +x: U32
  {
    By.Bytes.to_list(By.Bytes.reverse(By.Bytes.singleton(x)))
      == x <> Nil{}
    : List<&2, U32>
  }

# eq(empty, empty) is True.
law eq_empty:
  { By.Bytes.eq(By.Bytes.empty(), By.Bytes.empty()) == True{} : Bool }

# eq(empty, singleton(x)) is False.
law eq_empty_singleton:
  for +x: U32
  { By.Bytes.eq(By.Bytes.empty(), By.Bytes.singleton(x)) == False{} : Bool }

# eq of distinct concrete singletons is False.
law eq_singleton_diff:
  { By.Bytes.eq(By.Bytes.singleton(1), By.Bytes.singleton(2)) == False{} : Bool }

# hex(empty) is "".
law hex_empty:
  { By.Bytes.hex(By.Bytes.empty()) == "" : String }

# hex(singleton(0)) is "00".
law hex_byte_zero:
  { By.Bytes.hex(By.Bytes.singleton(0)) == "00" : String }

# hex(singleton(255)) is "ff".
law hex_byte_ff:
  { By.Bytes.hex(By.Bytes.singleton(255)) == "ff" : String }

# hex(singleton(10)) is "0a".
law hex_byte_0a:
  { By.Bytes.hex(By.Bytes.singleton(10)) == "0a" : String }

# hex(singleton(16)) is "10".
law hex_byte_10:
  { By.Bytes.hex(By.Bytes.singleton(16)) == "10" : String }

# hex(singleton(127)) is "7f".
law hex_byte_7f:
  { By.Bytes.hex(By.Bytes.singleton(127)) == "7f" : String }

# hex of two bytes concatenates.
law hex_two_bytes:
  {
    By.Bytes.hex(By.Bytes.append(By.Bytes.singleton(0), By.Bytes.singleton(255)))
      == "00ff"
    : String
  }