Set a boundary between trusted and verified for RabbitMQ controller

[marshtompsxd]

After this PR our rabbitmq controller example consists of four folders:

• trusted: all the trusted code, including the top-level theorems and unverified wrapper object (like vstd::Vec).
• exec: the executable code that is verified.
• model: the ghost version of the executable code. This is not trusted.
• proof: the proof for liveness (and safety).

Notably, files in trusted only import other files from trusted or Anvil's trusted specs---they don't import anything from exec, model, or proof. Everything outside trusted is verified---they don't have any external or external_body proof functions.

After this refactoring, the liveness theorem inside trusted now takes a Maker trait as a placeholder for the sub-resource objects created by the controller implementation:

pub open spec fn liveness<M: Maker>(rabbitmq: RabbitmqClusterView) -> TempPred<RMQCluster> {
    always(lift_state(desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::<M>(rabbitmq))))
}

...

pub open spec fn current_state_matches<M: Maker>(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
    |s: RMQCluster| {
        forall |sub_resource: SubResource|
            #[trigger] resource_state_matches::<M>(sub_resource, rabbitmq, s.resources())
    }
}

pub open spec fn resource_state_matches<M: Maker>(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, resources: StoredState) -> bool {
    match sub_resource {
        SubResource::HeadlessService => {
            ...
            &&& obj.metadata.labels == M::make_headless_service(rabbitmq).metadata.labels
            &&& obj.metadata.annotations == M::make_headless_service(rabbitmq).metadata.annotations
        },
        ...
    }
}

And our liveness proof inside proof instantiates this theorem with the concrete maker RabbitmqMaker and proves it:

proof fn liveness_proof_forall_rabbitmq()
    ensures
        liveness_theorem::<RabbitmqMaker>(),
{ ... }

Maker trait is defined inside trusted and RabbitmqMaker (which implements Maker) is not in trusted.

[marshtompsxd]

Hi @jonhnet I implemented the placeholder thing we discussed in today's meeting. Could you please read the description of this PR and let me know whether it makes sense? No need to go through all the changes as it might be overwhelming and my description summarizes all the changes.

[marshtompsxd]

One more question I have is about the entry point of the controller program (where main function is defined). The entry point is not verified (which makes it trusted) but it has to import the verified reconciliation implementation---it seems to me this import is inevitable.

[jonhnet]

Yep, this looks sensible. I'd suggest calling spec directory model, since spec is a hopelessly overloaded term in our community. I'd also suggest, in your description above, noting that:
model is all counted as proof (untrusted burden)
proof is all counted as proof
exec is counted as part-implementation (stuff that survives to the compiler) and part-proof (everything else, which was untrusted proof burden)