What gets generated

fn main(
    context_root: pub Field, params_commitment: pub Field, state_in: pub Field,
    state_out: pub Field, attestation_out: pub Field,
    w: GeneratedWitness,          // params + salt, opened regions, state leaves, rule witness
) {
    let p = Params::from_limbs(w.params);
    assert(commit_params(p) == params_commitment, "weld/params-weld");
    let ctx = Ctx::<Accept>::open(context_root, w.regions);     // weld/context-root, weld/schema-min
    let s = State::<Ledger>::open(state_in, w.state);           // weld/state-in (0 = empty)
    let (s2, v, att) = <Velocity as StatefulRule<_, _>>::on_accept(p, ctx, s);
    v.assert_all();                                              // one assert per (cond, id)
    assert(s2.root() == state_out, "weld/state-out");
    assert(att.commit() == attestation_out, "weld/attestation-out");
}