29 Meeting C

29.1 Calling C — mark, right, effects line#

module area_ffi .

rem the body lives in C — it carries all three: marker, rights and effects
unsafe extern proc c_area do
  input k cap c .
  input w i64 .
  input h i64 .
  output i64 .
  effects unsafe .
  link "lw_c_area" .
end

unsafe proc area_twice input k cap c . input w i64 . input h i64 . output i64 .
  effects unsafe .
do
  return add (c_area k w h) (c_area k w h) .
end

$ lowentc --check area.low
== check: ok ==

An op that calls a C function has all three.

An extern op’s body is in C, so there is no body here. Instead, the way a struct holds its fields, it holds its clauses in do … end, and among them link "lw_c_area" names the C side. A statement in that block would be a second body: E-FFI-BODY. The processor does not make the name up from the op’s name. It is a promise made to another language, so whoever promises writes it — leaving it out is E-FFI-LINK. area_twice calls that op, so it is itself unsafe and receives cap c. The mark and the right travel up the call chain.

module nounsafe .
rem expect: E-FFI-NOUNSAFE

extern proc c_area do
  input k cap c .
  input w i64 .
  input h i64 .
  output i64 .
  effects unsafe .
  link "lw_c_area" .
end

$ lowentc --check nounsafe.low
nounsafe.low:4:0 E-UNSAFE-UNDECLARED: this op declares the `unsafe` EFFECT but is not marked `unsafe`. The effect says WHAT it does; the modifier says WHO takes responsibility. Write `unsafe proc …` — an unsafe op that nobody signed for is exactly the hole the discipline exists to close
nounsafe.low:4:0 E-FFI-NOUNSAFE: calling C without `unsafe`. Inside that C function every invariant this language enforces can be broken, and the tool cannot see it. What cannot be checked must at least be MARKED (RFC-0063 D1)

module nocap_ffi .
rem expect: E-FFI-NOCAP

unsafe extern proc c_area do
  input w i64 .
  input h i64 .
  output i64 .
  effects unsafe .
  link "lw_c_area" .
end

$ lowentc --check nocap.low
nocap.low:4:0 E-FFI-NOCAP: this op calls C but receives NO right to do so. Calling into C is a capability you are HANDED — `input k cap c .` — exactly like the heap (RFC-0043), the device bus (RFC-0042) and raw machine instructions (RFC-0041). An ambient door into C is one every caller silently inherits

With only one of the three, the call “could work”. But then this language could not say what it has given up.

29.2 Types that cross the boundary#

Only what the C ABI can express crosses the boundary. option, result, vectors and containers do not exist in C, and the processor does not pretend they do.

module fftype .
rem expect: E-FFI-TYPE

unsafe extern proc c_find do
  input k cap c .
  input key u64 .
  output option u64 .
  effects unsafe .
  link "lw_c_find" .
end

$ lowentc --check fftype.low
fftype.low:4:0 E-FFI-TYPE: this signature carries a type the C ABI cannot express (option / result / vector / container). C has no such thing, and the tool will not PRETEND it does: pass integers, f64, or a byte slice (which becomes a POINTER and a LENGTH — two C arguments, because that is what a slice honestly IS in C)

Only slices are mapped automatically. slice τ becomes two arguments, “a pointer to τ” and “a count”. The width is known too — slice u32 is uint32_t *, not a byte pointer. Capabilities are not values, so they do not cross into C. There is one ABI name, c. “What C is on this machine” is already decided by the machine building it.

29.3 C calls Lowent#

The other direction. An exported op becomes a symbol callable from C.

module exported .
rem run: clamp_add 100 50

export fn clamp_add input a u32 . input b u32 . output u32 .
  requires le a 1000 .
  requires le b 1000 .
  ensures le ret 2000 .
do
  return add a b .
end

export fn sum_bytes input xs slice u8 . output u64 .
do
  var s u64 be 0 .
  for x xs do
    set s (add s (widen u64 x)) .
  end
  return s .
end

$ lowentc --run clamp_add exported.low 100 50
clamp_add(100, 50) = 150

--emit-h emits the header. A header written by hand keeps signatures in two places, and one day they diverge.

long long clamp_add(long long, long long);
long long sum_bytes(const unsigned char *, size_t);

