Embedded C target

Embedded C target#

hawk can emit a kernel as freestanding C for a safety-critical embedded build: a <name>.c and a <name>.h that include nothing from hawk, aether or eagle, only <math.h>, <stdint.h>, <stdbool.h>, <stddef.h> and <float.h>. The text follows MISRA C:2012 (with its amendments), is serial, and under the native host profile it is bit-identical to the host build of the same kernel: the C is built with -ffp-contract=off, every reduction and product follows aether’s evaluation order, and the scalar math is libm.

The target id is c. It sits beside host and cuda; their emitted text is unchanged. hawk.embedded is the engine; hawk.build(..., targets=("c",)) is the same engine behind the build door.

Quickstart#

One kernel, straight to a directory:

import hawk
from hawk import Mutable, Param, Vector
from hawk.math import norm


@hawk.kernel
def drag(state: Vector[3], rho: Param, out: Mutable[Vector[3]]):
    out = -rho * state * norm(state)

art = hawk.embedded.export(drag, "out/")
art.c_path, art.h_path, art.report_path   # drag.c, drag.h, drag.embedded.json

For a runnable walk-through (export, the header and report, a bit-for-bit comparison with the host build, and the refusals), see the embedded C example.

or through the build door, alone or beside the native targets:

hawk.build([drag], "out/", targets=("c",))
hawk.build([drag], "out/", targets=("host", "c"))

export writes three files: <name>.c, <name>.h and <name>.embedded.json (the report). targets=("c",) writes the same three plus the build stamp, and neither a manifest nor a sidecar: the c target never enters the eagle manifest (exec_targets lists the native targets only), so hawk.load (given the directory) and hawk.artifact.plugins (given the build’s Bundle) refuse a c-only build and say it is source for an embedded build. A profile reaches the door as embedded_profile=; it is also a term of the build’s cache key.

Compile the output with any C99 compiler. Keep floating-point contraction off, or the result is not the host build’s:

cc -std=c99 -ffp-contract=off -O2 -c out/drag.c -o drag.o

The entry is <name>_c(args, base, count, n_samples). It returns a status instead of trusting its inputs:

status	value	meaning
`HAWK_OK`	0	the partition ran
`HAWK_E_NULL`	1	the args pointer or a plane pointer is null
`HAWK_E_RANGE`	2	`0 <= base <= n_samples` or `0 <= count <= n_samples - base` failed, or a runtime length is below 1

On an error the entry returns before it touches any plane. It is re-entrant and allocation-free, with one exit point.

The ABI contract#

drag.h, exactly as hawk.embedded.render(drag).header returns it (export writes it to drag.h) for the drag kernel above (float64, default profile):

/* drag.h -- generated by hawk 0.5.0; do not edit.
 * TRACEABILITY:
 *   kernel         drag
 *   hawk version   0.5.0
 *   walk digest    bcc450195db6caa95fb54687b8b395c13f1bcffbf63d1c0ef69191cda2624a84
 *   kernel sha256  dff29da0d5195f0021bb40af3d7f8744baa15a824f4b2e59a2cccd565a50bed5
 *   scalar mode    float64
 *   target         c, MISRA C:2012+AMD, C99 dialect, serial
 *   profile        EmbeddedProfile(max_trips=None, max_ops=None, max_stack_bytes=None, fp_domain='record', index_policy='clamp', require_cppcheck=False, c_std='c99')
 *   aether core    aether-c/1
 * BUDGETS (per sample, worst case):
 *   loop trips     0
 *   ops            arith32 0, arith64 14, special32 0, special64 0, loads 3, gathers 0, chain32 0, chain64 3, chainSpecial32 0, chainSpecial64 0, stores 3
 *   fp64 ops       14
 *   static bytes   tapes 0, carries 0, temporaries 72, total 72
 *   libm           sqrt
 * INTERFACE CONTRACT: planes are SoA; rank-1 extent N stores component c of sample i at
 *   base[(c * n_samples) + i]; rank-2 (R,C) at base[(((r*C)+c) * n_samples) + i]; rank-0 at
 *   base[i]. The pitch is ALWAYS n_samples, also for a partition [base, base+count).
 *   A runtime-length plane carries its length in the int64_t field after its pointer.
 *   field      role     dir  dtype shape  init-by-caller
 *   mut_out    mutable  out  f64   (3,)   no
 *   vin_state  vec_in   in   f64   (3,)   yes
 *   uni_rho    uniform  in   f64   ()     yes (by value)
 *   drag_c() validates args and every pointer, 0 <= base <= n_samples and
 *   0 <= count <= n_samples - base, returning HAWK_E_NULL / HAWK_E_RANGE untouched otherwise.
 *   Re-entrant, allocation-free. */
