AlphaGitHub
Source/Systems

Bob.Build.NativeHost

systems/bob/src/Bob/Build/NativeHost.alpha

882 lines46 declarations32.2 KiBSHA-256 3f8d3aa22d4e
Download exact fileView at revision426597bda5753d86c4

def · lines 754–766

bobHostCertified

Full file
754def bobHostCertified =
755  (lambda unrestricted qmdLength : Nat .
756    (lambda unrestricted pushLength : Nat .
757      (lambda unrestricted gpfifoLength : Nat .
758        (naturalAnd
759          bobHostSubmitsPlan
760          (naturalAnd
761            bobHostMovesCheckpoint
762            (nvidiaPlanHostRequestAdmitted
763              (bobHostLayout b"" qmdLength pushLength)
764              bobSubmissionCount
765              (bobRecipeFills qmdLength pushLength gpfifoLength)
766              bobHostSteps))))))

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.