Library contracts: mica.external

A contract is how a Mica program learns what a foreign library offers: its functions, their exact machine-level names, the types that cross the boundary, and how each function announces failure. The compiler consumes contracts instead of parsing C headers — the contract states the facts once, in one reviewable file, and every import resolves against it.

This page is the normative reference for the format. The guided introduction is Mica calls C; the failure-lifting discipline has its own article in error domains.

Where contracts come from, and where they are found

Three roads produce a contract file:

• You author one beside a C library you want to call — the MicaCallsC example is a full worked instance, and DebugWalk a minimal one.
• The compiler emits one when linking a Mica library with --emit-contract: the file mica.external lands beside the archive, so another program can import the library by resolving that contract.
• Some ship inside the compiler. The C standard library, POSIX, and Linux surfaces are embedded contract sets selected by imp ... : c, : posix, : linux — nothing on disk is consulted. The Dragon SDK’s curated contract is installed for reading at /usr/share/doc/mica-dragon-sdk/dragon-engine.json, a real contract over a real shipped archive you can open on your own machine.

A consumed contract is found beside the sources, named explicitly with --external-contract, or listed in mica.project. The published JSON schema ships in the container as reference/library_contracts.schema.json.

The file

One JSON document: a description and a list of libraries. Every name a program imports resolves against exactly one library entry.

{
  "description": "External library contracts for the MicaCallsC example",
  "libraries": [
    {
      "name": "micacallsc",
      "language": "c",
      "type": "external",
      "contract": { ... }
    }
  ]
}

A C library’s version belongs to the machine the program is built for, so a contract names the library’s package and the build asks that machine’s pkg-config, as autoconf, meson and CMake ask it: pkg-config for the machine’s own architecture, aarch64-linux-gnu-pkg-config or x86_64-linux-gnu-pkg-config for a cross build. The version it answers is the one the build names, Using library 'sqlite3' 3.46.1, the one the manifest records and the one a project’s requires reads, and a system below the minimum answers with the library’s name:

the C library 'sqlite3' is at version '3.31.1' on this machine, as 'pkg-config' answers for the package 'sqlite3', and its contract requires at least '3.35.0'

A tool that is not installed and a package it does not know are refused by the library’s name the same way; the development files of the library for the build’s target are what the system needs.

The link block

What joins the link line when any function of this library is consumed — stated per link profile, chosen by the --external flag:

"link": {
  "static": { "flags": ["../build/MicaCallsC/libmicacallsc.a"] },
  "shared": { "flags": ["-lmicacallsc"] }
}

Both profiles are required; each is a list of linker arguments, spelled exactly as they should reach the linker.

Types

Types declared here become importable Mica types, and they are the only types that may cross the boundary by name. kind selects the shape:

A library compiled with --emit-contract writes its exported aliases this way: exp Same = Inner becomes an alias over the named reference to Inner, and exp Count = int64 an alias over the built-in, so an importer spells the name the library declared and gets the type it declared it over.

An opaque type is C’s incomplete type, struct sqlite3;: the library knows its layout and the contract states none. Mica never holds one by value, only a pointer to it, and such a pointer is a handle: it names an object the C library owns and Mica never reads. So a handle crosses into a generator or a stream’s element as the word it is, and every activation it is handed to holds the same object. A task or a stream placed on a process refuses a handle, because the worker’s copy of the word names nothing there.

"thread_safe": true states that the C library allows one of its objects on several threads at once, as sqlite does for a connection opened in its serialized mode. Only a handle to such a type crosses into a task on a carrier or into a stream a scheduled producer feeds, because the task runs beside the activation that scheduled it and both hold the handle. Every other handle stays on the thread that holds it: a generator the program pulls takes it, and tasks share it only through a variable of the activation that scheduled them, touched in synchronized statements, whose lock then admits one task at a time. State thread_safe only when every function of the contract that takes the handle is safe from several threads at once, and never for an object whose functions answer memory another thread’s call can free, such as the text a sqlite statement answers for a column. When one function of an otherwise safe object answers such memory, a library keeps it in a contract of its own that programs never consume, and reaches it only under the lock that makes it safe: the sqlite library keeps sqlite3_errmsg beside the connection’s mutex in sqlite3-internal.external.

Everywhere a type is referenced — a field, a parameter, a return — the reference is an object with its own kind:

{"kind": "builtin", "name": "int32"}
{"kind": "named",   "name": "ScalarPacket"}
{"kind": "pointer",       "to": {"kind": "named", "name": "ScalarPacket"}}
{"kind": "const_pointer", "to": {"kind": "builtin", "name": "uint8"}}
{"kind": "borrowed_pointer", "to": {"kind": "named", "name": "Sqlite"}}
{"kind": "dynamic_array", "element": {"kind": "builtin", "name": "float64"}}
{"kind": "tracked", "element": {"kind": "builtin", "name": "float64"}}
{"kind": "c_text"}
{"kind": "void"}

