8.4. Work-Report Computation🔗

Combines is-authorized and refinement to produce a complete work report from a work package.

def

Jar.Services.computeWorkReport [Jar.JamConfig] (pkg : Jar.WorkPackage)
  (context : Jar.RefinementContext)
  (services : Dict Jar.ServiceId Jar.ServiceAccount)
  (resolveImport : ImportResolver := fun x x_1 => none) :
  Option (Jar.WorkReport × Jar.Gas)
Jar.Services.computeWorkReport
  [Jar.JamConfig] (pkg : Jar.WorkPackage)
  (context : Jar.RefinementContext)
  (services :
    Dict Jar.ServiceId Jar.ServiceAccount)
  (resolveImport : ImportResolver :=
    fun x x_1 => none) :
  Option (Jar.WorkReport × Jar.Gas)

Ξ(p, c) : Work-report computation. GP eq (14.12). Given a work-package p and context c, computes the work-report by running authorization and then refining each work-item. resolveImport provides segment data for work-item imports — requires guarantor-level DA infrastructure (not yet implemented).