C interop

extern fn declares a function written in C so Brine code can call it. For now an extern function may only take and return integers, floats and bools, and only the C standard library (with the math library) is linked in.

extern fn cbrt(x: float) -> float
extern fn hypot(x: float, y: float) -> float
extern fn atan2(y: float, x: float) -> float
extern fn llabs(x: i64) -> i64
extern fn toupper(c: i32) -> i32

fn main():
    print(cbrt(27.0), hypot(3.0, 4.0), atan2(1.0, 1.0) * 4.0)
    print(llabs(-42), chr(int(toupper(i32(ord("a"))))))

Output

3.0 5.0 3.141592653589793
42 A

Declaring a C function

• Write extern fn name(params) -> type at the top level, with no body. name is the C symbol, exactly as written.
• Parameter and return types must be integer types (int/i64, i32, u8, …), floats (float/f64, f32) or bool. The return type may be left out for a C function that returns void.
• Call it like any Brine function.

Match the C types exactly, because Brine trusts the declaration:

C	Brine
int	i32
unsigned int	u32
long long, int64_t	i64 (= int)
size_t on 64-bit systems	u64
double	float (= f64)
float	f32
bool (C99 _Bool)	bool
void result	no ->

C’s long is 32 bits on Windows and 64 bits on Linux and macOS, so prefer functions that use int, long long or fixed-width types (llabs, not labs).

What’s not supported

Strings, arrays, pointers, structs, callbacks and variadic functions (printf) can’t cross the boundary, and ref and mut parameters aren’t allowed:

extern fn puts(s: str) -> i32

fn main():
    puts("hi")

error[E0311]: extern functions may only take integers, floats and bools
 --> main.br:1:16
  |
1 | extern fn puts(s: str) -> i32
  |                ^ parameter has type `str`
  = run `brine explain E0311` for more about this error
error: could not compile due to 1 error

There is also no way yet to link other C libraries or your own C files: the program links against the C standard library and the math library (on Linux and macOS also pthread and dl).

brine check doesn’t link, so a misspelled or missing C function shows up only when you build or run, as error E0705 naming the undefined symbol:

error[E0705]: linking the program failed
  = note: ... undefined reference to `no_such_c_function'

What Brine knows about C calls

Brine can’t see inside a C function, so:

• The prover knows nothing about the result beyond its type. Add an assert to hand it a fact: let r = rand() then assert r >= 0.
• The compiler allows extern calls inside par. Only call functions there that are safe to call from several threads at once. Pure math functions like cbrt are; rand is not.
• In a world program, a value returned by C may differ between ranks, so it counts as rank-dependent and can’t decide whether a world call happens (E0510):

extern fn rand() -> i32

fn main():
    if rand() % 2 == 0:
        world.barrier()

error[E0510]: some ranks might not reach this communication
 --> main.br:5:9
  |
5 |         world.barrier()
  |         ^^^^^^^^^^^^^^^ calls `world.barrier`
4 |     if rand() % 2 == 0:
  |        --------------- this may differ between ranks
  |
  = note: every rank must make the same `world` calls in the same order, otherwise the program could hang
  = help: move the call out of the rank-dependent branch or loop; compute rank-specific values first, then communicate on every rank
  = run `brine explain E0510` for more about this error
error: could not compile due to 1 error

Related: built-in functions (most math is built in: sqrt, sin, exp, pow, …), functions, proofs.