Macros work badly with [trigger | type check]

[Catoverflow]

I'm trying to use macro to express a predicate that accepts a flexible number of arguments. It worked but broke the types and triggers.

// eq_step is the tricky workaround for error, see src/v2/controllers/vdeployment_controller/trusted/step.rs
#[macro_export]
macro_rules! at_step_internal {
    ($vds:expr, ($step:expr, $pred:expr)) => {
        $vds.reconcile_step.eq_step($step) && $pred($vds)
    };

    ($vds:expr, $step:expr) => {
        $vds.reconcile_step.eq_step($step)
    };

    ($vds:expr, $head:tt, $($tail:tt)+) => {
        at_step_internal!($vds, $head) || at_step_internal!($vds, $($tail)+)
    };
}

// usage: at_step!(step,*)
// step* = step | (step, pred)
#[macro_export]
macro_rules! at_step {
    ( $($tokens:tt)+ ) => {
        closure_to_fn_spec(|s: ReconcileLocalState| {
            let vds = VDeploymentReconcileState::unmarshal(s).unwrap();
            at_step_internal!(vds, $($tokens)+)
        })
    };
}

Code also available at anvil

I have encountered a few type check problems:

Closure and SpecFn

I have to call closure_to_fn_spec to make Verus aware that it can be a spec, the minimum reproduction code is

#[macro_export]
macro_rules! should_be_spec_fn {
    () => {
        |n| n == n
    };
}
pub open spec fn foo(n: nat) -> bool
{
    bar(should_be_spec_fn!(), n)
}
pub open spec fn bar(f: spec_fn(nat) -> bool, n: nat) -> bool
{
    f(n)
}

error[E0308]: mismatched types
  --> example.rs:16:9
   |
11 |         |n| n == n
   |         --- the found closure
...
16 |     bar(should_be_spec_fn!(), n)
   |     --- ^^^^^^^^^^^^^^^^^^^^ expected `FnSpec<(nat,), bool>`, found closure
   |     |
   |     arguments to this function are incorrect
   |
   = note: expected struct `builtin::FnSpec<(builtin::nat,), bool>`
             found closure `{closure@example.rs:11:9: 11:12}`
note: function defined here
  --> example.rs:18:18
   |
18 | pub open spec fn bar(f: spec_fn(nat) -> bool, n: nat) -> bool
   |                  ^^^ -----------------------

error: aborting due to 1 previous error

closure_to_fn_spec is not documented. I found this using -Zunpretty=expanded following Bryan's suggestions (thank you Bryan!). I think this conversion should also be automated.

Integer Type Conversion

This may apply to other types but I didn't test

This problem happens for macro and enum, I have to choose between E0308 and E0605:

If I use at_step!((AfterScaleDownOldVRS, |vds| vds.old_vrs_list.len() == 0) I got

error[E0308]: mismatched types
   --> src/v2/controllers/vdeployment_controller/proof/liveness/terminate.rs:262:77
    |
262 |         at_step!((AfterScaleDownOldVRS, |vds| vds.old_vrs_list.len() == 0)),
    |                                                                         -   ^ expected `nat`, found integer
    |                                                                         |
    |                                                                         expected because this is `builtin::nat`

If I use at_step!((AfterScaleDownOldVRS, |vds| vds.old_vrs_list.len() == 0 as nat) I got

error[E0605]: non-primitive cast: `{integer}` as `builtin::nat`
   --> src/v2/controllers/vdeployment_controller/proof/liveness/terminate.rs:262:77
    |
262 |         at_step!((AfterScaleDownOldVRS, |vds| vds.old_vrs_list.len() == 0 as nat),
    |                                                                             ^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

enum's version can be found here:

// we have to use zero instead of 0 as nat
let zero: nat = 0;
temp_pred_equality(
    lift_state(at_step_state_pred(controller_id, vrs, VReplicaSetRecStepView::AfterCreatePod(zero))),
    lift_state(Cluster::at_expected_reconcile_states(controller_id, vrs.object_ref(), at_step_closure(VReplicaSetRecStepView::AfterCreatePod(zero))))
);

The solution is hacky:

#[macro_export]
macro_rules! nat0 {
    () => {
        spec_literal_nat("0")
    };
}

#[macro_export]
macro_rules! nat1 {
    () => {
        spec_literal_nat("1")
    };
}

== in macro

You may noticed the strange way of using ==: $vds.reconcile_step.eq_step($step). If I use == I got

error: The verifier does not yet support the following Rust feature: ==/!= for non smt equality types: Datatype(Path(Path(Some("v2_vdeployment_controller"), ["vdeployment_controller" :: "trusted" :: "step" :: "VDeploymentReconcileStepView"])), [], []) and Datatype(Path(Path(Some("v2_vdeployment_controller"), ["vdeployment_controller" :: "trusted" :: "step" :: "VDeploymentReconcileStepView"])), [], [])
  --> src/v2/controllers/vdeployment_controller/proof/predicate.rs:22:9
   |
22 |         $vds.reconcile_step == $step
   |         ^^^^^^^^^^^^^^^^^^^
   |
  ::: src/v2/controllers/vdeployment_controller/proof/liveness/terminate.rs:27:5
   |
27 |     temp_at_step!(controller_id, vd, (AfterScaleDownOldVRS, old_vrs_list_len(n)), Error)
   |     ------------------------------------------------------------------------------------ in this macro invocation
   |
   = note: this error originates in the macro `at_step_internal` which comes from the expansion of the macro `temp_at_step` (in Nightly builds, run with -Z macro-backtrace for more info)

The actual type that trigger this error was not shown, so I hacked Verus to print the types on each side of ==. VDeploymentReconcileStepView is a ghost type and can be compared safely in spec, so my workaround is

impl VDeploymentReconcileStepView {
    pub open spec fn eq_step(self, other: VDeploymentReconcileStepView) -> bool {
        self == other
    }
}

Is it because of the type information is not fully available during macro substitution?

[Catoverflow]

Trigger

If I use #![trigger at_step!((AfterScaleDownOldVRS, old_vrs_list_len(n)), Error)] I got

error: triggers cannot contain let/forall/exists/lambda/choose
  --> src/v2/controllers/vdeployment_controller/proof/predicate.rs:34:28
   |
34 |           closure_to_fn_spec(|s: ReconcileLocalState| {
   |  ____________________________^
35 | |             let vds = VDeploymentReconcileState::unmarshal(s).unwrap();
36 | |             at_step_internal!(vds, $($tokens)+)
37 | |         })
   | |_________^
   |
  ::: src/v2/controllers/vdeployment_controller/proof/liveness/terminate.rs:93:47
   |
93 |               assert forall |n: nat| #![trigger at_step!((AfterScaleDownOldVRS, old_vrs_list_len(n)), Error)] n > 0 implies spec.entails(temp_at_step!(controller_id, vd, (AfterScaleDownOldVRS, old_vrs_list_len(n)), Error)
   |                                                 ------------------------------------------------------------ in this macro invocation
   |
   = note: this error originates in the macro `at_step` (in Nightly builds, run with -Z macro-backtrace for more info)

Verus is unhappy with let and closure here. But I think Verus should be able to see this macro is total? If I switch back to spec_fn the trigger works but I have to define many spec functions because they are not flexible in arguments.