Claude
3bd81097e1
The header scan (Captain Bob, 2026-11-10): 788 source files -- 351 with the
SL-1.0 header, 12 with the old name (docs/working/experiments, kept by
ruling), 31 under someone else's licence (tools/kconfig, Linux's, GPL-2.0:
kept), and 394 with none. Ruled: the SPDX form; capsules (.4th, .f18) and
proofs (.thy) left for a ruling of their own (mkcapsule's 64x16 block format,
content-addressed capsules).
253 files now begin
SPDX-License-Identifier: LicenseRef-Starship-1.0
Copyright (c) 2023-2026 Robert A. James
as a /* */ block (C, headers, assembly, linker scripts) or # lines (scripts,
Makefiles, Kconfig; below a shebang or a coding line); tools/mkcapsule.c,
which had the copyright line, gets the SPDX line only.
Not touched: docs/working/ (archive and old campaign material, as the
ruling kept the experiments); v4/system/post_cases.c (generated by
v4/tools/mkpost.py, "do not edit" -- the generator has the header).
Comments only: the kernel builds on amd64, aarch64, riscv64; make -C v4
test-32: 39 programs, 0 failures; every changed script parses.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
36 lines
1.7 KiB
C
36 lines
1.7 KiB
C
/* SPDX-License-Identifier: LicenseRef-Starship-1.0
|
|
* Copyright (c) 2023-2026 Robert A. James
|
|
*/
|
|
/* umul.h -- unsigned multiply fixing UM* under D-3 constraints.
|
|
*
|
|
* DECOMPOSITION.md section 4 first said of UM* (since rewritten to be exact over
|
|
* the full range; see test_foundation.c): "NEEDS REVISION: written for the carry-keeping
|
|
* +* that D-3 rejected. With plain F18 +* the carry out of T is lost, so this
|
|
* is only correct when the partial sums never overflow T (operands below 2^31).
|
|
* A full-range UM* needs a correction step; to be rewritten and proven on the
|
|
* golden model."
|
|
*
|
|
* D-3 states: "Plain F18 semantics. The carry out of T is not kept."
|
|
* The +* defined in the F18 shifts T:A right; the add is T <- T+S when bit 0
|
|
* of A was set, but any carry out of that addition is discarded (not shifted
|
|
* into the high part). That means UM* as written only works for inputs whose
|
|
* partial products don't generate a carry beyond T's width during the loop.
|
|
*
|
|
* We need a correct full-range unsigned multiply (u1*u2 -> ulo, uhi) that is
|
|
* correct for all cell-width values of u1,u2, expressed in terms of the v4
|
|
* primitives or at least specified precisely for the golden model. Since
|
|
* we're building the golden model in C first, the canonical implementation is
|
|
* the width-correct C multiplication split into high/low halves at V4_CELL_BITS.
|
|
* This header provides both: a reference C implementation (for verification)
|
|
* and a documented form that matches D-3's +* constraint.
|
|
*/
|
|
#ifndef V4_UMUL_H
|
|
#define V4_UMUL_H
|
|
|
|
#include "v4/cell.h"
|
|
|
|
/* Unsigned multiply: (u1, u2) -> (ulo, uhi). Full range, width-correct. */
|
|
void v4_umul(v4_ucell u1, v4_ucell u2, v4_ucell *ulo, v4_ucell *uhi);
|
|
|
|
#endif /* V4_UMUL_H */
|