Exact algebraic RAM instances

Values are tagged natural words or exact field elements. Only the natural arm can address memory; a configuration w bounds words and control labels by 2 ^ w. Arithmetic on words faults on overflow, subtraction underflow, or zero divisors. Field arithmetic is exact; division by zero faults. There is a one-way word-to-field operation, no field-to-word cast, floor, transcendental operation, or square root.

Programs contain natural-word and rational literal symbols, never arbitrary field constants. A rational literal faults when its denominator becomes zero in the field. Thus constants are countable syntax even for the real model; positive characteristic is handled explicitly.

The real instance follows the separation of word addresses and exact real values in Erickson, van der Hoog, and Miltzow, §6.1. This is a tagged, finite-register variant with one tagged memory, not their literal pair of word/real arrays. It also uses checked word arithmetic rather than modular arithmetic. The real interpretation is noncomputable mathematical semantics. Prime ZMod instances are executable and offer equality, but no ordering of field elements. Every instruction uses the generic core's unit cost; no bit-cost or Turing-machine implementation of exact real arithmetic is claimed.

Main definitions

• Algebraic.model: a field with an explicitly supplied optional strict comparison.
• Algebraic.real: exact real arithmetic and comparison with bounded natural addresses.
• Algebraic.primeField: exact prime-field arithmetic with bounded natural addresses.

References

• [Erickson, van der Hoog, and Miltzow, Smoothing the Gap Between NP and ER] [EvdHM24], §6.1.

inductive Cslib.GenericRAM.Algebraic.Const : Type

Finitely representable literal syntax, independent of arbitrary field inputs.

• word (n : ℕ) : Const

  A natural word, subject to the configured width.

• rational (q : ℚ) : Const

  A rational field literal, defined only when its denominator remains nonzero.

def Cslib.GenericRAM.Algebraic.instDecidableEqConst.decEq (x✝ x✝¹ : Const) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.GenericRAM.Algebraic.instDecidableEqConst : DecidableEq Const

inductive Cslib.GenericRAM.Algebraic.Operation : Type

Typed word and field operations. Mixed tags fault except for toField.

• wordAdd : Operation

  Natural addition, checked for overflow by result admissibility.

• wordSub : Operation

  Natural subtraction, undefined on underflow.

• wordMul : Operation

  Natural multiplication, checked for overflow by result admissibility.

• wordDiv : Operation

  Natural quotient, undefined at zero divisor.

• wordMod : Operation

  Natural remainder, undefined at zero divisor.

• add : Operation

  Exact addition.

• sub : Operation

  Exact subtraction.

• mul : Operation

  Exact multiplication.

• div : Operation

  Exact division, undefined at zero divisor.

• neg : Operation

  Exact additive inverse.

• toField : Operation

  Convert a natural word to its field value, with no inverse conversion.

@[instance_reducible]

instance Cslib.GenericRAM.Algebraic.instDecidableEqOperation : DecidableEq Operation

@[reducible, inline]

abbrev Cslib.GenericRAM.Algebraic.Operation.arity : Operation → ℕ

Unary conversion/negation and binary arithmetic.

@[reducible, inline]

abbrev Cslib.GenericRAM.Algebraic.operations : Circuits.Signature

The algebraic operation signature.

inductive Cslib.GenericRAM.Algebraic.Test : Type

Tests do not compare values with different tags.

• wordEq : Test

  Equality of natural words.

• wordLt : Test

  Strict order of natural words.

• eq : Test

  Equality in the field.

• lt : Test

  The supplied partial strict comparison in the field.

@[instance_reducible]

instance Cslib.GenericRAM.Algebraic.instDecidableEqTest : DecidableEq Test

@[reducible, inline]

abbrev Cslib.GenericRAM.Algebraic.tests : Circuits.Signature

Every test takes two registers.

def Cslib.GenericRAM.Algebraic.admissible {K : Type u_1} (w : ℕ) : ℕ ⊕ K → Bool

Check natural words; exact field values have no bit bound.

def Cslib.GenericRAM.Algebraic.address {K : Type u_1} (w : ℕ) : ℕ ⊕ K → Option ℕ

Extract only a bounded natural address; even integral field values are rejected.

def Cslib.GenericRAM.Algebraic.constant {K : Type u_1} [Field K] [DecidableEq K] : Const → Option (ℕ ⊕ K)

Interpret rational symbols only when the denominator is nonzero in the field.

def Cslib.GenericRAM.Algebraic.evalOp {K : Type u_1} [Field K] [DecidableEq K] (op : Operation) : (Fin op.arity → ℕ ⊕ K) → Option (ℕ ⊕ K)

Partial arithmetic interpretation; operands must have the indicated tags.

def Cslib.GenericRAM.Algebraic.evalTest {K : Type u_1} [DecidableEq K] (less : K → K → Option Bool) (t : Test) (xs : Fin 2 → ℕ ⊕ K) : Option Bool

Partial test interpretation. Finite fields supply no order comparison.

@[reducible, inline]

abbrev Cslib.GenericRAM.Algebraic.model (K : Type u_2) [Field K] [DecidableEq K] (less : K → K → Option Bool) : Model

The tagged field model; less determines which field-order tests are available.

@[reducible, inline]

noncomputable abbrev Cslib.GenericRAM.Algebraic.real : Model

Exact real RAM semantics, with decidable equality/order supplied classically.

@[reducible, inline]

abbrev Cslib.GenericRAM.Algebraic.primeField (p : ℕ) [Fact (Nat.Prime p)] : Model

An executable prime-field RAM. Its field-order test always faults.