Foreign Function Interface

[lukaszcz]

Currently, we keep adding each new AnomaLib function as a builtin. Each time, this requires compiler modification, and the number of builtins has grown unreasonably. AnomaLib functions should not be compiler builtin operations, but just external callable functions.

I propose general syntax of the form:

extern kind {attribs} 
f : Nat -> Nat;

The kind indicates the kind of external definition, e.g., anomalib. attribs are attributes specific to kind.

For example,

extern anomalib {path := 2131}
listDelta : List Action -> Delta;

[janmasrovira]

Alternative approach:

type IsNockmaBuiltin (A : Type) := mk {
..
};

axiom
keccak256 : Nat -> Nat;

instance I : IsNockmaBuiltin keccak := mk@{
  stdlibCall := [9 2 0 1] ;
  isDebug := ...;

};

[lukaszcz]

Using traits and instances for this doesn't fit with their current concept, because they are defined for types, but we typically want to define functions to be external not types. Besides, we wouldn't use the instance resolution mechanism much, so I don't see the point in defining these as actual instances.

We could still use Juvix records instead of ad-hoc attribute syntax to represent the attributes, e.g.:

type AnomaFFI (Singature : Type) := mk@{
   stdlibCall : Nock.Noun;
   isDebug : Bool;
   juvixCode : Maybe Signature;
};

extern
keccak256 : AnomaFFI (Nat -> Nat) := AnomaFFI.mk@{
   stdlibCall := Noun.cell (..) (..);
   isDebug := false;
   juvixCode := nothing;
};

[lukaszcz]

Well, maybe a bit different, because we want keccak256 : Nat -> Nat.

type AnomaFFI (Singature : Type) := mk@{
   stdlibCall : Nock.Noun;
   isDebug : Bool;
   juvixCode : Maybe Signature;
   externAxiom : Signature;
};

axiom keccak256 : Nat -> Nat;

extern
keccak256FFI : AnomaFFI (Nat -> Nat) := AnomaFFI.mk@{
   stdlibCall := Noun.cell (..) (..);
   isDebug := false;
   juvixCode := nothing;
   externAxiom := keccak256;
};