Question: opaque types and capabilities

I've been learning a lot reading through the specification and tutorial for Austral. It's a great project!

Specifically i've been looking at the tutorial page for capability-based security and i'm having a little trouble wrapping my head around something and was hoping somebody may be able to help clarify (what I assume) is a misconception of mine.

Regarding:

module Env is
    type EnvCap: Linear;

    generic [R: Region]
    function acquire(root: &[RootCapability, R]): EnvCap;

    function release(cap: EnvCap): Unit;

    ...

The tutorial explains that creating an EnvCap capability as a Linear Type is a way of ensuring a consumer of a module has access to the Root Capability. It mentions that:

EnvCap is a linear value that represents the ability to access the environment. Since it is an opaque type, it cannot be created by clients. The only way to construct an instance of the EnvCap type is via the acquire function. Dually, the release function consumes the capability.

This concept of the opaque type is where i'm getting stuck, as it's not obvious to me how the EnvCap type is marked as opaque. Copying this .aui file from the tutorial and creating a basic module body for it still allows me to import EnvCap and, more importantly, create an instance of the record type using let env_cap: EnvCap := EnvCap();, bypassing the requirement for the acquire function at all, letting me forge an EnvCap capability which as I understand should not be possible.

I thought that maybe i'd done something silly in my implementation of the module body, so I found a similar capability pattern in standard IO.aum and IO.aui for the TerminalCapability and copied it to my test project and found the same issue.

The following program is accepted by the compiler - creating a TerminalCapability without needing to call the acquireTerminal function, nor pass it a RootCapability

import Standard.IO (acquireTerminal, releaseTerminal, TerminalCapability);

module body Hello is 

    function foo(): Unit is
        let x: TerminalCapability := TerminalCapability();
        releaseTerminal(x);

        return nil;
    end;

    function main(): ExitCode is
        foo();
        return ExitSuccess();
    end;
end module body.

The most obvious explanation here is that my interpretation of opaque types is incorrect. Any help in figuring out where my understanding has gone wrong would be appreciated.

Thanks!

austral / austral

Question: opaque types and capabilities #601