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

On Wed, Dec 16, 2009 at 6:05 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> On Wed, Dec 16, 2009 at 5:19 PM, Sam TH <samth at ccs.neu.edu> wrote:
>> The program at the end of this message behaves in arbitrary ways.  In
>> particular, it segfaults on my system.  However, this should be safe:
>> Typed Scheme is checking that only vectors are passed to `f'.  But the
>> `cheater' macro uses `local-expand' to extract a reference to `f', and
>> use it in arbitrary ways.
>
> You provided 'f'.  Certificates do not protect identifiers that are
> provided from the module that defines them.

As Jay points out, I didn't really provide `f'.  I provided a
rename-transformer that points to `f'.  Here's a more explicit version
of the original module:

(module m typed/scheme
  (require scheme/unsafe/ops (for-syntax scheme/base))
  (: f ((Vectorof (U)) -> Any))
  (define (f x) (unsafe-vector-length x))
  (define-syntax f*
    (make-rename-transformer #'f))
  (provide (rename-out [f* f])))

This suggests to me that this is a bug in the interaction of
rename-transformers and certificates.

-- 
sam th
samth at ccs.neu.edu