fix(panel-clades): #147's remaining ABI checks and docs, without the K9! preambles

panel-clades/scripts/check-abi.sh

@@ -23,8 +23,11 @@
 OUT="_build/check-abi"
 WRONG_REASON='Undefined name|Couldn.t parse|Parse error|not in the source directory|Can.t find import|Module .* not found|INTERNAL ERROR|does not match file name'
 fail=0
+# Print the supplied success message to standard output with a PASS prefix.
 pass() { printf 'PASS: %s\n' "$1"; }
+# Print the supplied failure message and set fail=1, then continue checking.
 err()  { printf 'FAIL: %s\n' "$1"; fail=1; }
+# Print the supplied failure message and terminate the gate with exit status 1.
 die()  { printf 'FAIL: %s\n' "$1"; exit 1; }
 
 command -v idris2 >/dev/null || die "idris2 not on PATH (a gate that cannot run must not report OK)"
@@ -33,15 +36,21 @@
 rm -rf "$OUT"; mkdir -p "$OUT"
 
 IPKG="src/abi/panel-clades-grades.ipkg"
-for f in src/abi/PanelClades/ABI/*.idr; do
+# Enumerate into a file, not a process substitution, so a failing find is seen.
+abi_list="$OUT/abi-files"
+find src/abi/PanelClades -type f -name '*.idr' -print0 > "$abi_list" \
+  || die "could not enumerate .idr files under src/abi/PanelClades"
+mapfile -d '' -t abi_files < "$abi_list"
+[ "${#abi_files[@]}" -gt 0 ] || die "no .idr files found under src/abi/PanelClades"
+for f in "${abi_files[@]}"; do
   mod="$(printf '%s' "${f#src/abi/}" | sed 's|\.idr$||; s|/|.|g')"
   grep -qE "^[[:space:]]*(modules[[:space:]]*=|,)[[:space:]]*${mod//./\\.}[[:space:]]*$" "$IPKG" \
     || err "$mod is not listed in $IPKG (it would never be checked)"
 done
-if grep -nE '\b(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO)\b' src/abi/PanelClades/ABI/*.idr; then
-  err "escape hatch in src/abi/PanelClades/ABI (lines above)"
+if grep -nE '\b(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO)\b' "${abi_files[@]}"; then
+  err "escape hatch in src/abi/PanelClades (lines above)"
 fi
-[ "$fail" -eq 0 ] && pass "every PanelClades/ABI module is listed in the ipkg; no escape hatches"
+[ "$fail" -eq 0 ] && pass "every PanelClades module is listed in the ipkg; no escape hatches"
 if bash scripts/gen-budgets.sh --check; then
   pass "Budgets.idr is current with the clade configs"
 else

panel-clades/scripts/gen-budgets.sh

@@ -27,12 +27,17 @@ set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 OUT="src/abi/PanelClades/ABI/Budgets.idr"
 mode="${1:-write}"
+# Write the supplied diagnostic to standard error and exit with status 1.
 fail() { printf 'gen-budgets: %s\n' "$1" >&2; exit 1; }
 
 # kebab-case clade id -> lowerCamelCase Idris name
 camel() { printf '%s' "$1" | sed -E 's/-([a-z0-9])/\U\1/g'; }
 
 nat='[0-9]+'
+# Emit the Idris budget module to standard output from clade resources blocks.
+# Exit with status 1 if a block fails the state, crossing or DESIGNED status
+# checks, or if no config declares resources.  Configs without resources are skipped.
+# Output may be partial on failure.
 emit() {
   cat <<'HEADER'
 -- SPDX-License-Identifier: MPL-2.0
@@ -68,13 +73,14 @@ HEADER
     grep -qE '^[[:space:]]*resources[[:space:]]*=' "$cfg" || continue
     dir="$(basename -- "$(dirname -- "$cfg")")"
     id="$(camel "$dir")"
-    state="$(grep -E "^[[:space:]]*state = \{ peak = $nat, drift = $nat, budget = $nat \},[[:space:]]*$" "$cfg" || true)"
-    crossing="$(grep -E "^[[:space:]]*crossing = \{ loss = $nat, tolerance = $nat \},[[:space:]]*$" "$cfg" || true)"
+    block="$(sed -n '/^[[:space:]]*resources[[:space:]]*=/,/^[[:space:]]*},[[:space:]]*$/p' "$cfg")"
+    state="$(printf '%s\n' "$block" | grep -E "^[[:space:]]*state = \{ peak = $nat, drift = $nat, budget = $nat \},[[:space:]]*$" || true)"
+    crossing="$(printf '%s\n' "$block" | grep -E "^[[:space:]]*crossing = \{ loss = $nat, tolerance = $nat \},[[:space:]]*$" || true)"
     [ "$(printf '%s\n' "$state" | grep -c .)" -eq 1 ] \
       || fail "$cfg: resources.state is not one line of the form { peak = n, drift = n, budget = n }"
     [ "$(printf '%s\n' "$crossing" | grep -c .)" -eq 1 ] \
       || fail "$cfg: resources.crossing is not one line of the form { loss = n, tolerance = n }"
-    grep -qE '^[[:space:]]*status = "DESIGNED",' "$cfg" \
+    printf '%s\n' "$block" | grep -qE '^[[:space:]]*status = "DESIGNED",' \
       || fail "$cfg: resources.status must be \"DESIGNED\" (nothing measures these values yet)"
     read -r peak drift budget < <(printf '%s\n' "$state" | sed -E 's/.*peak = ([0-9]+), drift = ([0-9]+), budget = ([0-9]+).*/\1 \2 \3/')
     read -r loss tolerance < <(printf '%s\n' "$crossing" | sed -E 's/.*loss = ([0-9]+), tolerance = ([0-9]+).*/\1 \2/')

