Testing the register file

The read-only half of what a wide machine does with its registers. A program has to ask questions about a whole register before it can act on it – is the mirror equal to the target?, is it zero?, has the working cell reached the end of the tape? – and each of them is one pass:

walk the file downwards in the passing state; at the first register that fails the test, drop into the failing state and stay there.

DescriptiveComplexity.IxFile.reachesIn_fileTest is that pass, at an arbitrary property P of the registers. It writes nothing – the tape it ends with is the tape it started with – so a program may run as many tests as it likes between two computations and disturb neither.

The verdict comes back in the state, as DescriptiveComplexity.accStateAfter WMLe P qy qn bot, which DescriptiveComplexity.accStateAfter_bot_pos and DescriptiveComplexity.accStateAfter_bot_neg read as the two cases: the passing state exactly when every register passes. A caller instantiates P with whatever it is asking – two tracks agree, a track is clear, a track is set – and the transitions it supplies say how to see that in one symbol.

A pass costs one move per register plus the step off the file, so a caller that is counting bounds the moves – the addresses between consecutive registers – and gets the product.

theorem DescriptiveComplexity.IxFile.reachesIn_fileTest {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} [Finite A] [Finite I] (F : IxFile A I ile) {f : (A → Prop) → A} (h : IsLinOrd ile) (ha : IsLinOrd WMLe) {b : A} {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (hpass : ∀ (u : I), P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ qy ∧ WMWrite τ (f (F.cell u)) ∧ ¬WMRight τ) (hfail : ∀ (u : I), ¬P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ qn ∧ WMWrite τ (f (F.cell u)) ∧ ¬WMRight τ) (hkeep : ∀ (v : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ qn ∧ WMRead τ (f (F.cell v)) ∧ WMDst τ qn ∧ WMWrite τ (f (F.cell v)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), q = qy ∨ q = qn → ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (p : A → Prop), WMIncr WMLe p (F.cell bot) ∧ (wideData A).ReachesIn ((ixRank ile top - ixRank ile bot) * w + 1) { state := Sum.inr qy, head := Sum.inl (F.cell top), tape := wideTape f b } { state := Sum.inr (accStateAfter ile P qy qn bot), head := Sum.inl p, tape := wideTape f b }

A test of the register file. From the last register in the passing state, the machine walks down the file and arrives just below the first register in the state the verdict names: passing exactly when every register passed (DescriptiveComplexity.accStateAfter_bot_pos, DescriptiveComplexity.accStateAfter_bot_neg). The tape is untouched throughout.

Instantiate P with the question: these two tracks agree at this register, this track is clear here, this track is set here. The transitions the caller supplies are then a single symbol comparison each. The cost is one move per register, each bounded by w, plus the step off the file.

theorem DescriptiveComplexity.IxFile.reaches_fileTest {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} [Finite A] [Finite I] (F : IxFile A I ile) {f : (A → Prop) → A} (h : IsLinOrd ile) (ha : IsLinOrd WMLe) {b : A} (hpass : ∀ (u : I), P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ qy ∧ WMWrite τ (f (F.cell u)) ∧ ¬WMRight τ) (hfail : ∀ (u : I), ¬P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ qn ∧ WMWrite τ (f (F.cell u)) ∧ ¬WMRight τ) (hkeep : ∀ (v : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ qn ∧ WMRead τ (f (F.cell v)) ∧ WMDst τ qn ∧ WMWrite τ (f (F.cell v)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), q = qy ∨ q = qn → ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (p : A → Prop), WMIncr WMLe p (F.cell bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr qy, head := Sum.inl (F.cell top), tape := wideTape f b } { state := Sum.inr (accStateAfter ile P qy qn bot), head := Sum.inl p, tape := wideTape f b }

A test of the register file, the budget forgotten.

theorem DescriptiveComplexity.reaches_fileTest {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {P : A → Prop} {qy qn : A} (h : IsLinOrd WMLe) {b : A} {f : (A → Prop) → A} (hpass : ∀ (u : A), P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (wmSeg u)) ∧ WMDst τ qy ∧ WMWrite τ (f (wmSeg u)) ∧ ¬WMRight τ) (hfail : ∀ (u : A), ¬P u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qy ∧ WMRead τ (f (wmSeg u)) ∧ WMDst τ qn ∧ WMWrite τ (f (wmSeg u)) ∧ ¬WMRight τ) (hkeep : ∀ (w : A), ∃ (τ : A), WMTr τ ∧ WMSrc τ qn ∧ WMRead τ (f (wmSeg w)) ∧ WMDst τ qn ∧ WMWrite τ (f (wmSeg w)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), q = qy ∨ q = qn → ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (wmSeg x) r) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) {top bot : A} (htop : ∀ (v : A), WMLe v top) (hbot : ∀ (v : A), WMLe bot v) : ∃ (p : A → Prop), WMIncr WMLe p (wmSeg bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr qy, head := Sum.inl (wmSeg top), tape := wideTape f b } { state := Sum.inr (accStateAfter WMLe P qy qn bot), head := Sum.inl p, tape := wideTape f b }

A test of the register file the input channel marks.