Bounded signed integer RAM

Signed.model instantiates the generic RAM with the operational choices of LeanTrominoes.ComplexityAbstract.RAM at revision 6d5b36c1 (MIT–ULB CompGeom Group). Values are integers, addresses are naturals, and the configuration is a word width. Every produced, moved, stored, or returned value must fit the signed word range. Address registers must be nonnegative and below 2^w; the current program counter and every continuation label must also be below 2^w.

Arithmetic uses Lean's integer division and remainder, including their total zero-divisor conventions. Each instruction, including halt, costs one. This is the source's signed model, not the unsigned Cslib.WordRAM instance; in particular subtraction is not truncated.

Main definitions

• Arithmetic, Test: the original arithmetic and comparison symbols.
• Fits, model: signed word bounds and the generic RAM instance.
• initial, InputFits: the original input layout and admissibility predicate.

Main results

• fits_zero, fits_one: basic representable values.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

inductive Cslib.GenericRAM.Signed.Arithmetic : Type

The five arithmetic operations of the original signed RAM.

• add : Arithmetic
• sub : Arithmetic
• mul : Arithmetic
• div : Arithmetic
• mod : Arithmetic

@[instance_reducible]

instance Cslib.GenericRAM.Signed.instDecidableEqArithmetic : DecidableEq Arithmetic

def Cslib.GenericRAM.Signed.instReprArithmetic.repr : Arithmetic → ℕ → Std.Format

@[instance_reducible]

instance Cslib.GenericRAM.Signed.instReprArithmetic : Repr Arithmetic

def Cslib.GenericRAM.Signed.Arithmetic.eval : Arithmetic → ℤ → ℤ → ℤ

Integer arithmetic, with Lean's total division and remainder conventions.

inductive Cslib.GenericRAM.Signed.Test : Type

Equality and signed strict comparison.

• eq : Test
• lt : Test

@[instance_reducible]

instance Cslib.GenericRAM.Signed.instDecidableEqTest : DecidableEq Test

@[instance_reducible]

instance Cslib.GenericRAM.Signed.instReprTest : Repr Test

def Cslib.GenericRAM.Signed.instReprTest.repr : Test → ℕ → Std.Format

def Cslib.GenericRAM.Signed.Test.eval : Test → ℤ → ℤ → Bool

Interpret a comparison on signed integers.

def Cslib.GenericRAM.Signed.Fits (w : ℕ) (value : ℤ) : Prop

Signed two's-complement range, requiring a positive word width.

@[instance_reducible]

instance Cslib.GenericRAM.Signed.instDecidableFits (w : ℕ) (value : ℤ) : Decidable (Fits w value)

theorem Cslib.GenericRAM.Signed.fits_zero {w : ℕ} (positive : 0 < w) : Fits w 0

Zero fits at every positive width.

theorem Cslib.GenericRAM.Signed.fits_one {w : ℕ} (wide : 2 ≤ w) : Fits w 1

One fits at every width of at least two bits.

@[reducible, inline]

abbrev Cslib.GenericRAM.Signed.model : Model

The original bounded signed integer RAM, as a generic machine model. All writes and halts check Fits; addresses and control labels use the unsigned range.

def Cslib.GenericRAM.Signed.initial {r : ℕ} (input : List ℤ) : State model r

Zero registers and an input length header at address zero, followed by input words. Input placement is a calling convention, not part of the instruction cost.

def Cslib.GenericRAM.Signed.InputFits (w : ℕ) (input : List ℤ) : Prop

Input words and their length header fit the signed range.