You can see sum_bytes’s slice u8 split into a pointer and a length.

 Lowent
   input xs slice u8 .

 C (the header --emit-h writes)
   sum_bytes(const unsigned char *, size_t)
             └──────┬────────────┘ └─┬──┘
                    │                count (len xs)
                    pointer (xs's first item)

--no-main emits C holding only the entry points of exported ops, without main and the command-line dispatcher, ready to drop into someone else’s build. The following C program uses the two.

// host-for: exported.low
#include <stdio.h>
#include "lowent.h"

int main(void) {
    const unsigned char bytes[] = {1, 2, 3, 4};
    printf("clamp_add(100, 50) = %lld\n", clamp_add(100, 50));
    printf("sum_bytes = %lld\n", sum_bytes(bytes, 4));
    fflush(stdout);
    printf("clamp_add(5000, 1) = %lld\n", clamp_add(5000, 1));
    return 0;
}

$ cc host.c <exported.low 을 --no-main 으로 낸 C> && ./host
clamp_add(100, 50) = 150
sum_bytes = 10
panic: requires violated at entry
(종료 코드 70)

The first two calls get answers. The third breaks requires le a 1000 .. C does not know contracts, but the place being called into is this side’s door, so the op’s contract is enforced on the arguments and it stops on entry. Lowent answers for inside the door, C for outside.

Both directions in one picture. Going out, it is written in the head; coming in, it is measured at the door.

 going out --- Lowent calls C
   area_twice ──▶ c_area ══ link "lw_c_area" ══▶  lw_c_area (C)
   unsafe · cap c · effects unsafe                inside is unchecked; a person answers

 coming in --- C calls Lowent
   host.c ── clamp_add(5000, 1) ══▶ ┃ requires le a 1000 .
                                    ┃ 5000 breaks the promise
                                    ┗━▶ stops at entry (exit code 70)

29.4 Callbacks and ownership#

To let C call a Lowent function back, take the address of an export extern op with unsafe_fn <op> and pass it as a value. There is no new convention. Two rules apply.

• unsafe_fn may point only at export extern ops (E-FN-NOTEXPORT). The address of a door C cannot call is not an address.
• An op used as a callback cannot require capabilities (E-FN-CAP). It is C that enters the callback, and C has no capabilities to hand over. Work needing capabilities is done outside the callback; inside, it only computes.

Passing owned τ to an extern moves the responsibility to dispose of it to C. This side’s obligation ends there, and whether it is later released is not verified. C functions taking an unfixed number of arguments after the fixed ones can be called with a variadic . clause, but contracts do not reach those arguments, and the opposite direction (C calling our variadics) does not exist.

module variadic .

rem C's char*; unsafe_ptr is a qualifier placed before a type
newtype cstr unsafe_ptr u8 .

unsafe extern proc c_printf do
  input k cap c .
  input fmt cstr .
  output i32 .
  effects unsafe .
  rem takes an unspecified number of arguments after the fixed ones
  variadic .
  link printf .
end

rem after the fixed argument (the format) one more value, 42, is passed; neither type checks nor contracts reach it
unsafe proc report input k cap c . output i32 . effects unsafe .
do
  return c_printf k (cstr_of "sum=%d\n\0") 42 .
end

$ lowentc --check variadic.low
== check: ok ==

• newtype cstr unsafe_ptr u8 . turns C’s char* into a named type. unsafe_ptr is not a type used on its own but a qualifier placed before a type.
• The variadic . clause says “takes more after the fixed arguments”, and link printf . writes the C name. The 42 at the call site follows the fixed arguments, so neither type checks nor contracts reach it. The classic C defect of a format not matching its arguments is not stopped here, and that is why unsafe is attached.
• cstr_of "…\0" views a string literal ending in a zero byte as a C string. The VM cannot call C, so this example is only checked; built natively, it prints sum=42.

29.5 Common mistakes#

module mistake_noeffect .
rem expect: E-FFI-NOEFFECT

rem ✘ no effects line --- callers cannot learn from the head what they take on
unsafe extern proc c_area do
  input k cap c .
  input w i64 .
  input h i64 .
  output i64 .
  link "lw_c_area" .
end

$ lowentc --check mistake_noeffect.low
mistake_noeffect.low:5:0 E-UNSAFE-UNUSED: this op is marked `unsafe` but declares no `unsafe` effect. An `unsafe` that buys nothing is a FALSE ALARM — and false alarms are how real ones stop being read. Drop the modifier
mistake_noeffect.low:5:0 E-FFI-NOEFFECT: this op calls C and declares no effect. The effect row is how a CALLER learns what it is taking on; C that hides in a clean signature is the hidden cost this language exists to remove (declare at least `effects unsafe`)

module mistake_nolink .
rem expect: E-FFI-LINK

rem ✘ no `link` clause --- nothing says which C symbol is called
unsafe extern proc c_area do
  input k cap c .
  input w i64 .
  input h i64 .
  output i64 .
  effects unsafe .
end

unsafe proc area_twice input k cap c . input w i64 . input h i64 . output i64 .
  effects unsafe .
do
  return add (c_area k w h) (c_area k w h) .
end

$ lowentc --check mistake_nolink.low
mistake_nolink.low:5:0 E-FFI-LINK: an `extern` op does not say which C symbol it calls. Write `link "strlen" .` (and `link "sin" from "m" .` when it lives in a library). The C name is a promise made to another language, so the author writes it: derived from the op name it would change the moment the op is renamed, with nothing in the source saying so (RFC-0063)

module mistake_callerunsafe .
rem expect: E-UNSAFE-UNDECLARED

unsafe extern proc c_area do
  input k cap c .
  input w i64 .
  input h i64 .
  output i64 .
  effects unsafe .
  link "lw_c_area" .
end

rem ✘ calls an op that calls C, but leaves out the `unsafe` marker
proc area_twice input k cap c . input w i64 . input h i64 . output i64 .
  effects unsafe .
do
  return add (c_area k w h) (c_area k w h) .
end

$ lowentc --check mistake_callerunsafe.low
mistake_callerunsafe.low:14:0 E-UNSAFE-UNDECLARED: this op declares the `unsafe` EFFECT but is not marked `unsafe`. The effect says WHAT it does; the modifier says WHO takes responsibility. Write `unsafe proc …` — an unsafe op that nobody signed for is exactly the hole the discipline exists to close

module mistake_cbplain .
rem expect: E-FN-NOTEXPORT

fn by_value input a i64 . input b i64 . output i64 .
  requires ge a -1000000 .
  requires le a 1000000 .
  requires ge b -1000000 .
  requires le b 1000000 .
do
  return sub a b .
end

unsafe proc callback_addr input k cap c . output u64 . effects unsafe .
do
  rem ✘ tries to hand C the address of an ordinary op --- it has no door C can call
  let f u64 be unsafe_fn by_value .
  return f .
end

$ lowentc --check mistake_cbplain.low
mistake_cbplain.low:14:1 W-EFFECT-OVER: this op DECLARES `unsafe` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)
mistake_cbplain.low:16:0 E-FN-NOTEXPORT: `unsafe_fn <op>` needs an `export extern` op — only those have a C-callable symbol whose entry checks the contract (RFC-0066 §2). A plain op has no address C can call

module mistake_cbcap .
rem expect: E-FN-CAP

rem the op meant as a callback takes a capability as input
export extern fn cmp_logged input out cap io . input a i64 . input b i64 . output i64 .
  requires ge a -1000000 .
  requires le a 1000000 .
  requires ge b -1000000 .
  requires le b 1000000 .
do
  return sub a b .
end

unsafe proc callback_addr input k cap c . output u64 . effects unsafe .
do
  rem ✘ when C calls back, it has no capability to hand over
  let f u64 be unsafe_fn cmp_logged .
  return f .
end

$ lowentc --check mistake_cbcap.low
mistake_cbcap.low:15:1 W-EFFECT-OVER: this op DECLARES `unsafe` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)
mistake_cbcap.low:17:0 E-FN-CAP: `unsafe_fn <op>` names an op that requires a CAPABILITY (a `cap` parameter) — but a callback is entered BY C, and C has no capability to hand it. Do the capability-needing work OUTSIDE the callback and keep the callback pure or limited-effect (RFC-0066)

29.6 This chapter’s syntax at a glance#