[cap-talk] Haskell @inert-like construct

[Toby Murray]

On Tue, 2008-09-02 at 17:40 -0700, Tyler Close wrote:
> interface Exporter {
>     String run(@inert Object x);
> }
> 
> static public String
> encode(final Exporter export, final @inert ConstArray<?> values);
> 
> The encode() method generates a JSON text that represents the
> immutable parts of the object tree reachable from the values argument.

> In a security review, it might be important to know a couple things
> about the implementation of the encode() method. For example, it might
> be important to know that
> A. the encode() implementation will not mutate any of the state
> reachable via the "values" argument.
> B. the output will be the same if you call the method with the same
> arguments (important to know if you want to cache the output)
>
> Today, you'd have to manually inspect the implementation of the
> encode() method to determine whether or not these properties hold.

Does the encode() method being functionally pure not guarantee these
properties? 

> I proposed the @inert
> auditor.

I remember reading the description of the @inert auditor when it was
first posted to e-lang. Both times I've failed to understand what it's
doing, based on the rules the verifier is enforcing. Can you elaborate
further?

> For example, given the following API:
> 
> class Foo {
>    public final Object x;
>    Foo(@inert final Object x) {
>        this.x = x;
>    }
> }
> 
> static public Foo
> bar(@inert final Object x) {
>    return new Foo(x);
> }
> 
> the following code is valid:
> 
> final Object a = ...
> final Foo aFoo = new Foo(a);
> final Foo aBar = bar(a);
> return new Foo(a);
> return bar(a);
> final @inert Object b = ...
> final @inert Foo bFoo = new Foo(b);
> final @inert Foo bBar = bar(b);
> return new Foo(b);
> return bar(b);
> 
> the following code is invalid:
> 
> final Foo bFoo = new Foo(b);
> final Foo bBar = bar(b);
> return new Foo(b);
> return bar(b);

Again, I've failed to understand the crucial difference between the
correct and incorrect cases here. Could you explain further why the
second cases are invalid and what property is being enforced here?

Cheers

Toby