proof/wrapper.ss
#lang scheme/base

(require (for-template "event.ss"))

(provide dracula-expr dracula-event dracula-keyword dracula-special-event)

(define (wrap-certificates stx)
  (syntax-property stx 'certify-mode 'transparent))

(define ((dracula-wrapper id) stx)
  (wrap-certificates
   (quasisyntax/loc stx (#,id #,stx))))

(define dracula-expr (dracula-wrapper #'#%dracula-expr))
(define dracula-event (dracula-wrapper #'#%dracula-event))
(define dracula-keyword (dracula-wrapper #'#%dracula-keyword))
(define (dracula-special-event logical executable)
  (wrap-certificates
   (quasisyntax/loc executable
     (#%dracula-special-event #,logical #,executable))))