Friend modules

Interfaces provide a way to hide module's implementation details from a client. However, sometimes those details may need to be accessed by specific, trusted clients. In such cases, the friend declaration is your friend.

See this test-case for the simplest usage, reproduced here.

FriendProvider

A module whose implementation is hidden by an interface

In FriendProvider.fst:

module FriendProvider
let x : int = 0

And in FriendProvider.fsti:

module FriendProvider
val x : int

FriendConsumer

A client module that wants to prove, say, that FriendProvider.x is out of luck: that detail is explicitly hidden by the FriendProvider interface.

But, if you know what you're doing and you really need to access that part of FriendProvider's implementation, you can write:

In FriendConsumer.fst

module FriendConsumer
friend FriendProvider //this reveals implementation details of FriendProvider
let test = assert (FriendProvider.x == 0)

And you can even expose this fact to other modules:

In FriendConsumer.fsti:

module FriendConsumer
val test : squash (FriendProvider.x == 0)

Some restrictions

The friend M construct

1. can only appear in the implementation of a module N (i.e., N.fst) when an interface for N also exists (i.e., N.fsti also exists). This is to prevent a client module L of N silently becoming a friend of M (in case friend M appears in N.fsti).

2. is valid only if both M.fst and M.fsti exist (if M.fsti didn't exist, a friend wouldn't be necessary in the first place)