Skip to main content

Module proof

Module proof 

Source
Expand description

Correctness and security proof traits for Vest combinators.

Traits§

EquivSerializers
DPS ↔ non-DPS serializer equivalence on the empty buffer.
EquivSerializersGeneral
Full DPS ↔ non-DPS serializer equivalence for any output buffer.
Leaf
This is a marker trait for combinators that are “leaves” in the combinator hierarchy.
LeafNonMalleable
Similar to Leaf, but also includes the parser soundness and non-malleability properties.
NoLookAhead
No-lookahead property for parsers.
NonAmbiguous
Serializer unambiguity (injectivity on consistent values).
NonMalleable
Parser non-malleability.
PSRoundTrip
Parse-serialize roundtrip.
Productive
Productivity for parsers.
SPRoundTrip
Serialize-parse roundtrip.
SPRoundTripDps
Serialize-parse roundtrip (DPS).
StrictCombinator
A “strict” combinator that satisfies all the core correctness and security properties proven by the library’s combinators.