# 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:

```python
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](examples/05_embedded_c_target).

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

```python
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](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:

```bash
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.

(abi)=
## 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):

```c
/* 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](verify)).

**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

```text
 *   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.

(verify)=
## 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:

```text
'<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.

(report)=
## 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.