More Vest DSL Features

[y1ca1]

More Vest DSL Features

This PR introduces three major extensions to the Vest DSL that enhance its expressiveness for specifying complex binary formats. These features were motivated by the need to precisely specify IKEv2 (RFC 5996), where payload lengths are context sensitive and fields depend on previously-parsed nested structures.

New Features

1. Length Expressions: |fmt|

A new syntax to reference the wire length of any format with a fixed (compile-time known) size.

Syntax: |T| evaluates to the wire length of format T as a compile-time constant.

Examples:

// Primitive sizes
|u8|   = 1
|u16|  = 2
|u32|  = 4

// Named format sizes
header = {
    @len: u16 | { 3..0xffff },
    flags: u8,
}
named_size = {
    bytes: [u8; |header|],  // |header| = 3 bytes
}

Future extension: The syntax |@hdr| would enable referring to the runtime-dependent parsed/serialized length of a field (obtained from the backend combinator API). This is not yet implemented but the design allows for it.

---

2. Arithmetic in Length Expressions

Length positions now support full arithmetic expressions with +, -, *, /, and parentheses.

Examples:

// Multi-variable subtraction
multi_arith(@total: u32 | { 263..0xffffffff }, @hdr_len: u8 | { 0..255 }) = {
    body: [u8; @total - @hdr_len - 8],
}

// Multiplication
multiply(@count: u16, @size: u8 | { 1 }) = {
    items: [u8; @count * @size],
}

// Division
divide(@total: u32) = {
    chunks: [u8; @total / 4],
}

// Parenthesized expressions
paren_expr(@a: u16 | { 255..0xffff }, @b: u8 | { 0..255 }, @c: u8 | { 1 }) = {
    data: [u8; (@a - @b) * @c],
}

// Mixed constants and sizes
payload_with_header(@hdr: header) = {
    data: [u8; @hdr.len - |header|],
}

IKEv2 use case: The payload_length field includes the 4-byte generic header, so body length = @payload_length - |generic_payload_header|:

generic_payload_header = {
    next_payload:      next_payload_type,
    critical_reserved: payload_critical,
    @payload_length:   u16 | {4..0xffff},
}

nonce_payload_body(@payload_length: u16 | {20..260}) = {
    nonce_data: [u8; @payload_length - |generic_payload_header|],
}

Note: Vest simply translates the arithmetic expression to Verus expressions and Verus guarantees the arithmetic safety. Though, to make Verus happy, it's still user's responsibility to properly bound the integers (e.g., using refinements) before doing any arithmetics.

---

3. Nested Field Access: @hdr.field

When a dependent field is itself a struct, you can access its sub-fields using dot notation.

Examples:

generic_header = {
    next_type: u8,
    reserved: u8,
    @payload_length: u16 | { 8..0xffff },
}

// Single level of nesting
payload_with_header = {
    @hdr: generic_header,
    body: [u8; @hdr.payload_length - 4],
}

// Two levels of nesting
outer_header = {
    magic: u32,
    @inner: generic_header,
}

deep_nested = {
    @outer: outer_header,
    data: [u8; @outer.inner.payload_length - 8],
}

// Combined with parameters and arithmetic
combined_example(@total_len: u32 | { 65535..0xffffffff }) = {
    @header: generic_header,
    body: [u8; @total_len - @header.payload_length],
}

IKEv2 use case: The IKE message header contains the total length:

ike_header = {
    initiator_spi: [u8; 8],
    responder_spi: [u8; 8],
    next_payload:  next_payload_type,
    version:       ike_version_byte,
    exchange_type: exchange_type,
    flags:         ike_flags,
    message_id:    u32,
    @length:       u32 | {28..0xffffffff},
}

ike_message = {
    @header:  ike_header,
    payloads: [u8; @header.length - |ike_header|],
}

---

4. Nested Anonymous Struct/Choose Formats

Anonymous struct and choose formats can now be deeply nested while correctly capturing dependent fields from outer scopes.

Examples:

// Capturing outer dependent field in nested anonymous struct
capture_outer_and_local = {
    @frame_len: u8 | { 1.. },
    payload: [u8; @frame_len] >>= {
        @tag: u8,
        body: choose(@tag) {
            0 => [u8; @frame_len - |u8|],  // uses outer @frame_len
            _ => {
                @count: u8,
                items: [u8; @count],       // uses local @count
            },
        },
    },
}

// Nested choose with captured parameters
nested_inner_choice(@choice1: a_or_b, @choice2: c_or_d) = {
    x: choose(@choice1) {
        A => choose(@choice2) {
            C => u8,
            D => u16,
        },
        B => u32,
    },
}

// Anonymous struct inside choose branches
capture_param_and_local(@choice1: a_or_b, @choice2: c_or_d) = {
    x: choose(@choice1) {
        A => {
            @len: u8,
            payload: choose(@choice2) {
                C => [u8; @len],
                D => [u8; @len],
            },
        },
        B => {
            @tag: u8,
            y: choose(@tag) {
                0 => u8,
                _ => u16,
            },
        },
    },
}

---

test/src/ikev2.vest is an LLM-authored Vest specification for IKEv2. It's primarily used to motivate the new DSL features and is currently incomplete and hasn't been tested for compliance.