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

Latest commit

 

History

History
37 lines (19 loc) · 1.16 KB

QUICMutators.md

File metadata and controls

37 lines (19 loc) · 1.16 KB

module QUICMutators

  • Mutator helper functions

QUIC Mutators - helper functions to mutate data within the QUIC state

let ((strm_get_mutable (strm:pointer quic_stream)):(Stack (quic_stream_mutable) ((requires ((fun _ -> true)))) ((ensures ((fun _ _ _ -> true)))))):let  strm' = !*(strm) in !*((strm'.p.qsm_state))

Get a readonly copy of the mutable part of a quic_stream

let ((upd_state (strmm:pointer quic_stream_mutable) (newstate:quic_stream_state)):(Stack unit ((requires ((fun _ -> true)))) ((ensures ((fun _ _ _ -> true)))))):.()<-(strmm, 0, {.()(strmm, 0) with state=newstate})

Update the 'state' field

let ((landc_get_mutable (cs:pointer connection)):(Stack (lossAndCongestion_mutable) ((requires ((fun _ -> true)))) ((ensures ((fun _ _ _ -> true)))))):let  cs' = !*(cs) in .()(cs'.landc_state, 0)

Get a readonly view of the mutable LossAndCongestion state

let ((conn_get_mutable (cs:pointer connection)):(Stack (connection_mutable) ((requires ((fun _ -> true)))) ((ensures ((fun _ _ _ -> true)))))):let  cs' = !*(cs) in .()(cs'.csm_state, 0)

Get a readonly view of the mutable connection state