Little-endian register digits

The digit value and boundedness predicates do not depend on an arithmetic routine or a workspace layout. They apply to any register count, including an empty register file.

Main definitions

• Cslib.WordRAM.Multiword.value: reconstruct a natural number from little-endian digits.
• Cslib.WordRAM.Multiword.Bounded: every listed register holds a digit below the radix.

def Cslib.WordRAM.Multiword.value {r : ℕ} (β : ℕ) (x : Data r) (ds : List (Fin r)) : ℕ

The value of a little-endian register list.

def Cslib.WordRAM.Multiword.Bounded {r : ℕ} (β : ℕ) (x : Data r) (ds : List (Fin r)) : Prop

Every register in a digit list contains a radix digit.