Skip to content
This repository has been archived by the owner on Jun 17, 2024. It is now read-only.

Latest commit

 

History

History
110 lines (62 loc) · 3.42 KB

QUICFFI.md

File metadata and controls

110 lines (62 loc) · 3.42 KB

module QUICFFI

Make calls into Everest and Windows APIs

QUIC FFI - Calls from QUIC code into miTLS, libquiccrypto, or Windows APIs.

val createEvent:Unidentified product: [Int32.t] Unidentified product: [Int32.t] (Stack intptr_t ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

This is implemented in QUICFStar.c and calls CreateEventW with a NULL name and default security

val monitorAlloc:Unidentified product: [unit] (Stack intptr_t ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Implemented in QUICFStar.c, calls InitializeCriticalsection

val monitorEnter:Unidentified product: [intptr_t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Implemented in QUICFStar.c, calls EnterCriticalsection

val monitorExit:Unidentified product: [intptr_t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Implemented in QUICFStar.c, calls LeaveCriticalsection

val waitForSingleObject:Unidentified product: [intptr_t] Unidentified product: [U32.t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Call Windows WaitForSingleObject, with a timeout in milliseconds

val setEvent:Unidentified product: [intptr_t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Call Windows SetEvent()

val resetEvent:Unidentified product: [intptr_t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Call Windows ResetEvent()

val getSystemTime:Unidentified product: [unit] (Stack I64.t ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Get the system time, in UTC, measured in Windows FILETIME units (10,000ns) The absolute value doesn't matter, as all computation is relative.

val qsort64:Unidentified product: [(pointer U64.t)] Unidentified product: [(U32.t)] Unidentified product: [comparator] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Use the CRT qsort() to sort an array of UInt64.t in-place

type abbrev

Type of a timer callback function. First argument is a TP_CALLBACK_INSTANCE, and should be ignored Third argument is the PTP_TIMER that fired

val createTimer:Unidentified product: [(pointer connection)] Unidentified product: [timercallback] (Stack intptr_t ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Create a timer with callback

val setOneShotTimer:Unidentified product: [intptr_t] Unidentified product: [Int64.t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Set a one-shot timer. Positive times are absolute, negative are relative, in 100ns ticks

val cancelOneShotTimer:Unidentified product: [intptr_t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Cancel a one-shot timer.

val setRepeatingTimer:Unidentified product: [intptr_t] Unidentified product: [U32.t] (Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun h0 _ h1 -> modifies_none h0 h1)))))

Set a repeating timer, with period specified in milliseconds