pointer and const_pointer differ exactly as the C qualifier does, and the compiler holds an import to it: a const_pointer parameter cannot be written through. A borrowed_pointer carries no ownership with it: the cell it designates belongs to someone else — a C library’s own handle above all — so the importing program’s ownership analysis demands no release for it. It is how a Mica library’s borrowed pointer T result crosses an emitted contract whole. c_text is a C function’s result alone: the NUL-terminated UTF-8 a const char * points to, which the C side owns. The Mica signature answers a string, and every call copies the text into it, decoded for the program’s encoding, each ill-formed byte sequence one replacement character and a null pointer the empty string. tracked belongs to a Mica library alone: a tracked value, a float or a float tensor paired with the id of its tape node, whose id crosses a call beside the value as a word of its own, so no C signature has a place for it. A record whose shape genuinely differs per target may declare variants keyed by architecture (amd64, arm64) in place of the base fields — it must state every supported architecture, so a port cannot silently inherit the wrong layout. An emitted contract may additionally carry layout (sizes, alignments, field offsets), and it states every type’s fingerprint with its fingerprint_version: a digest of the type’s shape as the library compiled it. The importing compiler computes the digest again from the contract it reads, so a contract edited after the compiler wrote it is refused by the type’s name. An authored contract omits them.

Functions

{
  "language_name": "InotifyInit",
  "external_name_utf8": "inotify_init1",
  "external_name_utf32": "",
  "parameters": [
    {"name": "flags", "type": {"kind": "builtin", "name": "int32"},
     "passing_mode": "call_by_value"}
  ],
  "return_type": {"kind": "builtin", "name": "int32"},
  "variadic": false,
  "format_string": "none",
  "errors": {
    "convention": "negative_errno",
    "domain": "posix.OsError"
  },
  "description": "Create an inotify instance ...",
  "interface_file": "sys/inotify.h"
}

Two passing modes keep a parameter out of the Mica signature:

• fixed with a value: the contract’s own argument, a machine integer every call passes at the parameter’s position, such as the -1 byte count and the SQLITE_TRANSIENT destructor sqlite3_bind_text takes. A value outside the parameter’s type is refused, and so is a fixed parameter in a variadic function or one that takes a callback.
• call_by_result: the parameter’s type is a pointer to the word the C function writes, an integer or a pointer such as a handle, and the Mica call answers that word, as sqlite3_open_v2 answers its connection through a sqlite3 **. The call passes the address of a hidden word, zeroed before every call. The C function’s own result, its status or nothing, is what its errors convention reads. Where the C library answers a resource even when the call fails and asks for it back, the parameter’s release_on_failure names the library’s function that releases it, and a failing call hands a non-null word to it before the failure reaches the caller.

{"name": "database", "type": {"kind": "pointer", "to": {"kind": "pointer", "to": {"kind": "named", "name": "Sqlite"}}},
 "passing_mode": "call_by_result", "release_on_failure": "SqliteCloseV2"},
{"name": "vfs", "type": {"kind": "builtin", "name": "int64"}, "passing_mode": "fixed", "value": 0}

Two more fields appear only in contracts the compiler writes, never in one you author: effects on a Mica-borne entry records what the exporting unit’s transitive effect walk proved about the body (an empty object is the walked-and-clean statement), and intrinsic names an entry the compiler realizes inline at each call site — the embedded standard-library surface’s own bookkeeping.

Callback slots

A C library that takes a function pointer declares that parameter a callback slot: the parameter itself carries the void-pointer type — the pointer-sized code address is what actually crosses — and the slot beside it states everything the compiler holds a binding to:

{
  "name": "visit",
  "type": {"kind": "pointer", "to": {"kind": "void"}},
  "passing_mode": "call_by_value",
  "callback": {
    "class": "during_call",
    "parameters": [
      {"name": "context", "type": {"kind": "pointer", "to": {"kind": "void"}},
       "passing_mode": "call_by_value"},
      {"name": "value", "type": {"kind": "builtin", "name": "int64"},
       "passing_mode": "call_by_value"}
    ],
    "return_type": {"kind": "builtin", "name": "int64"},
    "userdata_index": 2
  }
}

The only thing that may stand at a callback slot is the name of a Mica callback declaration — the third declared subprogram kind beside task and generator. A callback is never called from Mica and never a value; the library behind the slot performs every firing, and the callback’s whole environment is the explicit context record its userdata pointer carries plus the unit’s own root storage.

The errors block

The errors block is what turns a C failure idiom into Mica’s failure channel: the compiler synthesizes the check the convention describes and lifts the failure, so the caller handles it with on fail like any Mica failure — no -1 tests in user code, ever.

The first three read the reason from errno. status_code reads none: the block states success, the statuses a call answers when it succeeded, each the call’s plain result, and every other status fails the call with the code whose value it is, or with the domain’s first code where no code states it.

