arc-deref-pattern

Anti-Pattern: "Closures Can't Capture Data with Specs"

The Wrong Assumption

When implementing parallel (Mt) algorithms in Verus, do NOT assume:

• "Closures can't capture ArraySeqMtEphS<T> with specs"
• "Arc prevents verification because Verus can't deref it"
• "Send + 'static closures can't reference ghost variables like spec_f"
• "The only way to verify this is to make it sequential"

These are FALSE. The pattern below solves all of them.

The Pattern: Factor Verification Away from Concurrency

Problem

join closures need Send + 'static. The verified algorithm needs f: &F (for direct Fn trait spec access). Arc<F> is opaque to Verus — you can't deref it with spec guarantees.

Solution

1. Factor the verified algorithm into a helper that takes f: &F:

   fn reduce_contract_verified<T, F>(a: &ArraySeqMtEphS<T>, f: &F, ...) -> (result: T)
       requires f.requires(...), ...
       ensures result == ...
       decreases a.spec_len(),
   { /* Full proof here — identical to StEph version */ }
   

2. The trait impl delegates through Arc deref:

   fn reduce_contract_parallel(a, f: Arc<F>, ...) -> (result: T) {
       reduce_contract_verified(a, &*f, Ghost(spec_f), id)
   }
   

3. Small external_body helpers for Arc-specific operations:

   #[verifier::external_body]
   pub fn call_f<T, F>(f: &Arc<F>, a: &T, b: &T) -> (result: T)
       requires f.requires((a, b)),
       ensures f.ensures((a, b), result),
   { (**f)(a, b) }
   

4. Parallel primitives as external_body with strong specs:

   #[verifier::external_body]
   pub fn contract_parallel<T, F>(a, f: &Arc<F>, Ghost(spec_f), half) -> (b: ArraySeqMtEphS<T>)
       ensures b.spec_index(j) == spec_f(a.spec_index(2*j), a.spec_index(2*j+1)),
   { /* Uses join internally */ }
   

Trust Boundaries

Helper	Trust	Obviousness
call_f	Arc deref preserves function	Trivially correct
contract_parallel	Parallel loop computes pairs	Auditable in 10 lines