New Invariant

Phase 2: Explore Context

1. Read jolt-eval/src/invariant/mod.rs to understand the current JoltInvariants enum and dispatch! macro.
2. Read an existing invariant for reference:
   • Simple: jolt-eval/src/invariant/split_eq_bind.rs
   • Complex (with setup, enrich_input): jolt-eval/src/invariant/soundness.rs
3. If the invariant tests jolt-core functionality, explore the relevant jolt-core modules to understand the types and APIs involved.

Phase 3: Implement

Create the invariant file at jolt-eval/src/invariant/<invariant_name>.rs with:

Input Type

#[derive(Debug, Clone, serde::Serialize, serde::Deserialize, schemars::JsonSchema)]
pub struct <Name>Input {
    // fields
}

impl<'a> Arbitrary<'a> for <Name>Input {
    fn arbitrary(u: &mut Unstructured<'a>) -> arbitrary::Result<Self> {
        // Generate random inputs with reasonable bounds
    }
}

Key requirements for the input type:

• Must derive Debug, Clone, Serialize, Deserialize, JsonSchema
• Must implement Arbitrary manually (for fuzzing)
• Use bounded ranges in Arbitrary impl (e.g. u.int_in_range(2..=16)?) to keep inputs meaningful

Invariant Struct

#[jolt_eval_macros::invariant(Test, Fuzz, RedTeam)]  // adjust targets as needed
#[derive(Default)]
pub struct <Name>Invariant;

impl Invariant for <Name>Invariant {
    type Setup = ();  // or a custom setup type
    type Input = <Name>Input;

    fn name(&self) -> &str { "<invariant_name>" }
    fn description(&self) -> String { "...".into() }
    fn setup(&self) -> Self::Setup { /* ... */ }
    fn check(&self, setup: &Self::Setup, input: Self::Input) -> Result<(), CheckError> {
        // 1. Validate input — return Err(CheckError::InvalidInput(...)) for degenerate cases
        // 2. Run the property check
        // 3. Return Ok(()) if the invariant holds
        // 4. Return Err(CheckError::Violation(...)) if violated
    }
    fn seed_corpus(&self) -> Vec<Self::Input> {
        // Include: minimal case, typical case, edge case (large values, boundary conditions)
    }
}

Guidelines for check()

• Use CheckError::InvalidInput for degenerate inputs that should be skipped (not counted as violations)
• Use CheckError::Violation(InvariantViolation::with_details(...)) for actual violations — include diagnostic info
• Compare against a known-correct reference implementation when testing optimized code

Phase 4: Register

Edit jolt-eval/src/invariant/mod.rs:

1. Add pub mod <invariant_name>; to the module declarations at the top.
2. Add a variant to JoltInvariants:

   <VariantName>(<invariant_name>::<Name>Invariant),
   

3. Add the variant to JoltInvariants::all():

   Self::<VariantName>(<invariant_name>::<Name>Invariant),
   

   Use <Name>Invariant::default() if the struct has fields.
4. Add the variant to the dispatch! macro:

   JoltInvariants::<VariantName>($inv) => $body,
   

Phase 5: Create Fuzz Target (if targets include Fuzz)

Create jolt-eval/fuzz/fuzz_targets/<invariant_name>.rs:

#![no_main]
use jolt_eval::invariant::<invariant_name>::<Name>Invariant;
jolt_eval::fuzz_invariant!(<Name>Invariant::default());

Then run ./jolt-eval/sync_targets.sh to update fuzz/Cargo.toml.

Phase 6: Validate

Run these commands (all must pass):

# Format
cargo fmt -q

# Lint
cargo clippy -p jolt-eval -q --all-targets -- -D warnings

# Run auto-generated tests (seed_corpus + random_inputs)
cargo nextest run -p jolt-eval --cargo-quiet invariant::<invariant_name>

# If fuzz target was created, verify it compiles
cd jolt-eval/fuzz && cargo check 2>&1 | head -20

If any step fails, fix the issue and re-run.

Task: Implement a new invariant for jolt-eval. {{ARGUMENTS}}