Concrete finite Exact Triangle callees for the native host

A callee is actual finite standard code, with raw unsigned protocol registers 0–5 and a raw Boolean in register 6. Matrix cells use the existing signed encoding. The callee must preserve the complete memory prefix below AB, including every remaining preprocessing instance.

The charged time and logarithmic width guarantee are proof obligations about that code, not instructions or runtime oracles. No fast solver is assumed to have been constructed.

Main definitions

• Callee: concrete code and its explicit width, frame, correctness and instruction contract.

This native calling convention and its composition interface are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.Host.Callee (r : ℕ) : Type

A certified finite solver block. Unused registers and old workspace contents are arbitrary. The caller delivers all six arguments; the solver establishes its own scratch initialization.

• code : WordRAM.Code WordRAM.Basis.standard (r + 7)

  The one fixed native code block, including its seven protocol registers.

• time : ℕ → ℕ → ℕ

  Charged instruction budget, independent of physical width, layout and matrix contents.

• widthCoefficient : ℕ

  Multiplier for a logarithmic width guarantee, including addresses and scratch arithmetic.

• coefficient_pos : 0 < self.widthCoefficient

  The guarantee gives a positive width at every admitted call.

• not_readsWidth : ¬self.code.ReadsWidth

  Wider words do not change the mathematical execution.

• exec (w t F ab bc ac free : ℕ) (x : WordRAM.Data (r + 7)) (A B C : Fin t → Fin t → ℤ) : 0 < t → 0 < F → ab + t * t ≤ bc → bc + t * t ≤ ac → ac + t * t ≤ free → self.widthCoefficient * Nat.clog 2 (free + F + t + 2) ≤ w → x.regs (solverArg 0) = t → x.regs (solverArg 1) = F → x.regs (solverArg 2) = ab → x.regs (solverArg 3) = bc → x.regs (solverArg 4) = ac → x.regs (solverArg 5) = free → (∀ (i j : Fin t), x.mem (ab + ↑i * t + ↑j) = WordRAM.Signed.encode (A i j)) → (∀ (i j : Fin t), x.mem (bc + ↑i * t + ↑j) = WordRAM.Signed.encode (B i j)) → (∀ (i j : Fin t), x.mem (ac + ↑i * t + ↑j) = WordRAM.Signed.encode (C i j)) → (∀ (i j : Fin t), |A i j| ≤ ↑F) → (∀ (i j : Fin t), |B i j| ≤ ↑F) → (∀ (i j : Fin t), |C i j| ≤ ↑F) → ∃ (y : WordRAM.Data (r + 7)), WordRAM.ExecWithin w self.code x y (self.time t F) ∧ y.regs (solverArg 6) ≤ 1 ∧ (y.regs (solverArg 6) = 1 ↔ ExactTriangle.HasZeroTriangle A B C) ∧ ∀ a < ab, y.mem a = x.mem a

  Actual execution, exact verdict and caller-prefix preservation for arbitrary old memory.