#ifndef HAWK_DRAG_H
#define HAWK_DRAG_H
#include <stdint.h>
#include <stddef.h>
#ifndef HAWK_EMBEDDED_TYPES
#define HAWK_EMBEDDED_TYPES 64
typedef double  hawk_real_t;
typedef int64_t hawk_int_t;
typedef enum { HAWK_OK = 0, HAWK_E_NULL = 1, HAWK_E_RANGE = 2 } hawk_status_t;
#elif HAWK_EMBEDDED_TYPES != 64
#error "drag.h: float64 unit; another hawk header in this build defined hawk_real_t at a different width"
#endif
typedef struct {
    hawk_real_t*       mut_out;    /* mutable out  Vector[3] SoA, pitch n_samples */
    const hawk_real_t* vin_state;  /* vec_in  in   Vector[3] SoA, pitch n_samples */
    hawk_real_t        uni_rho;    /* uniform in   Scalar    by value */
} drag_args_t;
hawk_status_t drag_c(const drag_args_t* args, int64_t base, int64_t count, int64_t n_samples);
#endif

The TRACEABILITY digests shown are those of the test suite’s drag kernel (tests/_kernels.py); a kernel you define carries its own walk and source digests.

The contract the comment states is part of the interface.

Layout. Every plane is structure-of-arrays. A rank-1 extent N stores component c of sample i at base[(c * n_samples) + i]; a rank-2 (R, C) plane stores component (r, c) at base[(((r*C)+c) * n_samples) + i]; a rank-0 plane at base[i]. The pitch is always n_samples, also when the call covers only the partition [base, base + count). This is the layout of a NumPy array of shape (prod(shape), n) in C order.

Runtime lengths. A plane whose length is a runtime value (a lookup table, a wide input or output) carries it in the int64_t field after its pointer, <field>_len. The entry requires it to be at least 1 (zero is refused too, with HAWK_E_RANGE); indices into it are clamped to it (see the verify pass).

Directions. The header’s interface table and the report’s interface rows give each field a direction, and the caller must initialise every field marked init-by-caller:

role	direction	init by caller
`per_sample`, `vec_in`, `mat_in`, `lookup`, `wide_in`, `uniform`	in	yes
`mutable`	out; inout when the kernel reads it before writing	no; yes when inout
`mutable`, `wide_out` on the sample’s own column, under a mask guard	inout (a masked sample keeps the prior value; the reason names the guard’s masks)	yes
`out` (a tape write’s plane)	inout (one row is written per launch, the rest kept)	yes
`wide_out`, `accum_out` on the sample’s own column	out	no
`accum_out` on the sample’s own column, under a mask guard	inout (one partial per sample; a masked sample keeps its own)	yes (zeroed)
`wide_out` written at a computed index	inout (the rows written are replaced, the rest kept)	yes
`accum_out` written at a computed index	inout (`+=` into the prior value)	yes (zeroed)
`terminated`	in; inout when it is the finish mask	yes
`finished_count`, `dispatchN_mix`	inout	yes (zeroed)

A store is under a mask guard when the kernel binds, in the terminated role, a mask its kind’s guard names (the default guard names terminated; a finishing kernel binds its finish mask there too). The generated loop then skips a masked sample entirely, exactly as the host build does, so the plane keeps whatever the caller put there. Every interface row carries the bound mask fields as guard (empty for an unguarded kernel), and the header’s contract prints a line for each writable mutable or wide_out field of a guarded kernel naming them, for example

 *   mut_y: masked samples keep the prior value (guard: trm_terminated); the caller initialises it.

Partials. An accum_out written on the sample’s own column holds one partial per sample, length n_samples. Nothing in a standalone build folds them; the caller reduces the plane. The interface row says layout: "partials" and gives that reason. Under a mask guard a masked sample keeps its partial, so the caller zeroes the plane first, then reduces it.

