IndisputableMonolith.Certificates.Consent

   1import Mathlib
   2import IndisputableMonolith.LNAL.Compiler
   3
   4namespace IndisputableMonolith
   5namespace Certificates
   6
   7open IndisputableMonolith
   8open IndisputableMonolith.LNAL
   9
  10/-- ConsentDerivative audit certificate summarising static gate status. -/
  11structure ConsentCert where
  12  enabled    : Bool
  13  ok         : Bool
  14  violations : List Nat := []
  15  messages   : List String := []
  16deriving Repr
  17
  18@[simp] def ConsentCert.verified (c : ConsentCert) : Prop := c.ok = true
  19
  20def ConsentCert.fromReport (report : CompileReport) : ConsentCert :=
  21  { enabled := report.consent.enabled,
  22    ok := report.consent.ok,
  23    violations := report.consent.violations,
  24    messages :=
  25      if report.consent.enabled then
  26        if report.consent.ok then []
  27        else ["ConsentDerivative gate violated"]
  28      else if report.consent.violations.isEmpty then []
  29      else ["ConsentDerivative gate disabled; potential violations detected"] }
  30
  31noncomputable def ConsentCert.fromSource (src : String) (enableGate : Bool := false) : ConsentCert :=
  32  let (report, _) := compile src enableGate
  33  fromReport report
  34
  35end Certificates
  36end IndisputableMonolith
  37