locus: Blueprint

8.4. The app model🔗

Definition8.4.1
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 8.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgednew

The app model follows the deployed app feature by feature. Its outside world E is a parameter: phonetic codes, IPA and translation of a text, and the database's pattern matching, regular expressions and collation order, each a total function. The family F_A(E) consists of the view and language rules, the practice rules (record, check pronunciation with or without capture of the word, add a word) and the vocabulary rules (search, sort, edit, save, delete, notes, auto-fill, practise the listing, add from a passage, import), each instance under its side condition. Its vocabulary table is one control \mathsf{vocabE}\,t, whose rows have the key (normalised word, language, user).

Class: famA BRIDGED; App.Env NEW.

Lean code for Definition8.4.1●2 definitions
  • defdefined in Miolingo/App.lean
    complete
    def famA (E : App.Env) (r : RuleD Ctl) : Bool
    def famA (E : App.Env) (r : RuleD Ctl) : Bool
    **The family**, decidable, for a given outside world `E`.
  • structure(6 fields)defined in Miolingo/App.lean
    complete
    structure Env : Type
    structure Env : Type

    Fields

    phon : String → String → String
    espeak `-x` codes of a text, with a voice. 
    ipaOf : String → String → Option String
    espeak IPA of a text in a language (`none`: unavailable). 
    translate : String → String → String → Option String
    translation of a text from one language to another (`none`: error). 
    like : String → String → Bool
    MySQL `LIKE` under the table's collation (pattern, text). 
    regexp : String → String → Bool
    MySQL `REGEXP` (pattern, text). 
    collLe : String → String → Bool
    MySQL ordering of keys under the collation (`≤`).
Theorem8.4.2
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The invariants of the app model, for every outside world E, from the one-user agent a_A, by checked reactions and user actions:

a_A \Rightarrow^{\mathsf u}_{F_A(E)} a \;\Longrightarrow\; \text{every } \mathsf{vocabE} \text{ and } \mathsf{vocabT} \text{ of } a \text{ has distinct keys} \;\wedge\; \mathrm{KeysDistinct}(a) \;\wedge\; \#\{\text{nodes } \mathsf{shown}\,v \text{ of } a\} \le 1 .

The reachable set is not the start state alone: a list of states in which each follows the one before by a user action or by a step the simulator returns is a walk, and every state of a checked walk is reachable (walkA_sound). The scenario "say Bonjour, check it", ending with one vocabulary row and one attempt, is such a walk in the stand-in world: TESTED in the library, and PROVED by kernel evaluation in Miolingo/ActChecks.lean (s1_reachableU), a module built on demand.

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Env, Item, Occ, Opts, Par, Prefs, ReachU and 9 more; not audited: KeysDistinct, agentA, walkA.

Lean code for Theorem8.4.2●2 theorems
  • theoremdefined in Miolingo/Act.lean
    complete
    theorem invariantsAU (E : App.Env) {a : BD Ctl}
  (h : ReachU (CStepA E) agentA a) :
  a.ctrls.all tblOk = true ∧
    KeysDistinct a ∧ List.countP isShown a.ctrls ≤ 1
    theorem invariantsAU (E : App.Env) {a : BD Ctl}
  (h : ReachU (CStepA E) agentA a) :
  a.ctrls.all tblOk = true ∧
    KeysDistinct a ∧
      List.countP isShown a.ctrls ≤ 1
    **(H5)** App model, for every outside world `E`: distinct table keys,
codes and ids are keys, at most one view shown, in every state
reachable by checked reactions and user actions.
  • theoremdefined in Miolingo/Act.lean
    complete
    theorem walkA_sound (E : App.Env) (l : List (BD Ctl)) (a0 a : BD Ctl) :
  ReachU (CStepA E) a0 a →
    walkA E a l = true → ∀ (x : BD Ctl), x ∈ l → ReachU (CStepA E) a0 x
    theorem walkA_sound (E : App.Env)
  (l : List (BD Ctl)) (a0 a : BD Ctl) :
  ReachU (CStepA E) a0 a →
    walkA E a l = true →
      ∀ (x : BD Ctl),
        x ∈ l → ReachU (CStepA E) a0 x
    **(W1)** Every state of a checked walk from `a` is reachable from `a`.
Definition8.4.3
Statement uses 2
Statement dependency previews
Preview
Definition 8.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsnew

NEW. The shape of a state of the app model is stated by parents, because a checked reaction keeps the parent of a node outside the redex. Each control c has a list \mathrm{homes}(c) of places it may sit in: the server's root, a session's root, or inside a container of a given class; the list is empty for a control that is not of the app model. The place \mathrm{place}_a(p) a parent p gives is the server for root 0, a session for any other root, and the class of its control for a node (none when that control is not a container).

W_1(a) \;:\Longleftrightarrow\; \text{every node of } a \text{ with control } c \text{ and parent } p \text{ has } c \text{ a request control, or } \mathrm{place}_a(p) \in \mathrm{homes}(c) ,

I_3(a) \;:\Longleftrightarrow\; \text{for every node } \mathsf{langSel}\,A\,B\,s\,c \text{ of } a,\ \text{nodes } \mathsf{lang}\,s \text{ and } \mathsf{lang}\,c \text{ occur in } a .

Both are decidable. The check \mathrm{ruleOk}(r) is the conjunction of eleven decidable conditions on one rule r, among them R_1 (inside the reactum a node under a node sits in a home), R_2' (under each root the redex has a node that is not a request, and every home common to the redex's such nodes there is a home of each reactum node there), R_3 (a kept site stays under the same class of container, or the same root), R_5 (a discarded site is the whole content of an audio or result slot of the redex) and R_6 (the reactum keeps every \mathsf{lang} node of the redex, and a setting of the reactum that is not one of the redex names only languages named by the redex's settings or present in the redex).

Lean code for Definition8.4.3●6 definitions
  • inductive(11 constructors)defined in Miolingo/Shape.lean
    complete
    inductive Cls : Type
    inductive Cls : Type
    The classes of container, as parents.

    Constructors

    catalogue : Shape.Cls
    users : Shape.Cls
    progress : Shape.Cls
    attempt : Shape.Cls
    sidebar : Shape.Cls
    helm : Shape.Cls
    main : Shape.Cls
    audioIn : Shape.Cls
    resultIn : Shape.Cls
    reader : Shape.Cls
    view (v : View) : Shape.Cls
  • defdefined in Miolingo/Shape.lean
    complete
    def homes : Ctl → List Shape.Home
    def homes : Ctl → List Shape.Home
    The homes of a control of the app model (none: not a control of the app model).
  • defdefined in Miolingo/Shape.lean
    complete
    def placeOf (d : BD Ctl) : Par → Option Shape.Home
    def placeOf (d : BD Ctl) :
  Par → Option Shape.Home
    The place a parent gives: by the parent's class, or by the root.
  • defdefined in Miolingo/Shape.lean
    complete
    def W1 (d : BD Ctl) : Bool
    def W1 (d : BD Ctl) : Bool
    W1: every node that is not a request sits in one of its homes.
  • defdefined in Miolingo/Shape.lean
    complete
    def I3 (d : BD Ctl) : Bool
    def I3 (d : BD Ctl) : Bool
    I3: the languages of every setting are present.
  • defdefined in Miolingo/Shape.lean
    complete
    def ruleOk (r : RuleD Ctl) : Bool
    def ruleOk (r : RuleD Ctl) : Bool
    All the per-rule checks in force.
Lemma8.4.4
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

One step keeps the shape. For any signature and rule family F, an occurrence o of a rule r that passes the checker in a, with result b:

o \checkmark_F a \;\wedge\; R_1(r) \wedge R_2'(r) \wedge R_3(r) \;\wedge\; W_1(a) \;\Longrightarrow\; W_1(b) ,

o \checkmark_F a \;\wedge\; R_5(r) \wedge R_6(r) \;\wedge\; W_1(a) \wedge I_3(a) \;\Longrightarrow\; I_3(b) ,

and a user action keeps each:

a \rightsquigarrow b \;\wedge\; W_1(a) \;\Longrightarrow\; W_1(b) , \qquad a \rightsquigarrow b \;\wedge\; I_3(a) \;\Longrightarrow\; I_3(b) .

Rests on UNBRIDGED: Act; NEW: Act, Att, Occ, Prefs, Shape.I3, Shape.R1, Shape.R2', Shape.R3 and 3 more; not audited: EditForm, Row, Table, View.

Lean code for Lemma8.4.4●4 theorems
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem w1_react {S : Sig Ctl} {fam : RuleD Ctl → Bool} {a : BD Ctl}
  {o : Occ Ctl} (hc : Occ.check S fam a o = true)
  (h1 : Shape.R1 o.rule = true) (h2 : Shape.R2' o.rule = true)
  (h3 : Shape.R3 o.rule = true) (hW : Shape.W1 a = true) :
  Shape.W1 o.result = true
    theorem w1_react {S : Sig Ctl}
  {fam : RuleD Ctl → Bool} {a : BD Ctl}
  {o : Occ Ctl}
  (hc : Occ.check S fam a o = true)
  (h1 : Shape.R1 o.rule = true)
  (h2 : Shape.R2' o.rule = true)
  (h3 : Shape.R3 o.rule = true)
  (hW : Shape.W1 a = true) :
  Shape.W1 o.result = true
    **T1, one reaction.** A checked reaction of a rule passing `R1`, `R2'`
and `R3` keeps `W1`.
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem w1_act {a b : BD Ctl} (h : Act a b) (hW : Shape.W1 a = true) :
  Shape.W1 b = true
    theorem w1_act {a b : BD Ctl} (h : Act a b)
  (hW : Shape.W1 a = true) :
  Shape.W1 b = true
    **T1, one action.** A user action keeps `W1`.
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem i3_react {S : Sig Ctl} {fam : RuleD Ctl → Bool} {a : BD Ctl}
  {o : Occ Ctl} (hc : Occ.check S fam a o = true)
  (h5 : Shape.R5 o.rule = true) (h6 : Shape.R6 o.rule = true)
  (hW : Shape.W1 a = true) (hI : Shape.I3 a = true) :
  Shape.I3 o.result = true
    theorem i3_react {S : Sig Ctl}
  {fam : RuleD Ctl → Bool} {a : BD Ctl}
  {o : Occ Ctl}
  (hc : Occ.check S fam a o = true)
  (h5 : Shape.R5 o.rule = true)
  (h6 : Shape.R6 o.rule = true)
  (hW : Shape.W1 a = true)
  (hI : Shape.I3 a = true) :
  Shape.I3 o.result = true
    **T2, one reaction.** A checked reaction of a rule passing `R5` and `R6`
keeps `I3`, from a state with `W1`.
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem i3_act {a b : BD Ctl} (h : Act a b) (hI : Shape.I3 a = true) :
  Shape.I3 b = true
    theorem i3_act {a b : BD Ctl} (h : Act a b)
  (hI : Shape.I3 a = true) :
  Shape.I3 b = true
    **T2, one action.** A user action keeps `I3`.
Theorem8.4.5
Statement uses 2
Statement dependency previews
Preview
Theorem 8.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

CONDITIONAL on the hypothesis \mathrm{F}(E): every rule in Member E passes \mathrm{ruleOk}, where Member E contains every rule of the family F_A(E) (member_of_famA) and may contain more. \mathrm{F}(E) is a hypothesis of the theorem and is not proved: OPEN (TESTED on the fixed rules and on instances of the others). Assuming it, for every outside world E and every start state a_0,

\mathrm{F}(E) \;\wedge\; W_1(a_0) \wedge I_3(a_0) \;\wedge\; a_0 \Rightarrow^{\mathsf u}_{F_A(E)} a \;\Longrightarrow\; W_1(a) .

The start agents satisfy the hypothesis on a_0, by kernel evaluation: W_1(a_A) \wedge I_3(a_A) for the one-user agent and the same for the two-user agent.

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Env, Opts, ReachU, Shape.I3, Shape.W1, Shape.ruleOk; not audited: agent2A, agentA.

Lean code for Theorem8.4.5●3 theorems
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem t1 (E : App.Env)
  (hF : ∀ (r : RuleD Ctl), Member E r → Shape.ruleOk r = true)
  {a0 a : BD Ctl} (h0 : Shape.W1 a0 = true ∧ Shape.I3 a0 = true)
  (h : ReachU (CStepA E) a0 a) : Shape.W1 a = true
    theorem t1 (E : App.Env)
  (hF :
    ∀ (r : RuleD Ctl),
      Member E r → Shape.ruleOk r = true)
  {a0 a : BD Ctl}
  (h0 :
    Shape.W1 a0 = true ∧
      Shape.I3 a0 = true)
  (h : ReachU (CStepA E) a0 a) :
  Shape.W1 a = true
    **T1** (CONDITIONAL on `F`).
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem agentA_ok : Shape.W1 agentA = true ∧ Shape.I3 agentA = true
    theorem agentA_ok :
  Shape.W1 agentA = true ∧
    Shape.I3 agentA = true
    The start agents satisfy `W1` and `I3` (kernel-checked).
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem agent2A_ok : Shape.W1 agent2A = true ∧ Shape.I3 agent2A = true
    theorem agent2A_ok :
  Shape.W1 agent2A = true ∧
    Shape.I3 agent2A = true
Theorem8.4.6
Statement uses 2
Statement dependency previews
Preview
Lemma 8.4.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

CONDITIONAL on the same hypothesis \mathrm{F}(E) (every rule in Member E, which contains the family F_A(E), passes \mathrm{ruleOk}), which is not proved: OPEN. Assuming it, for every E and every start state a_0,

\mathrm{F}(E) \;\wedge\; W_1(a_0) \wedge I_3(a_0) \;\wedge\; a_0 \Rightarrow^{\mathsf u}_{F_A(E)} a \;\Longrightarrow\; I_3(a) .

Rests on NEW: Env, ReachU, Shape.I3, Shape.W1, Shape.ruleOk.

Lean code for Theorem8.4.6●1 theorem
  • theoremdefined in Logic/MiolingoShape.lean
    complete
    theorem t2 (E : App.Env)
  (hF : ∀ (r : RuleD Ctl), Member E r → Shape.ruleOk r = true)
  {a0 a : BD Ctl} (h0 : Shape.W1 a0 = true ∧ Shape.I3 a0 = true)
  (h : ReachU (CStepA E) a0 a) : Shape.I3 a = true
    theorem t2 (E : App.Env)
  (hF :
    ∀ (r : RuleD Ctl),
      Member E r → Shape.ruleOk r = true)
  {a0 a : BD Ctl}
  (h0 :
    Shape.W1 a0 = true ∧
      Shape.I3 a0 = true)
  (h : ReachU (CStepA E) a0 a) :
  Shape.I3 a = true
    **T2** (CONDITIONAL on `F`).
Theorem8.4.7
uses 1used by 1✓L∃∀N

The generator \mathrm{genL}_E, which proposes rule instances from a list of controls, is complete for the family: for every list \mathit{cs} of controls and every rule r,

r \in F_A(E) \;\wedge\; \mathrm{ctrls}(\mathrm{redex}\ r) \subseteq \mathit{cs} \;\Longrightarrow\; r \in \mathrm{genL}_E(\mathit{cs}) .

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Env, GenComplete, Item, Opts, Par, Prefs, evalScore and 4 more; not audited: genL.

Lean code for Theorem8.4.7●1 theorem
  • theoremdefined in Miolingo/AppInv.lean
    complete
    theorem genL_genComplete (E : App.Env) :
  GenComplete (fun r => famA E r = true) (App.genL E)
    theorem genL_genComplete (E : App.Env) :
  GenComplete (fun r => famA E r = true)
    (App.genL E)
    **`GenComplete` for the app family**, the hypothesis of the logic
lane's `rulesOf_lf`: with `brs_imageFinite_lf`, the library BRS of the
app family is image-finite, for every `E`.
Theorem8.4.8
uses 1used by 0✓L∃∀N

CLASSICAL. For every E, the reactive system of the app model's rules is image-finite up to support equivalence: for every agent a, label L and set of locations there is a finite list l of agents with

a \xrightarrow{L} a' \;\Longrightarrow\; \exists c \in l.\;\; a' \bumpeq c ,

the transitions being those of \mathrm{BRS}(\mathrm{rulesOf}(F_A(E))) at those locations. The theorem is in Miolingo/AppImageFinite.lean.

Rests on NEW: Env, ImageFinite, rulesOf, sig.

Lean code for Theorem8.4.8●1 theorem
  • theoremdefined in Miolingo/AppImageFinite.lean
    complete
    theorem app_imageFinite (E : App.Env) :
  ImageFinite (BRS (rulesOf fun r => famA E r = true))
    theorem app_imageFinite (E : App.Env) :
  ImageFinite
    (BRS
      (rulesOf fun r => famA E r = true))
    **Image-finiteness of the app model**, up to support equivalence.