Initial Algebras & Foldsconcept:initial-algebras-folds

hom-eq-cata-effclaim:hom-eq-cata-eff

Pointwise equality of algebra homomorphisms with cata_eff

Module

Effect4.Program.Fold

Literature

MeijerFokkingaPaterson1991, audit P24 (definitionUsed)

Literature

Gibbons2002, audit P12 (proofTechnique)

∀ {Op : Type} {R : Effect4.Program.EffFam → Type u} {alg : Effect4.Program.EffAlgebra Op R}
  (hom : Effect4.Program.EffHom alg) (node : Effect4.Program.Eff Op),
  Eq (hom.f_eff node) (Effect4.Program.cata_eff alg node)

inhabited-iff-fitsclaim:inhabited-iff-fits

Syntactic inhabited fold agrees with semantic value existence in Fits

Inhabitance agrees with membership (proved), on every type: the fold says true exactly when some world has a member. Row 127's agreement theorem.

Module

Effect4.Laws.Program.Typed.Membership

Literature

TAPL, §16.1, p. 210 (adaptedResult)

∀ (t : Effect4.Program.Ty),
  Iff (Eq (Effect4.Program.inhabited t) Bool.true)
    (Exists fun w => Exists fun v => Effect4.Program.Typed.Fits w v t)

cata-eff-congr-onclaim:cata-eff-congr-on

Fold congruence along agreeing signature algebras

Fold congruence at Eff.

Module

Effect4.Laws.Program.Signature

∀ {Op : Type} {R : Effect4.Program.EffFam → Type u} {alg₁ alg₂ : Effect4.Program.EffAlgebra Op R}
  {okOp : Op → Prop} {okKey : Effect4.ServiceKey → Prop} {okDef : Nat → Prop},
  alg₁.AgreeOn alg₂ okOp okKey okDef →
    ∀ (e : Effect4.Program.Eff Op),
      Effect4.Program.cata_eff (Effect4.Program.readsAlg okOp okKey okDef) e →
        Eq (Effect4.Program.cata_eff alg₁ e) (Effect4.Program.cata_eff alg₂ e)

addressed-replacementclaim:addressed-replacement

Successful same-sort path replacement reads back, retains the root sort, and restores the original tree

A successful addressed edit exposes its replacement, preserves the root sort, and is reversed by restoring the original node. This is the structural witness for Concept 7's proposed addressed-replacement claim, consumed by the layer laws below.

Module

Effect4.Laws.Program.References

∀ {Op : Type} {node result replacement : Effect4.Program.Node Op} {path : List Nat},
  Eq (node.replaceAt path replacement) (Option.some result) →
    And (Eq (result.at_ path) (Option.some replacement))
      (And (Eq result.ctorIdx node.ctorIdx)
        (∀ (old : Effect4.Program.Node Op),
          Eq (node.at_ path) (Option.some old) → Eq (result.replaceAt path old) (Option.some node)))

address-composesclaim:address-composes

An address is a composite of child lenses: the node and the environment at p ++ q are the ones at q inside the node at p (Node.at_append, Node.envAt_append), and an edit at p ++ q is the edit at q inside the node at p, put back at p (Node.replaceAt_append); below an edit the edited node reads the replacement; nothing of typing, of behaviour, or of a moved subtree's variable levels and layer-reference targets (seat ORG's theory map, section 3)

An edit at p ++ q is the edit at q inside the node at p, put back at p. The pointer of address-composes. No proof consumes it yet: the splice over a whole program's parts reads a block's two children directly (Node.replaceAt_defs_main, Node.replaceAt_defs_body). A move or a paste of a subtree is its first consumer.

Module

Effect4.Laws.Program.Address

∀ {Op : Type} (n : Effect4.Program.Node Op) (p q : List Nat) (r : Effect4.Program.Node Op),
  Eq (n.replaceAt (instHAppendOfAppend.hAppend p q) r)
    ((n.at_ p).bind fun m => (m.replaceAt q r).bind fun m' => n.replaceAt p m')

path-fold-naturalclaim:path-fold-natural

A path fold is natural in its base: the fold from q ++ r is the fold from r with each yield read below q (foldMapAt_eff_base and six siblings), and a map that keeps the operation commutes with the fold (foldMapAt_eff_hom); the address list's shift is their instance; nothing of a judgment, a table, or a refusal's location, which the checker's base law owns (checker-base-natural; seat ORG's L5 and L6)

A path fold from q ++ r is the fold from r, each yield read below q. At a program. The pointer of path-fold-natural.

Module

Effect4.Laws.Program.Address

