jolt: Skill for Claude Code

This skill handles all the boilerplate: creating the invariant struct + input type, implementing the Invariant trait, registering it in the JoltInvariants enum, creating a fuzz target (if applicable), and running sync_targets.sh.

<Execution_Policy>

• The user must provide an invariant name (lowercase with underscores, e.g. sumcheck_binding).
• Ask the user what property is being checked and what the input type should look like before writing code.
• Follow existing patterns exactly — study the split_eq_bind and soundness invariants as models.
• Always run clippy and the auto-generated tests before reporting success. </Execution_Policy>

Phase 1: Gather Requirements

1. Validate the argument {{ARGUMENTS}}: must be a valid Rust identifier (lowercase alphanumeric + underscores). Reject otherwise.
2. Ask the user:
   • What property does this invariant check? (becomes the description())
   • What does the input look like? (fields, types, ranges)
   • What synthesis targets should it support? (Test, Fuzz, RedTeam)
   • Does it need non-trivial setup? (e.g. preprocessing, compilation — default to Setup = ())

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-prover-legacy functionality, explore the relevant jolt-prover-legacy 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
    }
}