Rule sets and certificates for polynomial-time programs

polytime searches the Aesop rule set PolyTime. A certificate for a named program is registered with @[program_certificate]. Certificates are indexed by their efficiency predicate and by the constant at the head of the program, looking through an output encoding. A goal's certificates are looked up using its own program head, so similarly implemented algorithms do not unfold into each other's rules. Certificates are also registered with fun_prop, reusing any existing global registration, so the same annotation supports calls inside larger functional programs without duplicating search rules. Parameterized IsPPT certificates are uncurried to the definitionally equal IsPPTOn statement before registration, keeping both tactic interfaces on the same encoded-input contract.

The certificate index is adapted from the cslib crypto branch. Both computation predicates use separate input and output encodings. Tactic.PPT combines the PPT and PolyTime rule sets for closed probabilistic programs; machine witnesses remain behind their certificates.

Main definitions

• program_certificate: register a named efficiency theorem before its implementation unfolds.

Aesop's index cannot see inside the program, which is a function, so the lookup is a single tactic rule for each efficiency predicate rather than one apply rule for each certificate.

References

Adapted from Cslib/Tactic/PolyTime/Init.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, sharing routine-call matching between both tactics.

def Cslib.Tactic.programHead? (body : Lean.Expr) : Option (Lean.Name × Bool)

The constant naming a program body, and whether it was found under an output encoding. An application of an encoding is looked through, and so is List.replicate n true, the simp-normal form of a unary encoding.

def Cslib.Tactic.efficiencyKey (statement : Lean.Expr) : Lean.MetaM (Lean.Name × Lean.Name × Bool)

The efficiency predicate and program head of an efficiency statement, and whether the program returns its result under an encoding. IsPPT statements are indexed under IsPPTOn, which they unfold to. A certificate stated under an encoding only applies to goals stated the same way.

opaque Cslib.Tactic.certificateExt : Lean.SimpleScopedEnvExtension ((Lean.Name × Lean.Name × Bool) × Lean.Name × Array Lean.Name) (Std.HashMap (Lean.Name × Lean.Name × Bool) (Array (Lean.Name × Array Lean.Name)))

Registered certificates, indexed by efficiency predicate and program head. Each certificate carries the hypotheses to solve as soon as it is applied.

def Cslib.Tactic.programCertificate : Lean.ParserDescr

@[program_certificate] registers an efficiency certificate for polytime and ppt. Its conclusion must be a ComputableInPolyTime, ComputableTidilyInPolyTime, IsPPTOn or IsPPT statement, or one of the word-RAM predicates WordRAM.Refines, WordRAM.ComputableInPolyTime, WordRAM.UniformComputableInPolyTime used by Tactic.WordRAM. The indexed argument must apply a constant, possibly under an output encoding. Other predicates are rejected rather than indexed by an unrelated final argument. Certificates are also registered with fun_prop for use in larger compositions, unless the same declaration already has a global registration.

@[program_certificate h₁ … hₙ] additionally solves the hypotheses h₁ … hₙ immediately after the certificate is applied. This is needed when such a hypothesis determines an encoding that other hypotheses mention, so that proof search does not reach those goals with the encoding unknown.

def Cslib.Tactic.solveTagged (name : Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Solve the goal tagged name, or else one whose tag ends in name as for case, by proof search: PPT and PolyTime rules for a PPT goal, and PolyTime rules otherwise.

def Cslib.Tactic.applyCertificates (predicate : Lean.Name) : Aesop.RuleTac

Expose every matching named certificate as an Aesop alternative. Eager premises are solved before exposing the remaining obligations, while different certificates keep independent metavariable assignments until the surrounding proof search has also succeeded.

def Cslib.Tactic.applyKnownCall (predicate : Lean.Name) (programIndex : ℕ) (rule argumentName certificateName : Lean.Name) : Aesop.RuleTac

Apply local routine certificates through a composition rule, exposing tuple arguments. Predicate parameters select the program; rule parameter names select the argument and certificate. Each candidate retains separate assignments and leaves argument preparation to the surrounding proof search, so other obligations can constrain its encoding.