∀ {Op : Type} {M : Type u} (unit : M) (op : M → M → M) (e : Effect4.Program.Eff Op) (q r : List Nat)
  (f1 : Effect4.Program.Eff Op → List Nat → M) (f2 : Effect4.Program.Stmt Op → List Nat → M)
  (f3 : Effect4.Program.Stmts Op → List Nat → M) (f4 : Effect4.Program.Effs Op → List Nat → M)
  (f5 : Effect4.Program.ActionTerm Op → List Nat → M)
  (f6 : Effect4.Program.LayerTerm Op → List Nat → M)
  (f7 : Effect4.Program.LayerTerms Op → List Nat → M),
  Eq
    (Effect4.Program.foldMapAt_eff unit op (instHAppendOfAppend.hAppend q r) e f1 f2 f3 f4 f5 f6 f7)
    (Effect4.Program.foldMapAt_eff unit op r e (fun x p => f1 x (instHAppendOfAppend.hAppend q p))
      (fun x p => f2 x (instHAppendOfAppend.hAppend q p))
      (fun x p => f3 x (instHAppendOfAppend.hAppend q p))
      (fun x p => f4 x (instHAppendOfAppend.hAppend q p))
      (fun x p => f5 x (instHAppendOfAppend.hAppend q p))
      (fun x p => f6 x (instHAppendOfAppend.hAppend q p)) fun x p =>
      f7 x (instHAppendOfAppend.hAppend q p))

checker-base-naturalclaim:checker-base-natural

The checker is natural in its base path: checking at q ++ p is checking at p with each refusal moved below q (Checker.check_rebase and its six siblings), so a subtree's table at q ++ a is its table at a with each entry moved below q (tableAt_rebase); nothing of the verdict's correctness (check_sound), of a definition block's module check, or of cost (seat ORG's L7 and L8)

The checker at q ++ p is the checker at p, its refusal moved below q. The pointer of checker-base-natural.

Module

Effect4.Laws.Program.Typing.Rebase

∀ {Op : Type} (sig : Effect4.Program.Signature Op) (q : List Nat) (env : Effect4.Program.TyEnv)
  (p : List Nat) (e : Effect4.Program.Eff Op),
  Eq (Effect4.Program.Checker.check sig env (instHAppendOfAppend.hAppend q p) e)
    (Except.mapError (Effect4.Program.TypeRefusal.rebase q)
      (Effect4.Program.Checker.check sig env p e))

operation-data-scopedclaim:operation-data-scoped

The scope fold decides a perform node: scoped exactly when its operation's own data (the alphabet's ScopedOp) and its request are

An operation's own data is scope-checked. A perform node is scoped at level n exactly when its operation's data is, by the alphabet's ScopedOp instance, and its request is: the generated operation arm of the scope fold (scopedAlgebra, Program/Scoped.lean), read as a decision.

Concept initial-algebras-folds, claim operation-data-scoped (role decidability), serving R4 (state plan T0). Reach: the scope check Eff.scopedAt, at every level, at every alphabet with a ScopedOp instance, with no other hypothesis. It does not establish term typing: scope is not typing, and the type of a term an operation carries is state plan T3's (rowTy). It does not establish that an instance follows ScopedOp's binder convention, which is each instance's contract. Consumer: T3's term rows, where the checker refuses an unscoped term before typing it; the red controls are Test/Program/ScopedOpContract.lean.

Module

Effect4.Laws.Program.Authoring

∀ {Op : Type} [inst : Effect4.Program.ScopedOp Op] (n : Nat) (op : Op) (arg : Effect4.Program.Term),
  Iff (Eq (Effect4.Program.Eff.scopedAt n (Effect4.Program.Eff.perform op arg)) Bool.true)
    (And (Eq (inst.scopedAt op n) Bool.true) (Eq (Effect4.Program.Term.scoped n arg) Bool.true))

reference-expansion-completeclaim:reference-expansion-complete

A program with well-formed layer references expands to a program with no reference site, at the bound of expandRefs

A well-formed program expands to a program with no reference site, at the bound that Eff.expandRefs uses: one more round than the program has reference sites. The case of no reference site is the same statement, at one round.

Module

Effect4.Laws.Program.ReferenceExpansion

∀ {Op : Type} (root : Effect4.Program.Eff Op),
  Eq root.layerRefsWF Bool.true →
    Eq (Effect4.Program.Eff.refSites List.nil root.expandRefs) List.nil

sketch-conservativeclaim:sketch-conservative

A program that performs no hole row is checked the same with any hole table appended after the application's rows, refusals included, at every environment and path (decisions rows 288, 291)

H1, the claim sketch-conservative: a program that performs no hole is checked the same with any hole table, refusals included, at every environment and path. The premise is SigProgram at the application's signature: every operation that the program performs is one of the application's, and every service key that it reads has a carrier. It is C3's reflection (check_restrict) at the hole table.

Module

Effect4.Laws.Program.Sketch

∀ (app : Effect4.Program.SigApp) (holes : Effect4.Program.RowTable) {e : Effect4.Program.NativeEff},
  Effect4.Program.SigProgram app.signature e →
    ∀ (env : Effect4.Program.TyEnv) (p : List Nat),
      Eq (Effect4.Program.Checker.check (app.withHoles holes).signature env p e)
        (Effect4.Program.Checker.check app.signature env p e)

sketch-weakeningclaim:sketch-weakening

A program with holes that the checker admits stays admitted at its type with more holes declared, and the checker reads the rows of the holes that the program performs and no later row

