Wire.ParamSourceFormal parameters for codecs.
A parameter lets a codec depend on a value that is not in the buffer. An input parameter is supplied by the caller before decoding -- use it in constraints or size expressions. An output parameter is written by an action during decoding -- read it back afterwards to extract a computed result.
Both kinds carry a wire type (uint8 ... uint64, bool, enum) so the same definition can be projected to EverParse 3D.
let max_len = Param.input "max_len" uint16be
let out_len = Param.output "out_len" uint16be
let f_length = Field.v "Length" uint16be
let f_data =
Field.v "Data"
~action:
(Action.on_success [ Action.assign out_len (Field.ref f_length) ])
(byte_slice ~size:(Field.ref f_length))
let codec =
let open Codec in
v "Bounded"
~where:Expr.(Field.ref f_length <= Param.expr max_len)
(fun len data -> { len; data })
[ (f_length $ fun r -> r.len); (f_data $ fun r -> r.data) ]
let env = Codec.env codec |> Param.bind max_len 1024
let _ = Codec.decode_with codec env buf 0
let len = Param.get env out_lenDo not share an env across concurrent decodes.
Phantom kind for input parameters.
Phantom kind for output parameters.
Typed handle for one formal parameter.
bind p v env returns an environment with input p set to v.