Version: 4.2.1

2.3 Certification for Same-Phase Code Generators

Synopsis: Same-phase code generators that produce references to private variables must manually certify the references.

Related patterns:

Here is a variation of the Code Generators example program. It is like the example of same-phase code generators from that section, except that instead of providing all of the structure procedures, the 'promises module only provides the make-promise procedure.

  (module promises scheme/base
    (require (for-syntax scheme/base))
    (provide make-promise
             (for-syntax gen-update-thunk-code))
  
    (define-struct promise (thunk))
  
    (begin-for-syntax
      ; gen-update-thunk-code : identifier stx -> stx
      (define (gen-update-thunk-code p-var expr)
        #`(lambda ()
            (let ([value #,expr])
              (set-promise-thunk! #,p (lambda () value))
              value)))))
  
  (module delay scheme/base
    (require 'promises
             (for-syntax scheme/base))
    (provide delay)
  
    (define-syntax (delay stx)
      (syntax-case stx ()
        [(delay e)
         #`(letrec ([p (make-promise
                        #,(gen-update-thunk-code #'p #'e))])
             p)])))

This program does not work; it raises an uncertified access error.

The code generator gen-update-thunk-code produces syntax containing references to private members of its enclosing module. The syntax is consumed by a macro in a different module, so the macro’s automatic certifier does not grant access to those references; they must be certifed manually by the code generator.

Here is a revised program that creates a certifier for the enclosing module using syntax-local-certifier and applies it to the generated code.

  (module promises scheme/base
    (require (for-syntax scheme/base))
    (provide make-promise
             (for-syntax gen-update-thunk-code))
  
    (define-struct promise (thunk))
  
    (begin-for-syntax
      (define certify (syntax-local-certifier))
  
      ; gen-update-thunk-code : identifier stx -> stx
      (define (gen-update-thunk-code p-var expr)
        (certify
         #`(lambda ()
             (let ([value #,expr])
               (set-promise-thunk! #,p (lambda () value))
               value))))))

Note: It would not work to call syntax-local-certifier within the execution of gen-update-thunk-code; the certifier returned then would be a certifier for the 'delay module, since that is the module containing the macro currently executing.

This version of the program works. But it certifies too much, if the intention is to protect the promise struct procedures from being used in unforseen ways. If the expression passed to gen-update-thunk-code contained an illegal access to one of the private struct procedures, the certifier would bless it and the access would be allowed. But the certifier only intends to certify the application of set-promise-thunk!.

One way to tailor the certification to avoid certifying illegal accesses in the subexpression is to use marks to distinguish the embedded expression from the code surrounding it. By associating the certificate with a mark that only covers the surrounding code, the code generator can ensure that the access to set-promise-thunk! is allowed but illegal accesses in the subexpression are not allowed.

VERIFY

  (module promises scheme/base
    (require (for-syntax scheme/base))
    (provide make-promise
             (for-syntax gen-update-thunk-code))
  
    (define-struct promise (thunk))
  
    (begin-for-syntax
      (define the-certifier (syntax-local-certifier))
  
      ; gen-update-thunk-code : identifier stx -> stx
      (define (gen-update-thunk-code p-var expr)
        (let* ([mark (make-syntax-introducer)]
               [m-expr (mark expr)]
               [m-p (mark p)])
          (certify
           (mark
            #`(lambda ()
                (let ([value #,m-expr])
                  (set-promise-thunk! #,m-p (lambda () value))
                  value)))
           #f
           mark)))))