Native access to fixed tuples of packed words

The number of words is a syntactic constant. Addressing uses literal multiples and native PLUS; it does not presuppose a multiplication relation. Decoding a field checks all bits, including zeros above its width and zeros at unused addresses.

Main definitions

• Cslib.Logic.FO.Ordered.packedBit: read a bit across a fixed tuple of words.
• Cslib.Logic.FO.Ordered.packedField: decode a bounded-width field.

Main results

• Cslib.Logic.FO.Ordered.realize_packedBit: exact word-address semantics.
• Cslib.Logic.FO.Ordered.realize_packedField: exact natural-number field semantics.

References

• N. Immerman, Descriptive Complexity, Theorem 1.17(1)

noncomputable def Cslib.Logic.FO.Ordered.packedBit (L : FirstOrder.Language) {α : Type u_1} {B : ℕ} (h : (language L).Term α) (w : Fin B → (language L).Term α) (a : (language L).Term α) : (language L).Formula α

Read a bit in a fixed tuple. Each scale is a syntactic literal, independent of the universe.

noncomputable def Cslib.Logic.FO.Ordered.packedField (L : FirstOrder.Language) {α : Type u_1} {B : ℕ} (h : (language L).Term α) (w : Fin B → (language L).Term α) (a s z : (language L).Term α) : (language L).Formula α

Decode exactly s bits starting at a, with all higher bits explicitly zero.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_packedBit {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {B : ℕ} (h : (language L).Term α) (w : Fin B → (language L).Term α) (a : (language L).Term α) (v : α → Fin n) : (packedBit L h w a).Realize v ↔ ∃ (r : Fin B) (b : Fin n), ↑r * ↑(FirstOrder.Language.Term.realize v h) + ↑b = ↑(FirstOrder.Language.Term.realize v a) ∧ ↑b < ↑(FirstOrder.Language.Term.realize v h) ∧ (↑(FirstOrder.Language.Term.realize v (w r))).testBit ↑b = true

packedBit L h w a holds exactly when position a falls in one of the B words w, of width h, at a set bit.

theorem Cslib.Logic.FO.Ordered.realize_packedField {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {B : ℕ} (h : (language L).Term α) (w : Fin B → (language L).Term α) (a s z : (language L).Term α) (v : α → Fin n) (hspace : B * ↑(FirstOrder.Language.Term.realize v h) < n) : (packedField L h w a s z).Realize v ↔ ↑(FirstOrder.Language.Term.realize v z) = BitString.readPackedField (↑(FirstOrder.Language.Term.realize v h)) (fun (r : Fin B) => ↑(FirstOrder.Language.Term.realize v (w r))) ↑(FirstOrder.Language.Term.realize v a) ↑(FirstOrder.Language.Term.realize v s)

When B words of width h fit in the universe, packedField L h w a s z holds exactly when z is the field of s bits at position a (BitString.readPackedField).