the residents and certificate for a shape's data and a program's region
245def linearStepPlanResidentsForProgram =
246 (lambda unrestricted program : (family SM86Program) .
247 (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
248 (lambda unrestricted submissions : Nat .
249 (linearStepPlanResident b"pushbuffer" linearStepPlanPushbufferOffset linearStepPlanPushbufferBudget 4096
250 (linearStepPlanResident b"semaphores" linearStepPlanSemaphoreOffset (naturalMultiply linearStepPlanSemaphoreStride submissions) 4096
251 (linearStepPlanResident b"program" linearStepPlanProgramOffset (linearStepPlanProgramBytesOf program) linearStepPlanRegionAlignment
252 (linearStepPlanResident b"qmd" linearStepPlanQMDOffset linearStepPlanQMDTableBytes linearStepPlanRegionAlignment
253 (linearStepPlanResident b"weights" linearStepPlanWeightsOffset (linearStepPlanWeightsBytesFor m k) 4
254 (linearStepPlanResident b"input" linearStepPlanInputOffset (linearStepPlanInputBytesFor k) 4
255 (linearStepPlanResident b"target" linearStepPlanTargetOffset (linearStepPlanTargetBytesFor m) 4
256 (linearStepPlanResident b"output" linearStepPlanOutputOffset (linearStepSM86OutputRecordBytesFor m k) 4
257 (constructor ArenaResidents ArenaResidentsEnd)))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.