proof_cap_mint_private: a private function mints a proof capability

A proof cap may be minted only by a public function of the module that declares it. Those functions are the module’s documented ways of establishing the fact the capability stands for; a private helper is not one.

A program that triggers it

mod Main do
  needs IO
  mod Db do
    proof cap Migrated
    needs IO

    pfn migrate(c : Cap(IO)) : Cap(Db.Migrated) do
      mint_cap(c)
    end
  end

  fn main(_c : Cap(IO)) do
    ()
  end
end

The fix

Make the minting function public (fn), so it is part of the module’s interface:

mod Main do
  needs IO
  mod Db do
    proof cap Migrated
    needs IO

    fn migrate(c : Cap(IO)) : Cap(Db.Migrated) do
      mint_cap(c)
    end
  end

  fn main(_c : Cap(IO)) do
    ()
  end
end

Why the rule exists

Keeping minting in public functions keeps the list of places that can produce the proof short and visible: reading the module’s public API tells you every way the fact can come to be. A private helper could be called from anywhere inside the module without that review.

See also: the language reference.