Store Typingconcept:store-typing

fits-monoclaim:fits-mono

Membership is monotone under host world order

Membership is monotone under the host world order.

Module

Effect4.Laws.Program.Typed.Membership

Literature

TAPL, §13.5, pp. 165–169 (proofTechnique)

Literature

Ahmed2004, audit P1 (adaptedResult)

∀ {w w' : Effect4.Program.Typed.World},
  w.leHost w' →
    ∀ {ty : Effect4.Program.Ty} {v : Effect4.Machine.Val},
      Effect4.Program.Typed.Fits w v ty → Effect4.Program.Typed.Fits w' v ty

fits-subnclaim:fits-subn

Membership is closed under the checker's subtyping order

Membership is closed under the checker's order.

Module

Effect4.Laws.Program.Typed.Membership

Literature

TAPL, §15.1, p. 181 (definitionUsed)

∀ (w : Effect4.Program.Typed.World) {a b : Effect4.Program.Ty},
  Eq (a.subN b) Bool.true →
    ∀ (v : Effect4.Machine.Val), Effect4.Program.Typed.Fits w v a → Effect4.Program.Typed.Fits w v b

fits-normalizeclaim:fits-normalize

Membership is invariant under type normalization

Membership is invariant under normalization (row 137; E4-TYPED-CE-009's repair).

Module

Effect4.Laws.Program.Typed.Membership

Literature

Castagna2024, audit P6 (adaptedResult)

∀ (w : Effect4.Program.Typed.World) (t : Effect4.Program.Ty) (v : Effect4.Machine.Val),
  Iff (Effect4.Program.Typed.Fits w v t.normalize) (Effect4.Program.Typed.Fits w v t)

fits-scope-invclaim:fits-scope-inv

A member of Ty.scope is a present scope's handle

A member of Ty.scope is a present scope's handle (row 156): the handle former's scope arm reads the scope store, and no other arm accepts the scope target. The posts that answer a scope handle state Fits w' ans Ty.scope; their consumers read the scope back here.

Module

Effect4.Laws.Program.Typed.Membership

Literature

ATTAPL, ch. 3, pp. 87–136 (analogy)

∀ {w : Effect4.Program.Typed.World} {v : Effect4.Machine.Val},
  Effect4.Program.Typed.Fits w v Effect4.Program.Ty.scope →
    Exists fun sc =>
      And (Eq v (Effect4.Machine.Val.scopeHandle sc)) (Effect4.Program.Typed.ScopeLive w sc)

term-maps-monoclaim:term-maps-mono

A binder term's map between member types is monotone under host world order

The term relation is closed under later worlds, by the order's transitivity: what storePre_mono needs of a read-modify-write row. Quantifying over later worlds is what closes it; a statement at one world is not closed (the control termMaps_oneWorld_not_mono of the retired battery git:68856e778:Test/Program/ProtocolPosts.lean).

Module

Effect4.Laws.Program.Typed.Residual

Literature

Ahmed2004, audit P1 (adaptedResult)

∀ {w w' : Effect4.Program.Typed.World} {f : Effect4.Program.Term} {env : List Effect4.Machine.Val}
  {A R : Effect4.Program.Ty},
  w.leHost w' →
    Effect4.Program.Typed.TermMaps w f env A R → Effect4.Program.Typed.TermMaps w' f env A R

term-typed-mapsclaim:term-typed-maps

A binder term the term typer admits at the node's environment and the cell's type maps that type into its own type at every later world, over an environment that fits (the state plan's T3b)

A typed binder term maps its parameter into its type, at every later world (the claim term-typed-maps): a term the checker types at tys ++ [A] with type R, over an environment that fits tys, runs at env ++ [a] for every member a of A to a member of R. It is the term relation's fundamental property for the term typer (TermMaps, Typed/Residual.lean): the environment stays typed at every later world (envTyped_mono), the current value extends it (envTyped_append), and a typed term over fitting values evaluates into its type (evalTerm_progress). Under any signature whose atoms are the native table's. Its consumer is syncRow_typed, which discharges a read-modify-write row's pre from the term's typing. It says nothing of a term the checker refuses.

Module

Effect4.Laws.Program.Typed.Denotation.Terms

Literature

Ahmed2004, audit P1 (adaptedResult)

∀ {sig : Effect4.Program.Signature Effect4.Program.NativeOp},
  Eq sig.atomOf Effect4.Program.nativeAtomTy →
    ∀ {w : Effect4.Program.Typed.World} {tys : Effect4.Program.TyEnv}
      {env : List Effect4.Machine.Val},
      Effect4.Program.Typed.EnvTyped w tys env →
        ∀ {f : Effect4.Program.Term} {A R : Effect4.Program.Ty},
          Eq (Effect4.Program.termTy sig (instHAppendOfAppend.hAppend tys (List.cons A List.nil)) f)
              (Option.some R) →
            Effect4.Program.Typed.TermMaps w f env A R

fold-typed-atomic-updateclaim:fold-typed-atomic-update

The list fold with two binders, the accumulator and the element: its scope, evaluation, failure, weakening and typing rules; a fold the checker types answers a member of its type over values that fit, in a fixed world; a term reads back from its printed image; one Ref.modify whose term the checker types is one store step that answers B and stores A (decisions row 228)

The list fold's rules hold (the claim fold-typed-atomic-update), at every signature. Each field is one theorem: the two definitional equations, the builder's scope law (Authoring.fold_scoped), foldlM_refuses, evalTerm_weaken, termTy_weaken, termTy_fold_inv, fold_fits, the fold's cases of evalTerm_progress and of evalTerm_fitsAll, refModify_typed_step, and the fold's cases of readTerm_printTerm and readTerm_exact.

It establishes nothing about a module that uses the fold and no agreement with a target. Its consumer is the Queue's service pass (decisions row 228), on the M5 and M6 path through syncRow_typed.

Module

Effect4.Laws.Program.Typed.ListFold

Literature

Ahmed2004, audit P1 (adaptedResult)

∀ (sig : Effect4.Program.Signature Effect4.Program.NativeOp),
  Effect4.Program.Typed.ListFoldRules sig

handle-identity-lawsclaim:handle-identity-laws

The identity of a handle in a term: sameHandle is total on two members of one handle type at any payload types, reflexive and symmetric, and it decides key equality; a handle an allocation just made is the same as no handle of a value that fits the earlier world; a later world keeps a list's membership; a term's handles are its environment's (decisions row 229)

The laws of a handle's identity hold (the claim handle-identity-laws). Each field is one theorem: sameHandle_eval, the two totality theorems, sameHandle_refl, sameHandle_symm, the two allocation facts, the two freshness theorems and their two list forms, list_later, and RawHandles.evalTerm_handles with its fold case.

It establishes no correspondence in a target: that two handles have equal keys exactly when their host objects are one object is each target's relation. Its consumer is the Queue's withdrawal by identity (decisions row 229).

Module

Effect4.Laws.Program.Typed.ListFold

Literature

Ahmed2004, audit P1 (analogy)

Effect4.Program.Typed.HandleIdentityLaws

saved-mask-image-membershipclaim:saved-mask-image-membership

The mask's saved state: membership at Ty.maskRestore is exactly the two saved images, in Fits and in the shape check; the image is no Boolean, a Boolean is no image, and no subtyping relates the two types; the target is reserved against an external allocation, a host answer column and a service carrier; an image holds no handle, so every world, every store and every environment keep its membership (decisions row 244; no reply admission)

The saved state's membership (the claim saved-mask-image-membership; concept store-typing, requirement R4; decisions row 244). The image is the frame ctor 7 over the bit (Value.maskImage, src/Effect4/Machine/Value.lean): data, with no handle.

Reach: Fits at any world, Val.hasTy at any allocation table, the three refusals at their own functions. It does not establish reply admission: externalValue asked at the type admits an image as it admits any handle-free member, and the refusal of a host answer is the column scan at table admission. Its consumers are the getter's typed clause and M5 arm (clause_getInterruptible, getInterruptible_arm), the restore node's arm (restore_arm), and every store that holds a saved value.

Module

Effect4.Laws.Program.Typed.Mask

Effect4.Program.Typed.SavedMaskImage

modeled-membershipclaim:modeled-membership

On the checked domain, every carrier value's encoding inhabits its type at every allocation table: the refusal fold answers none at the type, and the carrier and its image are the carrier fold's (Model.member); an instance of Modeled inherits it across its equivalence, with no proof of its own (Modeled.member); nothing for an identity type, an optional field or a refused constructor, and no codec admission (decisions row 330, slice L1)

Membership on the checked domain (claim modeled-membership): every carrier value's encoding inhabits its type, at every allocation table.

Module

Effect4.Laws.Schema.Modeled

∀ (t : Effect4.Program.Ty),
  Eq (Effect4.Schema.Model.refusal t) Option.none →
    ∀ (x : Effect4.Schema.Model.Carrier t) (alloc : List String),
      Eq (Effect4.Program.Val.hasTy ((Effect4.Schema.Model.image t).toVal x) t alloc) Bool.true

step-language-typedclaim:step-language-typed

A stored step translates to its indexed type from native atom typing, typed caller inputs and Step.Facts; records retain formation and normality, and empty-value subtyping follows from the shared construction law; a fold additionally requires the caller type list to match the source scope length; Step.normal derives Facts for a closed step; no run, optional field, allocation or host behavior follows (decisions row 330)

The typing law, requiring scope alignment only when a fold occurs.

Module

Effect4.Laws.Step

∀ {Γ : List Effect4.Program.Ty} {Op : Type} (sig : Effect4.Program.Signature Op),
  Eq sig.atomOf Effect4.Program.nativeAtomTy →
    ∀
      {src :
        {t : Effect4.Program.Ty} → Effect4.Modules.Input Γ t → Effect4.Program.Authoring.TermSrc}
      {env : Effect4.Program.Authoring.Env} {path : List Nat} {types : List Effect4.Program.Ty},
      (∀ {t : Effect4.Program.Ty} (x : Effect4.Modules.Input Γ t),
          Effect4.Modules.TypesEach sig (src x) env path types t) →
        ∀ {s : Effect4.Program.Ty} (e : Effect4.Modules.Step Γ s),
          e.Facts →
            autoParam (e.ScopeFacts env types.length) Effect4.Modules.Step.typed._auto_1 →
              Effect4.Modules.TypesEach sig (Effect4.Modules.Step.term (fun {t} => src) e) env path
                types s

store-safetyclaim:store-safety

Store safety through inductive configuration typing

Literature

TAPL, §13.5, pp. 165–169 (excludedFeature)

semaphore-profile-closedclaim:semaphore-profile-closed

Each transition of Semaphore's abstract model keeps the first profile, with no premise on its request (the model's half of semaphore-accounting-preserved; nothing about a program, and no progress of a waiter; decisions rows 259 to 261 and 265)

The first profile is closed. Each transition of the model leaves a state of the profile. No premise names the request: a take removes its own entry first, and a release is total. Consumer: the public law, along a run. It establishes nothing about a program, and no progress of a waiter.

Module

Effect4.Laws.Library.Semaphore.Profile

∀ (s : Effect4.Semaphore.Model.State) (op : Effect4.Semaphore.Model.Op),
  Effect4.Semaphore.Model.Profile s →
    Effect4.Semaphore.Model.Profile (Effect4.Semaphore.Model.step s op)

waiting-wrapper-typedclaim:waiting-wrapper-typed

The waiting wrapper at a caller's restore answers its result type at every typed scope, when the module's part is typed: its attempt answers the join of what its two exits answer, and its withdrawal answers a type; the wrapper with no loop answers its hint's type from the same part, with no premise on that type (waitAnswer_answers, HintTy.canonical) (the shared typing of a module that waits, decisions row 275, point 3; its users are Semaphore's take and its protected form, and the Queue's take and offer; a result type in normal form; no run)

The loop at a caller's restore answers the result, where the module's part is typed and the caller's restore keeps what its argument answers, at every scope that the surface's binders reach. The result type is its own normal form.

Module

Effect4.Laws.Step.Waiting

∀ {table : Effect4.Program.RowTable}
  {restore :
    Effect4.Program.Authoring.Src Effect4.Program.NativeOp →
      Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {result : Effect4.Program.Ty} {ended : String} {w : Effect4.Modules.Waiter}
  {s : Effect4.Modules.TypedScope} {F : Effect4.Program.Ty},
  Eq result.normalize result →
    (∀ (t : Effect4.Modules.TypedScope)
        (inner : Effect4.Program.Authoring.Src Effect4.Program.NativeOp) (Y : Effect4.Program.Ty),
        s.Reaches t →
          Effect4.Modules.Answers (Effect4.Program.nativeSignature table) inner t Y →
            Effect4.Modules.Answers (Effect4.Program.nativeSignature table) (restore inner) t Y) →
      Effect4.Modules.Waiter.Typed table w s result F →
        Effect4.Modules.Answers (Effect4.Program.nativeSignature table)
          (Effect4.Modules.waitRetryAt restore result ended w) s result

protected-form-typedclaim:protected-form-typed

The protected form keeps its body's effect type: one mask over an acquisition that answers a type, a body of any effect type at the restore site, and a release that answers a type under the exit's binder; the form has the body's answer, its failure type in normal form and its requirement (decisions row 276, point 1; its users are Semaphore's two protected forms; typing only: no run, no law of the mask and no release at an exit)

The protected body has its body's effect type, with the failure type in normal form. The acquisition answers a type with no failure, for every restore function that keeps what its argument answers. The body has one effect type for every kept reader of the acquired value: it may fail, and it may require a service. The release answers a type with no failure, under the body's exit.

Module

Effect4.Laws.Step.Waiting

∀ {table : Effect4.Program.RowTable}
  {acquire :
    (Effect4.Program.Authoring.Src Effect4.Program.NativeOp →
        Effect4.Program.Authoring.Src Effect4.Program.NativeOp) →
      Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {release body :
    Effect4.Program.Authoring.TermSrc → Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {s : Effect4.Modules.TypedScope} {G F : Effect4.Program.Ty} {b : Effect4.Program.EffTy},
  (∀
      (restore :
        Effect4.Program.Authoring.Src Effect4.Program.NativeOp →
          Effect4.Program.Authoring.Src Effect4.Program.NativeOp),
      (∀ (t : Effect4.Modules.TypedScope)
          (inner : Effect4.Program.Authoring.Src Effect4.Program.NativeOp) (Y : Effect4.Program.Ty),
          (s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore).Reaches t →
            Effect4.Modules.Answers (Effect4.Program.nativeSignature table) inner t Y →
              Effect4.Modules.Answers (Effect4.Program.nativeSignature table) (restore inner) t Y) →
        Effect4.Modules.Answers (Effect4.Program.nativeSignature table) (acquire restore)
          (s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore) G) →
    (∀ (got : Effect4.Program.Authoring.TermSrc),
        Effect4.Modules.Kept (Effect4.Program.nativeSignature table) got
            ((s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore).push
              Effect4.Modules.Stem.answer G)
            G →
          Effect4.Modules.Has (Effect4.Program.nativeSignature table) (body got)
            ((s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore).push
              Effect4.Modules.Stem.answer G)
            b) →
      (∀ (got : Effect4.Program.Authoring.TermSrc),
          Effect4.Modules.Kept (Effect4.Program.nativeSignature table) got
              ((s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore).push
                Effect4.Modules.Stem.answer G)
              G →
            Effect4.Modules.Answers (Effect4.Program.nativeSignature table) (release got)
              (((s.push Effect4.Modules.Stem.restore Effect4.Program.Ty.maskRestore).push
                    Effect4.Modules.Stem.answer G).push
                Effect4.Modules.Stem.exit (b.answer.exitOf b.error))
              F) →
        Effect4.Modules.Has (Effect4.Program.nativeSignature table)
          (Effect4.Modules.protectedBy acquire release body) s
          { answer := b.answer, error := b.error.normalize, requires := b.requires }

pool-use-typedclaim:pool-use-typed

Pool's use keeps its body's effect type at every typed scope: for a kept handle at the reference type of Pool's cell and a body of one effect type at every kept resource, the form has the body's answer, its failure type in normal form and its requirement; the lease and the return add no failure and no requirement, and the refusal at a closed pool adds none, since an interruption has no failure type (the protected form's second user; decisions rows 267, 276 and 279; a resource type in normal form whose item record and cell record are formed; typing only: no run, no law of the mask and no return at an exit)

Pool.use is typed at every scope, for a body of one effect type at every kept reader of a resource and at every scope that the surface's binders reach. It keeps the body's answer, its failure type in normal form and its requirement: the lease and the return add no failure and no requirement.

Module

Effect4.Laws.Library.Pool.Ops

∀ {table : Effect4.Program.RowTable} {A : Effect4.Program.Ty},
  Effect4.Pool.Model.ResourceTy A →
    ∀ {pool : Effect4.Program.Authoring.TermSrc}
      {body :
        Effect4.Program.Authoring.TermSrc → Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
      {s : Effect4.Modules.TypedScope} {b : Effect4.Program.EffTy},
      Effect4.Modules.Kept (Effect4.Program.nativeSignature table) pool s
          (Effect4.Pool.cellTy A).refOf →
        (∀ (t : Effect4.Modules.TypedScope) (r : Effect4.Program.Authoring.TermSrc),
            s.Reaches t →
              Effect4.Modules.Kept (Effect4.Program.nativeSignature table) r t A →
                Effect4.Modules.Has (Effect4.Program.nativeSignature table) (body r) t b) →
          Effect4.Modules.Has (Effect4.Program.nativeSignature table) (Effect4.Pool.use A pool body)
            s { answer := b.answer, error := b.error.normalize, requires := b.requires }

pool-make-typedclaim:pool-make-typed

Pool's make answers the pool's handle at every typed scope, for an acquisition of one effect type whose answer is the resource's type: its failure type is the acquisition's in normal form, so a failed acquisition fails make, and its requirement is the acquisition's with the scope's key, so a pool is made inside a scope (decisions rows 267 and 268; a positive size, and a resource type in normal form whose item record and cell record are formed; typing only: no run and no finalizer's run; an acquisition whose answer type is another type is outside the statement)

Pool.make is typed at every scope, for an acquisition of one effect type at every scope that the surface's binders reach, whose answer is the resource's type. It answers the handle of a cell at Pool's cell type. Its failure type is the acquisition's, in normal form: a failed acquisition fails make. Its requirement is the acquisition's, with the scope's service: make registers the close as a finalizer of the scope that it runs in, so a pool is made inside a scope.

Module

Effect4.Laws.Library.Pool.Ops

∀ {table : Effect4.Program.RowTable} {A : Effect4.Program.Ty},
  Effect4.Pool.Model.ResourceTy A →
    ∀ (size : Nat) (positive : instLTNat.lt 0 size)
      {acquire : Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
      {s : Effect4.Modules.TypedScope} {a : Effect4.Program.EffTy},
      Eq a.answer A →
        (∀ (t : Effect4.Modules.TypedScope),
            s.Reaches t → Effect4.Modules.Has (Effect4.Program.nativeSignature table) acquire t a) →
          Effect4.Modules.Has (Effect4.Program.nativeSignature table)
            (Effect4.Pool.make A size acquire positive) s
            { answer := (Effect4.Pool.cellTy A).refOf, error := a.error.normalize,
              requires :=
                a.requires.union
                  (Effect4.Machine.Env.Requirement.single
                    (Effect4.Program.nativeSignature table).scopeKey) }

pool-close-typedclaim:pool-close-typed

Pool's close answers the unit at every typed scope, with no failure and no requirement, for a kept handle at the reference type of Pool's cell: the close's first step, the posted wake at the counted waiters, and the closer's loop over the closer's step; so it is a release that cannot fail, and make registers it (decisions rows 268 and 276, point 2; a resource type in normal form whose item record and cell record are formed; typing only: no wait along a run, no end of the loop and no finalizer's run)

The close is typed at every scope: it answers nothing, it has no failure and it requires nothing. So it is a release that cannot fail, and make registers it.

Module

Effect4.Laws.Library.Pool.Ops

∀ {table : Effect4.Program.RowTable} {A : Effect4.Program.Ty},
  Effect4.Pool.Model.ResourceTy A →
    ∀ {pool : Effect4.Program.Authoring.TermSrc} {s : Effect4.Modules.TypedScope},
      Effect4.Modules.Kept (Effect4.Program.nativeSignature table) pool s
          (Effect4.Pool.cellTy A).refOf →
        Effect4.Modules.Answers (Effect4.Program.nativeSignature table) (Effect4.Pool.close pool) s
          Effect4.Program.Ty.unit

pool-profile-closedclaim:pool-profile-closed

Each transition of Pool's abstract model keeps the first profile, with no premise on its request (the model's half of pool-profile-preserved; nothing about a program, and no progress of a waiter; decisions rows 267 to 269)

The first profile is closed. Each transition of the model leaves a state of the profile. No premise names the request: a lease removes its own entry first, and a return of a lease that holds nothing changes nothing. Consumer: the public law, along a run. It establishes nothing about a program, and no progress of a waiter.

Module

Effect4.Laws.Library.Pool.Profile

∀ (s : Effect4.Pool.Model.State) (op : Effect4.Pool.Model.Op),
  Effect4.Pool.Model.Profile s → Effect4.Pool.Model.Profile (Effect4.Pool.Model.step s op)

pool-lease-enrolsclaim:pool-lease-enrols

One lease of Pool's model enrols its request exactly when the pool is open and a lease holds every item (on the profile's states; a helper of the public waiting wrapper; no fairness and no liveness)

The enrolment rule. Lease or enrol adds a waiter only when the pool is open and no item is idle: on a state of the profile, the request is enrolled after the step exactly when the pool is open and a lease holds every item. The request's own entry leaves first, so an entry after the step is this step's enrolment. Consumers: the lease step's agreement, and then the public waiting wrapper. It is a fact of this one transition. It states no fairness and no liveness, and nothing about a later selection.

Module

Effect4.Laws.Library.Pool.Profile

∀ {s : Effect4.Pool.Model.State},
  Effect4.Pool.Model.Profile s →
    ∀ (id : Nat),
      Iff (List.instMembership.mem (Effect4.Pool.Model.lease s id).fst.waiters id)
        (And (Eq s.closing Bool.false)
          (∀ (it : Effect4.Pool.Model.Item),
            List.instMembership.mem s.items it → Eq it.borrowed Bool.true))

stream-source-declarationsclaim:stream-source-declarations

An accepted definition-backed Stream source derives its normalized batch/completion protocol, open and close state requests, and unit close answer from the supplied operation declarations; each invocation uses the corresponding declaration name; no body admission, nonempty batch, execution, finalization or host behavior follows

An accepted adapter derives its metadata and invocations from the same declarations. Equality of normalized columns does not establish admission of any definition body.

Module

Effect4.Laws.Library.Stream.Definitions

∀ {opened pull close : Effect4.Program.Authoring.DefSrc Effect4.Program.NativeOp}
  {arguments : List Effect4.Program.Authoring.TermSrc} {source : Effect4.Stream.Source},
  Eq (Effect4.Stream.Source.fromDefinitions opened pull close arguments) (Except.ok source) →
    And
      (Eq pull.answer.normalize (Effect4.Program.Stream.pulledTy source.elem source.done).normalize)
      (And (Eq opened.answer.normalize pull.decl.request.normalize)
        (And (Eq close.decl.request.normalize pull.decl.request.normalize)
          (And (Eq close.answer.normalize Effect4.Program.Ty.unit)
            (And (Eq source.opened (Effect4.Program.Authoring.Def.invoke opened.name arguments))
              (And
                (∀ (state : Effect4.Program.Authoring.TermSrc),
                  Eq (source.pull state)
                    (Effect4.Program.Authoring.Def.invoke pull.name (List.cons state List.nil)))
                (∀ (state : Effect4.Program.Authoring.TermSrc),
                  Eq (source.close state)
                    (Effect4.Program.Authoring.Def.invoke close.name
                      (List.cons state List.nil))))))))