panel-clades/src/abi/PanelClades/ABI/Foreign.idr

@@ -109,8 +109,10 @@ export
 %foreign "C:panel_clades_load_clade, libpanel_clades"
 prim__loadClade : Bits64 -> String -> PrimIO Bits32
 
-||| Safely load a clade definition into the library context.
-||| Returns Ok on success or an error Result on failure.
+||| Submit a clade identifier to the library.  The current FFI validates
+||| that it is non-empty but does not store a clade definition.
+||| Returns Right () for Ok, Left with a recognised error Result, or
+||| Left Error for an unknown result code.
 export
 loadClade : Handle -> String -> IO (Either Result ())
 loadClade h cladeIdStr = do
@@ -164,7 +166,12 @@ export
 %foreign "C:panel_clades_process_array, libpanel_clades"
 prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
 
-||| Safe array processor
+||| Submit a buffer address and its length in bytes to the library.
+||| The caller must supply memory covering that length; this wrapper
+||| does not check the buffer or its bounds.  The current FFI validates
+||| the pointers and handle state but does not process the contents.
+||| Returns Right () for Ok, Left with a recognised error Result, or
+||| Left Error for an unknown result code.
 export
 processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
 processArray h buf len = do

panel-clades/src/abi/PanelClades/ABI/Grades.idr

@@ -174,7 +174,7 @@ declaredState d = MkHWM (peak d) (drift d) (fits (drift d) (peak d))
 
 ||| A clade's contract built from its config alone.  It typechecks exactly
 ||| when the declared peak fits the declared budget and the declared loss
-||| fits the declared tolerance.
+||| fits the declared tolerance, with declared drift no greater than peak.
 public export
 declaredContract : (cladeId : String) -> (d : DeclaredResources)
                 -> {auto okDrift : So (lte (drift d) (peak d))}

panel-clades/src/abi/PanelClades/ABI/Layout.idr

@@ -40,6 +40,7 @@ data Divides : Nat -> Nat -> Type where
 ||| Units of `unit` bytes needed to cover `size` bytes, counting down a
 ||| fuel bound.  Structural, so it computes during type checking (Nat `div`
 ||| does not).  With fuel ≥ size and unit ≥ 1 the fuel never runs out.
+||| The result is capped at fuel; for unit = 0 and size > 0 it is fuel.
 public export
 unitsFor : (fuel : Nat) -> (size : Nat) -> (unit : Nat) -> Nat
 unitsFor Z        _     _    = Z
@@ -54,11 +55,14 @@ alignUnits _    Z         = Z
 alignUnits size (S align) = unitsFor size size (S align)
 
 ||| Round up to the next alignment boundary: a whole number of units.
+||| Returns a byte count, unchanged when already aligned, or 0 when
+||| the alignment is 0.
 public export
 alignUp : (size : Nat) -> (alignment : Nat) -> Nat
 alignUp size alignment = alignUnits size alignment * alignment
 
 ||| Padding needed after `offset` to reach the next boundary.
+||| Returns bytes; 0 when already aligned or when the alignment is 0.
 public export
 paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
 paddingFor offset alignment = alignUp offset alignment `minus` offset
@@ -105,7 +109,7 @@ public export
 nextFieldOffset : Field -> Nat
 nextFieldOffset f = alignUp (fieldEnd f) f.alignment
 
-||| The furthest byte any field reaches
+||| The greatest field end offset in bytes, or 0 for an empty list.
 public export
 structEnd : List Field -> Nat
 structEnd = foldr (\f, acc => max (fieldEnd f) acc) 0
