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

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.

This is what I thought certificates were designed to prevent, but they
don't seem to be doing it here.  I've tried changing the 'certify-mode
property on the result of Typed Scheme's `#%module-begin' expansion to
be 'opaque, but that didn't help.  Is there something else I should
try?

#lang scheme/load

(module m typed/scheme
  (require scheme/unsafe/ops)
  (: f ((Vectorof (U)) -> Any))
  (define (f x) (unsafe-vector-length x))
  (provide f))

(module n scheme

  (require (prefix-in t: typed-scheme))

  (define-syntax (cheater stx)
    (define v (local-expand #'(t:#%module-begin (require 'm) (define z (f #())))
                            'module-begin null))
    (syntax-case v ()
      [(mb r (d-v (z) (_ f e)) rest ...)  #'f]))

  ((cheater) 3)
  )

(require 'n)

-- 
sam th
samth at ccs.neu.edu