We want to add functional postconditions to some CBMC contracts, but CBMC assumes a callee's postcondition at every call site that replaces the call with its contract. Expensive functional clauses then burden callers that don't need them: in #1287, a quantified postcondition on mld_sig_unpack_hints blew up the sign_verify_internal proof.
We'd like a way to attach a postcondition that is (1) verified in the function's own proof, (2) not assumed by callers, and (3) enforced, so a spec can't be declared but never proven.
Tried in #1287: a functional() macro that keeps the clause only in the function's own proof and removes it elsewhere. We rejected this because nothing guarantees the clause is proven anywhere. The merged interim is a cassert in the function body (verified, not assumed, but lives outside the contract).
Is there a clean way to get this from CBMC?
We want to add functional postconditions to some CBMC contracts, but CBMC assumes a callee's postcondition at every call site that replaces the call with its contract. Expensive functional clauses then burden callers that don't need them: in #1287, a quantified postcondition on
mld_sig_unpack_hintsblew up thesign_verify_internalproof.We'd like a way to attach a postcondition that is (1) verified in the function's own proof, (2) not assumed by callers, and (3) enforced, so a spec can't be declared but never proven.
Tried in #1287: a
functional()macro that keeps the clause only in the function's own proof and removes it elsewhere. We rejected this because nothing guarantees the clause is proven anywhere. The merged interim is acassertin the function body (verified, not assumed, but lives outside the contract).Is there a clean way to get this from CBMC?