The mix plane. A dispatch kernel counts how often each branch ran in a uint32_t plane of K cells (one per branch), incremented by the generated code; the caller zeroes it before the first call.

Types. hawk_real_t is double or float by the scalar mode, hawk_int_t is int64_t; an Index input plane is an int32_t* (an Index[int64] one is int64_t*), widened where the body reads it. The three typedefs and the status enum sit behind HAWK_EMBEDDED_TYPES, so several hawk headers of one width coexist in a build; a header of another width fails with #error. The .c also checks the sizes with _Static_assert, but only under C11 (__STDC_VERSION__ >= 201112L): a strict -std=c99 build compiles the asserts out and relies on the HAWK_EMBEDDED_TYPES guard alone.

The verify pass#

Before anything is emitted, hawk.embedded.verify reads the IR. It refuses what the C target does not build, then computes (without refusing) the report’s numbers, and a profile turns chosen numbers into refusals.

What it checks.

Bounds and budgets. Worst-case loop trips per sample (nested loops multiplied, a runtime-count loop at its static trip, which the C clamps to), the per-sample operation counts from kernel_cost, and the static bytes: tapes, loop carries and the named temporaries the renderer declares.
Index safety. Every runtime index is classified proven or clamped. A table read’s length is a runtime value, so a gather index is clamped (hawk_clamp_index); a parameter cell, a loop index with a static range inside the extent, and a tape ordinal are proven and emit the raw index. Clamping changes nothing in an execution the C++ build defines, so the bit identity holds.
Floating-point domain. Each divisor, sqrt, rsqrt, log*, acos, asin, atanh, acosh and pow base is reported with whether its operand is provably in the domain (safe, with the reason, or unknown). The proof reads signs off the operand, for example positive (a positive literal, 1 + x*x, x*x + c or norm(v) + c with c positive), nonneg (exp, which underflows to +0, abs, norm, dot(v, v), x*x, a zero literal, sqrt of a nonneg value) or unknown (anything else, sqrt of an unknown value among it). A divisor, log* and rsqrt need positive, sqrt needs nonneg. A sign claim holds for non-NaN operands: a NaN propagates identically on both sides (clip passes it through), so the report speaks for every value that is a number.
Interface. One row per slot: field, role, direction, dtype, shape, layout, runtime length, init by caller, guard (the bound mask fields that skip a sample, the same on every row; empty when unguarded), reason.

The profile. EmbeddedProfile carries the opt-in caps and policies. The default refuses only what the target cannot build.

field	default	effect
`max_trips`	`None`	refuse above this many worst-case loop trips per sample (`budget.trips`)
`max_ops`	`None`	refuse above this many arithmetic and special operations per sample (`budget.ops`)
`max_stack_bytes`	`None`	refuse above this many static bytes (tapes, carries, temporaries; `budget.stack`)
`fp_domain`	`"record"`	`"refuse"` refuses an `unknown` domain site (`fp.domain`)
`index_policy`	`"clamp"`	`"refuse"` refuses any `clamped` index site (`index.unproven`)
`require_cppcheck`	`False`	an absent cppcheck raises instead of being recorded as skipped
`c_std`	`"c99"`	the dialect the consumer compiles under, `"c99"` or `"c11"`

The refusal shape. Every refusal is a HawkError naming the kernel, the node, the rule, why, and what to do:

'<kernel>': the C target refuses node <pos> (<kind>) under <rule>: <why>; <fix>

<pos> is the node’s index in the walk, or loop<i>.<k> for a node in a loop body; a refusal about the whole kernel (active_set, compensated, two_path, budget.ops, budget.stack) uses the position kernel. An audit refusal has a different shape and no fix clause: '<kernel>': the C target refuses line <N> under audit.<kind>: <text>. Rules are unsupported.<feature>, budget.trips, budget.ops, budget.stack, index.unproven, fp.domain and audit.<kind>.

Refused features. Checked first, and always:

feature	why	fix
`random`	a random draw lowers to aether’s counter-based generator	draw in the caller and pass the values in as a plane
`raw_device`	a `raw_device` block splices C++ text	spell the block with `hawk.math`
`sample_reduction`	a reduction over lanes (`hawk.sum(x)`, `hawk.max(x)`, …) needs the wrapper’s cross-sample fold	commit the own column and reduce in the caller
`cross_sample_at`	`u.at(i)` reads another lane’s value, which a partition call may not hold	pass the values the kernel needs as a `Table` plane
`active_set`	an index map (an active-set guard or a lane set) is a plane the C entry does not take	run without the index map (the plain mask guard)
`segmented`	a segmented dispatch is a per-unit split	export each branch as its own kernel
`compensated`	the compensated sink policy commits a correction plane	use the plain sink policy
`fused_lanes`	a fused lane group is composed for a launching runtime	export each lane as its own kernel
`two_path`	an automatic kernel branches once per launch on a runtime step word	export `kernel.step` or `hawk.steps(step, K)` with an integer `K`
`int_libm`	a libm function on an `Int` operand takes an implicit double round-trip	use `maximum(minimum(i, hi), lo)` (`Int` min, max and abs are allowed) or convert to `Real` explicitly
`scattered_tensor_accum`	a scattered accumulate of a rank>=1 value is not lowered (hawk’s tracer refuses it first)	declare one scalar accumulate plane per component
`zero_trip_loop`	a loop that never runs is dead code (MISRA C:2012 Rule 14.3)	give the loop at least one trip
`tensor_select_cond`	a select on a rank>=1 condition picks per component	select per component with a rank-0 condition

After rendering, a text audit reads the .c and .h (rule audit.<kind>): no allocation, goto, stdio, union, volatile, #pragma, C++ casts or namespaces, no launch-geometry token; only the whitelisted includes; at most one break; per for body; every switch with a default: and a break; in each clause; no unreferenced helper; distinct external identifiers in 31 characters; block comments only; no brace initialiser. A hit refuses the export before any file is written.

The report file#

<name>.embedded.json is indented JSON, always in this key order (hawk.embedded.REPORT_KEYS):

key	holds
`kernel`	the kernel name
`generator`	`"hawk.embedded/1"`
`hawk_version`	`hawk.__version__`
`walk_digest`	the digest of the traced walk
`source_digest`	sha256 of the kernel’s source (`Kernel.source_digest`), or `"unavailable"` for a hand-built or derived kernel
`scalar_mode`	`"float64"` or `"float32"`
`profile`	`repr` of the `EmbeddedProfile`
`interface`	one row per slot, as above
`budgets`	`max_trips`, `ops`, `fp64_ops`, `static_bytes` (tapes, carries, temporaries, estimate, total), `loops`
`indices`	every runtime index site with its `proven` or `clamped` status and reason
`fp_domain`	every domain-sensitive site and its verdict (a sign claim holds for non-NaN operands)
`fp_equality_sites`	walk positions that compare reals with `==` or `!=`
`int_division_sites`	positions of integer divisions
`int_ub_sites`	positions of every `Index` `+`, `-`, ``, negation and true division `/`: infix in the C++ build (signed overflow, a zero divisor and `MIN / -1` undefined), defined through `hawk_i64_` in the C
`literal_specials`	`NAN` / `INFINITY` literals the unit spells
`libm`	every libm function the unit calls, sorted
`helpers`	the hawk-owned helper functions emitted
`core`	the aether core functions inlined
`core_version`	the aether core’s version, `aether-c/1`
`deviations`	the deviations table below, plus one `float-equality` note carrying the `fp_equality_sites` list and one `defined_where_cpp_is_ub` note carrying the `int_ub_sites` list, each when there are any
`unsupported_checked`	the refused features that were checked
`audit`	`{"hits": []}` (a hit refuses before the report exists)
`checks`	the compiler and cppcheck runs

There are no timestamps and no temporary paths: exporting the same kernel again writes the same bytes, and the header carries the same walk and source digests.

Toolchain and checks#

export runs the checks (check=True), and hawk.embedded.check runs them on a rendered source. The C compiler runs twice, -std=c99 and -std=c11, with -pedantic -Wall -Wextra -Wconversion -Wsign-conversion -Wdouble-promotion -Werror -fsyntax-only; then cppcheck runs with the MISRA addon (--addon=misra --std=c99 --language=c --enable=warning,style). Any compiler diagnostic or cppcheck finding raises a HawkError with the command and output. The .c and .h are written first, so a failing check leaves them for inspection; the report is written only after the checks pass.

