[plt-dev] certificates, #%module-begin, and typed-scheme's soundness

At Thu, 17 Dec 2009 10:54:58 -0700, Matthew Flatt wrote:
> The example below is independent of Typed Scheme.
> 
> The problem is that a macro introduces `f' by itself. As soon as that
> macro returns, the identifier `f' is certified to stand alone.
> 
> The result seems wrong, particularly since the macro that expanded to
> `f' is not itself exported, but that's how the system is currently
> defined. In other words, you've run into a limitation of the design, as
> opposed to merely a bug in the implementation.
> 
> I think the certification of `f' should instead depend on staying in
> the context where `p-ex' was certified. (To be continued.)

Too complicated. Even if it works, I couldn't figure out how to
implement it efficiently, and I found a less complicated solution.

There's a similar issue with inactive certificates; see section
16.2.5.1 in the Guide (in http://docs.plt-scheme.org/guide/stx-certs.html).
The problem with inactive certificates is solved by lifting them to the
surrounding context where they're activated. A similar lifting of
active certificates solves the problem in our examples.

Finding the right time to lift turns out to be tricky. Lifting on every
transformer result isn't right, because a lifted certificate might then
apply to a binding where it didn't before, which would defeat the check
to ensure that references are no more certified than their bindings.
(See 16.2.5 on why that check is needed.) Lifting at the point where
`expand' or `local-expand' returns is closer to the right idea, in part
because it directly addresses the use of `expand' or `local-expand' to
cheat. But that's still not quite right when `local-expand' is used for
partial expansion.

So, active certificates are now lifted for the result of `expand' or
`local-expand', but in the latter case only when the stop list is empty
(i.e., when `local-expand' is used for full expansion, instead of
partial expansion).

The `local-expand' rule send us down another little detour. The
exception for a non-empty stop lists makes sense only when the stop
list includes the primitive expression forms. We've long been
suspicious of using `local-expand' with incomplete stop lists, anyway,
because expansion can go wrong if the stop points are not consistent.
Now that "go wrong" includes gaining access to identifiers that
shouldn't be directly accessible, we need to rule it out. So,
`local-expand' now automatically adds missing core-form identifiers to
a non-empty stop list. (Raising an exception would break a lot of code.
Automatically adding identifiers broke only one use of `local-expand'
that I could find, and in that case the stop list really should have
been empty. In a future clean-up of the macro toolbox, `local-expand'
should be split into two different functions.)

I'm skipping some fine points of lifting certificates related to the
'certify-mode property and bindings like `begin'. See the docs for
details.

These changes close that Typed Scheme hole that Sam described in his
original message, as far as I can tell. We can look more closely at the
short example:

 #lang scheme/load

 (module m scheme
   (define (f x) x)
   (define-syntax (p-ex stx)
     #'f)
   (define-syntax (ex stx)
     #'((p-ex) 10))
   (provide ex))

 (module n scheme
   (require 'm)
   (define-syntax (cheater stx)
     (define v (local-expand #'(ex) 
                             'expression 
                             null))
     (syntax-case v ()
       [(app f v)  #'f]))
   ((cheater) 3))

 (require 'n)

when `(#%app f 10)' is produced by the `local-expand' call, the
certificate on `f' is lifted to the whole `(#%app f 10)' form, so `f'
cannot be extracted without losing the certificate.

If the stop list for `local-expand' were non-empty, then local
expansion would stop with `((p-ex) 10)'. In that case, there is no
certificate lifting, but stopping at core forms means that there's
wasn't any nested expansion, so there are no candidates for lifting
anyway. That is, the certificate to allow the reference to `p-ex' is
already on the whole form, so it cannot be lifted out.


A slightly different example illustrates a remaining limitation of
syntax-certificate tracking:

  ....
  (define-syntax (ex stx)
    #`(#,(local-expand #'(p-ex) 'expression null) 10))
  ....
  (define-syntax (cheater stx)
    (define v (local-expand #'(ex) 
                            'expression 
                            (list #'app)))
    (syntax-case v ()
      [(f arg) #'f]))
  ....

In this case, the `cheater' macro successfully extracts a certified
`f'. For now, I'm inclined to call this case too rare to worry about;
it's not a problem with using `local-expand' in general, but in using
`local-expand' on an identifier that is available only in the
environment of the use of `local-expand' (i.e., using `local-expand' on
the local macro `p-ex'). In that situation, a programmer is far more
likely to use a compile-time helper function directly instead of going
through `local-expand'.


The changes to syntax-certificate handling are not completely
backward-compatible, but problems should be rare. I found three little
problems in the SVN trunk, and all were easily fixed.