Std.Flag

1module Std.Flag
2
3-- Nat-encoded boolean flags (zero = false, succ zero = true): not / and / or,
4-- and byte equality as a flag. Lifted VERBATIM out of Inference.Runtime by the
5-- R4b reroute (2026-09-09, tools/refactor/extract_contract.py, reconstruction
6-- proof): the SM86 sampling realization and the float32 bit-pattern contract
7-- both need exactly these, so they belong in foundation (RFC S2 standard =
8-- numbers). The `inference` prefix of the def names is the lifted identity —
9-- renaming is the later namespace chunk. Inference.Runtime imports this module
10-- and never redeclares the defs. Imports nothing; must stay that way (R6/R6b/
11-- R6c walls).
12def inferenceFlagNot =
13  (lambda unrestricted flag : Nat .
14    (nat-eliminate
15      (lambda unrestricted current : Nat . Nat)
16      (succ zero)
17      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
18      flag))
19
20def inferenceFlagAnd =
21  (lambda unrestricted left : Nat .
22    (lambda unrestricted right : Nat .
23      (nat-eliminate
24        (lambda unrestricted current : Nat . Nat)
25        zero
26        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
27        left)))
28
29def inferenceFlagOr =
30  (lambda unrestricted left : Nat .
31    (lambda unrestricted right : Nat .
32      (nat-eliminate
33        (lambda unrestricted current : Nat . Nat)
34        right
35        (lambda unrestricted predecessor : Nat .
36          (lambda unrestricted induction : Nat . (succ zero)))
37        left)))
38
39def inferenceByteEqual =
40  (lambda unrestricted left : Byte .
41    (lambda unrestricted right : Byte .
42      (inferenceFlagNot (inferenceFlagOr (byte-less-than left right) (byte-less-than right left)))))