[racket-dev] A tricky chaperone puzzle

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Thu Jul 24 21:31:13 EDT 2014

Yes, true!

Robby

On Thu, Jul 24, 2014 at 8:07 PM, Sam Tobin-Hochstadt
<samth at cs.indiana.edu> wrote:
> Struct chaperones are the important part, I think.
>
> But the theorem would be false under option 1, I think. Adding contracts can
> add non-contract errors -- the error you get when a you supply the wrong
> accessor for struct-chaperone.
>
> Sam
>
> On Jul 24, 2014 7:54 PM, "Robby Findler" <robby at eecs.northwestern.edu>
> wrote:
>>
>> Ah, nope. That model doesn't include function chaperones!
>>
>> Robby
>>
>> On Thu, Jul 24, 2014 at 6:14 PM, Robby Findler
>> <robby at eecs.northwestern.edu> wrote:
>> > I also lean towards #2. What does the redex model say? Most of those
>> > pieces are in it, I think.
>> >
>> > Robby
>> >
>> > On Thu, Jul 24, 2014 at 3:25 PM, Matthew Flatt <mflatt at cs.utah.edu>
>> > wrote:
>> >> Nice example. Offhand, I think that #2 is right, but I'll have to look
>> >> at it more to be sure.
>> >>
>> >> At Thu, 24 Jul 2014 15:45:18 -0400, Sam Tobin-Hochstadt wrote:
>> >>> Consider the following module:
>> >>>
>> >>> (module m racket
>> >>>   (struct x [a])
>> >>>   (define v1 (x 'secret))
>> >>>   (define v2 (x 'public))
>> >>>   (provide v1 v2)
>> >>>   (provide/contract [x-a (-> x? (not/c 'secret))]))
>> >>>
>> >>> It appears that this ensures that you can't get 'secret. But, it turns
>> >>> out that I can write a function outside of `m` that behaves like `x-a`
>> >>> without the contract:
>> >>>
>> >>> (require (prefix-in m: 'm))
>> >>>
>> >>> (define (x-a v)
>> >>>   (define out #f)
>> >>>   (with-handlers ([void void])
>> >>>     (m:x-a (chaperone-struct v m:x-a (λ (s v) (set! out v) v))))
>> >>>   out)
>> >>>
>> >>> Now this works:
>> >>>
>> >>> (displayln (x-a m:v1)) ;; => 'secret
>> >>>
>> >>> The problem is that `m:x-a` is treated as a
>> >>> `struct-accessor-procedure?`, which is a capability for accessing the
>> >>> a field, even though it's a significantly restricted capability.
>> >>>
>> >>> There are a couple possible solutions I've thought of:
>> >>>
>> >>> 1. Require a non-chaperoned/impersonated accessor.
>> >>> 2. Actually use the chaperoned/impersonatored accessor to get the
>> >>> value out instead of the underlying accessor.
>> >>>
>> >>> 1 is a little less expressive. But note that 2 means that you have to
>> >>> only allow chaperoned procedures with `chaperone-struct`, and imposes
>> >>> significant complication on the runtime.
>> >>>
>> >>> I favor 1.
>> >>>
>> >>> Sam
>> >>>
>> >>> _________________________
>> >>>   Racket Developers list:
>> >>>   http://lists.racket-lang.org/dev
>> >>
>> >> _________________________
>> >>   Racket Developers list:
>> >>   http://lists.racket-lang.org/dev
>
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev
>


Posted on the dev mailing list.