law parts_of

bend-osdev-word64@0.1.1.0 · LAWS.bend:64

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

64# Interface law: a word is its two halves joined (for every word). Other
65# packages' proofs use this instead of looking inside W64.
66law parts_of:
67  for v: W.W64
68  {W.W64.from_parts(W.W64.hi(v), W.W64.lo(v)) == v : W.W64}