[e-lang] Bindings and guard-based auditing

[Thomas Leonard]

On Tue, 2010-05-25 at 09:22 -0400, Kevin Reid wrote:
> On May 25, 2010, at 7:18, Thomas Leonard wrote:
> 
> > Ah, I hadn't spotted that the binding is vouching for the slot itself
> > (not just the values it returns).
> >
> > Still, I don't see the advantage. The information we may want the
> > auditor to see for any name includes:
> >
> > - the slot's auditors (e.g. "this is a FinalSlot")
> > - the slot's guard (e.g. "the value is always DeepFrozen")
> > - the slot's value (e.g. "true")
> > - other selected properties of the slot
> 
> The advantage is in not explicitly coding in this list of information  
> in the auditing interface, but rather in the code which provides it  
> (combined with the default rules given below).
> 
> > How does a piece of code say what the auditor is allowed to see?
> >
> > If I say:
> >
> > def x := 3
> > def &y := makeWackySlot(4)
> >
> > def obj implements Auditor {
> >  to getValue() { return x + y }
> > }
> >
> > what can Auditor see by default? How do I control this?
> 
> Each binding pattern chooses what the binding-guard is. Here are the  
> results as implemented in current E-on-CL:
> 
>     Pattern       Binding guard
>     -------       -------------
>     x             FinalSlot[any]
>     x :int        FinalSlot[int]
>     var x         VarSlot
>     var x :int    GuardedSlot         Seems like it should be
>                                       GuardedSlot[int]. Bug?
>     &x            any
>     &x :FooSlot   FooSlot
>     &&x           specimen.getGuard() where specimen is a CoercedSlot
>                                       (binding).
> 
> 
> In your particular case, the auditor knows only that x is final (but  
> not even what type of value it is) and nothing about y.
> 
> 
> A notable high-level pattern (used for all values in the safeEnv in E- 
> on-CL) is to guard values with the Same guard, which accepts exactly  
> one value and therefore communicates that value to the auditor. For  
> example, in (def x :Same[3] := 3), the auditor can see that x has the  
> value 3. This is particularly useful when the binding is of a flow- 
> control construct or well-known function and the auditor needs to see  
> that it has the behavior expected.
> 
> The current example of this pattern is the SubrangeGuard auditor in E- 
> on-CL: If the Foo :SubrangeGuard[Bar], then the possible results of  
> Foo#coerce/2 are a subset of the possible resoluts of Bar#coerce/2.  
> For example, 1..10 is a SubrangeGuard[int] and  
> SubrangeGuard[DeepFrozen], so if an auditor sees x :(1..10) then it  
> knows that x is DeepFrozen even if it doesn't know about numeric  
> interval guards. SubrangeGuard[Bar] needs to be able to see explicitly  
> that the implementation of Foo#coerce/2 coerces by the specific guard  
> Bar (well, or a SubrangeGuard of it et cetera; this isn't as fully  
> general/complete lattice as it could be) and this is done using the  
> Same scheme.
> 
> Repeating the value is indeed clunky and was one of the things that  
> bothered me when I was last working on GBA; I now see that it can be  
> improved:
> 
> def exposed(value, _) {
>    return makeCoercedSlot(FinalSlot[Same[value]],  
> makeFinalSlot(value), throw)
> }
> def via (exposed) &&x := 3
> 
> 
> (or, somewhat 'cute' implementation:)
> def exposed(value, _) {
>    def expValue :Same[value] := value
>    return &&expValue
> }
> 

OK, that's helpful. So we should be able to compare now.

For the slots-only case, I'm imagining that there's some method on Slot
to get details for an auditor (getAuditionInfo or some-such). This is
only called for known slot types (FinalSlot, VarSlot, etc). For other
slot types, we pass no information to auditors.

(yes, this makes some slot types special, but as I understand it the
bindings proposal makes certain binding types special)

These cases would be the same (assuming the built-in slot types used in
the expansion give up their guard to auditors):

  def x := 3
  def x :int := 3
  var x := 3
  var x :int := 3

But in:

  def &x := makeSlot(...)

the information given up to an auditor would depend on makeSlot (whereas
with bindings no information is given up), and in

  def &x :FooSlot := ...

it would depend on FooSlot (but isn't necessarily equal to FooSlot).
Finally,

  def via (exposed) &&x := 3

would become one of these (I think I prefer the third, even if it is the
longest):

  def via (exposed) &x := 3
  def &x :exposed := makeFinalSlot(3)
  def &x := makeFinalSlot(3).exposed()

For wacky slots:

  def &&wacky := makeCoercedSlot(WackySlot, makeWackySlot(value))

becomes

  def &wacky :CoercedSlot[WackySlot] := makeWackySlot(value)

where CoercedSlot is a trusted slot type which simply proxies to the
underlying slot, coerced by the guard. It gives up the guard (WackySlot)
to the auditor, which can process it as it pleases. makeWackySlot could
do the coercion itself if desired.


The two proposals seem pretty similar. They both provide a way for an
auditor to get the type of a slot, preventing the slot from lying, and
can provide extra information as needed in the type.

The main difference is that bindings add new syntax (&&x and "def ...
as").



-- 
Dr Thomas Leonard
IT Innovation Centre
2 Venture Road
Southampton
Hampshire SO16 7NP

Tel: +44 0 23 8076 0834
Fax: +44 0 23 8076 0833
mailto:tal at it-innovation.soton.ac.uk
http://www.it-innovation.soton.ac.uk