Memory-access traces of word-RAM executions

The decorated execution relation retains the exact instruction count of Exec while exposing successful reads and writes, including their addresses and word values. Branches and loop control keep their ordinary instruction charges and produce no memory probes. A trace is an observation of a RAM execution, not the full cell-probe model with arbitrary free computation.

Main definitions

• Probe: a read or write event with address and value.
• TraceExec: structured execution with its memory-access transcript.
• Probe.readCount, Probe.writeCount: additive resource interpretations.

Main results

• TraceExec.exec: forgetting the transcript recovers exact Exec.
• Exec.exists_trace: every execution has a transcript.
• Probe.readCount_append, Probe.writeCount_append: compositional probe accounting.

References

The machine and its exact compilation costs are those of WordRAM.Structured.

inductive Cslib.WordRAM.Probe : Type

An observed memory access, with the value read or written.

• read (address value : ℕ) : Probe

  Read a word from an address.

• write (address value : ℕ) : Probe

  Write a word at an address.

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqProbe : DecidableEq Probe

def Cslib.WordRAM.instDecidableEqProbe.decEq (x✝ x✝¹ : Probe) : Decidable (x✝ = x✝¹)

def Cslib.WordRAM.instReprProbe.repr : Probe → ℕ → Std.Format

@[instance_reducible]

instance Cslib.WordRAM.instReprProbe : Repr Probe

def Cslib.WordRAM.Op.probes {B : Basis} {r : ℕ} (o : Op B r) (x : Data r) : List Probe

The memory accesses made by a data instruction in its initial state.

inductive Cslib.WordRAM.TraceExec {B : Basis} {r : ℕ} (w : ℕ) : Code B r → Data r → Data r → ℕ → List Probe → Prop

An exact structured execution decorated with its successful memory probes.

• op {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} : Op.eval w o x = some y → TraceExec w (Code.op o) x y 1 (o.probes x)

  A successful data instruction.

• seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x y z : Data r} {m n : ℕ} {ts us : List Probe} : TraceExec w c₁ x y m ts → TraceExec w c₂ y z n us → TraceExec w (c₁.seq c₂) x z (m + n) (ts ++ us)

  Sequential traces concatenate.

• branch_pos {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} {ts : List Probe} : c.Holds x → TraceExec w pos x y n ts → TraceExec w (Code.branch c pos neg) x y (n + 1) ts

  The positive branch pays one control instruction.

• branch_neg {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} {ts : List Probe} : ¬c.Holds x → TraceExec w neg x y n ts → TraceExec w (Code.branch c pos neg) x y (n + 2) ts

  The negative branch pays two control instructions.

• loop_exit {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x : Data r} : ¬c.Holds x → TraceExec w (Code.loop c body) x x 2 []

  Loop termination pays two control instructions and has no probes.

• loop_iter {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x y z : Data r} {m n : ℕ} {ts us : List Probe} : c.Holds x → TraceExec w body x y m ts → TraceExec w (Code.loop c body) y z n us → TraceExec w (Code.loop c body) x z (m + n + 2) (ts ++ us)

  A loop iteration concatenates its body's trace and the remaining trace.

theorem Cslib.WordRAM.TraceExec.exec {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} {ts : List Probe} (h : TraceExec w c x y n ts) : Exec w c x y n

Erasing probes leaves the original exact instruction-count theorem.

theorem Cslib.WordRAM.Exec.exists_trace {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} (h : Exec w c x y n) : ∃ (ts : List Probe), TraceExec w c x y n ts

Every successful structured execution admits its exact memory transcript.

def Cslib.WordRAM.Probe.readCount : List Probe → ℕ

Number of reads in a transcript.

def Cslib.WordRAM.Probe.writeCount : List Probe → ℕ

Number of writes in a transcript.

theorem Cslib.WordRAM.Probe.readCount_append (ts us : List Probe) : readCount (ts ++ us) = readCount ts + readCount us

Read counts add across consecutive executions.

theorem Cslib.WordRAM.Probe.writeCount_append (ts us : List Probe) : writeCount (ts ++ us) = writeCount ts + writeCount us

Write counts add across consecutive executions.

theorem Cslib.WordRAM.Probe.readCount_add_writeCount (ts : List Probe) : readCount ts + writeCount ts = ts.length

Every probe is exactly one read or one write.

def Cslib.WordRAM.Probe.writes : List Probe → Finset ℕ

The finite set of cells actually written by a transcript.

theorem Cslib.WordRAM.Probe.writes_append (ts us : List Probe) : writes (ts ++ us) = writes ts ∪ writes us

Sequential write footprints combine by union, allowing repeated writes.

theorem Cslib.WordRAM.Op.eval_modifies {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} (h : eval w o x = some y) : Modifies (Probe.writes (o.probes x)) x.mem y.mem

A successful primitive instruction preserves every cell absent from its write transcript.

theorem Cslib.WordRAM.TraceExec.modifies {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} {ts : List Probe} (h : TraceExec w c x y n ts) : Modifies (Probe.writes ts) x.mem y.mem

An execution changes memory only at addresses appearing as writes in its transcript.

theorem Cslib.WordRAM.TraceExec.frame {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} {ts : List Probe} (h : TraceExec w c x y n ts) {P : HeapAssertion} (hP : P.holds x.mem) (hdisj : Disjoint P.footprint (Probe.writes ts)) : P.holds y.mem

A concrete execution preserves any assertion disjoint from its write transcript.

theorem Cslib.WordRAM.TraceExec.length_le {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} {ts : List Probe} (h : TraceExec w c x y n ts) : ts.length ≤ n

No instruction makes more than one memory access.