Scope Lifetime & Finalizationconcept:scope-lifetime-finalization

finalizer-starts-boundedclaim:finalizer-starts-bounded

Every native decision prefix starts an onExit finalizer no more often than it pushes that source's finalizer frame; arbitrary program, table and budget; no progress, source uniqueness or cleanup-log claim

Finalizer starts spend recorded pushes, retaining any unspent stack credits. Every native decision prefix satisfies the bound.

Module

Effect4.Laws.Program.FinalizerRun

∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) (cf : Nat)
  (m : Effect4.Program.NativeMachine) (q : List Nat),
  Effect4.Program.Guard.Reachable p table cf m →
    instLENat.le
      (List.countP (Effect4.Program.FinalizerRun.startedAt q)
        (m.trace
          (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)))
      (List.countP (Effect4.Program.FinalizerRun.registeredAt q)
        (m.trace
          (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)))

once-placed-finalizerclaim:once-placed-finalizer

A once-placed source pushes its finalizer frame at most once across every fiber of a native decision prefix; no progress or log-writer claim

Control-source uniqueness obligation of the at-most-once claim. A once-placed source pushes its finalizer frame at most once across all fibers. Consumer: the atomic cleanup-log claim. It supplies no finalizer progress.

Module

Effect4.Laws.Program.FinalizerRun

∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) (cf : Nat)
  (m : Effect4.Program.NativeMachine) (q : List Nat),
  Eq (Effect4.Program.OncePlaced (Effect4.Program.Node.eff p) q) Bool.true →
    Effect4.Program.Guard.Reachable p table cf m →
      instLENat.le
        (List.countP (Effect4.Program.FinalizerRun.registeredAt q)
          (m.trace
            (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
            (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
            (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)))
        1

close-idempotentclaim:close-idempotent

Closing an already-closed scope returns void without re-running finalizers

Closing an already-closed scope returns it without running a finalizer. census: scope.close-state-first

Module

Effect4.Machine.Scope

Literature

PFPL, ch. 28, §28.1, p. 261 (adaptedResult)

∀ {κ φ : Type u} {β : Type v} {ε δ ι α : Type u}
  (run : φ → Effect4.Exit β ε δ ι α → Effect4.Exit Unit ε δ ι α)
  (self : Effect4.Scope κ φ β ε δ ι α) (exit : Effect4.Exit β ε δ ι α),
  Eq self.isClosed Bool.true →
    Eq (Effect4.Scope.close run self exit) { fst := self, snd := Effect4.Exit.void }

close-twiceclaim:close-twice

A second close runs nothing

A second close runs nothing. census: scope.close-state-first

Module

Effect4.Machine.Scope

∀ {κ φ : Type u} {β : Type v} {ε δ ι α : Type u}
  (run : φ → Effect4.Exit β ε δ ι α → Effect4.Exit Unit ε δ ι α)
  (self : Effect4.Scope κ φ β ε δ ι α) (first second : Effect4.Exit β ε δ ι α),
  Eq (Effect4.Scope.close run (Effect4.Scope.close run self first).fst second)
    { fst := (Effect4.Scope.close run self first).fst, snd := Effect4.Exit.void }

close-order-eqclaim:close-order-eq

Scope finalizers run in reverse registration order (LIFO)

Finalizers are materialised in insertion order and iterated backwards. census: scope.close-lifo

Module

Effect4.Machine.Scope

Literature

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

∀ {κ φ : Type u} {β : Type v} {ε δ ι α : Type u} (self : Effect4.Scope κ φ β ε δ ι α),
  Eq self.closeOrder (List.map Prod.snd self.finalizers).reverse

close-reentrant-addclaim:close-reentrant-add

Re-entrant finalizer addition observes closed state immediately

The sharp form of "state before finalizers": a finalizer that re-enters the scope while it closes sees a Closed scope, so its own registration runs immediately with the closing exit rather than being recorded. census: rule.scope-close-lifo-state-first

Module

Effect4.Machine.Scope

∀ {κ φ : Type u} {β : Type v} {ε δ ι α : Type u} [inst : DecidableEq κ]
  (run : φ → Effect4.Exit β ε δ ι α → Effect4.Exit Unit ε δ ι α)
  (self : Effect4.Scope κ φ β ε δ ι α) (exit : Effect4.Exit β ε δ ι α) (key : κ) (finalizer : φ),
  Eq self.isClosed Bool.false →
    Eq (Effect4.Scope.addExit run (self.closeState exit) key finalizer)
      { fst := self.closeState exit, snd := run finalizer exit }

close-seq-protocolclaim:close-seq-protocol

The sequential close walk meets the ambient iterator protocol at one row for admitted finalizers

A typed walk frame has its protocol: coinduction from the invariant.

Module

Effect4.Laws.Program.Typed.Commands.Clauses.Close

Literature

deVilhenaPottier2021, audit P8 (adaptedResult)

∀ {root : Effect4.Program.Typed.ProgramSource} {w : Effect4.Program.Typed.World}
  {row : Effect4.Machine.Env.Requirement} {tin tout : Effect4.Program.EffTy}
  {name : Effect4.Program.EffName},
  Effect4.Program.Typed.CloseSeqTyped root
      { fst := w,
        snd :=
          { fst := row,
            snd := { fst := row, snd := { fst := tin, snd := { fst := tout, snd := name } } } } } →
    Effect4.Program.Typed.AmbientIteratorProtocol root w row row tin tout name

saved-mask-restorationclaim:saved-mask-restoration

The mask's law at the boundaries of regions, on the frame machine: the getter masks and answers the image of the entry flag; a restore site at a true bit is the interruptible region over its body, and at a false bit it is its body's own code; a region's entry sets its own flag at every fiber and saves the earlier flag exactly when it changes it; the saved frame's pass returns that flag on every exit, and with a cause pending an exit that leaves the fiber interruptible fails there with it (decisions rows 227, 244 to 246; no progress, nothing about a module, and no statement for a region that changes no flag)

The mask's law at the boundaries of regions (the claim saved-mask-restoration; concept scope-lifetime-finalization, requirement R11; decisions rows 227 and 244 to 246).

Reach: the frame machine at the program's interpreter, any completed view, any fiber and any machine; the compile at a positive budget; both saved bits; any exit. It does not establish progress, and it names no module that uses the mask. It does not state that a region which changes no flag ends with its entry flag: such a region pushes no frame, and its exit flag is what its body left (the module's head; the receipt's open part). The reference machine's clause is related to the frame's by the simulation (evaluate_rel's cases actMask and actGetInterruptible, Laws/Program/Simulation/Evaluate.lean), and it keeps the typed state (clause_mask, clause_getInterruptible). Its consumers are the Queue's waiting wrapper and the Semaphore's protected permit.

Module

Effect4.Laws.Program.Typed.Mask

Effect4.Program.Typed.MaskRestoration

saved-mask-pop-disciplineclaim:saved-mask-pop-discipline

At one fixed base bit, the frame machine keeps the chain of restoring frames on a fiber's stack: FrameFiber.popFrom from an empty scratch stack, getCont, Machine.frameExitState and the entry of each region keep it, and two fibers with one base and one stack have one flag (a local law at every demand, skip flag and carried cause; no statement of a run, of a completed exit, of cleanup or of delivery)

The saved mask's chain through a pop of the stack (the proposed registry claim saved-mask-pop-discipline; concept scope-lifetime-finalization, requirement R11). It is a step of the open run-level half of saved-mask-restoration. Each field cites one theorem of this module, so its status is derived from theirs (#plan_status).

Reach: the polymorphic FrameFiber, at every stack, demand, skip flag and carried cause, with one fixed base. The pop asks for an empty scratch stack, as getCont calls it.

It does not establish a law of a run, a completed exit, a cleanup's multiplicity, a delivery, a budget or liveness. It says nothing of a host or of a printed form. The bracket of a whole region and each fiber's base in a run are not stated.

Its consumers are the later lift through Machine.Lift, then the waiting wrapper under a masked caller and Semaphore's protected permit.

Module

Effect4.Laws.Machine.MaskDiscipline

∀ (ν σ : Type u) (β : Type v) (ε δ ι α : Type u) [inst : DecidableEq ε] [inst_1 : DecidableEq δ]
  [inst_2 : DecidableEq ι] [inst_3 : DecidableEq α], Effect4.Machine.MaskPopDiscipline ν σ β ε δ ι α

saved-mask-chain-runsclaim:saved-mask-chain-runs

Each live fiber of a run of a compiled program holds the saved mask's chain at its start flag: the invariant MaskRuns, at a table of start flags, is kept by every decision tape and fuel at the compiled program's interpreter, from each machine that holds it; each command keeps it under the condition just before a clearing, which the command loop discharges, so each entry outside the machine that returns a machine keeps it, with no premise for the condition (the lift of saved-mask-pop-discipline to runs; no typing, no admission and no premise on the table; no bracket of a region, no flag or stack of an exited fiber, no cleanup's multiplicity, no delivery, no budget, no liveness)

Each live fiber of a run of a compiled program holds the saved mask's chain at its start flag (the proposed registry claim saved-mask-chain-runs; concept scope-lifetime-finalization, requirement R11). It is the placed statement of the claim: the lift of saved_mask_pop_discipline to runs, at the compiled program's interpreter interpOf root table and under the native evaluator evaluatorFor root table. A printed form of the statement hides that instance.

Its general form is Machine.saved_mask_chain_runs, at the frame evaluator. This statement is Machine.replayEval_maskRuns at the native evaluator's premise evaluateNative_keepsMask.

Reach: every program, row table, decision tape and fuel, from each machine that holds the invariant. It asks for no typing, no admission and no premise on the table.

It does not establish the bracket of a region, a flag or a stack of an exited fiber as a state invariant, a cleanup's multiplicity, a delivery, a budget or liveness. An invariant is not progress.

Its consumers are the bracket's law, then the waiting wrapper under a masked caller, Semaphore's protected permit and Pool's use.

Module

Effect4.Laws.Program.MaskRuns

∀ (root : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) (fuel : Nat)
  (tape :
    List
      (Effect4.Machine.RunDecision Effect4.Program.EffName Effect4.Program.EffThunk
        Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
        Effect4.Machine.Ann))
  (bases : List Bool)
  (m :
    Effect4.Machine.RunMachine Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
      Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann
      Effect4.Machine.Ctx Effect4.Machine.Stores),
  Effect4.Machine.MaskRuns bases m →
    Exists fun bases' =>
      And (bases.IsPrefix bases')
        (Effect4.Machine.MaskRuns bases'
          (Effect4.Machine.replayEval (Effect4.Program.interpOf root table) fuel tape m).machine)

saved-mask-region-bracketclaim:saved-mask-region-bracket

A region of a compiled program ends at its entry's stack and at its entry flag, for an arbitrary body: at two cuts of one command loop's run where a pending command steps the fiber, the later cut's stack shape above ++ below is a premise, and it is the region's only mark on the machine; the theorem then gives the entry's stack and the entry flag at the region's end, which is the fiber that the pop of the own frames leaves where no own frame answers, and the pop goes on from it; it does not give that a body's run keeps that shape (the run-level half of saved-mask-restoration; no premise on an exit, by stepped-fiber-live; no cleanup, no release count, no delivery, no budget, no liveness; nothing of a region whose fiber exits inside it; the client premise of the mask's derived form stays: nothing acquired or registered before the body begins, decisions rows 227, 244 to 246)

A region of a compiled program ends at its entry's stack and at its entry flag, for an arbitrary body (the proposed registry claim saved-mask-region-bracket; concept scope-lifetime-finalization, requirement R11). It is the run-level half of saved-mask-restoration, at the compiled program's interpreter interpOf p table and under the native evaluator.

The two cuts are cuts of one command loop's run (LoopCut, at tables in the prefix order), and at each a pending command steps the fiber. The first is the region's entry: its stack is the entry's stack, and its flag is the entry flag. At the second the fiber is inside the region: its stack is the own frames above over the entry's stack. Where the pop of the own frames answers nothing, the body's exit has passed each own frame. Then the region's end has the entry's stack and the entry flag, and the pop of the fiber goes on as the pop of the region's end (RegionEnds).

Its two facts are its steps. The stack at the region's end is the entry's stack (FrameFiber.regionEnd_stack). The fiber is live at both cuts (stepped_live), so the statement takes no premise on an exit. Its general form is Machine.saved_mask_region_bracket, which takes that premise.

Reach: every program, row table, demand, skip flag and carried cause. It asks for no typing and no admission. A region that changes its flag and a region that changes no flag are one case: the statement reads the entry's stack and the entry flag alone.

The later cut's stack shape above ++ below is a premise, and it is the region's only mark on the machine. The theorem then gives the entry's stack and the entry flag at the region's end. It does not give that a body's run keeps that shape.

It gives no cleanup, no release count, no delivery, no budget and no liveness, and nothing of a region whose fiber exits inside it. The client premise of the mask's derived form stays with the client: nothing is acquired or registered before the body begins (decisions rows 227 and 244 to 246).

Its consumers are the waiting wrapper under a masked caller, then Semaphore's protected permit and Pool's use.

Module

Effect4.Laws.Program.MaskBracket

∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) {bases bases' : List Bool}
  {m m' : Effect4.Program.NativeMachine} {cmds cmds' : List Effect4.Program.Guard.NCmd},
  Effect4.Program.LoopCut p table bases m cmds →
    Effect4.Program.LoopCut p table bases' m' cmds' →
      bases.IsPrefix bases' →
        ∀ {c c' : Effect4.Program.Guard.NCmd},
          List.instMembership.mem cmds c →
            List.instMembership.mem cmds' c' →
              ∀ {id : Effect4.FiberId},
                Effect4.Machine.Steps id c →
                  Effect4.Machine.Steps id c' →
                    ∀ {f g : Effect4.Program.Guard.NFiber},
                      Eq (Effect4.Machine.RunMachine.fiber? m id) (Option.some f) →
                        Eq (Effect4.Machine.RunMachine.fiber? m' id) (Option.some g) →
                          ∀ {above : List Effect4.Program.NCode},
                            Eq
                                (g.frame
                                    (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk
                                      Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect
                                      Effect4.FiberId Effect4.Machine.Ann)
                                    (Effect4.FrameFiber Effect4.Program.EffName
                                      Effect4.Program.EffThunk Effect4.Machine.Val
                                      Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                                      Effect4.Machine.Ann)).stack
                                (instHAppendOfAppend.hAppend above
                                  (f.frame
                                      (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk
                                        Effect4.Machine.Val Effect4.Machine.Err
                                        Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
                                      (Effect4.FrameFiber Effect4.Program.EffName
                                        Effect4.Program.EffThunk Effect4.Machine.Val
                                        Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                                        Effect4.Machine.Ann)).stack) →
                              ∀ (demand : Effect4.Arm) (skip : Bool)
                                (cause : Option Effect4.Machine.CauseV),
                                Eq
                                    (((g.frame
                                                (Effect4.Prim Effect4.Program.EffName
                                                  Effect4.Program.EffThunk Effect4.Machine.Val
                                                  Effect4.Machine.Err Effect4.Machine.Defect
                                                  Effect4.FiberId Effect4.Machine.Ann)
                                                (Effect4.FrameFiber Effect4.Program.EffName
                                                  Effect4.Program.EffThunk Effect4.Machine.Val
                                                  Effect4.Machine.Err Effect4.Machine.Defect
                                                  Effect4.FiberId Effect4.Machine.Ann)).own
                                            above).getCont
                                        demand skip cause).answer
                                    Effect4.ContAnswer.empty →
                                  (f.frame
                                        (Effect4.Prim Effect4.Program.EffName
                                          Effect4.Program.EffThunk Effect4.Machine.Val
                                          Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                                          Effect4.Machine.Ann)
                                        (Effect4.FrameFiber Effect4.Program.EffName
                                          Effect4.Program.EffThunk Effect4.Machine.Val
                                          Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                                          Effect4.Machine.Ann)).RegionEnds
                                    (g.frame
                                      (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk
                                        Effect4.Machine.Val Effect4.Machine.Err
                                        Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
                                      (Effect4.FrameFiber Effect4.Program.EffName
                                        Effect4.Program.EffThunk Effect4.Machine.Val
                                        Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                                        Effect4.Machine.Ann))
                                    above demand skip cause

stepped-fiber-liveclaim:stepped-fiber-live

At each cut of a compiled command loop, a fiber that a pending command steps has not exited: the guard's queue gives the fiber of each pending Cmd.loop and Cmd.deliver as running, and the guard's state gives each exited fiber as not running (every program and row table, each machine and pending commands that hold GuardState and GuardQueue; false at a hand-written interpreter; no statement that a fiber is stepped, and nothing of a fiber that no pending command steps)

At each cut of a compiled command loop, a fiber that a pending command steps has not exited (the proposed registry claim stepped-fiber-live; concept scope-lifetime-finalization, requirement R11). The guard's queue gives the fiber of each pending Cmd.loop and Cmd.deliver as running and not parked, and the guard's state gives each exited fiber as not running. It is the second fact of the bracket, and its own source.

So no compiled program reaches a machine where the command loop steps an exited fiber. The invariant MaskRuns ranges over the live fibers for that machine's sake (Laws/Machine/MaskRuns.lean).

Reach: every program and row table, and each machine and pending commands that hold the guard's state and the guard's queue. Guard.driveStep_invariants keeps both along a command loop, and Guard.guardState_reachable gives the state at each reachable machine.

It does not establish that a fiber is stepped, and it gives nothing of a fiber that no pending command steps. The statement is false at a hand-written interpreter: there the command loop steps an exited fiber, and Test/Machine/MaskBracket.lean holds two such cuts.

Its consumers are compiled_region_bracket, and each law that reads a fiber at its own step.

Module

Effect4.Laws.Program.MaskBracket

∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable)
  {m : Effect4.Program.NativeMachine} {cmds : List Effect4.Program.Guard.NCmd},
  Effect4.Program.Guard.GuardState m →
    Effect4.Program.Guard.GuardQueue p table m cmds →
      ∀ {c : Effect4.Program.Guard.NCmd},
        List.instMembership.mem cmds c →
          ∀ {id : Effect4.FiberId},
            Effect4.Machine.Steps id c →
              ∀ {f : Effect4.Program.Guard.NFiber},
                Eq (Effect4.Machine.RunMachine.fiber? m id) (Option.some f) →
                  Eq
                    (f.exit
                      (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk
                        Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect
                        Effect4.FiberId Effect4.Machine.Ann)
                      (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk
                        Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect
                        Effect4.FiberId Effect4.Machine.Ann))
                    Option.none

pool-return-frontclaim:pool-return-front

A return of a lease that holds its item puts the item at the front of the idle items, keeps every item, and leaves the lease holding nothing (a helper of pool-lease-return; no finalizer's run)

A return puts its item at the front, and it keeps every item. Where the lease holds the item, the item's stamp joins the front of the idle stamps, the lease returned, and a wake is owed exactly when a waiter is enrolled. Every item stays, with its resource: a return finalizes nothing. After it the lease holds no item. Consumer: the proposed claim pool-lease-return. It states one transition, and nothing about a finalizer's run.

Module

Effect4.Laws.Library.Pool.Profile

∀ {s : Effect4.Pool.Model.State} {i l : Nat},
  Eq (s.items.any fun x => x.heldBy i l) Bool.true →
    And (Eq (Effect4.Pool.Model.giveBack s i l).fst.available (List.cons i s.available))
      (And
        (Eq (Effect4.Pool.Model.giveBack s i l).snd
          { fst := Bool.true, snd := s.waiters.isEmpty.not })
        (And
          (Eq
            (List.map (fun it => { fst := it.stamp, snd := it.resource })
              (Effect4.Pool.Model.giveBack s i l).fst.items)
            (List.map (fun it => { fst := it.stamp, snd := it.resource }) s.items))
          (Eq ((Effect4.Pool.Model.giveBack s i l).fst.items.any fun x => x.heldBy i l)
            Bool.false)))

pool-return-onceclaim:pool-return-once

A second return of one lease changes nothing in Pool's model, and it owes no wake (a helper of pool-lease-return, from pool-return-front; the model's step only: no program and no finalizer's run)

A lease returns at most once. After a return of a lease, a second return of the same lease changes nothing and owes no wake, whatever the first one did. Consumer: the proposed claim pool-lease-return.

Module

Effect4.Laws.Library.Pool.Profile

∀ (s : Effect4.Pool.Model.State) (i l : Nat),
  Eq (Effect4.Pool.Model.giveBack (Effect4.Pool.Model.giveBack s i l).fst i l)
    { fst := (Effect4.Pool.Model.giveBack s i l).fst,
      snd := { fst := Bool.false, snd := Bool.false } }

pool-close-refusesclaim:pool-close-refuses

After the close's first step of Pool's model every lease is refused, and a refused lease changes no item (a helper of pool-close-waits; no wait for a lease and no finalizer's run; decisions row 268)

After the close's first step no lease begins. The step leaves a closing pool, it tells whether it began the close, and its count is the count of the waiters. At a closing pool every lease is refused, and a refused lease changes no item, no idle stamp and no stamp of a lease. No transition opens the pool again (step_closing). Consumer: the proposed claim pool-close-waits. It states no wait for a lease, no finalizer's run and no completed close.

Module

Effect4.Laws.Library.Pool.Profile

∀ (s : Effect4.Pool.Model.State),
  And (Eq (Effect4.Pool.Model.close s).fst.closing Bool.true)
    (And (Eq (Effect4.Pool.Model.close s).snd { fst := s.closing.not, snd := s.waiters.length })
      (∀ (id : Nat),
        Eq (Effect4.Pool.Model.lease (Effect4.Pool.Model.close s).fst id)
          { fst := Effect4.Pool.Model.withdraw (Effect4.Pool.Model.close s).fst id,
            snd := { fst := Bool.true, snd := Option.none } }))

pool-drain-waitsclaim:pool-drain-waits

The closer's step of Pool's model answers that the pool is drained exactly when no lease is outstanding, it enrols the closer exactly otherwise, and it changes the waiters alone (a helper of pool-close-waits; one transition: no wait along a run, no progress of the closer and no finalizer's run; decisions rows 268 and 276)

The closer's step answers true exactly where no lease is outstanding (decisions rows 268 and 276, point 2). It enrols the closer exactly otherwise: the closer's own entry leaves first, so an entry after the step is this step's enrolment. The check and the enrolment are one transition, so each later return finds a waiter. The step changes the waiters alone: it frees no item, and it finalizes none. Consumer: the proposed claim pool-close-waits. It states one transition. It states no wait along a run, no progress of the closer and no finalizer's run.

Module

Effect4.Laws.Library.Pool.Profile

∀ (s : Effect4.Pool.Model.State) (id : Nat),
  And
    (Iff (Eq (Effect4.Pool.Model.drain s id).snd Bool.true)
      (Eq (Effect4.Pool.Model.leases s) List.nil))
    (And
      (Iff (List.instMembership.mem (Effect4.Pool.Model.drain s id).fst.waiters id)
        (Ne (Effect4.Pool.Model.leases s) List.nil))
      (Eq (Effect4.Pool.Model.drain s id).fst
        { items := s.items, available := s.available,
          waiters := (Effect4.Pool.Model.drain s id).fst.waiters, closing := s.closing,
          next := s.next }))