Function encode_into 

pub fn encode_into(
    input: &[u8],
    output: &mut [u8],
) -> Result<usize, InvalidSize>

Constant-Time Hex Encoding

Arguments

• input - A slice of bytes to be hex-encoded.
• output - The buffer to write the hex string into.

Returns

The number of bytes written to the output buffer (which will always be twice the length of the input).

Errors

This function returns Err(InvalidSize) if the output buffer has a length less than input.len() * 2.

Security

This function is designed to operate in constant-time, avoiding data-dependent branches that could lead to timing side-channel attacks. The encoding process uses arithmetic and bitwise operations to guarantee uniform execution time regardless of the input values.

UTF-8 Considerations

Rust’s str::from_utf8 is discouraged in contexts that require constant-time execution due to the presence of data-dependent branches plus lookup tables in its implementation.

It is safe to use str::from_utf8_unchecked on the output of this function, however, it is only safe over the encoded region of the output buffer (up until the returned length). If you need a str representation, consider the less error-prone encode_str function.

If you are curious / skeptical of the safety in this recommendation, please read the verification section below.

Example

use wolf_crypto::{hex, ct_eq};

let mut output = [0u8; 22]; // 11 * 2
let len = hex::encode_into(b"hello world", &mut output).unwrap();

assert_eq!(len, 22);
assert!(
    // since we are using a constant-time encoding, we probably also want
    // to use a constant-time comparison.
    ct_eq(
        // SAFETY: The encoded output is formally guaranteed to be valid
        // UTF-8. This is just for example, ct_eq can of course compare slices.
        unsafe { core::str::from_utf8_unchecked(&output[..len]) },
        "68656c6c6f20776f726c64"
    )
);

// or use the `encode_str` function, which is simply a less error-prone variant of this
// if `str` representation is a requirement.

let mut output = [0u8; 22];
let str_repr = hex::encode_str(b"hello world", &mut output).unwrap();

// ...

Verification

The correctness and safety of the encode_into function have been rigorously verified using a combination of formal methods and property-based testing. This multi-faceted approach ensures a high degree of confidence in the function’s behavior and its adherence to the specified properties.

Formal Verification

We employed formal verification techniques using the Kani Rust Verifier to prove key properties of the encode_into function and its components.

Inductive Proof Strategy

The verification process follows an inductive proof strategy:

1. Base Case: We prove that encoding a single byte always produces valid UTF-8.
2. Inductive Step: We prove that if encoding n bytes produces valid UTF-8, then encoding n+1 bytes also produces valid UTF-8.

This approach allows us to reason about the correctness of encode_into for inputs of arbitrary length without needing to verify all possible inputs exhaustively.

Key Proofs

1. Single Byte Encoding: The encode_byte_is_always_utf8 proof verifies that for any input byte, the output of encode_byte is always valid hexadecimal (and thus valid UTF-8).

2. Inductive Step:

   • The verify_encode_n_plus_1_bytes_symbolic proof demonstrates that if encoding n bytes produces valid UTF-8, encoding an additional byte preserves this property.
   • The verify_hex_encode_inductive_step_symbolic proof applies this principle to the encode_into function itself, verifying that the UTF-8 validity is maintained for arbitrary input lengths.