law xts_sector

bend-osdev-cipher-modes@0.1.0.0 · LAWS.bend:149

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-word64@0.1.0.0/word64.bend as W
import bend-osdev-cipher-modes@0.1.0.0/xts.bend as T

149# the sequence number of sector n: n little-endian, zero-filled to 16 bytes
150law xts_sector:
151  {T.Xts.sector(W.W64.from_parts(0, 2591577138)) == B.Octets.of_list([50, 84, 120, 154, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) : B.Octets}