@@ -114,6 +118,7 @@ structEnd = foldr (\f, acc => max (fieldEnd f) acc) 0
 ||| alignment.  (Fields carry explicit offsets, so this is the C rule; the
 ||| earlier fold here ignored its accumulator and mixed up which field it
 ||| measured.)
+||| Returns bytes; 0 for an empty field list or an alignment of 0.
 public export
 calcStructSize : List Field -> Nat -> Nat
 calcStructSize fields align = alignUp (structEnd fields) align
@@ -149,6 +154,8 @@ data FieldsAligned : List Field -> Type where
 
 ||| Build a layout whose size is computed from its fields; refused when
 ||| the computed size does not cover them.
+||| Returns Right with the layout, or Left "Invalid struct size".
+||| Field offsets are checked separately by `checkCABI`.
 public export
 verifyLayout : (fields : List Field) -> (align : Nat) -> Either String StructLayout
 verifyLayout fields align =
@@ -185,7 +192,8 @@ proveFieldsAligned (f :: rest) =
         Left err => Left err
         Right restProof => Right (ConsField f rest here restProof)
 
-||| Check if layout follows C ABI
+||| Return a proof that every field offset is a multiple of its alignment,
+||| or propagate the first field-alignment error from `proveFieldsAligned`.
 public export
 checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
 checkCABI layout =
@@ -204,12 +212,14 @@ PlatformLayout _ _ = StructLayout
 
 ||| Check a per-platform layout on every platform in `allPlatforms`
 ||| (this used to return `Right ()` without looking).
+||| Returns Right () if all pass, or the first `checkCABI` error in that order.
 public export
 verifyAllPlatforms :
   (layouts : (p : Platform) -> PlatformLayout p t) ->
   Either String ()
 verifyAllPlatforms layouts = go allPlatforms
   where
+    ||| Check the remaining platforms, stopping at the first alignment error.
     go : List Platform -> Either String ()
     go [] = Right ()
     go (p :: ps) = case checkCABI (layouts p) of
@@ -253,6 +263,7 @@ exampleFieldsAligned =
         (DivideBy 2 Refl)
         NoFields))
 
+||| Prove that every field in the example layout is correctly aligned.
 export
 exampleLayoutValid : CABICompliant PanelClades.ABI.Layout.exampleLayout
 exampleLayoutValid = CABIOk exampleLayout exampleFieldsAligned
@@ -262,6 +273,7 @@ exampleLayoutValid = CABIOk exampleLayout exampleFieldsAligned
 --------------------------------------------------------------------------------
 
 ||| Find a field by name.
+||| Returns the first exact match, or Nothing if no field has that name.
 public export
 lookupField : (layout : StructLayout) -> (fieldName : String) -> Maybe Field
 lookupField layout name = find (\f => f.name == name) layout.fields

panel-clades/src/abi/PanelClades/ABI/Types.idr

@@ -93,6 +93,7 @@ resultTag InvalidParam = 2
 resultTag OutOfMemory  = 3
 resultTag NullPointer  = 4
 
+||| Decode a natural-number result tag; return Nothing for tags above 4.
 public export
 resultFromTag : Nat -> Maybe Result
 resultFromTag 0 = Just Ok
@@ -102,6 +103,7 @@ resultFromTag 3 = Just OutOfMemory
 resultFromTag 4 = Just NullPointer
 resultFromTag _ = Nothing
 
+||| Prove that decoding a result's natural-number tag recovers that result.
 public export
 resultTagRetract : (r : Result) -> resultFromTag (resultTag r) = Just r
 resultTagRetract Ok           = Refl
@@ -360,6 +362,7 @@ cladeKindTag Inspector  = 10
 cladeKindTag Bridge     = 11
 cladeKindTag Terminal   = 12
 
+||| Decode a natural-number clade tag; return Nothing for tags above 12.
 public export
 cladeKindFromTag : Nat -> Maybe CladeKind
 cladeKindFromTag 0  = Just Directive
@@ -377,6 +380,7 @@ cladeKindFromTag 11 = Just Bridge
 cladeKindFromTag 12 = Just Terminal
 cladeKindFromTag _  = Nothing
 
+||| Prove that decoding a kind's natural-number tag recovers that kind.
 public export
 cladeKindTagRetract : (k : CladeKind) -> cladeKindFromTag (cladeKindTag k) = Just k
 cladeKindTagRetract Directive  = Refl
@@ -465,6 +469,7 @@ namespace Verify
   ptrLinux : HasSize Linux CTPtr 8
   ptrLinux = SizeIs
 
+  ||| Prove that a WASM pointer occupies 4 bytes in this ABI.
   export
   ptrWasm : HasSize WASM CTPtr 4
   ptrWasm = SizeIs