The claim sketch-weakening, as one statement: H2 and H3 for one application and two hole tables. It is the pointer that the claim's row needs, and it adds nothing to its two parts.

Module

Effect4.Laws.Program.Sketch

∀ (app : Effect4.Program.SigApp) (holes more : Effect4.Program.RowTable),
  And
    (∀ {e : Effect4.Program.NativeEff} {env : Effect4.Program.TyEnv} {p : List Nat}
      {t : Effect4.Program.EffTy},
      Eq (Effect4.Program.Checker.check (app.withHoles holes).signature env p e) (Except.ok t) →
        Eq
          (Effect4.Program.Checker.check
            (app.withHoles (instHAppendOfAppend.hAppend holes more)).signature env p e)
          (Except.ok t))
    (∀ {e : Effect4.Program.NativeEff},
      Effect4.Program.SigProgram (app.withHoles holes).signature e →
        ∀ (env : Effect4.Program.TyEnv) (p : List Nat),
          Eq
            (Effect4.Program.Checker.check
              (app.withHoles (instHAppendOfAppend.hAppend holes more)).signature env p e)
            (Effect4.Program.Checker.check (app.withHoles holes).signature env p e))

hole-ruleclaim:hole-rule

A hole row with a unit request and closed, formed columns types its perform at those columns in normal form, in every environment, at any position of the hole table; no rule is added to HasTy

The hole's rule, the claim hole-rule: hole k has the type that its row declares, in every environment. The row is a hole row with closed columns that pass strict formation, the check that the row check runs at each use (checkRow). The answer and the error are read in normal form, as the checker gives every type.

No rule is added to the typing judgment: this is HasTy.perform at a closed row (rowTy_closed). The row has no parameter, and its request is a unit, which the literal has in any environment.

Module

Effect4.Laws.Program.Sketch

∀ (app : Effect4.Program.SigApp) (holes : Effect4.Program.RowTable) (k : Nat) {name : String}
  {answer error : Effect4.Program.Ty} {requires : List Effect4.ServiceKey}
  (env : Effect4.Program.TyEnv),
  Eq (List.instGetElem?NatLtLength.getElem? holes k)
      (Option.some (Effect4.Program.Row.hole name answer error requires)) →
    Eq answer.closed Bool.true →
      Eq error.closed Bool.true →
        Effect4.Program.Formation.Formed
            (Effect4.Program.Formation.instantiatedSites
              (Effect4.Program.Row.hole name answer error requires).normalizeTypes List.nil) →
          Conform.Effect4.Typing.HasTy (app.withHoles holes).signature env
            (Effect4.Program.Sketch.hole app k)
            { answer := answer.normalize, error := error.normalize,
              requires := Effect4.Machine.Env.Requirement.ofList requires }

defs-conservativeclaim:defs-conservative

A program that invokes no definition is checked the same at any definition block's signature, refusals included, at every environment and path, with no service key assumed typed (decisions row 328, G1)

G1, the claim defs-conservative (decisions row 328, point 5): a program that invokes no definition is checked the same at any block's signature, refusals included, at every environment and path. No service key is assumed typed: the block's signature changes only an invocation's domain bit and row.

Module

Effect4.Laws.Program.Definitions

∀ {Op : Type} (sig : Effect4.Program.Signature Op) (decls : List Effect4.Program.DefDecl)
  {e : Effect4.Program.Eff Op},
  Effect4.Program.NoInvocation sig e →
    ∀ (env : Effect4.Program.TyEnv) (p : List Nat),
      Eq (Effect4.Program.Checker.check (sig.withDefs decls) env p e)
        (Effect4.Program.Checker.check sig env p e)

invocation-ruleclaim:invocation-rule

At a block's signature the invocation of a definition has the type of the row it declares, in normal form, at its request's type; no rule is added to HasTy (decisions row 328, G2)

G2, the claim invocation-rule (decisions row 328): at a block's signature, the invocation of definition k has the type of the row that definition k declares, in normal form, at its request's type. It is HasTy.perform read at the block's signature: no rule is added to HasTy.

Module

Effect4.Laws.Program.Definitions

∀ {Op : Type} (sig : Effect4.Program.Signature Op) (decls : List Effect4.Program.DefDecl) {op : Op}
  {k : Nat} {d : Effect4.Program.DefDecl},
  Eq (sig.callOf op) (Option.some k) →
    Eq (List.instGetElem?NatLtLength.getElem? decls k) (Option.some d) →
      Eq d.params List.nil →
        ∀ (env : Effect4.Program.TyEnv) (request : Effect4.Program.Term)
          (t : Effect4.Program.EffTy),
          Iff
            (Conform.Effect4.Typing.HasTy (sig.withDefs decls) env
              (Effect4.Program.Eff.perform op request) t)
            (Exists fun requestTy =>
              And (Eq (Effect4.Program.termTy sig env request) (Option.some requestTy))
                (Eq (Effect4.Program.rowTy d.row.normalizeTypes requestTy (sig.termUse env op))
                  (Option.some t)))