"errors": {"convention": "status_code", "success": [100, 101], "domain": "SqliteCode"}

domain names the Mica error domain the lifted code lands in (posix.OsError above). A convention tests the value a function returns, so a function that returns nothing cannot state one. A language: "mica" entry never carries the block: a Mica-borne callee speaks the failure channel natively, with nothing to lift.

Constants

{"name": "InotifyCloexec", "type": {"kind": "builtin", "name": "int32"}, "value": 524288}

A constant carries name, type, and value — or values keyed per target architecture for the rare constant whose value depends on it, or encodings keyed utf-32 and utf-8 for the few facts that follow the build’s string encoding, which is how std states CodeUnitBytes. Exactly one of the three forms is present. Enum literals do not repeat here; declaring the enum type already imports its literals.

{"name": "Pi", "type": {"kind": "builtin", "name": "float64"}, "value": 3.141592653589793,
 "exact": "157079632679489661923/50000000000000000000"}

A real constant written without a type, such as math’s exp Pi = 3.14159265358979323846;, carries exact beside value: the value as written, as a rational p/q or a bare integer, or -0 for a negative zero. value is that value rounded to float64. A program that imports the constant rounds exact once to the type it meets, so it reads the value the library’s own code reads. exact stands beside value only, and the two agree: exact rounded to the constant’s type is value. The compiler writes the field under --emit-contract; a contract that breaks one of these rules is refused when it loads, naming the constant.

{"name": "Row", "type": {"kind": "named", "name": "Pair"}, "value": [1.5, 2.5]}

A typed array constant carries its elements’ values as a list, in index order, under its array type, which the library exports beside it: exp Row : Pair = (1.5, 2.5); is published with exp Pair = array[0..1] of float64;. A program that imports Row reads it whole or element by element, as the library’s own code does. A list of another length is refused when the contract loads, naming the constant. A float16 or bfloat16 constant carries its value as a number, which the program rounds once to its type.

Mica-borne libraries: generic templates

A contract with language: "mica" may carry generic_templates — the gen blocks of a Mica library, travelling as source because generics instantiate in the consuming compilation. Each entry names the template, its kind (type or function), its type parameters with their constraints, and the imports its body needs. You do not author these: the compiler emits them with the rest of the contract under --emit-contract.

An exported generator travels the same way, and so does every generator or template of the library that an exported one names. Because such a body is compiled in the program that imports it, what it names must reach that program with it:

A hidden entry carries "hidden": true and belongs to the library alone: the importing compilation imports it inside the copied body and nowhere else, and no import a program writes selects it. A private routine the body calls keeps its code in the library’s archive, linked by its symbol, and a private type brings the private types its own shape names.

A body that names a declaration from the right-hand column is refused when the library compiles, at the name, rather than in every program that imports it:

analyzer error 5557: the variable 'base' is private to this library, but the body of 'Counting' is compiled in every unit that imports 'Counting', where no private name of this library exists: read and write it through a private function or procedure, which crosses hidden with the body
analyzer error 5612: the type 'Fault' is private to this library, but the signature of 'Checked' is compiled in every unit that imports 'Checked', where every caller names the types it spells: export it with 'exp'

An object compiled beside a program follows the same rule. An ordinary exported function is compiled in its library and may name anything there.

Routines over tracked values

A library keeps a second body of every routine it exports that works on tracked values: the recording copy, whose body records onto the tape of the program that calls it. The copy is a hidden entry of its own, and the routine’s entry names it in recording:

{"language_name": "Logistic", "external_name_utf32": "Neural__Logistic",
 "parameters": [{"name": "z", "passing_mode": "call_by_value",
   "type": {"kind": "tracked", "element": {"kind": "builtin", "name": "float64"}}}],
 "return_type": {"kind": "tracked", "element": {"kind": "builtin", "name": "float64"}},
 "recording": "Logistic__tape", ...}
{"language_name": "Logistic__tape", "external_name_utf32": "Neural__Logistic__tape",
 "hidden": true, ...}

Outside every window a program calls the routine and computes plainly; a call inside a tape window runs the copy, which the compiler imports beside the routine’s own import, so what the routine records joins the program’s tape. A contract that names a copy without listing it is refused at that call, because the call could only record nothing:

analyzer error 5632: 'Logistic' records onto the tape through a recording copy, and library 'Neural' names the copy 'Logistic__tape' without listing it, so a call inside a window would record nothing — rebuild the library with this compiler, which publishes the copy beside the routine

Reading order for a new contract

Author top-down, the order the compiler resolves: the library entry and its link block first (the import now resolves and links), then the types the boundary needs, then functions one at a time — each one testable as soon as it is declared — and the errors block on every fallible entry before the function is called in anger. The MicaCallsC worked instance follows exactly this order, and every field this page documents appears in it, in the compiler’s shipped contracts, or in both.