Reusing RAM controller certificates

Named Refines, ComputableInPolyTime and UniformComputableInPolyTime proofs can be registered with program_certificate. The stateful and polytime tactics respectively retrieve them through the existing certificate index. Predicate and program heads are separate keys: a RAM certificate cannot discharge a Turing-machine polynomial-time goal. Local certificates remain ordinary hypotheses.

Use Refines.bind, branch, prepend, and call explicitly to choose intermediate assertions, representations and charged preparation code; automation then reuses the named subroutine proofs. No rule evaluates arbitrary host-language continuations for free or guesses an implementation.

Main definitions

• ramControllerCertificate: named fixed-code refinement proofs for stateful.
• ramFunctionCertificate: named polynomial RAM-time proofs for polytime.
• ramUniformFunctionCertificate: named uniform polynomial RAM-time proofs for polytime.

def Cslib.Tactic.ramControllerCertificate : Aesop.RuleTac

Close a named controller certificate from local hypotheses before case splitting changes its budget. Only complete proofs commit here; certificates with remaining obligations are alternatives in ramControllerAlternative.

def Cslib.Tactic.ramControllerAlternative : Aesop.RuleTac

Keep incomplete named controller proofs as alternatives with explicit proof obligations.

def Cslib.Tactic.ramFunctionCertificate : Aesop.RuleTac

Reuse a named function certificate with the RAM predicate, without changing machine models.

def Cslib.Tactic.ramUniformFunctionCertificate : Aesop.RuleTac

Reuse a named uniform function certificate under its own predicate key.