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": { ... }
    }
  ]
}

Field	Values	Meaning
`name`	string	the namespace the import names: `imp Touch : micacallsc`
`language`	`c` · `mica`	which side of the boundary the library was written on — it decides calling and failure semantics
`type`	`external` · `system` · `internal`	`external` links an archive the link block names; `system` names an external system library; `internal` marks a surface embedded in the compiler — you author `external`, and `system` where the linker should find the library itself
`import_protected`	boolean	when true, the library’s names are protected only at their import site — other units stay free to declare the same names for their own containers. The class a vocabulary unit wants: the `bits` unit’s `Count` beside the `maps` unit’s `Count`. The standard library carries this class, so a program may declare `Length` or `Capacity` for itself and reach the library’s own entry through the namespace it imported, `std.Length(values)`; importing the entry and declaring the name in one unit is what the import site refuses
`contract`	object	the surface itself: `link`, `types`, `constants`, `functions`, `generic_templates`

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:

`kind`	Declares	Carries
`record`	a field sequence	`fields`, optional `packed`, optional `layout`
`enum`	named literals	`literals`, `base_type`
`subrange`	a bounded integer	`base_type`, `lower_bound`, `upper_bound`
`array`	a fixed array	`element_type`, `dimensions` (each with `index_type` and both bounds)
`dynamic_array`	an `array of T`	`element_type`
`set`	a set over an ordinal	`base_type`
`bitset`	a fixed-width bit set	`base_type`
`bitrecord`	named bit fields in one carrier	`bit_fields` (each with `bit_offset` and `bit_width`), `base_type`

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": "dynamic_array", "element": {"kind": "builtin", "name": "float64"}}
{"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 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 a fingerprint — both are the compiler talking to itself across compilations; 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"
}

Field	Values	Meaning
`language_name`	PascalCase	the name Mica source calls
`external_name_utf8` / `external_name_utf32`	symbol names	the machine-level symbol per source encoding. A function that exists for one encoding only leaves the other empty, and consuming it from the wrong encoding is a compile error
`parameters`	list	each with `name`, `type`, and `passing_mode` — `call_by_value`, `call_by_constant_value` (the `const` promise on a scalar or small value, enforced on the Mica side), or `call_by_constant_address` (the `const` promise on a plain aggregate wider than 16 bytes: the value arrives as one pointer into caller-owned read-only storage, so a C consumer declares the parameter `const T *`)
`return_type`	type reference	omitted or `{"kind": "void"}` for none
`variadic`	boolean	the C `...` — a Mica-borne entry never carries it, because the language has no variadic functions
`format_string`	`none` · `write` · `read`	declares a printf/scanf-class function, which turns on compile-time checking of the format against the variadic arguments; `format_string_index` is the format parameter’s zero-based position — `0` for the printf shape, `1` for fprintf, `2` for snprintf
`errors`	object	see below
`abi`	object	optional; its `aggregate_return_mode` — `register` or `hidden_return` — states how the C side returns an aggregate by value, where the two conventions differ
`blocking`	boolean	optional, default false: this C entry waits on the outside world by design — the `fsync` class. The stamp sharpens the compiler’s boundary-under-mark warning from “may stall” to “is declared to wait”; it never rejects a call
`parks`	boolean	optional, default false: the call may park the calling task on a descriptor. A parking entry’s external names must name a `__mica_` parking shim — the runtime routine that tries the operation without blocking and suspends only the calling task until readiness
`requires_flags`	list	additional compiler or linker flags this one function needs on the link line
`description`	string	one sentence; surfaces in editor hover
`interface_file`	string	the C header documenting the function — documentation, not consumed

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.

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.

`convention`	The C idiom it lifts
`negative_errno`	a negative return announces failure — most of POSIX: `read`, `write`, `open`, the socket family
`null_errno`	a null pointer return announces failure — `getcwd`, the `fopen` class
`sentinel:<value>`	a stated sentinel value announces failure — `mmap`’s all-ones is the classic

domain names the Mica error domain the lifted code lands in (posix.OsError above). 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. Enum literals do not repeat here; declaring the enum type already imports its literals.

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.

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.

Where contracts come from, and where they are found#

The file#

The link block#

Types#

Functions#

The errors block#

Constants#

Mica-borne libraries: generic templates#

Reading order for a new contract#