8.2. The first models🔗

Theorem8.2.1

uses 1used by 1✓L∃∀N

Language codes and user ids are keys in every state reachable from the first agent a_0 by checked reactions and user actions: writing \mathrm{KeysDistinct}(a) when no two \mathsf{lang} nodes of a carry the same code and no two \mathsf{user} nodes the same id,

a_0 \Rightarrow^{\mathsf u}_{F_0} a \;\Longrightarrow\; \mathrm{KeysDistinct}(a) .

Rests on NEW: Att, Item, Occ, Par, Prefs, ReachU, agent0, sig; not audited: KeysDistinct, MStep.

Lean code for Theorem8.2.1●1 theorem

theoremdefined in Miolingo/Act.lean

complete

theorem keys_invariantU {a : BD Ctl} (h : ReachU MStep agent0 a) :
  KeysDistinct a

theorem keys_invariantU {a : BD Ctl}
  (h : ReachU MStep agent0 a) :
  KeysDistinct a

**(H1)** First model: codes and ids are keys in every state reachable
by checked reactions and user actions.

Theorem8.2.2

uses 1used by 1✓L∃∀N

The vocabulary table never holds a duplicate key. A row's key is its triple (word, language code, user id); from the agent a_D with an empty table, by checked reactions and user actions,

a_D \Rightarrow^{\mathsf u}_{F_D} a \;\Longrightarrow\; \text{for every node } \mathsf{vocabT}\,\mathit{rows} \text{ of } a,\ \text{the keys of } \mathit{rows} \text{ are pairwise distinct} .

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Occ, Prefs, ReachU, session, sig, tableKeysDistinct; not audited: CStep, agentD.

Lean code for Theorem8.2.2●1 theorem

theoremdefined in Miolingo/Act.lean

complete

theorem dedup_invariantU {a : BD Ctl} (h : ReachU CStep agentD a) :
  a.ctrls.all tableKeysDistinct = true

theorem dedup_invariantU {a : BD Ctl}
  (h : ReachU CStep agentD a) :
  a.ctrls.all tableKeysDistinct = true

**(H2)** D1: every `vocabT` has rows with distinct keys.

Theorem8.2.3

uses 1used by 0✓L∃∀N

Translation validation of the compilation \mathrm{enc} from the table-as-data model to the scan model: a compiled step is a checked step of F_D and carries a validated run of the scan model,

\mathrm{compileStep}(a) = (b, \mathit{ch}, \rho, \sigma) \;\Longrightarrow\; a \Rightarrow^{1}_{F_D} b \;\wedge\; \mathrm{validate}(a, b) = (\mathit{ch}, \rho, \sigma),

\mathrm{validate}(a, b) = (\mathit{ch}, \rho, \sigma) \;\Longrightarrow\; \mathit{ch} \text{ is a chain of certified reactions of } F_0 \text{ from } \mathrm{enc}(a) \text{ to some } l \text{ with } l \cdot \rho = \mathrm{enc}(b) \cdot \sigma ,

where \mathrm{enc}(a) and \mathrm{enc}(b) are defined, \Rightarrow^{1} is a single checked step, and \rho, \sigma are valid renumberings of nodes. Nothing is claimed for steps the validator rejects; the general simulation theorem is OPEN.

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Item, Occ, Par, Prefs, Run.Chain, enc, evalScore and 2 more; not audited: BD.n, CStep, EditForm, Row, Table, View, compileStep, validate.

Lean code for Theorem8.2.3●2 theorems

theoremdefined in Miolingo/D2.lean

complete

theorem compileStep_sound {a b : BD Ctl} {ch : List (BD Ctl)} {ρ σ : Ren}
  (h : compileStep a = some (b, ch, ρ, σ)) :
  CStep a b ∧ validate a b = some (ch, ρ, σ)

theorem compileStep_sound {a b : BD Ctl}
  {ch : List (BD Ctl)} {ρ σ : Ren}
  (h :
    compileStep a = some (b, ch, ρ, σ)) :
  CStep a b ∧
    validate a b = some (ch, ρ, σ)

theoremdefined in Miolingo/D2.lean

complete

theorem validate_sound {a b : BD Ctl} {ch : List (BD Ctl)} {ρ σ : Ren}
  (h : validate a b = some (ch, ρ, σ)) :
  ∃ ea eb last,
    D2.enc a = some ea ∧
      D2.enc b = some eb ∧
        Run.Chain (Run.Certified sig rules) ch ∧
          ch.head? = some ea ∧
            ch.getLast? = some last ∧
              ρ.check last.n = true ∧
                σ.check eb.n = true ∧ BD.perm ρ last = BD.perm σ eb

theorem validate_sound {a b : BD Ctl}
  {ch : List (BD Ctl)} {ρ σ : Ren}
  (h : validate a b = some (ch, ρ, σ)) :
  ∃ ea eb last,
    D2.enc a = some ea ∧
      D2.enc b = some eb ∧
        Run.Chain
            (Run.Certified sig rules) ch ∧
          ch.head? = some ea ∧
            ch.getLast? = some last ∧
              ρ.check last.n = true ∧
                σ.check eb.n = true ∧
                  BD.perm ρ last =
                    BD.perm σ eb

**(D2.1) What a validated step certifies**: a chain of certified
reactions of the scan model from `enc a` whose last state, renumbered,
is `enc b` renumbered.  By `step_sound` each link of the chain is a
reaction of the library's BRS; by `perm_sound` (S2a) the renumberings
are support translations.