IndisputableMonolith.Verification.RecognitionStabilityAudit.RL.Attr

   1import Mathlib.Init
   2
   3/-!
   4# RSA RL attributes (whitelists)
   5
   6This file defines:
   7
   8- `@[rsa_simp]`: whitelist for the `rsa_simp` tactic (allowed rewrite/unfold lemmas).
   9- `@[rsa_milestone]`: whitelist for the `rsa_step` tactic (allowed apply targets).
  10
  11We keep this separate from the tactics/goal suites to avoid initialization-order issues:
  12modules can safely *use* these attributes after importing this file.
  13-/
  14
  15public meta section
  16
  17namespace IndisputableMonolith
  18namespace Verification
  19namespace RecognitionStabilityAudit
  20
  21open Lean Meta
  22
  23/-! ## Environment extensions -/
  24
  25initialize rsaSimpLemmaExt : SimpleScopedEnvExtension Name (Array Name) ←
  26  registerSimpleScopedEnvExtension {
  27    initial := #[]
  28    addEntry := fun s n => s.push n
  29  }
  30
  31initialize rsaMilestoneExt : SimpleScopedEnvExtension Name (Array Name) ←
  32  registerSimpleScopedEnvExtension {
  33    initial := #[]
  34    addEntry := fun s n => s.push n
  35  }
  36
  37/-! ## Attributes -/
  38
  39/-- Attribute: whitelist a lemma/definition for `rsa_simp` (RSA RL simplifier). -/
  40syntax (name := rsaSimpAttr) "rsa_simp" : attr
  41
  42/-- Attribute: mark a lemma as an RSA RL milestone (allowed for `rsa_step`). -/
  43syntax (name := rsaMilestoneAttr) "rsa_milestone" : attr
  44
  45@[inherit_doc rsaSimpAttr]
  46initialize registerBuiltinAttribute {
  47  name := `rsaSimpAttr
  48  descr := "Whitelist a lemma/definition for `rsa_simp` (RSA RL simplifier)."
  49  add := fun declName _stx _kind =>
  50    MetaM.run' do
  51      rsaSimpLemmaExt.add declName
  52}
  53
  54@[inherit_doc rsaMilestoneAttr]
  55initialize registerBuiltinAttribute {
  56  name := `rsaMilestoneAttr
  57  descr := "Mark a lemma as an RSA RL milestone (allowed for `rsa_step`)."
  58  add := fun declName _stx _kind =>
  59    MetaM.run' do
  60      rsaMilestoneExt.add declName
  61}
  62
  63end RecognitionStabilityAudit
  64end Verification
  65end IndisputableMonolith
  66
  67end
  68