module Compiler.MachineX86NativeAssembly import Compiler.MachineX86Native import Compiler.MachineX86NativeOffset family X86NativeAssembly : Type 0 constructor X86NativeAssemblyEnd constructor X86NativeAssemblyEmit field unrestricted x86NativeAssemblyInstruction : (family X86NativeInstruction) recursive unrestricted x86NativeAssemblyAfterInstruction constructor X86NativeAssemblyLabel field unrestricted x86NativeAssemblyLabelName : Bytes recursive unrestricted x86NativeAssemblyAfterLabel constructor X86NativeAssemblyJump field unrestricted x86NativeAssemblyJumpTarget : Bytes recursive unrestricted x86NativeAssemblyAfterJump constructor X86NativeAssemblyJumpCondition field unrestricted x86NativeAssemblyJumpConditionValue : (family X86NativeCondition) field unrestricted x86NativeAssemblyJumpConditionTarget : Bytes recursive unrestricted x86NativeAssemblyAfterJumpCondition constructor X86NativeAssemblyLoadEffectiveAddressRIPLabel field unrestricted x86NativeAssemblyLEADestination : (family X86NativeRegister64) field unrestricted x86NativeAssemblyLEATarget : Bytes recursive unrestricted x86NativeAssemblyAfterLEA end-family family X86NativeLabelTable : Type 0 constructor X86NativeLabelTableEmpty constructor X86NativeLabelTableEntry field unrestricted x86NativeLabelName : Bytes field unrestricted x86NativeLabelOffset : (family X86NativeUnsigned32) recursive unrestricted x86NativeRemainingLabels end-family family X86NativeLabelLookupResult : Type 0 constructor X86NativeLabelFound field unrestricted x86NativeFoundLabelOffset : (family X86NativeUnsigned32) constructor X86NativeLabelMissing end-family family X86NativeAssemblyLayoutResult : Type 0 constructor X86NativeAssemblyLayoutSuccess field unrestricted x86NativeAssemblyLabels : (family X86NativeLabelTable) field unrestricted x86NativeAssemblySize : (family X86NativeUnsigned32) constructor X86NativeAssemblyDuplicateLabel field unrestricted x86NativeDuplicateLabelName : Bytes constructor X86NativeAssemblyOffsetOverflow end-family family X86NativeAssemblyResult : Type 0 constructor X86NativeAssemblyEncoded field unrestricted x86NativeAssemblyEncodedBytes : Bytes constructor X86NativeAssemblyEncodeDuplicateLabel field unrestricted x86NativeAssemblyEncodeDuplicateName : Bytes constructor X86NativeAssemblyEncodeOffsetOverflow constructor X86NativeAssemblyMissingLabel field unrestricted x86NativeAssemblyMissingLabelName : Bytes constructor X86NativeAssemblyDisplacementOutOfRange field unrestricted x86NativeAssemblyDistantLabelName : Bytes end-family def x86NativeLookupLabel : (pi unrestricted name : Bytes . (pi unrestricted table : (family X86NativeLabelTable) . (family X86NativeLabelLookupResult))) = (lambda unrestricted name : Bytes . (lambda unrestricted table : (family X86NativeLabelTable) . (eliminate X86NativeLabelTable (lambda unrestricted value : (family X86NativeLabelTable) . (family X86NativeLabelLookupResult)) table (branch X86NativeLabelTableEmpty . (constructor X86NativeLabelLookupResult X86NativeLabelMissing)) (branch X86NativeLabelTableEntry existingName offset remaining induction . (nat-eliminate (lambda unrestricted equal : Nat . (family X86NativeLabelLookupResult)) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted equalInduction : (family X86NativeLabelLookupResult) . (constructor X86NativeLabelLookupResult X86NativeLabelFound offset))) (bytes-equal name existingName)))))) def x86NativeAdvanceLayout : (pi unrestricted encoded : Bytes . (pi unrestricted offset : (family X86NativeUnsigned32) . (pi unrestricted continuation : (pi unrestricted nextOffset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult)) . (family X86NativeAssemblyLayoutResult)))) = (lambda unrestricted encoded : Bytes . (lambda unrestricted offset : (family X86NativeUnsigned32) . (lambda unrestricted continuation : (pi unrestricted nextOffset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult)) . (eliminate X86NativeUnsigned32Result (lambda unrestricted result : (family X86NativeUnsigned32Result) . (family X86NativeAssemblyLayoutResult)) (x86NativeAdvanceUnsigned32ByBytes offset encoded) (branch X86NativeUnsigned32Success nextOffset . (continuation nextOffset)) (branch X86NativeUnsigned32Overflow . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyOffsetOverflow)))))) def x86NativeLayoutAssemblyFrom : (pi unrestricted assembly : (family X86NativeAssembly) . (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult))) = (lambda unrestricted assembly : (family X86NativeAssembly) . (eliminate X86NativeAssembly (lambda unrestricted value : (family X86NativeAssembly) . (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult))) assembly (branch X86NativeAssemblyEnd . (lambda unrestricted offset : (family X86NativeUnsigned32) . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyLayoutSuccess (constructor X86NativeLabelTable X86NativeLabelTableEmpty) offset))) (branch X86NativeAssemblyEmit instruction tail layoutTail . (lambda unrestricted offset : (family X86NativeUnsigned32) . (x86NativeAdvanceLayout (x86EncodeNativeInstruction instruction) offset layoutTail))) (branch X86NativeAssemblyLabel name tail layoutTail . (lambda unrestricted offset : (family X86NativeUnsigned32) . (eliminate X86NativeAssemblyLayoutResult (lambda unrestricted result : (family X86NativeAssemblyLayoutResult) . (family X86NativeAssemblyLayoutResult)) (layoutTail offset) (branch X86NativeAssemblyLayoutSuccess labels finalSize . (eliminate X86NativeLabelLookupResult (lambda unrestricted lookup : (family X86NativeLabelLookupResult) . (family X86NativeAssemblyLayoutResult)) (x86NativeLookupLabel name labels) (branch X86NativeLabelFound existingOffset . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyDuplicateLabel name)) (branch X86NativeLabelMissing . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyLayoutSuccess (constructor X86NativeLabelTable X86NativeLabelTableEntry name offset labels) finalSize)))) (branch X86NativeAssemblyDuplicateLabel duplicateName . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyDuplicateLabel duplicateName)) (branch X86NativeAssemblyOffsetOverflow . (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyOffsetOverflow))))) (branch X86NativeAssemblyJump target tail layoutTail . (lambda unrestricted offset : (family X86NativeUnsigned32) . (x86NativeAdvanceLayout (bytes 0 0 0 0 0) offset layoutTail))) (branch X86NativeAssemblyJumpCondition condition target tail layoutTail . (lambda unrestricted offset : (family X86NativeUnsigned32) . (x86NativeAdvanceLayout (bytes 0 0 0 0 0 0) offset layoutTail))) (branch X86NativeAssemblyLoadEffectiveAddressRIPLabel destination target tail layoutTail . (lambda unrestricted offset : (family X86NativeUnsigned32) . (x86NativeAdvanceLayout (bytes 0 0 0 0 0 0 0) offset layoutTail))))) def x86NativeLayoutAssembly : (pi unrestricted assembly : (family X86NativeAssembly) . (family X86NativeAssemblyLayoutResult)) = (lambda unrestricted assembly : (family X86NativeAssembly) . (x86NativeLayoutAssemblyFrom assembly x86NativeUnsigned32Zero)) def x86NativeUnsigned32Displacement : (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeDisplacement32)) = (lambda unrestricted value : (family X86NativeUnsigned32) . (eliminate X86NativeUnsigned32 (lambda unrestricted current : (family X86NativeUnsigned32) . (family X86NativeDisplacement32)) value (branch X86NativeUnsigned32Value byte0 byte1 byte2 byte3 . (constructor X86NativeDisplacement32 X86NativeDisplacement32Value byte0 byte1 byte2 byte3)))) def x86NativePrependAssemblyBytes : (pi unrestricted prefix : Bytes . (pi unrestricted result : (family X86NativeAssemblyResult) . (family X86NativeAssemblyResult))) = (lambda unrestricted prefix : Bytes . (lambda unrestricted result : (family X86NativeAssemblyResult) . (eliminate X86NativeAssemblyResult (lambda unrestricted value : (family X86NativeAssemblyResult) . (family X86NativeAssemblyResult)) result (branch X86NativeAssemblyEncoded encoded . (constructor X86NativeAssemblyResult X86NativeAssemblyEncoded (bytes-append prefix encoded))) (branch X86NativeAssemblyEncodeDuplicateLabel duplicateName . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeDuplicateLabel duplicateName)) (branch X86NativeAssemblyEncodeOffsetOverflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow)) (branch X86NativeAssemblyMissingLabel missingName . (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel missingName)) (branch X86NativeAssemblyDisplacementOutOfRange distantName . (constructor X86NativeAssemblyResult X86NativeAssemblyDisplacementOutOfRange distantName))))) def x86NativeEncodeJumpToLabel : (pi unrestricted conditionFlag : Nat . (pi unrestricted condition : (family X86NativeCondition) . (pi unrestricted targetName : Bytes . (pi unrestricted labels : (family X86NativeLabelTable) . (pi unrestricted sourceEnd : (family X86NativeUnsigned32) . (pi unrestricted tailResult : (family X86NativeAssemblyResult) . (family X86NativeAssemblyResult))))))) = (lambda unrestricted conditionFlag : Nat . (lambda unrestricted condition : (family X86NativeCondition) . (lambda unrestricted targetName : Bytes . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) . (lambda unrestricted tailResult : (family X86NativeAssemblyResult) . (eliminate X86NativeLabelLookupResult (lambda unrestricted lookup : (family X86NativeLabelLookupResult) . (family X86NativeAssemblyResult)) (x86NativeLookupLabel targetName labels) (branch X86NativeLabelFound targetOffset . (eliminate X86NativeRelativeDisplacementResult (lambda unrestricted displacementResult : (family X86NativeRelativeDisplacementResult) . (family X86NativeAssemblyResult)) (x86NativeRelativeDisplacement targetOffset sourceEnd) (branch X86NativeRelativeDisplacementSuccess displacement . (nat-eliminate (lambda unrestricted conditional : Nat . (family X86NativeAssemblyResult)) (x86NativePrependAssemblyBytes (x86EncodeNativeInstruction (constructor X86NativeInstruction X86NativeJumpRelative32 (x86NativeUnsigned32Displacement displacement))) tailResult) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family X86NativeAssemblyResult) . (x86NativePrependAssemblyBytes (x86EncodeNativeInstruction (constructor X86NativeInstruction X86NativeJumpConditionRelative32 condition (x86NativeUnsigned32Displacement displacement))) tailResult))) conditionFlag)) (branch X86NativeRelativeDisplacementOutOfRange . (constructor X86NativeAssemblyResult X86NativeAssemblyDisplacementOutOfRange targetName)))) (branch X86NativeLabelMissing . (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel targetName))))))))) def x86NativeEncodeLEAToLabel : (pi unrestricted destination : (family X86NativeRegister64) . (pi unrestricted targetName : Bytes . (pi unrestricted labels : (family X86NativeLabelTable) . (pi unrestricted sourceEnd : (family X86NativeUnsigned32) . (pi unrestricted tailResult : (family X86NativeAssemblyResult) . (family X86NativeAssemblyResult)))))) = (lambda unrestricted destination : (family X86NativeRegister64) . (lambda unrestricted targetName : Bytes . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) . (lambda unrestricted tailResult : (family X86NativeAssemblyResult) . (eliminate X86NativeLabelLookupResult (lambda unrestricted lookup : (family X86NativeLabelLookupResult) . (family X86NativeAssemblyResult)) (x86NativeLookupLabel targetName labels) (branch X86NativeLabelFound targetOffset . (eliminate X86NativeRelativeDisplacementResult (lambda unrestricted displacementResult : (family X86NativeRelativeDisplacementResult) . (family X86NativeAssemblyResult)) (x86NativeRelativeDisplacement targetOffset sourceEnd) (branch X86NativeRelativeDisplacementSuccess displacement . (x86NativePrependAssemblyBytes (x86EncodeNativeInstruction (constructor X86NativeInstruction X86NativeLoadEffectiveAddressRIP destination (x86NativeUnsigned32Displacement displacement))) tailResult)) (branch X86NativeRelativeDisplacementOutOfRange . (constructor X86NativeAssemblyResult X86NativeAssemblyDisplacementOutOfRange targetName)))) (branch X86NativeLabelMissing . (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel targetName)))))))) def x86NativeEncodeAssemblyFrom : (pi unrestricted assembly : (family X86NativeAssembly) . (pi unrestricted labels : (family X86NativeLabelTable) . (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyResult)))) = (lambda unrestricted assembly : (family X86NativeAssembly) . (eliminate X86NativeAssembly (lambda unrestricted value : (family X86NativeAssembly) . (pi unrestricted labels : (family X86NativeLabelTable) . (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyResult)))) assembly (branch X86NativeAssemblyEnd . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (constructor X86NativeAssemblyResult X86NativeAssemblyEncoded b"")))) (branch X86NativeAssemblyEmit instruction tail encodeTail . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (let unrestricted encoded = (x86EncodeNativeInstruction instruction) in (eliminate X86NativeUnsigned32Result (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) . (family X86NativeAssemblyResult)) (x86NativeAdvanceUnsigned32ByBytes offset encoded) (branch X86NativeUnsigned32Success nextOffset . (x86NativePrependAssemblyBytes encoded (encodeTail labels nextOffset))) (branch X86NativeUnsigned32Overflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))))) (branch X86NativeAssemblyLabel name tail encodeTail . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (encodeTail labels offset)))) (branch X86NativeAssemblyJump target tail encodeTail . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (eliminate X86NativeUnsigned32Result (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) . (family X86NativeAssemblyResult)) (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0)) (branch X86NativeUnsigned32Success nextOffset . (x86NativeEncodeJumpToLabel zero (constructor X86NativeCondition X86NativeConditionZero) target labels nextOffset (encodeTail labels nextOffset))) (branch X86NativeUnsigned32Overflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow)))))) (branch X86NativeAssemblyJumpCondition condition target tail encodeTail . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (eliminate X86NativeUnsigned32Result (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) . (family X86NativeAssemblyResult)) (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0 0)) (branch X86NativeUnsigned32Success nextOffset . (x86NativeEncodeJumpToLabel (succ zero) condition target labels nextOffset (encodeTail labels nextOffset))) (branch X86NativeUnsigned32Overflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow)))))) (branch X86NativeAssemblyLoadEffectiveAddressRIPLabel destination target tail encodeTail . (lambda unrestricted labels : (family X86NativeLabelTable) . (lambda unrestricted offset : (family X86NativeUnsigned32) . (eliminate X86NativeUnsigned32Result (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) . (family X86NativeAssemblyResult)) (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0 0 0)) (branch X86NativeUnsigned32Success nextOffset . (x86NativeEncodeLEAToLabel destination target labels nextOffset (encodeTail labels nextOffset))) (branch X86NativeUnsigned32Overflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow)))))))) def x86NativeAssemble : (pi unrestricted assembly : (family X86NativeAssembly) . (family X86NativeAssemblyResult)) = (lambda unrestricted assembly : (family X86NativeAssembly) . (eliminate X86NativeAssemblyLayoutResult (lambda unrestricted layout : (family X86NativeAssemblyLayoutResult) . (family X86NativeAssemblyResult)) (x86NativeLayoutAssembly assembly) (branch X86NativeAssemblyLayoutSuccess labels size . (x86NativeEncodeAssemblyFrom assembly labels x86NativeUnsigned32Zero)) (branch X86NativeAssemblyDuplicateLabel duplicateName . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeDuplicateLabel duplicateName)) (branch X86NativeAssemblyOffsetOverflow . (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))