module Hardware.Nvidia.SM86.Command.Pushbuffer import Data.Bytes import Model.Word32 import Model.Word32Logic import Model.Word64 import Std.Byte import Std.Natural import Model.Parameter import Model.Config family PushbufferErrorCode : Type 0 constructor PushbufferOpcodeOutOfRange constructor PushbufferCountOutOfRange constructor PushbufferSubchannelOutOfRange constructor PushbufferMethodAddressUnaligned constructor PushbufferMethodAddressOutOfRange constructor PushbufferAddressUnaligned constructor PushbufferAddressOutOfRange constructor PushbufferLengthOutOfRange constructor PushbufferAlignmentOverflow constructor PushbufferQMDAddressUnaligned end-family family PushbufferBytesResult : Type 0 constructor PushbufferBytesReady field unrestricted pushbufferEncodedBytes : Bytes constructor PushbufferBytesRejected field unrestricted pushbufferBytesError : (family PushbufferErrorCode) end-family family PushbufferDwordList : Type 0 constructor PushbufferDwordEnd constructor PushbufferDwordNext field unrestricted pushbufferDwordHead : (family ModelWord32) recursive unrestricted pushbufferDwordTail end-family family PushbufferGPFIFOEntryResult : Type 0 constructor PushbufferGPFIFOEntryReady field unrestricted pushbufferGPFIFOLow : (family ModelWord32) field unrestricted pushbufferGPFIFOHigh : (family ModelWord32) constructor PushbufferGPFIFOEntryRejected field unrestricted pushbufferGPFIFOError : (family PushbufferErrorCode) end-family family PushbufferAlignedDwordsResult : Type 0 constructor PushbufferAlignedDwordsReady field unrestricted pushbufferAlignedDwords : (family ModelWord32) constructor PushbufferAlignedDwordsRejected field unrestricted pushbufferAlignedDwordsError : (family PushbufferErrorCode) end-family family PushbufferConstructionError : Type 0 constructor PushbufferInlineQMDLengthMismatch constructor PushbufferComputeConfigurationMismatch constructor PushbufferConstructionIdentityMalformed constructor PushbufferConstructionRejected field unrestricted pushbufferConstructionCause : (family PushbufferErrorCode) end-family family PushbufferComputeConfig : Type 0 constructor PushbufferComputeConfigValue field unrestricted pushbufferComputeClass : (family ModelWord32) field unrestricted pushbufferComputeSharedWindow : (family ModelWord64) field unrestricted pushbufferComputeLocalMemory : (family ModelWord64) field unrestricted pushbufferComputeLocalMemoryBytes : (family ModelWord64) field unrestricted pushbufferComputeLocalWindow : (family ModelWord64) field unrestricted pushbufferComputeSMCount : (family ModelWord32) field unrestricted pushbufferComputeSPAVersion : (family ModelWord32) end-family family PushbufferConstructionReceipt : Type 0 constructor PushbufferConstructionReceiptValue field unrestricted pushbufferConstructionIdentity : Bytes field unrestricted pushbufferConstructionBytes : Bytes field unrestricted pushbufferConstructionDwords : Nat field unrestricted pushbufferConstructionHostFallbacks : Nat end-family family PushbufferConstructionResult : Type 0 constructor PushbufferConstructionReady field unrestricted pushbufferConstructionReadyReceipt : (family PushbufferConstructionReceipt) constructor PushbufferConstructionFailed field unrestricted pushbufferConstructionError : (family PushbufferConstructionError) end-family def pushbufferErrorCodeBytes = (lambda unrestricted code : (family PushbufferErrorCode) . (eliminate PushbufferErrorCode (lambda unrestricted current : (family PushbufferErrorCode) . Bytes) code (branch PushbufferOpcodeOutOfRange . b"ALPHA-HPB-201") (branch PushbufferCountOutOfRange . b"ALPHA-HPB-202") (branch PushbufferSubchannelOutOfRange . b"ALPHA-HPB-203") (branch PushbufferMethodAddressUnaligned . b"ALPHA-HPB-204") (branch PushbufferMethodAddressOutOfRange . b"ALPHA-HPB-205") (branch PushbufferAddressUnaligned . b"ALPHA-HPB-206") (branch PushbufferAddressOutOfRange . b"ALPHA-HPB-207") (branch PushbufferLengthOutOfRange . b"ALPHA-HPB-208") (branch PushbufferAlignmentOverflow . b"ALPHA-HPB-209") (branch PushbufferQMDAddressUnaligned . b"ALPHA-HPB-210"))) def pushbufferDwordCount = (lambda unrestricted values : (family PushbufferDwordList) . (eliminate PushbufferDwordList (lambda unrestricted current : (family PushbufferDwordList) . Nat) values (branch PushbufferDwordEnd . zero) (branch PushbufferDwordNext head tail ih_tail . (succ ih_tail)))) def pushbufferEncodeDwords = (lambda unrestricted values : (family PushbufferDwordList) . (eliminate PushbufferDwordList (lambda unrestricted current : (family PushbufferDwordList) . Bytes) values (branch PushbufferDwordEnd . b"") (branch PushbufferDwordNext head tail ih_tail . (bytes-append (dataBytesWord32LE head) ih_tail)))) def pushbufferFlagAnd = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalAnd left right))) def pushbufferFlagOr = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalOr left right))) def pushbufferIfFlag = (lambda unrestricted condition : Nat . (lambda unrestricted whenTrue : Nat . (lambda unrestricted whenFalse : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) whenFalse (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue)) condition)))) def pushbufferByteIsZero = (lambda unrestricted value : Byte . (naturalIsZero (byte-to-nat value))) def pushbufferByteNonZero = (lambda unrestricted value : Byte . (naturalIsZero (pushbufferByteIsZero value))) def pushbufferWord32NonZero = (lambda unrestricted value : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . Nat) value (branch ModelWord32Value b0 b1 b2 b3 . (pushbufferFlagOr (pushbufferByteNonZero b0) (pushbufferFlagOr (pushbufferByteNonZero b1) (pushbufferFlagOr (pushbufferByteNonZero b2) (pushbufferByteNonZero b3))))))) def pushbufferAddressAligned4 = (lambda unrestricted address : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (naturalIsZero (naturalModuloUnchecked (byte-to-nat b0) (byte-to-nat (byte 4))))))) def pushbufferAddressAligned16 = (lambda unrestricted address : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (naturalIsZero (naturalModuloUnchecked (byte-to-nat b0) (byte-to-nat (byte 16))))))) def pushbufferAddressAligned256 = (lambda unrestricted address : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (pushbufferByteIsZero b0)))) def pushbufferAddressIn40Bits = (lambda unrestricted address : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (pushbufferFlagAnd (pushbufferByteIsZero b5) (pushbufferFlagAnd (pushbufferByteIsZero b6) (pushbufferByteIsZero b7)))))) def pushbufferMethodHeaderUnchecked = (lambda unrestricted opcode : Nat . (lambda unrestricted count : Nat . (lambda unrestricted subchannel : Nat . (lambda unrestricted byteAddress : Nat . (app (lambda unrestricted dwordAddress : Nat . (bytes (nat-to-byte (naturalModuloUnchecked dwordAddress (succ (byte-to-nat (byte 255))))) (nat-to-byte (naturalAdd (naturalDivideUnchecked dwordAddress (succ (byte-to-nat (byte 255)))) (naturalMultiply subchannel (byte-to-nat (byte 32))))) (nat-to-byte (naturalModuloUnchecked count (succ (byte-to-nat (byte 255))))) (nat-to-byte (naturalAdd (naturalDivideUnchecked count (succ (byte-to-nat (byte 255)))) (naturalMultiply opcode (byte-to-nat (byte 32))))))) (naturalDivideUnchecked byteAddress (byte-to-nat (byte 4)))))))) def pushbufferMethodHeader = (lambda unrestricted opcode : Nat . (lambda unrestricted count : Nat . (lambda unrestricted subchannel : Nat . (lambda unrestricted byteAddress : Nat . (nat-eliminate (lambda unrestricted opcodeValid : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferOpcodeOutOfRange)) (lambda unrestricted opcodePredecessor : Nat . (lambda unrestricted opcodeInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted countValid : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferCountOutOfRange)) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted countInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted subchannelValid : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferSubchannelOutOfRange)) (lambda unrestricted subchannelPredecessor : Nat . (lambda unrestricted subchannelInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted addressAligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferMethodAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted addressValid : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferMethodAddressOutOfRange)) (lambda unrestricted addressPredecessor : Nat . (lambda unrestricted addressInduction : (family PushbufferBytesResult) . (constructor PushbufferBytesResult PushbufferBytesReady (pushbufferMethodHeaderUnchecked opcode count subchannel byteAddress)))) (nat-less-than (naturalDivideUnchecked byteAddress (byte-to-nat (byte 4))) (naturalPowerOfTwo (byte-to-nat (byte 13))))))) (naturalIsZero (naturalModuloUnchecked byteAddress (byte-to-nat (byte 4))))))) (nat-less-than subchannel (byte-to-nat (byte 8)))))) (nat-less-than count (naturalPowerOfTwo (byte-to-nat (byte 13))))))) (nat-less-than opcode (byte-to-nat (byte 8)))))))) def pushbufferIncrementingMethod = (lambda unrestricted subchannel : Nat . (lambda unrestricted byteAddress : Nat . (lambda unrestricted values : (family PushbufferDwordList) . (eliminate PushbufferBytesResult (lambda unrestricted current : (family PushbufferBytesResult) . (family PushbufferBytesResult)) (pushbufferMethodHeader (succ zero) (pushbufferDwordCount values) subchannel byteAddress) (branch PushbufferBytesReady header . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append header (pushbufferEncodeDwords values)))) (branch PushbufferBytesRejected error . (constructor PushbufferBytesResult PushbufferBytesRejected error)))))) def pushbufferImmediateMethod = (lambda unrestricted subchannel : Nat . (lambda unrestricted byteAddress : Nat . (lambda unrestricted value : Nat . (pushbufferMethodHeader (byte-to-nat (byte 4)) value subchannel byteAddress)))) def pushbufferSemaphoreRelease = (lambda unrestricted address : (family ModelWord64) . (lambda unrestricted payload : (family ModelWord32) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append (bytes 23 32 5 32) (bytes-append (bytes b0 b1 b2 b3) (bytes-append (bytes b4 0 0 0) (bytes-append (dataBytesWord32LE payload) (bytes-append (bytes 0 0 0 0) (bytes 1 0 16 0))))))))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned4 address)))) def pushbufferSemaphoreAcquire = (lambda unrestricted address : (family ModelWord64) . (lambda unrestricted payload : (family ModelWord32) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append (bytes 23 32 5 32) (bytes-append (bytes b0 b1 b2 b3) (bytes-append (bytes b4 0 0 0) (bytes-append (dataBytesWord32LE payload) (bytes-append (bytes 0 0 0 0) (bytes 0 0 0 0))))))))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned4 address)))) def pushbufferSemaphoreReleaseTimestamp = (lambda unrestricted address : (family ModelWord64) . (lambda unrestricted payload : (family ModelWord64) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted currentAddress : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value a0 a1 a2 a3 a4 a5 a6 a7 . (eliminate ModelWord64 (lambda unrestricted currentPayload : (family ModelWord64) . (family PushbufferBytesResult)) payload (branch ModelWord64Value p0 p1 p2 p3 p4 p5 p6 p7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append (bytes 23 32 5 32) (bytes-append (bytes a0 a1 a2 a3) (bytes-append (bytes a4 0 0 0) (bytes-append (bytes p0 p1 p2 p3) (bytes-append (bytes p4 p5 p6 p7) (bytes 1 0 16 3))))))))))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned16 address)))) -- QMDV03/NVC56F release form used by the physically accepted multi-launch -- stream. The operation word is explicit because a pre-launch timestamp is -- RELEASE|TIMESTAMP (0x02000001), whereas the retiring fence is additionally -- RELEASE_WFI (0x02100001). Both carry a 32-bit payload and a zero high word. def pushbufferSemaphoreRelease32Operation = (lambda unrestricted address : (family ModelWord64) . (lambda unrestricted payload : (family ModelWord32) . (lambda unrestricted operation : (family ModelWord32) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted currentAddress : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value a0 a1 a2 a3 a4 a5 a6 a7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append -- SEM_EXECUTE belongs to the host subchannel (0), -- while the compute launch methods use subchannel 1. (bytes 23 0 5 32) (bytes-append (bytes a0 a1 a2 a3) (bytes-append (bytes a4 0 0 0) (bytes-append (dataBytesWord32LE payload) (bytes-append (bytes 0 0 0 0) (dataBytesWord32LE operation))))))))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned16 address))))) def pushbufferBarrier = (constructor PushbufferBytesResult PushbufferBytesReady (bytes 135 32 1 32 20 0 0 0)) def pushbufferPCASLaunch = (lambda unrestricted address : (family ModelWord64) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes 173 32 1 32 b1 b2 b3 b4 176 32 9 128)))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned256 address))) def pushbufferPCASLaunchWithBarrier = (lambda unrestricted address : (family ModelWord64) . (eliminate PushbufferBytesResult (lambda unrestricted current : (family PushbufferBytesResult) . (family PushbufferBytesResult)) (pushbufferPCASLaunch address) (branch PushbufferBytesReady launchBytes . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append launchBytes (bytes 135 32 1 32 20 0 0 0)))) (branch PushbufferBytesRejected error . (constructor PushbufferBytesResult PushbufferBytesRejected error)))) -- The accepted QMDV03 batch stream uses an explicit one-dword -- SEND_SIGNALING_PCAS2_B method followed by the idle barrier. Keep the older -- compact immediate-method owner above stable for its attested callers. def pushbufferPCASLaunchV03WithBarrier = (lambda unrestricted address : (family ModelWord64) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferBytesResult)) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes 173 32 1 32 b1 b2 b3 b4 176 32 1 32 3 0 0 0 135 32 1 32 20 0 0 0)))))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned256 address))) def pushbufferDwordLengthInRange = (lambda unrestricted dwords : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . Nat) dwords (branch ModelWord32Value b0 b1 b2 b3 . (pushbufferFlagAnd (pushbufferWord32NonZero dwords) (pushbufferFlagAnd (pushbufferByteIsZero b3) (nat-less-than (byte-to-nat b2) (byte-to-nat (byte 32)))))))) def pushbufferGPFIFOEntry = (lambda unrestricted address : (family ModelWord64) . (lambda unrestricted dwords : (family ModelWord32) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferGPFIFOEntryResult)) (constructor PushbufferGPFIFOEntryResult PushbufferGPFIFOEntryRejected (constructor PushbufferErrorCode PushbufferAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferGPFIFOEntryResult) . (nat-eliminate (lambda unrestricted inRange : Nat . (family PushbufferGPFIFOEntryResult)) (constructor PushbufferGPFIFOEntryResult PushbufferGPFIFOEntryRejected (constructor PushbufferErrorCode PushbufferAddressOutOfRange)) (lambda unrestricted rangePredecessor : Nat . (lambda unrestricted rangeInduction : (family PushbufferGPFIFOEntryResult) . (nat-eliminate (lambda unrestricted lengthValid : Nat . (family PushbufferGPFIFOEntryResult)) (constructor PushbufferGPFIFOEntryResult PushbufferGPFIFOEntryRejected (constructor PushbufferErrorCode PushbufferLengthOutOfRange)) (lambda unrestricted lengthPredecessor : Nat . (lambda unrestricted lengthInduction : (family PushbufferGPFIFOEntryResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferGPFIFOEntryResult)) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferGPFIFOEntryResult PushbufferGPFIFOEntryReady (constructor ModelWord32 ModelWord32Value (byteAnd b0 (byte 252)) b1 b2 b3) (modelWord32Or (constructor ModelWord32 ModelWord32Value b4 (byte 0) (byte 0) (byte 0)) (modelWord32ShiftLeft dwords (byte-to-nat (byte 10))))))))) (pushbufferDwordLengthInRange dwords)))) (pushbufferAddressIn40Bits address)))) (pushbufferAddressAligned4 address)))) def pushbufferCanAdd63 = (lambda unrestricted value : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . Nat) value (branch ModelWord32Value b0 b1 b2 b3 . (pushbufferIfFlag (nat-less-than (byte-to-nat b3) (byte-to-nat (byte 255))) (succ zero) (pushbufferIfFlag (nat-less-than (byte-to-nat b2) (byte-to-nat (byte 255))) (succ zero) (pushbufferIfFlag (nat-less-than (byte-to-nat b1) (byte-to-nat (byte 255))) (succ zero) (nat-less-than (byte-to-nat b0) (byte-to-nat (byte 193))))))))) def pushbufferAlignedSegmentDwords = (lambda unrestricted dwords : (family ModelWord32) . (nat-eliminate (lambda unrestricted nonzero : Nat . (family PushbufferAlignedDwordsResult)) (constructor PushbufferAlignedDwordsResult PushbufferAlignedDwordsRejected (constructor PushbufferErrorCode PushbufferLengthOutOfRange)) (lambda unrestricted nonzeroPredecessor : Nat . (lambda unrestricted nonzeroInduction : (family PushbufferAlignedDwordsResult) . (nat-eliminate (lambda unrestricted noOverflow : Nat . (family PushbufferAlignedDwordsResult)) (constructor PushbufferAlignedDwordsResult PushbufferAlignedDwordsRejected (constructor PushbufferErrorCode PushbufferAlignmentOverflow)) (lambda unrestricted overflowPredecessor : Nat . (lambda unrestricted overflowInduction : (family PushbufferAlignedDwordsResult) . (constructor PushbufferAlignedDwordsResult PushbufferAlignedDwordsReady (modelWord32And (modelWord32Add dwords 63) 4294967232)))) (pushbufferCanAdd63 dwords)))) (pushbufferWord32NonZero dwords))) def pushbufferConstructionErrorBytes = (lambda unrestricted error : (family PushbufferConstructionError) . (eliminate PushbufferConstructionError (lambda unrestricted current : (family PushbufferConstructionError) . Bytes) error (branch PushbufferInlineQMDLengthMismatch . b"ALPHA-HPBC-201") (branch PushbufferComputeConfigurationMismatch . b"ALPHA-HPBC-202") (branch PushbufferConstructionIdentityMalformed . b"ALPHA-HPBC-203") (branch PushbufferConstructionRejected cause . (pushbufferErrorCodeBytes cause)))) def pushbufferInlineLaunch = (lambda unrestricted stagingAddress : (family ModelWord64) . (lambda unrestricted descriptor : (family PushbufferDwordList) . (nat-eliminate (lambda unrestricted aligned : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned)) (lambda unrestricted alignedPredecessor : Nat . (lambda unrestricted alignedInduction : (family PushbufferBytesResult) . (nat-eliminate (lambda unrestricted descriptorLength : Nat . (family PushbufferBytesResult)) (constructor PushbufferBytesResult PushbufferBytesRejected (constructor PushbufferErrorCode PushbufferLengthOutOfRange)) (lambda unrestricted lengthPredecessor : Nat . (lambda unrestricted lengthInduction : (family PushbufferBytesResult) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family PushbufferBytesResult)) stagingAddress (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor PushbufferBytesResult PushbufferBytesReady (bytes-append (bytes 198 32 66 32 b5 b6 b7 0 b1 b2 b3 b4) (pushbufferEncodeDwords descriptor))))))) (naturalEqual (pushbufferDwordCount descriptor) (byte-to-nat (byte 64)))))) (pushbufferAddressAligned256 stagingAddress)))) def pushbufferAddressIn49Bits = (lambda unrestricted address : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) address (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (pushbufferFlagAnd (byte-equal b7 (byte 0)) (nat-less-than (byte-to-nat b6) (byte-to-nat (byte 2))))))) def pushbufferExtentIn40Bits = (lambda unrestricted extent : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Nat) extent (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (pushbufferFlagAnd (pushbufferWord32NonZero (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3)) (pushbufferFlagAnd (byte-equal b5 (byte 0)) (pushbufferFlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0)))))))) def pushbufferComputeArchitecturePairValid = (lambda unrestricted class : (family ModelWord32) . (lambda unrestricted spa : (family ModelWord32) . (naturalOr (naturalAnd (bytes-equal (dataBytesWord32LE class) (bytes 192 199 0 0)) (bytes-equal (dataBytesWord32LE spa) (bytes 6 8 0 0))) (naturalAnd (bytes-equal (dataBytesWord32LE class) (bytes 192 201 0 0)) (bytes-equal (dataBytesWord32LE spa) (bytes 9 8 0 0)))))) def pushbufferComputeConfigValid = (lambda unrestricted config : (family PushbufferComputeConfig) . (eliminate PushbufferComputeConfig (lambda unrestricted current : (family PushbufferComputeConfig) . Nat) config (branch PushbufferComputeConfigValue class shared local localBytes localWindow smCount spa . (naturalAnd (pushbufferComputeArchitecturePairValid class spa) (naturalAnd (bytes-equal (dataBytesWord64LE shared) (bytes 0 0 0 254 0 0 0 0)) (naturalAnd (bytes-equal (dataBytesWord64LE localWindow) (bytes 0 0 0 255 0 0 0 0)) (naturalAnd (pushbufferAddressIn49Bits local) (naturalAnd (pushbufferExtentIn40Bits localBytes) (naturalAnd (naturalAnd (pushbufferWord32NonZero smCount) (nat-less-than (modelWord32ToNatural smCount) (naturalPowerOfTwo (byte-to-nat (byte 9))))) 1))))))))) def pushbufferReferenceCounterBytes = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . Bytes) b"" (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-append (bytes 146 32 1 32 (nat-to-byte predecessor) 160 8 0) induction))) count)) def pushbufferComputeInitializationBytes = (lambda unrestricted config : (family PushbufferComputeConfig) . (eliminate PushbufferComputeConfig (lambda unrestricted current : (family PushbufferComputeConfig) . Bytes) config (branch PushbufferComputeConfigValue class shared local localBytes localWindow smCount spa . (eliminate ModelWord64 (lambda unrestricted currentShared : (family ModelWord64) . Bytes) shared (branch ModelWord64Value s0 s1 s2 s3 s4 s5 s6 s7 . (eliminate ModelWord64 (lambda unrestricted currentLocal : (family ModelWord64) . Bytes) local (branch ModelWord64Value l0 l1 l2 l3 l4 l5 l6 l7 . (eliminate ModelWord64 (lambda unrestricted currentBytes : (family ModelWord64) . Bytes) localBytes (branch ModelWord64Value z0 z1 z2 z3 z4 z5 z6 z7 . (eliminate ModelWord64 (lambda unrestricted currentWindow : (family ModelWord64) . Bytes) localWindow (branch ModelWord64Value w0 w1 w2 w3 w4 w5 w6 w7 . (bytes-append (bytes 0 32 1 32) (bytes-append (dataBytesWord32LE class) (bytes-append (bytes 64 32 1 32 0 0 0 0) (bytes-append (bytes 168 32 2 32 s4 s5 s6 s7 s0 s1 s2 s3) (bytes-append (bytes 228 33 2 32 l4 l5 (byteAnd l6 (byte 1)) 0 l0 l1 l2 l3) (bytes-append (bytes 236 33 2 32 w4 w5 (byteAnd w6 (byte 1)) 0 w0 w1 w2 w3) (bytes-append (bytes 185 32 3 32 z4 0 0 0 z0 z1 z2 z3) (bytes-append (dataBytesWord32LE smCount) (bytes-append (bytes 196 32 1 32) (bytes-append (dataBytesWord32LE spa) (pushbufferReferenceCounterBytes (byte-to-nat (byte 64)))))))))))))))))))))))) def pushbufferReferenceCounterBytesAscendingFrom = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted start : Nat . Bytes)) (lambda unrestricted start : Nat . b"") (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted start : Nat . Bytes) . (lambda unrestricted start : Nat . (bytes-append (bytes 146 32 1 32 (nat-to-byte start) 160 8 0) (induction (succ start)))))) count)) def pushbufferReferenceCounterBytesAscending = (lambda unrestricted count : Nat . (pushbufferReferenceCounterBytesAscendingFrom count zero)) -- Exact QMDV03 compute initialization used by the accepted Coppelius channel. -- In particular it writes the SPA version before the windows, emits the -- 64 CWD reference counters in ascending order, and invalidates the shader -- cache with value one. The older owner above remains byte-stable. def pushbufferComputeInitializationV03Bytes = (lambda unrestricted config : (family PushbufferComputeConfig) . (eliminate PushbufferComputeConfig (lambda unrestricted current : (family PushbufferComputeConfig) . Bytes) config (branch PushbufferComputeConfigValue class shared local localBytes localWindow smCount spa . (eliminate ModelWord64 (lambda unrestricted currentShared : (family ModelWord64) . Bytes) shared (branch ModelWord64Value s0 s1 s2 s3 s4 s5 s6 s7 . (eliminate ModelWord64 (lambda unrestricted currentLocal : (family ModelWord64) . Bytes) local (branch ModelWord64Value l0 l1 l2 l3 l4 l5 l6 l7 . (eliminate ModelWord64 (lambda unrestricted currentBytes : (family ModelWord64) . Bytes) localBytes (branch ModelWord64Value z0 z1 z2 z3 z4 z5 z6 z7 . (eliminate ModelWord64 (lambda unrestricted currentWindow : (family ModelWord64) . Bytes) localWindow (branch ModelWord64Value w0 w1 w2 w3 w4 w5 w6 w7 . (bytes-append (bytes 0 32 1 32) (bytes-append (dataBytesWord32LE class) (bytes-append (bytes 196 32 1 32) (bytes-append (dataBytesWord32LE spa) (bytes-append (bytes 168 32 2 32 s4 s5 s6 s7 s0 s1 s2 s3) (bytes-append (bytes 228 33 2 32 l4 l5 (byteAnd l6 (byte 1)) 0 l0 l1 l2 l3) (bytes-append (bytes 236 33 2 32 w4 w5 (byteAnd w6 (byte 1)) 0 w0 w1 w2 w3) (bytes-append (bytes 185 32 1 32 z0 z1 z2 z3) (bytes-append (pushbufferReferenceCounterBytesAscending (byte-to-nat (byte 64))) (bytes 135 32 1 32 1 0 0 0))))))))))))))))))))) def pushbufferBuildComputeInitialization = (lambda unrestricted identity : Bytes . (lambda unrestricted config : (family PushbufferComputeConfig) . (nat-eliminate (lambda unrestricted identityValid : Nat . (family PushbufferConstructionResult)) (constructor PushbufferConstructionResult PushbufferConstructionFailed (constructor PushbufferConstructionError PushbufferConstructionIdentityMalformed)) (lambda unrestricted identityPredecessor : Nat . (lambda unrestricted identityInduction : (family PushbufferConstructionResult) . (nat-eliminate (lambda unrestricted configValid : Nat . (family PushbufferConstructionResult)) (constructor PushbufferConstructionResult PushbufferConstructionFailed (constructor PushbufferConstructionError PushbufferComputeConfigurationMismatch)) (lambda unrestricted configPredecessor : Nat . (lambda unrestricted configInduction : (family PushbufferConstructionResult) . (app (lambda unrestricted encoded : Bytes . (constructor PushbufferConstructionResult PushbufferConstructionReady (constructor PushbufferConstructionReceipt PushbufferConstructionReceiptValue identity encoded (naturalDivideUnchecked (bytes-length encoded) (byte-to-nat (byte 4))) zero))) (pushbufferComputeInitializationBytes config)))) (pushbufferComputeConfigValid config)))) (naturalEqual (bytes-length identity) (byte-to-nat (byte 64))))))