law roundtrip

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:514

import Base

514# LAW 1 (roundtrip): with a well-formed table (all rule ids
515# distinct), decoding what was encoded returns the original bytes.
516law roundtrip:
517  for +table: List<&2, Rule>
518  for +bs: List<&2, Nat>
519  for +w: {True{} == wf(table) : Bool}
520  {decode(table, encode(table, lift(bs))) == bs : List<&2, Nat>}