module Runtime.DeviceArenaCertificate import Hardware.Nvidia.SM86.Command.WholeProgramPlan import Model.Parameter import Model.Word64 import Runtime.ArenaCertificate import Std.Foundation import Std.Natural -- THE DEVICE SIDE OF AN ARENA: which ranges a whole program's launches read -- and write, decided on the launch schedule itself. -- -- A plan names every tensor it places. Some live for the whole program -- (the globals: parameter banks, the residual stream); the rest belong to -- phases. Each launch carries its phase in its source identity (the -- backend never reads that field), and each phase declares its planes: -- fresh ones (written in the phase before they are read) and carried ones -- (holding a value an earlier phase left). Planes of different phases may -- share bytes -- that is how a workspace is reused -- and the certificate -- decides that the sharing is sound: -- (A) the globals are aligned, non-empty and pairwise disjoint; -- (B) each phase's planes are aligned, non-empty, pairwise disjoint and -- disjoint from the globals: two tensors live in one phase never -- share a byte; -- (C) every parameter word of every launch that lies in one of the -- plan's address windows lies in a plane of the launch's phase or in -- a global: no launch reaches memory its phase did not name. A -- repeat is not unrolled: each launch of its body stands for all its -- iterations, each word with intervals covering its values over them -- (the iteration's deltas, or its table frames, applied to the -- ordinals the launch stands for: an interval per iteration while -- they are few and one delta names the word, their hull otherwise); -- a word each of whose intervals lies in one named range lies in a -- named range at every iteration; -- (D) in the order the launches run -- the submission schedule's -- references, in order, each a range of the launch table -- a carried -- plane was declared, in the same place, by an earlier phase instance -- (a maximal run of executed launches of one phase), and no instance -- since declared a different plane over any of its bytes: no value is -- overwritten while a later phase still needs it. -- What it trusts is each phase's fresh/carried split; everything else is -- derived from the schedule. -- -- The verdict is 0 when certified; 1 when (A) or (B) fails; 2 + i when -- the i-th launch as written (counted from 0, a repeat's body once) breaks -- (C) -- a word in no named range, or a launch of no declared phase; 2 + n -- + k (n the launches as written) when the k-th executed instance breaks -- (D). family DeviceArenaPhase : Type 0 constructor DeviceArenaPhaseValue field unrestricted deviceArenaPhaseIdentity : Bytes field unrestricted deviceArenaPhaseFresh : (family ArenaResidents) field unrestricted deviceArenaPhaseCarried : (family ArenaResidents) end-family family DeviceArenaPhases : Type 0 constructor DeviceArenaPhasesEnd constructor DeviceArenaPhasesNext field unrestricted deviceArenaPhasesHead : (family DeviceArenaPhase) recursive unrestricted deviceArenaPhasesTail end-family -- a launch as the certificate sees it: its phase, the ordinals of the -- expanded schedule it stands for (base + the sum of k * stride over its -- generators, 0 <= k < count, outermost first), and, for each parameter -- word, intervals covering every value the word takes over them -- one per -- iteration of an enclosing repeat while few, their hull beyond that -- -- with what an enclosing repeat is accumulating: the sums of the positive -- and negative deltas naming the word, whether they are one delta naming -- each of its ordinals at most once, that delta, and those ordinals family DeviceArenaIntervals : Type 0 constructor DeviceArenaIntervalsEnd constructor DeviceArenaIntervalsNext field unrestricted deviceArenaIntervalLow : Nat field unrestricted deviceArenaIntervalHigh : Nat recursive unrestricted deviceArenaIntervalsTail end-family family DeviceArenaOrdinals : Type 0 constructor DeviceArenaOrdinalsEnd constructor DeviceArenaOrdinalsNext field unrestricted deviceArenaOrdinal : Nat recursive unrestricted deviceArenaOrdinalsTail end-family family DeviceArenaSpans : Type 0 constructor DeviceArenaSpansEnd constructor DeviceArenaSpansNext field unrestricted deviceArenaSpanOffset : Nat field unrestricted deviceArenaSpanIntervals : (family DeviceArenaIntervals) field unrestricted deviceArenaSpanRise : Nat field unrestricted deviceArenaSpanFall : Nat field unrestricted deviceArenaSpanUniform : Nat field unrestricted deviceArenaSpanDelta : Nat field unrestricted deviceArenaSpanOrdinals : (family DeviceArenaOrdinals) recursive unrestricted deviceArenaSpansTail end-family family DeviceArenaGenerators : Type 0 constructor DeviceArenaGeneratorsEnd constructor DeviceArenaGeneratorsNext field unrestricted deviceArenaGeneratorStride : Nat field unrestricted deviceArenaGeneratorCount : Nat recursive unrestricted deviceArenaGeneratorsTail end-family family DeviceArenaLaunch : Type 0 constructor DeviceArenaLaunchValue field unrestricted deviceArenaLaunchIdentity : Bytes field unrestricted deviceArenaLaunchBase : Nat field unrestricted deviceArenaLaunchGenerators : (family DeviceArenaGenerators) field unrestricted deviceArenaLaunchSpans : (family DeviceArenaSpans) end-family family DeviceArenaLaunches : Type 0 constructor DeviceArenaLaunchesEnd constructor DeviceArenaLaunchesNext field unrestricted deviceArenaLaunchesHead : (family DeviceArenaLaunch) recursive unrestricted deviceArenaLaunchesTail end-family -- the planes (D) tracks: each with whether a different plane has been -- declared over it since it was last declared family DeviceArenaTracked : Type 0 constructor DeviceArenaTrackedEnd constructor DeviceArenaTrackedNext field unrestricted deviceArenaTrackedResident : (family ArenaResident) field unrestricted deviceArenaTrackedClobbered : Nat recursive unrestricted deviceArenaTrackedTail end-family -- ---- the order the launches run ---- -- the launch table as runs of one phase: identity, first launch, count family DeviceArenaRuns : Type 0 constructor DeviceArenaRunsEnd constructor DeviceArenaRunsNext field unrestricted deviceArenaRunIdentity : Bytes field unrestricted deviceArenaRunFirst : Nat field unrestricted deviceArenaRunCount : Nat recursive unrestricted deviceArenaRunsTail end-family -- the executed instances: phase identities in the order they run family DeviceArenaInstances : Type 0 constructor DeviceArenaInstancesEnd constructor DeviceArenaInstancesNext field unrestricted deviceArenaInstanceIdentity : Bytes recursive unrestricted deviceArenaInstancesTail end-family -- ---- words modulo 2^64 (the build's naturals are 64-bit words) ---- def deviceArenaWordMaximum : Nat = 18446744073709551615 -- a + b modulo 2^64; both arms are evaluated, so neither may overflow def deviceArenaAddModulo = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (let unrestricted room = (naturalSaturatingSubtract deviceArenaWordMaximum a) in (naturalSelect (naturalLess room b) (naturalSaturatingSubtract (naturalSaturatingSubtract b room) 1) (naturalAdd a (naturalSelect (naturalLess room b) room b)))))) -- ---- residents ---- def deviceArenaResidentIdentity = (lambda unrestricted resident : (family ArenaResident) . (eliminate ArenaResident (lambda unrestricted current : (family ArenaResident) . Bytes) resident (branch ArenaResidentValue identity offset extent alignment . identity))) def deviceArenaContains = (lambda unrestricted resident : (family ArenaResident) . (lambda unrestricted address : Nat . (naturalAnd (naturalLessOrEqual (arenaResidentOffsetOf resident) address) (naturalLess address (arenaResidentEndOf resident))))) def deviceArenaAnyContains = (lambda unrestricted residents : (family ArenaResidents) . (lambda unrestricted address : Nat . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents (branch ArenaResidentsEnd . 0) (branch ArenaResidentsNext head tail induction . (naturalOr (deviceArenaContains head address) induction))))) def deviceArenaAppend = (lambda unrestricted left : (family ArenaResidents) . (lambda unrestricted right : (family ArenaResidents) . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . (family ArenaResidents)) left (branch ArenaResidentsEnd . right) (branch ArenaResidentsNext head tail induction . (constructor ArenaResidents ArenaResidentsNext head induction))))) -- a different plane over any byte of `resident` def deviceArenaOverlapsOther = (lambda unrestricted resident : (family ArenaResident) . (lambda unrestricted residents : (family ArenaResidents) . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents (branch ArenaResidentsEnd . 0) (branch ArenaResidentsNext head tail induction . (naturalOr (naturalAnd (naturalIsZero (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident))) (naturalIsZero (arenaDisjoint head resident))) induction))))) -- ---- phases ---- def deviceArenaPhaseIdentityOf = (lambda unrestricted phase : (family DeviceArenaPhase) . (eliminate DeviceArenaPhase (lambda unrestricted current : (family DeviceArenaPhase) . Bytes) phase (branch DeviceArenaPhaseValue identity fresh carried . identity))) def deviceArenaPhaseFreshOf = (lambda unrestricted phase : (family DeviceArenaPhase) . (eliminate DeviceArenaPhase (lambda unrestricted current : (family DeviceArenaPhase) . (family ArenaResidents)) phase (branch DeviceArenaPhaseValue identity fresh carried . fresh))) def deviceArenaPhaseCarriedOf = (lambda unrestricted phase : (family DeviceArenaPhase) . (eliminate DeviceArenaPhase (lambda unrestricted current : (family DeviceArenaPhase) . (family ArenaResidents)) phase (branch DeviceArenaPhaseValue identity fresh carried . carried))) def deviceArenaPhasePlanes = (lambda unrestricted phase : (family DeviceArenaPhase) . (deviceArenaAppend (deviceArenaPhaseFreshOf phase) (deviceArenaPhaseCarriedOf phase))) -- 1 when a phase of this identity is declared def deviceArenaPhaseKnown = (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted identity : Bytes . (eliminate DeviceArenaPhases (lambda unrestricted current : (family DeviceArenaPhases) . Nat) phases (branch DeviceArenaPhasesEnd . 0) (branch DeviceArenaPhasesNext head tail induction . (naturalOr (bytes-equal (deviceArenaPhaseIdentityOf head) identity) induction))))) -- the phase of this identity (the first declared; an unknown identity gets -- the empty phase, which the caller has refused already) def deviceArenaPhaseOf = (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted identity : Bytes . (eliminate DeviceArenaPhases (lambda unrestricted current : (family DeviceArenaPhases) . (family DeviceArenaPhase)) phases (branch DeviceArenaPhasesEnd . (constructor DeviceArenaPhase DeviceArenaPhaseValue identity (constructor ArenaResidents ArenaResidentsEnd) (constructor ArenaResidents ArenaResidentsEnd))) (branch DeviceArenaPhasesNext head tail induction . (nat-eliminate (lambda unrestricted found : Nat . (family DeviceArenaPhase)) induction (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family DeviceArenaPhase) . head)) (bytes-equal (deviceArenaPhaseIdentityOf head) identity)))))) -- (A) and (B): 1 when the globals and every phase's planes are placed def deviceArenaPlaced = (lambda unrestricted globals : (family ArenaResidents) . (lambda unrestricted phases : (family DeviceArenaPhases) . (naturalAnd (arenaCertificate deviceArenaWordMaximum globals) (eliminate DeviceArenaPhases (lambda unrestricted current : (family DeviceArenaPhases) . Nat) phases (branch DeviceArenaPhasesEnd . 1) (branch DeviceArenaPhasesNext head tail induction . (naturalAnd (arenaCertificate deviceArenaWordMaximum (deviceArenaAppend (deviceArenaPhasePlanes head) globals)) induction)))))) -- ---- saturating words ---- def deviceArenaSaturatingAdd = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (naturalAdd a (naturalSelect (naturalLess (naturalSaturatingSubtract deviceArenaWordMaximum a) b) (naturalSaturatingSubtract deviceArenaWordMaximum a) b)))) def deviceArenaSaturatingMultiply = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (let unrestricted room = (naturalDivideUnchecked deviceArenaWordMaximum a) in (naturalMultiply a (naturalSelect (naturalLess room b) room b))))) -- a delta word read as signed: the rise (below 2^63) or the fall (2^64 - d) def deviceArenaNegative = (lambda unrestricted delta : Nat . (naturalLess (naturalDivideUnchecked deviceArenaWordMaximum 2) delta)) def deviceArenaRise = (lambda unrestricted delta : Nat . (naturalSelect (deviceArenaNegative delta) 0 delta)) def deviceArenaFall = (lambda unrestricted delta : Nat . (naturalSelect (deviceArenaNegative delta) (deviceArenaSaturatingAdd (naturalSaturatingSubtract deviceArenaWordMaximum delta) 1) 0)) -- ---- the schedule as written ---- def deviceArenaSpansOf = (lambda unrestricted patches : (family NvidiaParameterPatches) . (eliminate NvidiaParameterPatches (lambda unrestricted current : (family NvidiaParameterPatches) . (family DeviceArenaSpans)) patches (branch NvidiaParameterPatchesEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd)) (branch NvidiaParameterPatchesNext head tail induction . (eliminate NvidiaParameterPatch (lambda unrestricted current : (family NvidiaParameterPatch) . (family DeviceArenaSpans)) head (branch NvidiaParameterPatchValue offset value . (let unrestricted word = (modelWord64Natural value) in (constructor DeviceArenaSpans DeviceArenaSpansNext offset (constructor DeviceArenaIntervals DeviceArenaIntervalsNext word word (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)) 0 0 1 0 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd) induction))))))) def deviceArenaLaunchOf = (lambda unrestricted template : (family NvidiaLaunchTemplate) . (eliminate NvidiaLaunchTemplate (lambda unrestricted current : (family NvidiaLaunchTemplate) . (family DeviceArenaLaunch)) template (branch NvidiaLaunchTemplateValue identity kernel block . (eliminate NvidiaParameterBlock (lambda unrestricted current : (family NvidiaParameterBlock) . (family DeviceArenaLaunch)) block (branch NvidiaParameterBlockValue patches . (constructor DeviceArenaLaunch DeviceArenaLaunchValue identity 0 (constructor DeviceArenaGenerators DeviceArenaGeneratorsEnd) (deviceArenaSpansOf patches))))))) def deviceArenaLaunchIdentityOf = (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . Bytes) launch (branch DeviceArenaLaunchValue identity base generators spans . identity))) def deviceArenaLaunchSpansOf = (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaSpans)) launch (branch DeviceArenaLaunchValue identity base generators spans . spans))) def deviceArenaAppendLaunches = (lambda unrestricted left : (family DeviceArenaLaunches) . (lambda unrestricted right : (family DeviceArenaLaunches) . (eliminate DeviceArenaLaunches (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches)) left (branch DeviceArenaLaunchesEnd . right) (branch DeviceArenaLaunchesNext head tail induction . (constructor DeviceArenaLaunches DeviceArenaLaunchesNext head induction))))) -- each launch moved `shift` ordinals on (a later part of a sequence) def deviceArenaShift = (lambda unrestricted shift : Nat . (lambda unrestricted launches : (family DeviceArenaLaunches) . (eliminate DeviceArenaLaunches (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches)) launches (branch DeviceArenaLaunchesEnd . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd)) (branch DeviceArenaLaunchesNext head tail induction . (constructor DeviceArenaLaunches DeviceArenaLaunchesNext (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) head (branch DeviceArenaLaunchValue identity base generators spans . (constructor DeviceArenaLaunch DeviceArenaLaunchValue identity (naturalAdd base shift) generators spans))) induction))))) -- 1 when ordinal `b` is one the launch stands for: the generators are -- nested (each stride is at least the extent of those inside it), so the -- decomposition is greedy def deviceArenaGenerated = (lambda unrestricted base : Nat . (lambda unrestricted generators : (family DeviceArenaGenerators) . (lambda unrestricted b : Nat . (naturalAnd (naturalLessOrEqual base b) (app (eliminate DeviceArenaGenerators (lambda unrestricted current : (family DeviceArenaGenerators) . (pi unrestricted rest : Nat . Nat)) generators (branch DeviceArenaGeneratorsEnd . (lambda unrestricted rest : Nat . (naturalIsZero rest))) (branch DeviceArenaGeneratorsNext stride count tail induction . (lambda unrestricted rest : Nat . (naturalAnd (naturalLess (naturalDivideUnchecked rest stride) count) (induction (naturalModuloUnchecked rest stride)))))) (naturalSaturatingSubtract b base)))))) def deviceArenaOrdinalsEmpty = (lambda unrestricted ordinals : (family DeviceArenaOrdinals) . (eliminate DeviceArenaOrdinals (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat) ordinals (branch DeviceArenaOrdinalsEnd . 1) (branch DeviceArenaOrdinalsNext ordinal tail induction . 0))) def deviceArenaOrdinalsHas = (lambda unrestricted ordinals : (family DeviceArenaOrdinals) . (lambda unrestricted wanted : Nat . (eliminate DeviceArenaOrdinals (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat) ordinals (branch DeviceArenaOrdinalsEnd . 0) (branch DeviceArenaOrdinalsNext ordinal tail induction . (naturalOr (naturalEqual ordinal wanted) induction))))) def deviceArenaOrdinalsCount = (lambda unrestricted ordinals : (family DeviceArenaOrdinals) . (eliminate DeviceArenaOrdinals (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat) ordinals (branch DeviceArenaOrdinalsEnd . 0) (branch DeviceArenaOrdinalsNext ordinal tail induction . (succ induction)))) -- a delta accumulated on the word at `offset` (a word the block does not -- patch is zero) def deviceArenaAccumulate = (lambda unrestricted ordinal : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted delta : Nat . (lambda unrestricted spans : (family DeviceArenaSpans) . (eliminate DeviceArenaSpans (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans)) spans (branch DeviceArenaSpansEnd . (constructor DeviceArenaSpans DeviceArenaSpansNext offset (constructor DeviceArenaIntervals DeviceArenaIntervalsNext 0 0 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)) (deviceArenaRise delta) (deviceArenaFall delta) (naturalLess ordinal deviceArenaWordMaximum) delta (constructor DeviceArenaOrdinals DeviceArenaOrdinalsNext ordinal (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)) spans)) (branch DeviceArenaSpansNext at intervals rise fall uniform last ordinals tail induction . (nat-eliminate (lambda unrestricted same : Nat . (family DeviceArenaSpans)) (constructor DeviceArenaSpans DeviceArenaSpansNext at intervals rise fall uniform last ordinals induction) (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family DeviceArenaSpans) . (let unrestricted first = (deviceArenaOrdinalsEmpty ordinals) in (constructor DeviceArenaSpans DeviceArenaSpansNext at intervals (deviceArenaSaturatingAdd rise (deviceArenaRise delta)) (deviceArenaSaturatingAdd fall (deviceArenaFall delta)) (naturalAnd uniform (naturalAnd (naturalLess ordinal deviceArenaWordMaximum) (naturalOr first (naturalAnd (naturalEqual delta last) (naturalIsZero (deviceArenaOrdinalsHas ordinals ordinal)))))) delta (constructor DeviceArenaOrdinals DeviceArenaOrdinalsNext ordinal ordinals) tail)))) (naturalEqual at offset)))))))) -- a frame's exact value taken into the word's span def deviceArenaInclude = (lambda unrestricted ordinal : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (lambda unrestricted spans : (family DeviceArenaSpans) . (eliminate DeviceArenaSpans (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans)) spans (branch DeviceArenaSpansEnd . (constructor DeviceArenaSpans DeviceArenaSpansNext offset (constructor DeviceArenaIntervals DeviceArenaIntervalsNext 0 0 (constructor DeviceArenaIntervals DeviceArenaIntervalsNext value value (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))) 0 0 1 0 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd) spans)) (branch DeviceArenaSpansNext at intervals rise fall uniform last ordinals tail induction . (nat-eliminate (lambda unrestricted same : Nat . (family DeviceArenaSpans)) (constructor DeviceArenaSpans DeviceArenaSpansNext at intervals rise fall uniform last ordinals induction) (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family DeviceArenaSpans) . (constructor DeviceArenaSpans DeviceArenaSpansNext at (constructor DeviceArenaIntervals DeviceArenaIntervalsNext value value intervals) rise fall uniform last ordinals tail))) (naturalEqual at offset)))))))) def deviceArenaIntervalCount = (lambda unrestricted intervals : (family DeviceArenaIntervals) . (eliminate DeviceArenaIntervals (lambda unrestricted current : (family DeviceArenaIntervals) . Nat) intervals (branch DeviceArenaIntervalsEnd . 0) (branch DeviceArenaIntervalsNext low high tail induction . (succ induction)))) def deviceArenaLowest = (lambda unrestricted intervals : (family DeviceArenaIntervals) . (eliminate DeviceArenaIntervals (lambda unrestricted current : (family DeviceArenaIntervals) . Nat) intervals (branch DeviceArenaIntervalsEnd . deviceArenaWordMaximum) (branch DeviceArenaIntervalsNext low high tail induction . (naturalSelect (naturalLess low induction) low induction)))) def deviceArenaHighest = (lambda unrestricted intervals : (family DeviceArenaIntervals) . (eliminate DeviceArenaIntervals (lambda unrestricted current : (family DeviceArenaIntervals) . Nat) intervals (branch DeviceArenaIntervalsEnd . 0) (branch DeviceArenaIntervalsNext low high tail induction . (naturalSelect (naturalLess induction high) high induction)))) -- every interval moved by `delta` (modulo 2^64), then `rest` def deviceArenaMoved = (lambda unrestricted delta : Nat . (lambda unrestricted intervals : (family DeviceArenaIntervals) . (lambda unrestricted rest : (family DeviceArenaIntervals) . (eliminate DeviceArenaIntervals (lambda unrestricted current : (family DeviceArenaIntervals) . (family DeviceArenaIntervals)) intervals (branch DeviceArenaIntervalsEnd . rest) (branch DeviceArenaIntervalsNext low high tail induction . (constructor DeviceArenaIntervals DeviceArenaIntervalsNext (deviceArenaAddModulo low delta) (deviceArenaAddModulo high delta) induction)))))) -- the intervals of `count` iterations, each the previous moved by `delta` def deviceArenaIterations = (lambda unrestricted count : Nat . (lambda unrestricted delta : Nat . (lambda unrestricted intervals : (family DeviceArenaIntervals) . (app (nat-eliminate (lambda unrestricted remaining : Nat . (pi unrestricted current : (family DeviceArenaIntervals) . (family DeviceArenaIntervals))) (lambda unrestricted current : (family DeviceArenaIntervals) . (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)) (lambda unrestricted p : Nat . (lambda unrestricted induction : (pi unrestricted current : (family DeviceArenaIntervals) . (family DeviceArenaIntervals)) . (lambda unrestricted current : (family DeviceArenaIntervals) . (deviceArenaMoved 0 current (induction (deviceArenaMoved delta current (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))))))) count) intervals)))) -- iterations kept apart while there are at most this many intervals def deviceArenaExactIntervals : Nat = 64 -- the accumulated deltas applied `steps` times: each span widened to -- cover every iteration def deviceArenaWiden = (lambda unrestricted steps : Nat . (lambda unrestricted stands : Nat . (lambda unrestricted spans : (family DeviceArenaSpans) . (eliminate DeviceArenaSpans (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans)) spans (branch DeviceArenaSpansEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd)) (branch DeviceArenaSpansNext at intervals rise fall uniform last ordinals tail induction . (let unrestricted hull = (constructor DeviceArenaIntervals DeviceArenaIntervalsNext (naturalSaturatingSubtract (deviceArenaLowest intervals) (deviceArenaSaturatingMultiply steps fall)) (deviceArenaSaturatingAdd (deviceArenaHighest intervals) (deviceArenaSaturatingMultiply steps rise)) (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)) in (let unrestricted exact = (naturalAnd uniform (naturalAnd (naturalEqual (deviceArenaOrdinalsCount ordinals) stands) (naturalLessOrEqual (deviceArenaSaturatingMultiply (succ steps) (deviceArenaIntervalCount intervals)) deviceArenaExactIntervals))) in (constructor DeviceArenaSpans DeviceArenaSpansNext at (nat-eliminate (lambda unrestricted adjusted : Nat . (family DeviceArenaIntervals)) intervals (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family DeviceArenaIntervals) . (nat-eliminate (lambda unrestricted apart : Nat . (family DeviceArenaIntervals)) hull (lambda unrestricted r : Nat . (lambda unrestricted unused : (family DeviceArenaIntervals) . (deviceArenaIterations (succ steps) last intervals))) exact))) (naturalIsZero (deviceArenaOrdinalsEmpty ordinals))) 0 0 1 0 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd) induction)))))))) -- the adjustments naming a launch (by one of its ordinals, or all blocks) -- folded into its spans by `step` def deviceArenaFold = (lambda unrestricted step : (pi unrestricted ordinal : Nat . (pi unrestricted offset : Nat . (pi unrestricted value : Nat . (pi unrestricted spans : (family DeviceArenaSpans) . (family DeviceArenaSpans))))) . (lambda unrestricted adjustments : (family NvidiaParameterAdjustments) . (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) launch (branch DeviceArenaLaunchValue identity base generators spans . (constructor DeviceArenaLaunch DeviceArenaLaunchValue identity base generators (eliminate NvidiaParameterAdjustments (lambda unrestricted current : (family NvidiaParameterAdjustments) . (family DeviceArenaSpans)) adjustments (branch NvidiaParameterAdjustmentsEnd . spans) (branch NvidiaParameterAdjustmentsNext head tail induction . (eliminate NvidiaParameterAdjustment (lambda unrestricted current : (family NvidiaParameterAdjustment) . (family DeviceArenaSpans)) head (branch NvidiaParameterAdjustmentValue scope offset value . (nat-eliminate (lambda unrestricted applies : Nat . (family DeviceArenaSpans)) induction (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family DeviceArenaSpans) . (step (eliminate NvidiaParameterAdjustmentScope (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) . Nat) scope (branch NvidiaParameterAdjustmentAllBlocks . deviceArenaWordMaximum) (branch NvidiaParameterAdjustmentBlock at . at)) offset (modelWord64Natural value) induction))) (eliminate NvidiaParameterAdjustmentScope (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) . Nat) scope (branch NvidiaParameterAdjustmentAllBlocks . 1) (branch NvidiaParameterAdjustmentBlock at . (deviceArenaGenerated base generators at)))))))))))))) def deviceArenaMapLaunches = (lambda unrestricted f : (pi unrestricted launch : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) . (lambda unrestricted launches : (family DeviceArenaLaunches) . (eliminate DeviceArenaLaunches (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches)) launches (branch DeviceArenaLaunchesEnd . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd)) (branch DeviceArenaLaunchesNext head tail induction . (constructor DeviceArenaLaunches DeviceArenaLaunchesNext (f head) induction))))) -- how many ordinals a launch stands for def deviceArenaStands = (lambda unrestricted generators : (family DeviceArenaGenerators) . (eliminate DeviceArenaGenerators (lambda unrestricted current : (family DeviceArenaGenerators) . Nat) generators (branch DeviceArenaGeneratorsEnd . 1) (branch DeviceArenaGeneratorsNext stride count tail induction . (naturalMultiply count induction)))) def deviceArenaWidenLaunch = (lambda unrestricted steps : Nat . (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) launch (branch DeviceArenaLaunchValue identity base generators spans . (constructor DeviceArenaLaunch DeviceArenaLaunchValue identity base generators (deviceArenaWiden steps (deviceArenaStands generators) spans)))))) -- frames of a table iteration: every value any frame gives a launch's -- word taken into its span def deviceArenaFrames = (lambda unrestricted frames : (family NvidiaParameterAdjustmentFrames) . (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate NvidiaParameterAdjustmentFrames (lambda unrestricted current : (family NvidiaParameterAdjustmentFrames) . (family DeviceArenaLaunch)) frames (branch NvidiaParameterAdjustmentFramesEnd . launch) (branch NvidiaParameterAdjustmentFramesNext frame tail induction . (deviceArenaFold deviceArenaInclude frame induction))))) -- a repeat's body launches, standing for all its iterations: spans widened -- by the iteration's deltas, and the repeat's generator added def deviceArenaRepeat = (lambda unrestricted count : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted iteration : (family NvidiaParameterIteration) . (lambda unrestricted body : (family DeviceArenaLaunches) . (deviceArenaMapLaunches (lambda unrestricted launch : (family DeviceArenaLaunch) . (eliminate DeviceArenaLaunch (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) (eliminate NvidiaParameterIteration (lambda unrestricted current : (family NvidiaParameterIteration) . (family DeviceArenaLaunch)) iteration (branch NvidiaParameterIterationUnchanged . launch) (branch NvidiaParameterIterationAffine adjustments . (deviceArenaWidenLaunch (naturalSaturatingSubtract count 1) (deviceArenaFold deviceArenaAccumulate adjustments launch))) (branch NvidiaParameterIterationQuotientRemainder divisor remainders quotients . (deviceArenaWidenLaunch (naturalDivideUnchecked (naturalSaturatingSubtract count 1) divisor) (deviceArenaFold deviceArenaAccumulate quotients (deviceArenaWidenLaunch (naturalSaturatingSubtract (naturalSelect (naturalLess count divisor) count divisor) 1) (deviceArenaFold deviceArenaAccumulate remainders launch))))) (branch NvidiaParameterIterationTable frames . (deviceArenaFrames frames launch))) (branch DeviceArenaLaunchValue identity base generators spans . (constructor DeviceArenaLaunch DeviceArenaLaunchValue identity base (constructor DeviceArenaGenerators DeviceArenaGeneratorsNext extent count generators) spans)))) body))))) -- the schedule's launches as written, each standing for its iterations def deviceArenaLaunches = (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . (family DeviceArenaLaunches)) schedule (branch NvidiaLaunchScheduleEmpty . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd)) (branch NvidiaLaunchScheduleOne template . (constructor DeviceArenaLaunches DeviceArenaLaunchesNext (deviceArenaLaunchOf template) (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd))) (branch NvidiaLaunchScheduleAppend left right il ir . (deviceArenaAppendLaunches il (deviceArenaShift (nvidiaLaunchScheduleCount left) ir))) (branch NvidiaLaunchScheduleRepeat count iteration body ib . (deviceArenaRepeat count (nvidiaLaunchScheduleCount body) iteration ib)))) -- ---- (C): every span in a window lies in one named range ---- def deviceArenaWithin = (lambda unrestricted residents : (family ArenaResidents) . (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents (branch ArenaResidentsEnd . 0) (branch ArenaResidentsNext head tail induction . (naturalOr (naturalAnd (deviceArenaContains head low) (deviceArenaContains head high)) induction)))))) def deviceArenaMeets = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) windows (branch ArenaResidentsEnd . 0) (branch ArenaResidentsNext head tail induction . (naturalOr (naturalAnd (naturalLess low (arenaResidentEndOf head)) (naturalLessOrEqual (arenaResidentOffsetOf head) high)) induction)))))) def deviceArenaIntervalsNamed = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted named : (family ArenaResidents) . (lambda unrestricted intervals : (family DeviceArenaIntervals) . (eliminate DeviceArenaIntervals (lambda unrestricted current : (family DeviceArenaIntervals) . Nat) intervals (branch DeviceArenaIntervalsEnd . 1) (branch DeviceArenaIntervalsNext low high tail induction . (naturalAnd (naturalOr (naturalIsZero (deviceArenaMeets windows low high)) (deviceArenaWithin named low high)) induction)))))) def deviceArenaSpansNamed = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted named : (family ArenaResidents) . (lambda unrestricted spans : (family DeviceArenaSpans) . (eliminate DeviceArenaSpans (lambda unrestricted current : (family DeviceArenaSpans) . Nat) spans (branch DeviceArenaSpansEnd . 1) (branch DeviceArenaSpansNext offset intervals rise fall uniform last ordinals tail induction . (naturalAnd (deviceArenaIntervalsNamed windows named intervals) induction)))))) -- ---- (D): carried planes intact ---- def deviceArenaTrackedEnd : (family DeviceArenaTracked) = (constructor DeviceArenaTracked DeviceArenaTrackedEnd) -- 1 when `resident` was declared, in the same place, and nothing has been -- declared over it since def deviceArenaIntact = (lambda unrestricted tracked : (family DeviceArenaTracked) . (lambda unrestricted resident : (family ArenaResident) . (eliminate DeviceArenaTracked (lambda unrestricted current : (family DeviceArenaTracked) . Nat) tracked (branch DeviceArenaTrackedEnd . 0) (branch DeviceArenaTrackedNext head clobbered tail induction . (nat-eliminate (lambda unrestricted same : Nat . Nat) induction (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . (naturalAnd (naturalIsZero clobbered) (naturalAnd (naturalEqual (arenaResidentOffsetOf head) (arenaResidentOffsetOf resident)) (naturalEqual (arenaResidentEndOf head) (arenaResidentEndOf resident)))))) (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident))))))) def deviceArenaAllIntact = (lambda unrestricted tracked : (family DeviceArenaTracked) . (lambda unrestricted carried : (family ArenaResidents) . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) carried (branch ArenaResidentsEnd . 1) (branch ArenaResidentsNext head tail induction . (naturalAnd (deviceArenaIntact tracked head) induction))))) -- 1 when a resident of this name is among `residents` def deviceArenaAnyNamed = (lambda unrestricted residents : (family ArenaResidents) . (lambda unrestricted resident : (family ArenaResident) . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . Nat) residents (branch ArenaResidentsEnd . 0) (branch ArenaResidentsNext head tail induction . (naturalOr (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident)) induction))))) -- an instance of a phase declaring `planes`: every tracked plane they -- overlap (under another name) is clobbered, and those some phase carries -- (the only ones a later instance can need) are tracked afresh def deviceArenaDeclare = (lambda unrestricted carried : (family ArenaResidents) . (lambda unrestricted tracked : (family DeviceArenaTracked) . (lambda unrestricted planes : (family ArenaResidents) . (eliminate ArenaResidents (lambda unrestricted current : (family ArenaResidents) . (family DeviceArenaTracked)) planes (branch ArenaResidentsEnd . (eliminate DeviceArenaTracked (lambda unrestricted current : (family DeviceArenaTracked) . (family DeviceArenaTracked)) tracked (branch DeviceArenaTrackedEnd . deviceArenaTrackedEnd) (branch DeviceArenaTrackedNext head clobbered tail induction . (nat-eliminate (lambda unrestricted redeclared : Nat . (family DeviceArenaTracked)) (constructor DeviceArenaTracked DeviceArenaTrackedNext head (naturalOr clobbered (deviceArenaOverlapsOther head planes)) induction) (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family DeviceArenaTracked) . induction)) (deviceArenaAnyNamed planes head))))) (branch ArenaResidentsNext head tail induction . (nat-eliminate (lambda unrestricted kept : Nat . (family DeviceArenaTracked)) induction (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family DeviceArenaTracked) . (constructor DeviceArenaTracked DeviceArenaTrackedNext head 0 induction))) (deviceArenaAnyNamed carried head))))))) -- ---- (C) over the launches as written ---- -- the first launch breaking (C), as 2 + its index among the launches as -- written (a repeat's body once); 0 when none does def deviceArenaWordsHazard = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted globals : (family ArenaResidents) . (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted launches : (family DeviceArenaLaunches) . (app (eliminate DeviceArenaLaunches (lambda unrestricted current : (family DeviceArenaLaunches) . (pi unrestricted index : Nat . Nat)) launches (branch DeviceArenaLaunchesEnd . (lambda unrestricted index : Nat . 0)) (branch DeviceArenaLaunchesNext head tail induction . (lambda unrestricted index : Nat . (let unrestricted identity = (deviceArenaLaunchIdentityOf head) in (let unrestricted later = (induction (succ index)) in (nat-eliminate (lambda unrestricted sound : Nat . Nat) (naturalAdd 2 index) (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . later)) (naturalAnd (deviceArenaPhaseKnown phases identity) (deviceArenaSpansNamed windows (deviceArenaAppend (deviceArenaPhasePlanes (deviceArenaPhaseOf phases identity)) globals) (deviceArenaLaunchSpansOf head))))))))) 0))))) def deviceArenaLaunchCount = (lambda unrestricted launches : (family DeviceArenaLaunches) . (eliminate DeviceArenaLaunches (lambda unrestricted current : (family DeviceArenaLaunches) . Nat) launches (branch DeviceArenaLaunchesEnd . 0) (branch DeviceArenaLaunchesNext head tail induction . (succ induction)))) -- ---- the order the launches run ---- -- the runs of a schedule, from ordinal 0: a repeat's body runs once per -- iteration, and neighbouring runs of one phase merge def deviceArenaPrependRun = (lambda unrestricted identity : Bytes . (lambda unrestricted first : Nat . (lambda unrestricted count : Nat . (lambda unrestricted rest : (family DeviceArenaRuns) . (eliminate DeviceArenaRuns (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns)) rest (branch DeviceArenaRunsEnd . (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest)) (branch DeviceArenaRunsNext nextIdentity nextFirst nextCount nextTail ignored . (nat-eliminate (lambda unrestricted merges : Nat . (family DeviceArenaRuns)) (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest) (lambda unrestricted q : Nat . (lambda unrestricted unused : (family DeviceArenaRuns) . (constructor DeviceArenaRuns DeviceArenaRunsNext identity first (naturalAdd count nextCount) nextTail))) (naturalAnd (bytes-equal identity nextIdentity) (naturalEqual (naturalAdd first count) nextFirst))))))))) -- `runs` moved `shift` on, then `rest` def deviceArenaRunsShifted = (lambda unrestricted shift : Nat . (lambda unrestricted runs : (family DeviceArenaRuns) . (lambda unrestricted rest : (family DeviceArenaRuns) . (eliminate DeviceArenaRuns (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns)) runs (branch DeviceArenaRunsEnd . rest) (branch DeviceArenaRunsNext identity first count tail induction . (deviceArenaPrependRun identity (naturalAdd first shift) count induction)))))) def deviceArenaRunsOf = (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . (family DeviceArenaRuns)) schedule (branch NvidiaLaunchScheduleEmpty . (constructor DeviceArenaRuns DeviceArenaRunsEnd)) (branch NvidiaLaunchScheduleOne template . (constructor DeviceArenaRuns DeviceArenaRunsNext (deviceArenaLaunchIdentityOf (deviceArenaLaunchOf template)) 0 1 (constructor DeviceArenaRuns DeviceArenaRunsEnd))) (branch NvidiaLaunchScheduleAppend left right il ir . (deviceArenaRunsShifted 0 il (deviceArenaRunsShifted (nvidiaLaunchScheduleCount left) ir (constructor DeviceArenaRuns DeviceArenaRunsEnd)))) (branch NvidiaLaunchScheduleRepeat count iteration body ib . (let unrestricted extent = (nvidiaLaunchScheduleCount body) in (nat-eliminate (lambda unrestricted remaining : Nat . (family DeviceArenaRuns)) (constructor DeviceArenaRuns DeviceArenaRunsEnd) (lambda unrestricted p : Nat . (lambda unrestricted induction : (family DeviceArenaRuns) . (deviceArenaRunsShifted (naturalMultiply (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) p) extent) ib induction))) count))))) -- the identities of the runs meeting [first, first + count), then `rest` def deviceArenaRangeInstances = (lambda unrestricted runs : (family DeviceArenaRuns) . (lambda unrestricted first : Nat . (lambda unrestricted count : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (eliminate DeviceArenaRuns (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaInstances)) runs (branch DeviceArenaRunsEnd . rest) (branch DeviceArenaRunsNext identity runFirst runCount tail induction . (nat-eliminate (lambda unrestricted meets : Nat . (family DeviceArenaInstances)) induction (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family DeviceArenaInstances) . (constructor DeviceArenaInstances DeviceArenaInstancesNext identity induction))) (naturalAnd (naturalLess runFirst (naturalAdd first count)) (naturalLess first (naturalAdd runFirst runCount)))))))))) -- a submission's references, `shift` launches on (a repeated submission's -- iteration), then `rest` def deviceArenaReferenceInstances = (lambda unrestricted runs : (family DeviceArenaRuns) . (lambda unrestricted references : (family NvidiaLaunchReferences) . (eliminate NvidiaLaunchReferences (lambda unrestricted current : (family NvidiaLaunchReferences) . (pi unrestricted shift : Nat . (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances)))) references (branch NvidiaLaunchReferencesEmpty . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . rest))) (branch NvidiaLaunchReferencesRange first count . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (deviceArenaRangeInstances runs (naturalAdd first shift) count rest)))) (branch NvidiaLaunchReferencesAppend left right il ir . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest)))))))) def deviceArenaSubmissionInstances = (lambda unrestricted runs : (family DeviceArenaRuns) . (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) . (eliminate NvidiaSubmissionSchedule (lambda unrestricted current : (family NvidiaSubmissionSchedule) . (pi unrestricted shift : Nat . (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances)))) submissions (branch NvidiaSubmissionScheduleEmpty . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . rest))) (branch NvidiaSubmissionScheduleOne batch . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (eliminate NvidiaSubmissionBatch (lambda unrestricted current : (family NvidiaSubmissionBatch) . (family DeviceArenaInstances)) batch (branch NvidiaSubmissionBatchValue identity semaphore references . (deviceArenaReferenceInstances runs references shift rest)))))) (branch NvidiaSubmissionScheduleAppend left right il ir . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest))))) (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body ib . (lambda unrestricted shift : Nat . (lambda unrestricted rest : (family DeviceArenaInstances) . (app (nat-eliminate (lambda unrestricted remaining : Nat . (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances))) (lambda unrestricted iterationShift : Nat . rest) (lambda unrestricted p : Nat . (lambda unrestricted induction : (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)) . (lambda unrestricted iterationShift : Nat . (ib iterationShift (induction (naturalAdd iterationShift referenceStride)))))) count) shift)))) -- a profile's releases touch only the semaphore region: the launches -- are the body's (branch NvidiaSubmissionScheduleProfiled offset body ib . ib)))) -- ---- (D) over the executed instances ---- -- the first instance breaking (D), as `base` + its index; 0 when none does. -- The build's evaluator evaluates both arms of a choice, so each step makes -- exactly one recursive call (the walk goes on past a hazard; the first one -- found wins). -- every plane some phase carries def deviceArenaCarriedAnywhere = (lambda unrestricted phases : (family DeviceArenaPhases) . (eliminate DeviceArenaPhases (lambda unrestricted current : (family DeviceArenaPhases) . (family ArenaResidents)) phases (branch DeviceArenaPhasesEnd . (constructor ArenaResidents ArenaResidentsEnd)) (branch DeviceArenaPhasesNext head tail induction . (deviceArenaAppend (deviceArenaPhaseCarriedOf head) induction)))) def deviceArenaLifetimeHazard = (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted base : Nat . (lambda unrestricted instances : (family DeviceArenaInstances) . (let unrestricted carried = (deviceArenaCarriedAnywhere phases) in (app (eliminate DeviceArenaInstances (lambda unrestricted current : (family DeviceArenaInstances) . (pi unrestricted tracked : (family DeviceArenaTracked) . (pi unrestricted previous : Bytes . (pi unrestricted index : Nat . Nat)))) instances (branch DeviceArenaInstancesEnd . (lambda unrestricted tracked : (family DeviceArenaTracked) . (lambda unrestricted previous : Bytes . (lambda unrestricted index : Nat . 0)))) (branch DeviceArenaInstancesNext identity tail induction . (lambda unrestricted tracked : (family DeviceArenaTracked) . (lambda unrestricted previous : Bytes . (lambda unrestricted index : Nat . (let unrestricted starts = (naturalIsZero (bytes-equal identity previous)) in (let unrestricted phase = (deviceArenaPhaseOf phases identity) in (let unrestricted broken = (naturalAnd starts (naturalIsZero (deviceArenaAllIntact tracked (deviceArenaPhaseCarriedOf phase)))) in (let unrestricted next = (nat-eliminate (lambda unrestricted fresh : Nat . (family DeviceArenaTracked)) tracked (lambda unrestricted q : Nat . (lambda unrestricted unused : (family DeviceArenaTracked) . (deviceArenaDeclare carried tracked (deviceArenaPhasePlanes phase)))) starts) in (let unrestricted later = (induction next identity (naturalAdd index starts)) in (nat-eliminate (lambda unrestricted found : Nat . Nat) later (lambda unrestricted q : Nat . (lambda unrestricted unused : Nat . (naturalAdd base index))) broken))))))))))) deviceArenaTrackedEnd b"\x00" 0))))) -- ---- the verdict ---- -- 0 when the plan's device side is certified (see the top of this module) def deviceArenaHazard = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted globals : (family ArenaResidents) . (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) . (nat-eliminate (lambda unrestricted placed : Nat . Nat) 1 (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . (let unrestricted launches = (deviceArenaLaunches schedule) in (let unrestricted words = (deviceArenaWordsHazard windows globals phases launches) in (let unrestricted lifetimes = (deviceArenaLifetimeHazard phases (naturalAdd 2 (deviceArenaLaunchCount launches)) (deviceArenaSubmissionInstances (deviceArenaRunsOf schedule) submissions 0 (constructor DeviceArenaInstances DeviceArenaInstancesEnd))) in (naturalSelect (naturalIsZero words) lifetimes words)))))) (deviceArenaPlaced globals phases))))))) -- 1 when certified def deviceArenaCertificate = (lambda unrestricted windows : (family ArenaResidents) . (lambda unrestricted globals : (family ArenaResidents) . (lambda unrestricted phases : (family DeviceArenaPhases) . (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) . (naturalIsZero (deviceArenaHazard windows globals phases schedule submissions)))))))