module-checkclaim:module-check

The whole module's check and the module judgment agree at the root: what the check accepts the judgment derives, and what the judgment derives the check accepts (decisions row 328, G2)

G2's soundness, the claim module-check: what the module check accepts, the module judgment derives.

Module

Effect4.Laws.Program.Definitions

∀ {Op : Type} (sig : Effect4.Program.Signature Op) (e : Effect4.Program.Eff Op)
  (t : Effect4.Program.EffTy),
  Eq (Effect4.Program.Checker.checkModule sig e) (Except.ok t) → Effect4.Program.ModuleHasTy sig e t

typed-replacementclaim:typed-replacement

A typed node splits at an address of a program into an environment and a type of the focus, and every program of that type in that environment, under every extension of the typing signature, stands in the focus's place with the node keeping its type; one statement over the six typing judgments, with no rule added; the environment and the type are existential, and the focus's type is kept exactly (decisions rows 288, 294)

The replacement law, at a node: the claim typed-replacement. A typed node splits at an address of a program into an environment and a type of the focus. Every program of that type in that environment, under every extension of the signature, stands in the focus's place, and the node keeps its type. The six statements below are its instances. It is NodeHasTy.replace_envAt without the function that names the environment.

Module

Effect4.Laws.Program.Typing.Replace

