module Std.Flag

-- Nat-encoded boolean flags (zero = false, succ zero = true): not / and / or,
-- and byte equality as a flag. Lifted VERBATIM out of Inference.Runtime by the
-- R4b reroute (2026-09-09, tools/refactor/extract_contract.py, reconstruction
-- proof): the SM86 sampling realization and the float32 bit-pattern contract
-- both need exactly these, so they belong in foundation (RFC S2 standard =
-- numbers). The `inference` prefix of the def names is the lifted identity —
-- renaming is the later namespace chunk. Inference.Runtime imports this module
-- and never redeclares the defs. Imports nothing; must stay that way (R6/R6b/
-- R6c walls).
def inferenceFlagNot =
  (lambda unrestricted flag : Nat .
    (nat-eliminate
      (lambda unrestricted current : Nat . Nat)
      (succ zero)
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
      flag))

def inferenceFlagAnd =
  (lambda unrestricted left : Nat .
    (lambda unrestricted right : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        zero
        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
        left)))

def inferenceFlagOr =
  (lambda unrestricted left : Nat .
    (lambda unrestricted right : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        right
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat . (succ zero)))
        left)))

def inferenceByteEqual =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (inferenceFlagNot (inferenceFlagOr (byte-less-than left right) (byte-less-than right left)))))