The C compiler is the first of: $HAWK_CC (must resolve); the C sibling of $HAWK_CXX (g++-13 becomes gcc-13, clang++ becomes clang), so the C and C++ checks agree on one toolchain; the first word of $CC; cc, clang, gcc on PATH; a zig cc wrapper from the ziglang wheel. cppcheck is $HAWK_CPPCHECK, else cppcheck on PATH. If it is absent the report records checks.cppcheck as skipped, and EmbeddedProfile(require_cppcheck=True) raises instead. The repository’s own test rows fail rather than skip without cppcheck: a skipped check certifies nothing.

Deviations. Deviations are applied as cppcheck --suppress flags and recorded in the report; they are never written as comments in the C.

rule	category	reason
`misra-c2012-8.7`	advisory	cppcheck analyses one translation unit; the entry function and its args struct are the unit’s API, referenced from the consumer’s unit, so the single-unit heuristic cannot see the reference
`misra-c2012-9.3`	required	a checker false positive: the addon reads a function-call initialiser of a struct with an array member as a partial brace initialiser. The emitted C has no brace initialiser, and the text audit (`audit.init`) refuses any `= {` in the `.c`, so the suppression cannot hide a real one
`misra-c2012-2.3`	advisory	the `HAWK_EMBEDDED_TYPES` block is the same text in every hawk header of a build; a unit that reads no integer still declares `hawk_int_t` for the units beside it, and the C11 size assert that uses it is compiled out under the C99 the checker analyses

Beyond the cppcheck table, a reviewer should know the unit does the following by design. The kernel’s own == and != on reals are kept (they mirror the host build bit for bit) and every site is listed in fp_equality_sites with a float-equality note in deviations. NAN and INFINITY appear as literals when the kernel writes them and are listed in literal_specials. The integer helpers wrap in the unsigned twin type and convert back to the signed type; the conversion of an out-of-range unsigned value is implementation-defined in C, which Directive 1.1 asks a project to document. Int32 and UInt32 arithmetic and every Index //, % and shift go through the same helpers in the host build, so the two agree everywhere. The C++ build spells an Index +, -, *, negation and true division / infix, where signed overflow, a zero divisor and MIN / -1 are undefined (the C’s hawk_i64_div returns 0 and MIN there), so for those the two builds agree wherever the C++ is defined; the defined_where_cpp_is_ub note in deviations lists every such site (int_ub_sites). The size asserts are guarded by the C11 version test, as above.

Bit identity#

The C unit is checked against the host build of the same kernel, in the same scalar mode, built under the native host profile, on the same machine. The comparison is on bytes (tobytes()), never a tolerance, over the corpus of emitted kernels, the loop forms (head, middle and tail breaks, runtime counts, hawk.steps with a finish, vjp, tapes), dispatch with the mix plane, mask guards (a masked sample keeps the caller’s value on both sides) and the integer kernels on their boundary grids. An Index +, -, *, negation and true division / are compared only where the C++ is defined (see int_ub_sites); at the overflow points the C alone is checked against NumPy’s int64 wrapping, and at a zero divisor and MIN / -1 against hawk_i64_div’s defined results. The conditions: -ffp-contract=off on both sides, the C compiler of the same vendor as the host compiler (hence the $HAWK_CXX sibling rule), and libm scalar math. abs, minimum and maximum on an Index use integer helpers with NumPy semantics in the C; the host build does not compile them (aether’s abs/fmin/fmax take only reals), so they have no host twin and sit outside the comparison. Without the native extension (for example on a Mac), a weaker row compares the C against the interpreter within a band.

What is deferred#

Not built, and refused by name: random draws (they need aether’s Philox generator in C), reductions over lanes (hawk.sum), cross-lane reads (.at), active-set guards, segmented units, the compensated sink policy, fused lanes and automatic (two-path) kernels. Nothing is threaded: scattered accumulates are plain +=. The scalar reference functions (every fold, product and component-wise operation) come from aether_dsc.c_core, version aether-c/1, which hawk inlines verbatim into the unit; hawk requires aether-dsc>=0.2.7 for it.