∀ {Op : Type} {s : Effect4.Program.Signature Op} (path : List Nat) {n : Effect4.Program.Node Op}
  {τ : Effect4.Program.NodeTy Op} {q : Effect4.Program.Eff Op},
  Effect4.Program.NodeHasTy s n τ →
    Eq (n.at_ path) (Option.some (Effect4.Program.Node.eff q)) →
      Exists fun env =>
        Exists fun t =>
          And (Conform.Effect4.Typing.HasTy s env q t)
            (∀ {s' : Effect4.Program.Signature Op} {q' : Effect4.Program.Eff Op}
              {n' : Effect4.Program.Node Op},
              Effect4.Program.SigExtends s s' →
                Conform.Effect4.Typing.HasTy s' env q' t →
                  Eq (n.replaceAt path (Effect4.Program.Node.eff q')) (Option.some n') →
                    Effect4.Program.NodeHasTy s' n' τ)

focus-functionclaim:focus-function

The typing rules invert along a path, as a function: at an address of a program in a typed node, the fold of the step function answers the environment of the focus, the checker answers its type there, and the replacement law holds at that pair with no existential; the step has one case for each arm of Node.child, and Checker.check does not change; one answer costs up to one check of the program (decisions rows 292, 296)

The law at the environment that the step function answers: the claim focus-function. A typed node splits at an address of a program into an environment and a type of the focus, and the environment is the one that Node.envAt computes from the node's own. Every program of that type in that environment, under every extension of the signature, stands in the focus's place, and the node keeps its type. NodeHasTy.replace is this statement without the function.

Module

Effect4.Laws.Program.Typing.Replace

∀ {Op : Type} {s : Effect4.Program.Signature Op} (path : List Nat) {n : Effect4.Program.Node Op}
  {τ : Effect4.Program.NodeTy Op} {q : Effect4.Program.Eff Op},
  Effect4.Program.NodeHasTy s n τ →
    Eq (n.at_ path) (Option.some (Effect4.Program.Node.eff q)) →
      Exists fun env =>
        Exists fun t =>
          And
            (Eq (Effect4.Program.Node.envAt s τ.env n path)
              (Option.some (Effect4.Program.NodeEnv.env env)))
            (And (Conform.Effect4.Typing.HasTy s env q t)
              (∀ {s' : Effect4.Program.Signature Op} {q' : Effect4.Program.Eff Op}
                {n' : Effect4.Program.Node Op},
                Effect4.Program.SigExtends s s' →
                  Conform.Effect4.Typing.HasTy s' env q' t →
                    Eq (n.replaceAt path (Effect4.Program.Node.eff q')) (Option.some n') →
                      Effect4.Program.NodeHasTy s' n' τ))

address-tableclaim:address-table

The address table of a program has one entry for each address of a node, and no other (mem_addresses_iff); an entry of a program holds the environment that the step function answers and the checker's answer there; the distinct refusals of the entries start with the located refusal of explain (refusals_head), and the list is empty exactly when the checker admits the program; an entry after a refused sibling is not reached and holds no answer; the table is a specification, and each entry costs up to one check of the program; no law orders the refusals after the head (decisions row 302)

The list of refusals is empty exactly when the checker admits the program. It is the table's form of explain_none_iff. The pointer of the claim address-table. Its consumer is the query driver's refusals (slice QUERY).

Module

Effect4.Laws.Program.Typing.Table

∀ {Op : Type} (s : Effect4.Program.Signature Op) (env0 : Effect4.Program.TyEnv)
  (p : Effect4.Program.Eff Op),
  Iff (Eq (Effect4.Program.refusals s env0 p) List.nil)
    (Eq (Effect4.Program.effTy s env0 p).isSome Bool.true)

edit-splices-tableclaim:edit-splices-table

An edit that keeps its focus's type splices the address table: in a program that the checker types, replace the sub-program at the address that focusAt answers by a program of the focus's type in the focus's environment; the edited program's table is the old table with the subtree's segment replaced by the new sub-program's table at the focus's environment and the subtree's own addresses (Table.splice), so nothing outside the subtree is checked again; nothing of an edit that changes the type, of layer references, of a refused program, or of a whole program with a block (cutover slice S1; Reps, Teitelbaum and Demers 1983; decisions rows 302 and 334)

An edit that keeps its focus's type splices the address table (the claim edit-splices-table). In a program that the checker types, take the focus that focusAt answers at an address. Replace the sub-program there by a program of the focus's type in the focus's environment. The edited program's table is the old table with the subtree at the address replaced by the new sub-program's table, at the focus's environment and at the subtree's own addresses. Nothing outside the subtree is checked again.

Module

Effect4.Laws.Program.Typing.Splice

∀ {Op : Type} {s : Effect4.Program.Signature Op} {env0 : Effect4.Program.TyEnv}
  {p p' q' : Effect4.Program.Eff Op} {T : Effect4.Program.EffTy} {path : List Nat}
  {f : Effect4.Program.Focus Op},
  Conform.Effect4.Typing.HasTy s env0 p T →
    Eq (Effect4.Program.focusAt s env0 p path) (Option.some f) →
      Conform.Effect4.Typing.HasTy s f.env q' f.ty →
        Eq ((Effect4.Program.Node.eff p).replaceAt path (Effect4.Program.Node.eff q'))
            (Option.some (Effect4.Program.Node.eff p')) →
          Eq (Effect4.Program.table s env0 p')
            (Effect4.Program.Table.splice (Effect4.Program.table s env0 p) path
              (Effect4.Program.tableAt s (Option.some (Effect4.Program.NodeEnv.env f.env))
                (Effect4.Program.Node.eff q') path))

edit-session-coherentclaim:edit-session-coherent

What an edit session shows after an open and any run of edits is the checker's answer on its sketch, refusals and type, definition blocks and holes included, because its table stays its sketch's table: the open computes it part by part, and each edit keeps it, splicing below the root where the table types the root and the edited address and the checker gives the new sub-program the old type at the part's signature (Sketch.table_fill), and computing it again elsewhere; nothing of an edit of the hole table, of a run of the program, or of the cost (decisions row 334)

What a session shows is the checker's answer on its sketch, after an open and any run of edits: the sketch's refusals, whose head is the check's and which are empty exactly when the sketch checks, and the sketch's type. An edit that splices checks only its new subtree; an edit that checks again checks the whole sketch. The pointer of edit-session-coherent.

Module

Effect4.Laws.Program.Edit

∀ (app : Effect4.Program.SigApp) (s : Effect4.Program.Sketch) (edits : List Effect4.Program.Edit),
  And
    (Eq ((Effect4.Program.EditSession.open app s).run edits).view.refusals
      (((Effect4.Program.EditSession.open app s).run edits).sketch.refusals app))
    (Eq ((Effect4.Program.EditSession.open app s).run edits).view.type
      (((Effect4.Program.EditSession.open app s).run edits).sketch.check app).toOption)

edit-session-undoclaim:edit-session-undo

An edit that applies, then the edit that puts back the old sub-program, restores a coherent edit session exactly, its table included: the path lens's get-put (replaceAt_spec) restores the sketch, and coherence the table; nothing of two edits at disjoint addresses, or of undoing a run (decisions row 334)

Undo: an edit that applies, then the edit that puts back the old sub-program, restores a coherent session exactly, its table included. The path lens's get-put (replaceAt_spec) restores the sketch, and coherence restores the table. The pointer of edit-session-undo.

Module

Effect4.Laws.Program.Edit

∀ {l : Effect4.Program.EditSession},
  l.Coherent →
    ∀ {a : List Nat} {q old : Effect4.Program.NativeEff} {s' : Effect4.Program.Sketch},
      Eq ((Effect4.Program.Node.eff l.sketch.program).at_ a)
          (Option.some (Effect4.Program.Node.eff old)) →
        Eq (l.sketch.fillAt a q) (Option.some s') →
          Eq
            ((l.feed (Effect4.Program.Edit.fill a q)).fst.feed
                (Effect4.Program.Edit.fill a old)).fst
            l

edit-repaint-setclaim:edit-repaint-set

A spliced edit repaints its subtree and nothing else: the addresses an edit session shows again after an edit that kept its focus's type are the new subtree's, at the edited address, and every entry of the new table at another address is an entry of the old table; nothing of an edit that changes the type, which shows the whole table again, or of a page drawn from the table (decisions row 334; the live authoring note's repaint set)

A spliced edit repaints its subtree and nothing else: the addresses it shows again are the new subtree's, and every entry of the new table at another address is an entry of the old table. The pointer of edit-repaint-set.

Module

Effect4.Laws.Program.Edit

∀ {l : Effect4.Program.EditSession} {a : List Nat} {q : Effect4.Program.NativeEff}
  {shown : List (List Nat)},
  Eq (l.feed (Effect4.Program.Edit.fill a q)).snd (Effect4.Program.Edit.Delta.spliced shown) →
    And
      (Eq shown
        (List.map (fun x => instHAppendOfAppend.hAppend a x)
          (Effect4.Program.Node.eff q).addresses))
      (∀ (x : Effect4.Program.Table.Entry),
        List.instMembership.mem (l.feed (Effect4.Program.Edit.fill a q)).fst.table x →
          Not (List.instMembership.mem shown x.path) → List.instMembership.mem l.table x)

module-address-tableclaim:module-address-table

The address table of a sketch reads a whole program, definition block included: the root's entry holds the module check's answer, and every other address is read in the part that holds it, at the part's signature and environment, located at the whole program's address; the distinct refusals start with the sketch's check's refusal (Sketch.refusals_head), and the list is empty exactly when the sketch checks; every part of a typed module is typed (moduleHasTy_partAt_typed); no law orders the refusals after the head, and no law yet equates the table with the program's off a block (cutover slice S1; decisions rows 302, 328 and 333)

The list of refusals of a sketch is empty exactly when the sketch checks, block included: the proposed claim module-address-table. Its consumer is the query tool's refusals.

Module

Effect4.Laws.Program.Sketch

∀ (s : Effect4.Program.Sketch) (app : Effect4.Program.SigApp),
  Iff (Eq (s.refusals app) List.nil) (Eq (s.check app).toOption.isSome Bool.true)

module-annotate-tableclaim:module-annotate-table

A sketch's address table, computed part by part (Sketch.annotate: the module check's answer at the root, each body's table at its base in its declared request, the main program's table at [1], all at the block's signature), is its table's specification (Sketch.table), refused sketches and mismatched blocks included; nothing of the cost (decisions rows 328, 333 and 334)

A sketch's table, part by part, is its table. The pointer of module-annotate-table.

Module

Effect4.Laws.Program.Typing.PartsTable

∀ (s : Effect4.Program.Sketch) (app : Effect4.Program.SigApp), Eq (s.annotate app) (s.table app)

module-table-splicesclaim:module-table-splices

A filling at a sketch's focus below the root, of the focus's type in the focus's environment at the part's signature, splices the whole program's table: the root keeps the module check's answer, the other parts' entries stay, and the edited part's segment is the splice law's, definition blocks included; nothing of an edit at the root, of an edit that changes the type, or of layer references (decisions rows 328, 333 and 334)

A filling at a sketch's focus, of the focus's type, splices the sketch's table. Below the root, in the part that holds the address, at the part's signature: the root's entry holds the same check, the other parts' entries stay, and the part's segment is the splice law's. The pointer of module-table-splices.

Module

Effect4.Laws.Program.Typing.PartsTable

∀ {s s' : Effect4.Program.Sketch} {app : Effect4.Program.SigApp} {T : Effect4.Program.EffTy}
  {path : List Nat} {f : Effect4.Program.Focus Effect4.Program.NativeOp}
  {q' : Effect4.Program.NativeEff},
  Eq (s.check app) (Except.ok T) →
    Ne path List.nil →
      Eq (s.focusAt app path) (Option.some f) →
        Conform.Effect4.Typing.HasTy (s.sigAt app path) f.env q' f.ty →
          Eq (s.fillAt path q') (Option.some s') →
            Eq (s'.table app)
              (Effect4.Program.Table.splice (s.table app) path
                (Effect4.Program.tableAt (s.sigAt app path)
                  (Option.some (Effect4.Program.NodeEnv.env f.env)) (Effect4.Program.Node.eff q')
                  path))

omit-splices-tableclaim:omit-splices-table

An omission at a typed sketch's focus below the root, whose hole row declares the focus's closed and normal columns, splices the table: the hole's one entry replaces the subtree's segment, because a typed sketch's table stays under a grown hole table (Sketch.table_more_holes); a planned goal; until it is proved, the edit session checks the table again at an omission (decisions row 334)

An omission at the focus's type splices the table: the hole row declares the focus's three columns, and the table is the old one with the subtree's segment replaced by the hole's one entry. The grown sketch keeps its table (Sketch.table_more_holes), and the hole is a filling of the focus's type (Sketch.table_fill). The pointer of omit-splices-table.

Module

Effect4.Laws.Program.Edit

∀ {s s' : Effect4.Program.Sketch} {app : Effect4.Program.SigApp} {T : Effect4.Program.EffTy}
  {path : List Nat} {f : Effect4.Program.Focus Effect4.Program.NativeOp} (name : String),
  Eq (s.check app) (Except.ok T) →
    Ne path List.nil →
      Eq (s.focusAt app path) (Option.some f) →
        Eq f.ty.answer.closed Bool.true →
          Eq f.ty.error.closed Bool.true →
            Eq f.ty.answer.normalize f.ty.answer →
              Eq f.ty.error.normalize f.ty.error →
                Effect4.Program.Formation.Formed
                    (Effect4.Program.Formation.instantiatedSites
                      (Effect4.Program.Row.hole name f.ty.answer f.ty.error
                          f.ty.requires.elems).normalizeTypes
                      List.nil) →
                  Eq
                      (s.omitAt app path
                        (Effect4.Program.Row.hole name f.ty.answer f.ty.error f.ty.requires.elems))
                      (Option.some s') →
                    Eq (s'.table app)
                      (Effect4.Program.Table.splice (s.table app) path
                        (List.cons
                          { path := path, env := Option.some (Effect4.Program.NodeEnv.env f.env),
                            result := Option.some (Except.ok f.ty) }
                          List.nil))

module-holes-conservativeclaim:module-holes-conservative

A sketch whose whole program performs no hole, each body and the main program read at the block's signature, is checked by the module check as its program, refusals included (Sketch.check_filled_module); the module check is unchanged under an extension of the signature for such a program (checkModule_restrict); nothing of a program that performs a hole (decisions rows 282 and 328)

H1 on a whole program: a sketch whose program performs no hole is checked as its program by the module check, definition block included. So a sketch with every hole filled is an ordinary module. The pointer of module-holes-conservative.

Module

Effect4.Laws.Program.Sketch

∀ (s : Effect4.Program.Sketch) (app : Effect4.Program.SigApp),
  Effect4.Program.ModuleSigProgram app.signature s.program →
    Eq (s.check app) (Effect4.Program.Checker.checkModule app.signature s.program)

call-instance-addressclaim:call-instance-address

The call instance at an address is the row check's answer: where callAt answers, the node there is a call of the instance's operation, its request has the instance's request type in the address's environment, and the row check at that type answers the instance's two columns; the instance keeps the row's bindings at the request (rowBindings), which instantiate the two columns where the row check answers (checkRow_rowBindings) (nothing about a run's call at that address: no registration records it; decisions row 310)

The call instance is the row check's answer at the request's type. Where callAt answers, the node at the address is a perform of the instance's operation. The request has the instance's request type in the environment at the address. The row check at that type answers the instance's two columns, and the instance's bindings are the row's there.

Module

Effect4.Laws.Program.Typing.Call

∀ {Op : Type} {s : Effect4.Program.Signature Op} {env0 : Effect4.Program.TyEnv}
  {p : Effect4.Program.Eff Op} {path : List Nat} {c : Effect4.Program.CallInstance Op},
  Eq (Effect4.Program.callAt s env0 p path) (Option.some c) →
    Exists fun request =>
      Exists fun env =>
        Exists fun t =>
          And
            (Eq ((Effect4.Program.Node.eff p).at_ path)
              (Option.some (Effect4.Program.Node.eff (Effect4.Program.Eff.perform c.op request))))
            (And
              (Eq
                (Effect4.Program.Node.envAt s (Effect4.Program.NodeEnv.env env0)
                  (Effect4.Program.Node.eff p) path)
                (Option.some (Effect4.Program.NodeEnv.env env)))
              (And (Eq (Effect4.Program.termTy s env request) (Option.some c.request))
                (And
                  (Eq (Effect4.Program.rowTy (s.rowOf c.op) c.request (s.termUse env c.op))
                    (Option.some t))
                  (And (Eq t.answer c.answer)
                    (And (Eq t.error c.error)
                      (Eq
                        (Effect4.Program.rowBindings (s.rowOf c.op) c.request (s.termUse env c.op))
                        (Option.some c.bindings)))))))

annotate-tableclaim:annotate-table

The address table in one traversal: annotate, the checker's seven functions with a record at each node, answers the address table at every program, entry for entry and in its order; each node's checker arm runs once, and a child's environment comes from the answers before it; past a refused read the subtree is not reached, as in the table; no theorem counts the cost, and the left child's entries are copied at each node (decisions rows 302, 324)

The one traversal answers the address table. annotate checks each node once, and its entries are the table's, in the table's order: the environment and the checker's answer at every address of a program, and no environment where a step reads a refused sibling. The pointer of the claim proposed as annotate-table; it implements the claim address-table, whose specification is the table. Its consumers are the typed print (slice P2) and the session's call instances.

It says nothing of the cost, and nothing past a refused read: there, as in the table, the subtree is not reached.

Module

Effect4.Laws.Program.Typing.Annotate

∀ {Op : Type} (s : Effect4.Program.Signature Op) (env0 : Effect4.Program.TyEnv)
  (p : Effect4.Program.Eff Op),
  Eq (Effect4.Program.annotate s env0 p) (Effect4.Program.table s env0 p)

term-slot-environmentclaim:term-slot-environment

On a typed node, the term in each slot whose rule extends the node's environment has a type at the environment that the slot table answers: the test of catchIf, the test, the step and the result of iterate, and an operation's own term at the instance of its parameter; the proof is the inversion of HasTy at the three constructors; it does not say that the environment is the only one, and it says nothing at a refused node (decisions row 302)

On a typed node, the term in a slot has a type at the slot's environment. The slot table answers an environment at each slot that the node has (Node.extSlotTerm), and the typing rule of the node types the slot's term there: the test of catchIf, the test, the step and the result of iterate, and an operation's own term at the instance of its parameter. The proof is the inversion of HasTy at the three constructors. The pointer of the claim term-slot-environment. Its consumer is the TypeScript printer at an eliminator inside such a term (slice PRINT).

It does not say that the environment is the only one at which the term has a type, and it says nothing at a node that the checker refuses.

Module

Effect4.Laws.Program.Typing.Table

∀ {Op : Type} {s : Effect4.Program.Signature Op} {env : Effect4.Program.TyEnv}
  {p : Effect4.Program.Eff Op} {T : Effect4.Program.EffTy},
  Conform.Effect4.Typing.HasTy s env p T →
    ∀ {slot : Effect4.Program.ExtSlot} {t : Effect4.Program.Term},
      Eq (Effect4.Program.Node.extSlotTerm s (Effect4.Program.Node.eff p) slot) (Option.some t) →
        Exists fun env' =>
          Exists fun ty =>
            And
              (Eq (Effect4.Program.Node.extSlotEnv s env (Effect4.Program.Node.eff p) slot)
                (Option.some env'))
              (Eq (Effect4.Program.termTy s env' t) (Option.some ty))

fold-cache-local-agreementclaim:fold-cache-local-agreement

Every answer that accepted entries of a type-fold cache hold is cata_ty of the same layer at its own source type: check accepts entries whose children stand in earlier entries and whose answers meet the layer's local equation over the generated view, so payloads, names, flags and child order are part of each equation; check accepts the entries that prepare builds at every type, so answer returns the fold at every type (answer_eq); nothing of speed, of reuse after an edit, of a typing judgment, or of an input the layer inherits (slice D6, serving R14)

Local agreement: every answer that accepted entries hold is cata_ty of the same layer at its own source. The pointer of the claim fold-cache-local-agreement. Its consumers are CheckedCache.query_agrees, answer_agrees and slice D6's memoized folds. It says nothing of a type that no entry holds, and nothing of speed.

Module

Effect4.Laws.Program.Folds.TyCache

∀ {R : Type u} [inst : DecidableEq R]
  (layer : Effect4.Program.TyCtor → List (Effect4.Program.TyArgF R) → R)
  (entries : Effect4.Program.TyCache.Entries R),
  Eq (Effect4.Program.TyCache.check layer entries) Bool.true →
    ∀ (t : Effect4.Program.Ty) (r : R),
      Eq (Effect4.Program.TyCache.lookup entries t) (Option.some r) →
        Eq r (Effect4.Program.cata_ty (Effect4.Program.TyAlgebra.ofLayer layer) t)

dependency-summary-exactclaim:dependency-summary-exact

A distance table that check accepts on a finite graph with cycles reports a label at a node if and only if a directed path from the node reaches a node that seeds the label: each seed and each child's label has an entry, and each entry is a seed or has a child at a smaller distance, one distance per node and label; #axiom_audit checked runs it over the axiom walk's answers and their captured graph (ProofGraph.checkDependencies); nothing of the capture's fidelity to the environment, of a theorem that a node names, or of speed

An accepted summary: a table that check accepts holds an entry at a node and a label if and only if a path from the node reaches a seed of the label. The pointer of the claim dependency-summary-exact. Its consumers are Checked.reports_iff, the axiom walk's checked summaries and the flow's directed queries. It certifies the supplied graph, not its extraction.

Module

Tools.Graph.Summary

∀ {n m : Nat} {g : Tools.Graph.Summary.Graph n m} {d : Tools.Graph.Summary.Distances n m},
  Eq (Tools.Graph.Summary.check g d) Bool.true →
    ∀ (u : Fin n) (l : Fin m),
      Iff (Tools.Graph.Summary.Present d u l) (Tools.Graph.Summary.Reaches g u l)

view-reachability-summary-exactclaim:view-reachability-summary-exact

A flow's distance table that checkReach accepts (every edge's ends below the position bound, and check on the reach graph) reports a target at a source if and only if Flow.Reach leads from the source to the target; an end at or above the bound is refused, never dropped; ReachTable answers directed queries under this law; nothing of a schedule, a layout, a forest or weak connectedness

A checked flow summary: when checkReach accepts a distance table, the table reports a target at a source if and only if Reach leads from the source to the target. The pointer of the claim view-reachability-summary-exact. Its consumers are directed queries of the application graph, explanations and impact reports. It establishes no schedule.

Module

Tools.View.FlowReach

∀ {n : Nat} {es : List Tools.View.Flow.Edge} {d : Tools.Graph.Summary.Distances n n},
  Eq (Tools.View.Flow.checkReach n es d) Bool.true →
    ∀ (source target : Fin n),
      Iff (Tools.Graph.Summary.Present d source target)
        (Tools.View.Flow.Reach es source.val target.val)