feat: even stricter word ram

[Shreyas4991]

This PR is a variant of #90 which introduced a stricter RAM model. There we moved all operations arguments and return values to opaque registers whose values can only be known with the model. We did leave comparison operations out of this, they could return boolean values. Ofc one could reconstruct the input bit by bit in n*w comparison queries and bit operations and then do pure operations in that PR.

Here we firstly plug this leak. We also require correct Progs to be free of lean parameters like the size of the input, so you can't pre-generate a Prog for each input size (that's to say, no non-uniform Progs should be allowed).

The latter creates a conundrum. We don't have any Booleans to condition or parameters to recurse on. Therefore, we have also added constructors for if-then-else and while. To make life easy, there is now some syntax. Here's a linear search example from this PR:

/-- Current address, and the result register on success. -/
abbrev index : Register 5 := 0
/-- Search key supplied by the initial machine state. -/
abbrev key : Register 5 := 1
/-- Scratch register for the loaded input word. -/
abbrev value : Register 5 := 2
/-- Register holding the constant one. -/
abbrev one : Register 5 := 3
/-- Inclusive last input address, loaded from the size header. -/
abbrev last : Register 5 := 4

/-- Inspect one cell, stopping at the first match or the inclusive last address. -/
def body (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5]
  value ←ᵣ mem[index]
  ifₚ value =ᵣ key then
    reset .ult
  else
    ifₚ index <ᵣ last then
      index ←ᵣ index + one
    else
      nop

/-- Read the size header and initialize the search at address one. -/
def setup (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5]
  reset .eq
  index ←ᵣ imm[0]
  last ←ᵣ mem[index]
  cmp (w := w) .ult index last
  one ←ᵣ imm[1]
  index ←ᵣ imm[1]

/-- Convert a found memory address to a zero-based array index. -/
def finish (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5]
  ifₚ flag .eq then
    index ←ᵣ index - one
  else
    nop


def linearSearch (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5]
  LinearSearch.setup w
  whileₚ .ult do
    LinearSearch.body w
  LinearSearch.finish w

/-- Store the size header, array, and search key. The program initializes its other registers. This is 
how we initialize the memory prior to linear search. It is used to state assumptions about initial state in theorems about linear search correctness -/
def linearSearchState (input : Array (Word w)) (target : Word w) : RAMState w 5 :=
  ⟨sizedArrayMemory input, fun r => if r = LinearSearch.key then target else 0, fun _ => false⟩...

At this point we have a deeply embedded DSL. So why stick to Prog? Reductions are convenient to have. we can still work with looser query models and reduce some of them to WordRAM to get WordRAM algorithms where we only count operations we want to count.

[Shreyas4991]

The experiment continues. Turns out we can make this viable.

previously this comment said

This experiment is over. In an attempt to remove any loopholes that might allow this so-called "cheating", I used GPT to rapidly go to an almost- fully deeply embedded word RAM assembly. Of course this means going further and further away from the lightweight-ness of this Free monad based framework. Clearly this is not a suitable way to proceed. Nevertheless I learnt quite a bit about the trade-offs between the lighter #90 and this PR, and in general between free monad DSLs and deep embeddings, even in this toy setting.