module Std.Word

import Std.Byte
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Std.Foundation
import Std.Codec
import Std.Natural
import Data.Bytes
import Std.Flag

-- Fixed-width integers (Language & Testing Evolution L11, PRD 08 N4). The public
-- vocabulary aliases the existing word owners; U8/U16, the signed I8..I64
-- families, div/rem, bit/shift, comparisons, conversions and byte codecs arrive
-- in L11c/L11d. `Model.Word*` names stay internal until the rename chunk
-- (NUM-009): `Std.Word` is the public name.
-- L11r adds division (StdDivision, stdU8..U64DivRem, stdI8..I64DivRem{Checked,Wrapping})
-- and the checked U32 shifts; see the DIVISION sections below.
-- I64: a signed 64-bit integer as a DISTINCT two's-complement wrapper over the
-- unsigned word (L11g). A distinct type keeps signed and unsigned apart in the
-- type system; the bits are a ModelWord64. Signed comparison/arithmetic (the
-- subtle two's-complement operations) land next; L11g provides the type,
-- construction/projection, and bit-equality.
family StdI64 : Type 0
constructor StdI64Of
field unrestricted stdI64Bits : (family ModelWord64)

end-family

-- I8: a signed 8-bit integer as a DISTINCT two's-complement wrapper over the
-- core Byte (L11i). Its comparisons are the direct core byte primitives (fast).
family StdI8 : Type 0
constructor StdI8Of
field unrestricted stdI8Bits : Byte

end-family

-- I32: a signed 32-bit integer as a DISTINCT two's-complement wrapper over the
-- unsigned ModelWord32 (L11k).
family StdI32 : Type 0
constructor StdI32Of
field unrestricted stdI32Bits : (family ModelWord32)

end-family

-- U16 / I16: the 16-bit widths (L11l). No Model.Word16 exists, so U16 is a
-- two-byte record here (field 0 = low byte, field 1 = high byte); I16 is its
-- distinct two's-complement wrapper.
family StdU16 : Type 0
constructor StdU16Of
field unrestricted stdU16Low : Byte
field unrestricted stdU16High : Byte

end-family

family StdI16 : Type 0
constructor StdI16Of
field unrestricted stdI16Bits : (family StdU16)

end-family

-- DIVISION (L11r, NUM-004). Division is the one arithmetic family with an
-- error EVERY API must report: x / 0 is an error in checked AND wrapping APIs.
-- The signed checked API additionally refuses signedMinimum / -1 (the quotient
-- 2^(width-1) is not representable); the signed WRAPPING API answers it with
-- (signedMinimum, 0), the two's-complement wrap. Quotients truncate toward
-- zero and the remainder carries the DIVIDEND's sign (the C / Rust / x86-64
-- `idiv` convention), so dividend = quotient * divisor + remainder always.
family StdDivisionErrorCode : Type 0
constructor StdDivisionByZero
constructor StdDivisionOverflow

end-family

-- The result of a division: both the quotient and the remainder (one traversal
-- produces both), or the error. The word type is a parameter (one family for
-- every width), the same shape as StdOption / StdResult.
family StdDivision : Type 0
parameter erased stdDivisionWord : Type 0
constructor StdDivisionSucceeded
field unrestricted stdDivisionQuotient : stdDivisionWord
field unrestricted stdDivisionRemainder : stdDivisionWord
constructor StdDivisionFailed
field unrestricted stdDivisionError : (family StdDivisionErrorCode)

end-family

-- Restoring-division state (remainder, quotient, the dividend bits still to
-- shift in), one family per loop width.
family StdU64DivisionState : Type 0
constructor StdU64DivisionStateOf
field unrestricted stdU64DivisionStateRemainder : (family ModelWord64)
field unrestricted stdU64DivisionStateQuotient : (family ModelWord64)
field unrestricted stdU64DivisionStateDividend : (family ModelWord64)

end-family

family StdU32DivisionState : Type 0
constructor StdU32DivisionStateOf
field unrestricted stdU32DivisionStateRemainder : (family ModelWord32)
field unrestricted stdU32DivisionStateQuotient : (family ModelWord32)
field unrestricted stdU32DivisionStateDividend : (family ModelWord32)

end-family

-- Fully qualified public spellings. The shorter aliases remain source
-- compatible, but public APIs can now name every unsigned width consistently
-- without exposing the historical Model.Word implementation owner.
def StdU8 =
  Byte

def StdU32 =
  (family ModelWord32)

def StdU64 =
  (family ModelWord64)

def U8 =
  StdU8

def U32 =
  StdU32

def U64 =
  StdU64

-- WRAPPING arithmetic (modular). Separate from the checked forms so an optimizer
-- may not swap them (§6.4).
def stdU32AddWrapping =
  modelWord32Add

def stdU64AddWrapping =
  modelWord64Add

def stdU64SubtractWrapping =
  modelWord64Subtract

-- CHECKED arithmetic: returns a ModelWord64CheckedResult carrying the
-- overflow/underflow error code on failure.
def stdU64AddChecked =
  modelWord64AddChecked

def stdU64SubtractChecked =
  modelWord64SubtractChecked

-- BITWISE (no overflow concept). L11c.
def stdU64And =
  modelWord64And

def stdU64Xor =
  modelWord64Xor

def stdU64Not =
  modelWord64Complement

def stdU32Xor =
  modelWord32Xor

-- COMPARISON (return the model's boolean flag).
def stdU64Equal =
  modelWord64Equal

def stdU64LessThan =
  modelWord64LessThan

def stdU64IsZero =
  modelWord64IsZero

-- SHIFTS by one.
def stdU64ShiftLeftOne =
  modelWord64ShiftLeftOne

def stdU64ShiftRightOne =
  modelWord64ShiftRightOne

-- CHECKED multiply (returns a ModelWord64MultiplyCheckedResult).
def stdU64MultiplyChecked =
  modelWord64MultiplyChecked

-- U8: the byte-width unsigned integer (L11d). It IS the core `Byte`; its
-- arithmetic is byte-add-with-carry (Std.Byte), and its comparison/conversion
-- are the core byte primitives, exposed here under the width vocabulary. The
-- signed families I8..I64 (two's complement) and U16 land in L11e.
def stdU8Equal =
  (lambda unrestricted a : U8 . (lambda unrestricted b : U8 . (byte-equal a b)))

def stdU8LessThan =
  (lambda unrestricted a : U8 . (lambda unrestricted b : U8 . (byte-less-than a b)))

def stdU8ToNatural =
  (lambda unrestricted a : U8 . (byte-to-nat a))

-- SHIFTS by n and BIT-POSITION queries (L11e), aliasing the proven Model ops.
def stdU32ShiftLeft =
  modelWord32ShiftLeft

def stdU32ShiftRight =
  modelWord32ShiftRight

def stdU32LeastBit =
  modelWord32LeastBit

def stdU32ToNatural =
  modelWord32ToNatural

def stdU64HighBit =
  modelWord64HighBit

def stdU64LeastBit =
  modelWord64LeastBit

-- I64 signed wrapper (L11g): type + construction/projection + bit-equality.
def I64 =
  (family StdI64)

def stdI64FromWord =
  (lambda unrestricted bits : (family ModelWord64) . (constructor StdI64 StdI64Of bits))

def stdI64ToWord =
  (lambda unrestricted value : (family StdI64) .
    (eliminate
      StdI64
      (lambda unrestricted current : (family StdI64) . (family ModelWord64))
      value
      (branch StdI64Of bits . bits)))

def stdI64BitsEqual =
  (lambda unrestricted a : (family StdI64) .
    (lambda unrestricted b : (family StdI64) . (modelWord64Equal (stdI64ToWord a) (stdI64ToWord b))))

-- I64 SIGNED comparison (two's complement, L11h). If the sign bits differ the
-- negative operand is less; if they agree, the unsigned order IS the signed
-- order. Returns the Nat flag ((succ zero) = less). Distinct from stdU64LessThan
-- (NUM-004: signed vs unsigned comparisons are distinct).
def stdI64LessThan =
  (lambda unrestricted a : (family StdI64) .
    (lambda unrestricted b : (family StdI64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
          (modelWord64HighBit (stdI64ToWord b)))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat .
            (nat-eliminate
              (lambda unrestricted current : Nat . Nat)
              (succ zero)
              (lambda unrestricted predecessorB : Nat .
                (lambda unrestricted inductionB : Nat .
                  (modelWord64LessThan (stdI64ToWord a) (stdI64ToWord b))))
              (modelWord64HighBit (stdI64ToWord b)))))
        (modelWord64HighBit (stdI64ToWord a)))))

-- I64 signed add / subtract: in two's complement these ARE the wrapping bit ops
-- on the underlying word (the sign falls out of the representation).
def stdI64AddWrapping =
  (lambda unrestricted a : (family StdI64) .
    (lambda unrestricted b : (family StdI64) .
      (stdI64FromWord (modelWord64Add (stdI64ToWord a) (stdI64ToWord b)))))

def stdI64SubtractWrapping =
  (lambda unrestricted a : (family StdI64) .
    (lambda unrestricted b : (family StdI64) .
      (stdI64FromWord (modelWord64Subtract (stdI64ToWord a) (stdI64ToWord b)))))

-- I8 signed wrapper (L11i): type, construction/projection, bit-equality,
-- two's-complement signed comparison, wrapping add.
def I8 =
  (family StdI8)

def stdI8FromByte =
  (lambda unrestricted bits : Byte . (constructor StdI8 StdI8Of bits))

def stdI8ToByte =
  (lambda unrestricted value : (family StdI8) .
    (eliminate
      StdI8
      (lambda unrestricted current : (family StdI8) . Byte)
      value
      (branch StdI8Of bits . bits)))

def stdI8BitsEqual =
  (lambda unrestricted a : (family StdI8) .
    (lambda unrestricted b : (family StdI8) . (byte-equal (stdI8ToByte a) (stdI8ToByte b))))

-- sign test: a byte is NON-negative iff it is below 128 (flag 1 = non-negative)
def stdI8IsNonNegative =
  (lambda unrestricted value : (family StdI8) . (byte-less-than (stdI8ToByte value) (byte 128)))

-- signed order: if the signs differ the negative operand is less; if they agree
-- the unsigned byte order IS the signed order.
def stdI8LessThan =
  (lambda unrestricted a : (family StdI8) .
    (lambda unrestricted b : (family StdI8) .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (byte-less-than (stdI8ToByte a) (stdI8ToByte b))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : Nat . (succ zero)))
          (stdI8IsNonNegative b))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat .
            (nat-eliminate
              (lambda unrestricted current : Nat . Nat)
              zero
              (lambda unrestricted predecessorB : Nat .
                (lambda unrestricted inductionB : Nat .
                  (byte-less-than (stdI8ToByte a) (stdI8ToByte b))))
              (stdI8IsNonNegative b))))
        (stdI8IsNonNegative a))))

-- wrapping add: the byte sum, carry discarded (two's complement wraps mod 256)
def stdI8AddWrapping =
  (lambda unrestricted a : (family StdI8) .
    (lambda unrestricted b : (family StdI8) .
      (eliminate
        ByteAddResult
        (lambda unrestricted current : (family ByteAddResult) . (family StdI8))
        (byteAddWithCarry (stdI8ToByte a) (stdI8ToByte b) zero)
        (branch ByteAddResultValue sum carry . (constructor StdI8 StdI8Of sum)))))

-- Nat-flag logic ((succ zero) = true). L11k.
-- Both delegate to the one owner (Std.Flag): alpha-equivalent to
-- inferenceFlagAnd/inferenceFlagOr (differing only in the parameter
-- names), found by `alpha-ast duplicates --alpha-equivalent` (L24y).
def stdFlagAnd =
  inferenceFlagAnd

def stdFlagOr =
  inferenceFlagOr

-- U32 comparison primitives (L11k). Model.Word32 is frozen and lacks them, so
-- they are built here over its four byte fields (field 0 = low byte, field 3 =
-- high byte, the carry direction of modelWord32Add) with the core byte ops.
def stdU32IsZero =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . Nat)
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (stdFlagAnd
          (byte-equal b0 (byte 0))
          (stdFlagAnd
            (byte-equal b1 (byte 0))
            (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))

def stdU32Equal =
  (lambda unrestricted a : (family ModelWord32) .
    (lambda unrestricted b : (family ModelWord32) . (stdU32IsZero (modelWord32Xor a b))))

-- the sign bit of the high byte (1 = the byte is >= 128)
def stdU32HighBit =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . Nat)
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (succ zero)
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
          (byte-less-than b3 (byte 128))))))

-- unsigned order: lexicographic from the high byte down
def stdU32LessThan =
  (lambda unrestricted a : (family ModelWord32) .
    (lambda unrestricted b : (family ModelWord32) .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . Nat)
        a
        (branch
          ModelWord32Value
          a0
          a1
          a2
          a3
          .
          (eliminate
            ModelWord32
            (lambda unrestricted current : (family ModelWord32) . Nat)
            b
            (branch
              ModelWord32Value
              b0
              b1
              b2
              b3
              .
              (stdFlagOr
                (byte-less-than a3 b3)
                (stdFlagAnd
                  (byte-equal a3 b3)
                  (stdFlagOr
                    (byte-less-than a2 b2)
                    (stdFlagAnd
                      (byte-equal a2 b2)
                      (stdFlagOr
                        (byte-less-than a1 b1)
                        (stdFlagAnd (byte-equal a1 b1) (byte-less-than a0 b0)))))))))))))

-- I32 signed wrapper (L11k): the I64 pattern over ModelWord32.
def I32 =
  (family StdI32)

def stdI32FromWord =
  (lambda unrestricted bits : (family ModelWord32) . (constructor StdI32 StdI32Of bits))

def stdI32ToWord =
  (lambda unrestricted value : (family StdI32) .
    (eliminate
      StdI32
      (lambda unrestricted current : (family StdI32) . (family ModelWord32))
      value
      (branch StdI32Of bits . bits)))

def stdI32BitsEqual =
  (lambda unrestricted a : (family StdI32) .
    (lambda unrestricted b : (family StdI32) . (stdU32Equal (stdI32ToWord a) (stdI32ToWord b))))

def stdI32LessThan =
  (lambda unrestricted a : (family StdI32) .
    (lambda unrestricted b : (family StdI32) .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
          (stdU32HighBit (stdI32ToWord b)))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat .
            (nat-eliminate
              (lambda unrestricted current : Nat . Nat)
              (succ zero)
              (lambda unrestricted predecessorB : Nat .
                (lambda unrestricted inductionB : Nat .
                  (stdU32LessThan (stdI32ToWord a) (stdI32ToWord b))))
              (stdU32HighBit (stdI32ToWord b)))))
        (stdU32HighBit (stdI32ToWord a)))))

def stdI32AddWrapping =
  (lambda unrestricted a : (family StdI32) .
    (lambda unrestricted b : (family StdI32) .
      (stdI32FromWord (modelWord32Add (stdI32ToWord a) (stdI32ToWord b)))))

-- U16 (L11l): construction and the byte-lexicographic primitives.
def U16 =
  (family StdU16)

def stdU16FromBytes =
  (lambda unrestricted low : Byte .
    (lambda unrestricted high : Byte . (constructor StdU16 StdU16Of low high)))

def stdU16IsZero =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . Nat)
      value
      (branch StdU16Of low high . (stdFlagAnd (byte-equal low (byte 0)) (byte-equal high (byte 0))))))

def stdU16Equal =
  (lambda unrestricted a : (family StdU16) .
    (lambda unrestricted b : (family StdU16) .
      (eliminate
        StdU16
        (lambda unrestricted current : (family StdU16) . Nat)
        a
        (branch
          StdU16Of
          aLow
          aHigh
          .
          (eliminate
            StdU16
            (lambda unrestricted current : (family StdU16) . Nat)
            b
            (branch
              StdU16Of
              bLow
              bHigh
              .
              (stdFlagAnd (byte-equal aLow bLow) (byte-equal aHigh bHigh))))))))

def stdU16HighBit =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . Nat)
      value
      (branch
        StdU16Of
        low
        high
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (succ zero)
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
          (byte-less-than high (byte 128))))))

def stdU16LessThan =
  (lambda unrestricted a : (family StdU16) .
    (lambda unrestricted b : (family StdU16) .
      (eliminate
        StdU16
        (lambda unrestricted current : (family StdU16) . Nat)
        a
        (branch
          StdU16Of
          aLow
          aHigh
          .
          (eliminate
            StdU16
            (lambda unrestricted current : (family StdU16) . Nat)
            b
            (branch
              StdU16Of
              bLow
              bHigh
              .
              (stdFlagOr
                (byte-less-than aHigh bHigh)
                (stdFlagAnd (byte-equal aHigh bHigh) (byte-less-than aLow bLow)))))))))

-- I16 signed wrapper (L11l): the verified I64/I32 pattern over StdU16.
def I16 =
  (family StdI16)

def stdI16FromU16 =
  (lambda unrestricted bits : (family StdU16) . (constructor StdI16 StdI16Of bits))

def stdI16ToU16 =
  (lambda unrestricted value : (family StdI16) .
    (eliminate
      StdI16
      (lambda unrestricted current : (family StdI16) . (family StdU16))
      value
      (branch StdI16Of bits . bits)))

def stdI16BitsEqual =
  (lambda unrestricted a : (family StdI16) .
    (lambda unrestricted b : (family StdI16) . (stdU16Equal (stdI16ToU16 a) (stdI16ToU16 b))))

def stdI16LessThan =
  (lambda unrestricted a : (family StdI16) .
    (lambda unrestricted b : (family StdI16) .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
          (stdU16HighBit (stdI16ToU16 b)))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat .
            (nat-eliminate
              (lambda unrestricted current : Nat . Nat)
              (succ zero)
              (lambda unrestricted predecessorB : Nat .
                (lambda unrestricted inductionB : Nat .
                  (stdU16LessThan (stdI16ToU16 a) (stdI16ToU16 b))))
              (stdU16HighBit (stdI16ToU16 b)))))
        (stdU16HighBit (stdI16ToU16 a)))))

-- CONVERSIONS (L11l, NUM-005): sign-extension and narrowing are byte assembly,
-- never a round trip through Natural (which would be unary).
-- the byte that extends a sign: 0xff for negative, 0x00 for non-negative
def stdI8SignByte =
  (lambda unrestricted value : (family StdI8) .
    (nat-eliminate
      (lambda unrestricted current : Nat . Byte)
      (byte 255)
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Byte . (byte 0)))
      (stdI8IsNonNegative value)))

def stdI8ToI16 =
  (lambda unrestricted value : (family StdI8) .
    (stdI16FromU16 (stdU16FromBytes (stdI8ToByte value) (stdI8SignByte value))))

def stdI8ToI32 =
  (lambda unrestricted value : (family StdI8) .
    (stdI32FromWord
      (constructor
        ModelWord32
        ModelWord32Value
        (stdI8ToByte value)
        (stdI8SignByte value)
        (stdI8SignByte value)
        (stdI8SignByte value))))

def stdI16ToI32 =
  (lambda unrestricted value : (family StdI16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . (family StdI32))
      (stdI16ToU16 value)
      (branch
        StdU16Of
        low
        high
        .
        (stdI32FromWord
          (constructor
            ModelWord32
            ModelWord32Value
            low
            high
            (nat-eliminate
              (lambda unrestricted current : Nat . Byte)
              (byte 255)
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : Byte . (byte 0)))
              (byte-less-than high (byte 128)))
            (nat-eliminate
              (lambda unrestricted current : Nat . Byte)
              (byte 255)
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : Byte . (byte 0)))
              (byte-less-than high (byte 128))))))))

-- narrowing keeps the low bytes (wrapping semantics; a checked narrow is later)
def stdI32ToI8 =
  (lambda unrestricted value : (family StdI32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdI8))
      (stdI32ToWord value)
      (branch ModelWord32Value b0 b1 b2 b3 . (stdI8FromByte b0))))

def stdI16ToI8 =
  (lambda unrestricted value : (family StdI16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . (family StdI8))
      (stdI16ToU16 value)
      (branch StdU16Of low high . (stdI8FromByte low))))

-- CHECKED NARROWING (L11n, NUM-005): `StdSome` exactly when the value is
-- representable at the narrower width, `StdNone` otherwise (the wrapping
-- narrows above keep the low bytes regardless). Unsigned: every dropped byte
-- must be zero. Signed: every dropped byte must equal the sign byte of the
-- kept part, so the value sign-extends back to itself.
def stdU16ToU8Checked =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . (family StdOption Byte))
      value
      (branch
        StdU16Of
        low
        high
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdOption Byte))
          (constructor StdOption StdNone Byte)
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family StdOption Byte) .
              (constructor StdOption StdSome Byte low)))
          (byte-equal high (byte 0))))))

def stdU32ToU8Checked =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdOption Byte))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdOption Byte))
          (constructor StdOption StdNone Byte)
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family StdOption Byte) .
              (constructor StdOption StdSome Byte b0)))
          (stdFlagAnd
            (byte-equal b1 (byte 0))
            (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))

def stdU32ToU16Checked =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdU16)))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
          (constructor StdOption StdNone (family StdU16))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family StdOption (family StdU16)) .
              (constructor StdOption StdSome (family StdU16) (stdU16FromBytes b0 b1))))
          (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0)))))))

def stdU64ToU32Checked =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family StdOption (family ModelWord32)))
      value
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
          (constructor StdOption StdNone (family ModelWord32))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
              (constructor
                StdOption
                StdSome
                (family ModelWord32)
                (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))
          (stdFlagAnd
            (byte-equal b4 (byte 0))
            (stdFlagAnd
              (byte-equal b5 (byte 0))
              (stdFlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0)))))))))

def stdI16ToI8Checked =
  (lambda unrestricted value : (family StdI16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . (family StdOption (family StdI8)))
      (stdI16ToU16 value)
      (branch
        StdU16Of
        low
        high
        .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
          (constructor StdOption StdNone (family StdI8))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family StdOption (family StdI8)) .
              (constructor StdOption StdSome (family StdI8) (stdI8FromByte low))))
          (byte-equal high (stdI8SignByte (stdI8FromByte low)))))))

def stdI32ToI8Checked =
  (lambda unrestricted value : (family StdI32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI8)))
      (stdI32ToWord value)
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (app
          (lambda unrestricted sign : Byte .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
              (constructor StdOption StdNone (family StdI8))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family StdOption (family StdI8)) .
                  (constructor StdOption StdSome (family StdI8) (stdI8FromByte b0))))
              (stdFlagAnd
                (byte-equal b1 sign)
                (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign)))))
          (stdI8SignByte (stdI8FromByte b0))))))

def stdI32ToI16Checked =
  (lambda unrestricted value : (family StdI32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI16)))
      (stdI32ToWord value)
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (app
          (lambda unrestricted sign : Byte .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family StdOption (family StdI16)))
              (constructor StdOption StdNone (family StdI16))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family StdOption (family StdI16)) .
                  (constructor
                    StdOption
                    StdSome
                    (family StdI16)
                    (stdI16FromU16 (stdU16FromBytes b0 b1)))))
              (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign))))
          (stdI8SignByte (stdI8FromByte b1))))))

def stdI64ToI32Checked =
  (lambda unrestricted value : (family StdI64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family StdOption (family StdI32)))
      (stdI64ToWord value)
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (app
          (lambda unrestricted sign : Byte .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
              (constructor StdOption StdNone (family StdI32))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family StdOption (family StdI32)) .
                  (constructor
                    StdOption
                    StdSome
                    (family StdI32)
                    (stdI32FromWord (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3)))))
              (stdFlagAnd
                (byte-equal b4 sign)
                (stdFlagAnd
                  (byte-equal b5 sign)
                  (stdFlagAnd (byte-equal b6 sign) (byte-equal b7 sign))))))
          (stdI8SignByte (stdI8FromByte b3))))))

-- U8 ARITHMETIC (L11p, REG-012): the owner is Std.Byte's byteAddWithCarry
-- (low byte + carry flag). Wrapping keeps the low byte; checked is absent
-- exactly when the carry is set (255 + 1 -> None; 254 + 1 -> Some 255).
def stdU8AddWrapping =
  (lambda unrestricted a : Byte .
    (lambda unrestricted b : Byte .
      (eliminate
        ByteAddResult
        (lambda unrestricted current : (family ByteAddResult) . Byte)
        (byteAddWithCarry a b zero)
        (branch ByteAddResultValue low carry . low))))

def stdU8AddChecked =
  (lambda unrestricted a : Byte .
    (lambda unrestricted b : Byte .
      (eliminate
        ByteAddResult
        (lambda unrestricted current : (family ByteAddResult) . (family StdOption Byte))
        (byteAddWithCarry a b zero)
        (branch
          ByteAddResultValue
          low
          carry
          .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family StdOption Byte))
            (constructor StdOption StdSome Byte low)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family StdOption Byte) .
                (constructor StdOption StdNone Byte)))
            carry)))))

-- CODECS (L11o, NUM-008). The OWNER of the fixed-width LE/BE codecs is
-- Data.Bytes (evidence/language-testing/L11n-codec-owner-audit.md); these are
-- the width-vocabulary names for its functions, never a second implementation.
--   Encode*   : value -> Bytes (byte assembly; LE = byte 0 first, BE = last)
--   Read*     : bounded read -> value + the remaining input, or InputTooShort
--   Decode*Exact : canonical decode -> value only when the input is EXACTLY the
--                  width (short AND trailing input -> MalformedLength)
def stdU32EncodeLE =
  dataBytesWord32LE

def stdU32EncodeBE =
  dataBytesWord32BE

def stdU64EncodeLE =
  dataBytesWord64LE

def stdU64EncodeBE =
  dataBytesWord64BE

def stdU32ReadLE =
  dataBytesReadWord32LE

def stdU32ReadBE =
  dataBytesReadWord32BE

def stdU64ReadLE =
  dataBytesReadWord64LE

def stdU64ReadBE =
  dataBytesReadWord64BE

def stdU32DecodeLEExact =
  dataBytesDecodeWord32LEExact

def stdU32DecodeBEExact =
  dataBytesDecodeWord32BEExact

def stdU64DecodeLEExact =
  dataBytesDecodeWord64LEExact

def stdU64DecodeBEExact =
  dataBytesDecodeWord64BEExact

-- answers of the owner's result families under the vocabulary: value-or,
-- remaining input (empty on failure), and a failed flag (1 = failed)
def stdU32ReadValueOr =
  (lambda unrestricted fallback : (family ModelWord32) .
    (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
      (eliminate
        DataBytesWord32DecodeResult
        (lambda unrestricted current : (family DataBytesWord32DecodeResult) . (family ModelWord32))
        result
        (branch DataBytesWord32Decoded value remaining . value)
        (branch DataBytesWord32DecodeFailed code . fallback))))

def stdU32ReadRemaining =
  (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
    (eliminate
      DataBytesWord32DecodeResult
      (lambda unrestricted current : (family DataBytesWord32DecodeResult) . Bytes)
      result
      (branch DataBytesWord32Decoded value remaining . remaining)
      (branch DataBytesWord32DecodeFailed code . b"")))

def stdU32ReadFailed =
  (lambda unrestricted result : (family DataBytesWord32DecodeResult) .
    (eliminate
      DataBytesWord32DecodeResult
      (lambda unrestricted current : (family DataBytesWord32DecodeResult) . Nat)
      result
      (branch DataBytesWord32Decoded value remaining . zero)
      (branch DataBytesWord32DecodeFailed code . (succ zero))))

def stdU32ExactValueOr =
  (lambda unrestricted fallback : (family ModelWord32) .
    (lambda unrestricted result : (family DataBytesWord32ExactDecodeResult) .
      (eliminate
        DataBytesWord32ExactDecodeResult
        (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) .
          (family ModelWord32))
        result
        (branch DataBytesWord32ExactlyDecoded value telemetry . value)
        (branch DataBytesWord32ExactDecodeFailed code telemetry . fallback))))

def stdU32ExactFailed =
  (lambda unrestricted result : (family DataBytesWord32ExactDecodeResult) .
    (eliminate
      DataBytesWord32ExactDecodeResult
      (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . Nat)
      result
      (branch DataBytesWord32ExactlyDecoded value telemetry . zero)
      (branch DataBytesWord32ExactDecodeFailed code telemetry . (succ zero))))

def stdU64ReadValueOr =
  (lambda unrestricted fallback : (family ModelWord64) .
    (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
      (eliminate
        DataBytesWord64DecodeResult
        (lambda unrestricted current : (family DataBytesWord64DecodeResult) . (family ModelWord64))
        result
        (branch DataBytesWord64Decoded value remaining . value)
        (branch DataBytesWord64DecodeFailed code . fallback))))

def stdU64ReadRemaining =
  (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
    (eliminate
      DataBytesWord64DecodeResult
      (lambda unrestricted current : (family DataBytesWord64DecodeResult) . Bytes)
      result
      (branch DataBytesWord64Decoded value remaining . remaining)
      (branch DataBytesWord64DecodeFailed code . b"")))

def stdU64ReadFailed =
  (lambda unrestricted result : (family DataBytesWord64DecodeResult) .
    (eliminate
      DataBytesWord64DecodeResult
      (lambda unrestricted current : (family DataBytesWord64DecodeResult) . Nat)
      result
      (branch DataBytesWord64Decoded value remaining . zero)
      (branch DataBytesWord64DecodeFailed code . (succ zero))))

def stdU64ExactValueOr =
  (lambda unrestricted fallback : (family ModelWord64) .
    (lambda unrestricted result : (family DataBytesWord64ExactDecodeResult) .
      (eliminate
        DataBytesWord64ExactDecodeResult
        (lambda unrestricted current : (family DataBytesWord64ExactDecodeResult) .
          (family ModelWord64))
        result
        (branch DataBytesWord64ExactlyDecoded value telemetry . value)
        (branch DataBytesWord64ExactDecodeFailed code telemetry . fallback))))

def stdU64ExactFailed =
  (lambda unrestricted result : (family DataBytesWord64ExactDecodeResult) .
    (eliminate
      DataBytesWord64ExactDecodeResult
      (lambda unrestricted current : (family DataBytesWord64ExactDecodeResult) . Nat)
      result
      (branch DataBytesWord64ExactlyDecoded value telemetry . zero)
      (branch DataBytesWord64ExactDecodeFailed code telemetry . (succ zero))))

-- U16 (no owner had a 16-bit codec): the same three shapes, built in the
-- owner's style. The bounded read answers Std.Codec's StdDecoded (value + rest,
-- or truncated); the exact decode answers StdOption (absent unless the input is
-- exactly two bytes).
def stdU16EncodeLE =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . Bytes)
      value
      (branch StdU16Of low high . (bytes-cons low (bytes-cons high b"")))))

def stdU16EncodeBE =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . Bytes)
      value
      (branch StdU16Of low high . (bytes-cons high (bytes-cons low b"")))))

def stdU16ReadLE =
  (lambda unrestricted input : Bytes .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdDecoded (family StdU16)))
      (constructor StdDecoded StdDecodedTruncated (family StdU16))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdDecoded (family StdU16)) .
          (constructor
            StdDecoded
            StdDecodedValue
            (family StdU16)
            (stdU16FromBytes (bytes-head input) (bytes-head (bytes-tail input)))
            (bytes-tail (bytes-tail input)))))
      (naturalLessOrEqual (succ (succ zero)) (bytes-length input))))

def stdU16ReadBE =
  (lambda unrestricted input : Bytes .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdDecoded (family StdU16)))
      (constructor StdDecoded StdDecodedTruncated (family StdU16))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdDecoded (family StdU16)) .
          (constructor
            StdDecoded
            StdDecodedValue
            (family StdU16)
            (stdU16FromBytes (bytes-head (bytes-tail input)) (bytes-head input))
            (bytes-tail (bytes-tail input)))))
      (naturalLessOrEqual (succ (succ zero)) (bytes-length input))))

def stdU16DecodeLEExact =
  (lambda unrestricted input : Bytes .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
      (constructor StdOption StdNone (family StdU16))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdOption (family StdU16)) .
          (constructor
            StdOption
            StdSome
            (family StdU16)
            (stdU16FromBytes (bytes-head input) (bytes-head (bytes-tail input))))))
      (naturalEqual (bytes-length input) (succ (succ zero)))))

def stdU16DecodeBEExact =
  (lambda unrestricted input : Bytes .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family StdOption (family StdU16)))
      (constructor StdOption StdNone (family StdU16))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family StdOption (family StdU16)) .
          (constructor
            StdOption
            StdSome
            (family StdU16)
            (stdU16FromBytes (bytes-head (bytes-tail input)) (bytes-head input)))))
      (naturalEqual (bytes-length input) (succ (succ zero)))))

-- DIVISION (L11r, NUM-004): see the StdDivision family for the contract.
-- EVALUATOR NOTE (measured at L11r): the reference evaluator is a NORMALIZER
-- -- it normalizes every closed subterm, including the branch an eliminator
-- does not select (a slow closed term under an unselected successor lambda
-- still costs its full time). No shape below therefore makes a REFUSED word
-- division cheap on the evaluator lane: the loop is normalized anyway. The
-- refusal is kept in the zero case and the work under the successor lambda
-- because that is the natural shape (the flag reads "may divide"), not for
-- laziness; the evaluator-lane laws cover U8 (bounded naturals) and the
-- native lane carries every word-width value and refusal (NUM-006).
def stdDivisionErrorCodeBytes =
  (lambda unrestricted code : (family StdDivisionErrorCode) .
    (eliminate
      StdDivisionErrorCode
      (lambda unrestricted current : (family StdDivisionErrorCode) . Bytes)
      code
      (branch StdDivisionByZero . b"ALPHA-STD-WORD-001")
      (branch StdDivisionOverflow . b"ALPHA-STD-WORD-002")))

-- Answer helpers over the result family (the word type is explicit).
def stdDivisionQuotientOr =
  (lambda erased word : Type 0 .
    (lambda unrestricted fallback : word .
      (lambda unrestricted result : (family StdDivision word) .
        (eliminate
          StdDivision
          (lambda unrestricted current : (family StdDivision word) . word)
          result
          (branch StdDivisionSucceeded quotient remainder . quotient)
          (branch StdDivisionFailed error . fallback)))))

def stdDivisionRemainderOr =
  (lambda erased word : Type 0 .
    (lambda unrestricted fallback : word .
      (lambda unrestricted result : (family StdDivision word) .
        (eliminate
          StdDivision
          (lambda unrestricted current : (family StdDivision word) . word)
          result
          (branch StdDivisionSucceeded quotient remainder . remainder)
          (branch StdDivisionFailed error . fallback)))))

def stdDivisionIsFailed =
  (lambda erased word : Type 0 .
    (lambda unrestricted result : (family StdDivision word) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision word) . Nat)
        result
        (branch StdDivisionSucceeded quotient remainder . zero)
        (branch StdDivisionFailed error . (succ zero)))))

-- The failure's code bytes, or empty bytes when the division succeeded.
def stdDivisionFailureBytes =
  (lambda erased word : Type 0 .
    (lambda unrestricted result : (family StdDivision word) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision word) . Bytes)
        result
        (branch StdDivisionSucceeded quotient remainder . b"")
        (branch StdDivisionFailed error . (stdDivisionErrorCodeBytes error)))))

-- Flag helpers on the 0/1 naturals the word owners use as booleans.
def stdFlagNot =
  modelWord64FlagNot

def stdFlagXor =
  (lambda unrestricted a : Nat .
    (lambda unrestricted b : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        b
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Nat . (modelWord64FlagNot b)))
        a)))

-- U64 restoring division: 64 iterations, each shifting the next dividend bit
-- into the partial remainder and subtracting the divisor when it fits. The
-- remainder is always < divisor, so 2r+1 can exceed 64 bits only when the
-- remainder's high bit was set; that bit is the carry out of the shift and
-- means the divisor fits (2r >= 2^64 > divisor), and the wrapped subtraction
-- still yields the exact new remainder (the true value is < 2^64).
def stdU64DivisionStep =
  (lambda unrestricted divisor : (family ModelWord64) .
    (lambda unrestricted state : (family StdU64DivisionState) .
      (eliminate
        StdU64DivisionState
        (lambda unrestricted current : (family StdU64DivisionState) . (family StdU64DivisionState))
        state
        (branch
          StdU64DivisionStateOf
          remainder
          quotient
          dividend
          .
          (app
            (lambda unrestricted shifted : (family ModelWord64) .
              (app
                (lambda unrestricted shiftedQuotient : (family ModelWord64) .
                  (app
                    (lambda unrestricted shiftedDividend : (family ModelWord64) .
                      (nat-eliminate
                        (lambda unrestricted current : Nat . (family StdU64DivisionState))
                        (constructor
                          StdU64DivisionState
                          StdU64DivisionStateOf
                          shifted
                          shiftedQuotient
                          shiftedDividend)
                        (lambda unrestricted predecessor : Nat .
                          (lambda unrestricted induction : (family StdU64DivisionState) .
                            (constructor
                              StdU64DivisionState
                              StdU64DivisionStateOf
                              (modelWord64Subtract shifted divisor)
                              (modelWord64Add shiftedQuotient modelWord64One)
                              shiftedDividend)))
                        (modelWord64FlagOr
                          (modelWord64HighBit remainder)
                          (modelWord64FlagNot (modelWord64LessThan shifted divisor)))))
                    (modelWord64ShiftLeftOne dividend)))
                (modelWord64ShiftLeftOne quotient)))
            (modelWord64Add
              (modelWord64ShiftLeftOne remainder)
              (modelWord64Select (modelWord64HighBit dividend) modelWord64One modelWord64Zero)))))))

def stdU64DivisionRun =
  (lambda unrestricted dividend : (family ModelWord64) .
    (lambda unrestricted divisor : (family ModelWord64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdU64DivisionState))
        (constructor
          StdU64DivisionState
          StdU64DivisionStateOf
          modelWord64Zero
          modelWord64Zero
          dividend)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdU64DivisionState) .
            (stdU64DivisionStep divisor induction)))
        modelWord64NaturalSixtyFour)))

-- U64 division: divisor zero -> StdDivisionByZero, else quotient + remainder.
def stdU64DivRem =
  (lambda unrestricted dividend : (family ModelWord64) .
    (lambda unrestricted divisor : (family ModelWord64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family ModelWord64)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family ModelWord64)
          (constructor StdDivisionErrorCode StdDivisionByZero))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family ModelWord64)) .
            (eliminate
              StdU64DivisionState
              (lambda unrestricted current : (family StdU64DivisionState) .
                (family StdDivision (family ModelWord64)))
              (stdU64DivisionRun dividend divisor)
              (branch
                StdU64DivisionStateOf
                remainder
                quotient
                rest
                .
                (constructor
                  StdDivision
                  StdDivisionSucceeded
                  (family ModelWord64)
                  quotient
                  remainder)))))
        (modelWord64FlagNot (modelWord64IsZero divisor)))))

-- U32: Model.Word32 is frozen and has no subtract/complement, so the wrapping
-- subtract is built here (a - b = a + not b + 1), then the same restoring
-- division over the four-byte word.
def stdU32AllOnes =
  (constructor ModelWord32 ModelWord32Value (byte 255) (byte 255) (byte 255) (byte 255))

def stdU32Not =
  (lambda unrestricted value : (family ModelWord32) . (modelWord32Xor value stdU32AllOnes))

def stdU32SubtractWrapping =
  (lambda unrestricted a : (family ModelWord32) .
    (lambda unrestricted b : (family ModelWord32) .
      (modelWord32Add a (modelWord32Add (stdU32Not b) modelWord32One))))

-- Delegates to the one owner (Model.Word32, already imported here); found
-- as an exact duplicate by `alpha-ast duplicates` (L24d).
def stdU32Select =
  modelWord32Select

def stdU32NaturalThirtyTwo =
  (byte-to-nat (byte 32))

def stdU32DivisionStep =
  (lambda unrestricted divisor : (family ModelWord32) .
    (lambda unrestricted state : (family StdU32DivisionState) .
      (eliminate
        StdU32DivisionState
        (lambda unrestricted current : (family StdU32DivisionState) . (family StdU32DivisionState))
        state
        (branch
          StdU32DivisionStateOf
          remainder
          quotient
          dividend
          .
          (app
            (lambda unrestricted shifted : (family ModelWord32) .
              (app
                (lambda unrestricted shiftedQuotient : (family ModelWord32) .
                  (app
                    (lambda unrestricted shiftedDividend : (family ModelWord32) .
                      (nat-eliminate
                        (lambda unrestricted current : Nat . (family StdU32DivisionState))
                        (constructor
                          StdU32DivisionState
                          StdU32DivisionStateOf
                          shifted
                          shiftedQuotient
                          shiftedDividend)
                        (lambda unrestricted predecessor : Nat .
                          (lambda unrestricted induction : (family StdU32DivisionState) .
                            (constructor
                              StdU32DivisionState
                              StdU32DivisionStateOf
                              (stdU32SubtractWrapping shifted divisor)
                              (modelWord32Add shiftedQuotient modelWord32One)
                              shiftedDividend)))
                        (stdFlagOr
                          (stdU32HighBit remainder)
                          (stdFlagNot (stdU32LessThan shifted divisor)))))
                    (modelWord32ShiftLeftOne dividend)))
                (modelWord32ShiftLeftOne quotient)))
            (modelWord32Add
              (modelWord32ShiftLeftOne remainder)
              (stdU32Select (stdU32HighBit dividend) modelWord32One modelWord32Zero)))))))

def stdU32DivisionRun =
  (lambda unrestricted dividend : (family ModelWord32) .
    (lambda unrestricted divisor : (family ModelWord32) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdU32DivisionState))
        (constructor
          StdU32DivisionState
          StdU32DivisionStateOf
          modelWord32Zero
          modelWord32Zero
          dividend)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdU32DivisionState) .
            (stdU32DivisionStep divisor induction)))
        stdU32NaturalThirtyTwo)))

def stdU32DivRem =
  (lambda unrestricted dividend : (family ModelWord32) .
    (lambda unrestricted divisor : (family ModelWord32) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family ModelWord32)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family ModelWord32)
          (constructor StdDivisionErrorCode StdDivisionByZero))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family ModelWord32)) .
            (eliminate
              StdU32DivisionState
              (lambda unrestricted current : (family StdU32DivisionState) .
                (family StdDivision (family ModelWord32)))
              (stdU32DivisionRun dividend divisor)
              (branch
                StdU32DivisionStateOf
                remainder
                quotient
                rest
                .
                (constructor
                  StdDivision
                  StdDivisionSucceeded
                  (family ModelWord32)
                  quotient
                  remainder)))))
        (stdFlagNot (stdU32IsZero divisor)))))

-- U16 divides as U32 (zero-extend, divide, keep the low bytes: both results
-- are bounded by the operands, so the narrow never drops a set bit).
def stdU16ToU32 =
  (lambda unrestricted value : (family StdU16) .
    (eliminate
      StdU16
      (lambda unrestricted current : (family StdU16) . (family ModelWord32))
      value
      (branch
        StdU16Of
        low
        high
        .
        (constructor ModelWord32 ModelWord32Value low high (byte 0) (byte 0)))))

def stdU32ToU16 =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdU16))
      value
      (branch ModelWord32Value b0 b1 b2 b3 . (stdU16FromBytes b0 b1))))

def stdU16DivRem =
  (lambda unrestricted dividend : (family StdU16) .
    (lambda unrestricted divisor : (family StdU16) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision (family ModelWord32)) .
          (family StdDivision (family StdU16)))
        (stdU32DivRem (stdU16ToU32 dividend) (stdU16ToU32 divisor))
        (branch
          StdDivisionSucceeded
          quotient
          remainder
          .
          (constructor
            StdDivision
            StdDivisionSucceeded
            (family StdU16)
            (stdU32ToU16 quotient)
            (stdU32ToU16 remainder)))
        (branch
          StdDivisionFailed
          error
          .
          (constructor StdDivision StdDivisionFailed (family StdU16) error)))))

-- U8 divides through the core naturals (values are at most 255, so this is
-- exact on every lane); Std.Natural owns the natural division and its
-- NaturalDivisionState already carries BOTH the quotient and the remainder, so
-- one traversal answers both. RECORDED (L11r): the owner's separate
-- naturalModuloUnchecked is pathological on the reference evaluator (255 mod 16
-- gives no answer in 100 s while naturalDivideUnchecked 255 16 answers in
-- 0.3 s), which is why the remainder is projected from the state, never
-- recomputed through the modulo.
def stdU8DivRem =
  (lambda unrestricted dividend : Byte .
    (lambda unrestricted divisor : Byte .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision Byte))
        (constructor
          StdDivision
          StdDivisionFailed
          Byte
          (constructor StdDivisionErrorCode StdDivisionByZero))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision Byte) .
            (eliminate
              NaturalDivisionState
              (lambda unrestricted current : (family NaturalDivisionState) .
                (family StdDivision Byte))
              (naturalDivisionState (byte-to-nat dividend) (byte-to-nat divisor))
              (branch
                NaturalDivisionStateValue
                remainder
                quotient
                .
                (constructor
                  StdDivision
                  StdDivisionSucceeded
                  Byte
                  (nat-to-byte quotient)
                  (nat-to-byte remainder))))))
        (byte-to-nat divisor))))

-- SIGNED division through magnitudes: |a| / |b| unsigned, then the quotient
-- is negated when the signs differ and the remainder when the dividend is
-- negative. |signedMinimum| = 2^(width-1) is representable unsigned, so the
-- wrapping API needs no special case: 2^(width-1) / 1 negated wraps back to
-- signedMinimum with remainder 0. The checked API refuses exactly that shape.
def stdU64NegateIf =
  (lambda unrestricted flag : Nat .
    (lambda unrestricted bits : (family ModelWord64) .
      (modelWord64Select flag (modelWord64Subtract modelWord64Zero bits) bits)))

def stdI64IsNegative =
  (lambda unrestricted value : (family StdI64) . (modelWord64HighBit (stdI64ToWord value)))

def stdI64Negate =
  (lambda unrestricted value : (family StdI64) .
    (stdI64FromWord (modelWord64Subtract modelWord64Zero (stdI64ToWord value))))

def stdI64Magnitude =
  (lambda unrestricted value : (family StdI64) .
    (stdU64NegateIf (stdI64IsNegative value) (stdI64ToWord value)))

def stdI64MinimumBits =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 128))

def stdU64AllOnes =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255))

def stdI64DivRemWrapping =
  (lambda unrestricted dividend : (family StdI64) .
    (lambda unrestricted divisor : (family StdI64) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision (family ModelWord64)) .
          (family StdDivision (family StdI64)))
        (stdU64DivRem (stdI64Magnitude dividend) (stdI64Magnitude divisor))
        (branch
          StdDivisionSucceeded
          quotient
          remainder
          .
          (constructor
            StdDivision
            StdDivisionSucceeded
            (family StdI64)
            (stdI64FromWord
              (stdU64NegateIf
                (stdFlagXor (stdI64IsNegative dividend) (stdI64IsNegative divisor))
                quotient))
            (stdI64FromWord (stdU64NegateIf (stdI64IsNegative dividend) remainder))))
        (branch
          StdDivisionFailed
          error
          .
          (constructor StdDivision StdDivisionFailed (family StdI64) error)))))

def stdI64DivRemChecked =
  (lambda unrestricted dividend : (family StdI64) .
    (lambda unrestricted divisor : (family StdI64) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family StdI64)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family StdI64)
          (constructor StdDivisionErrorCode StdDivisionOverflow))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family StdI64)) .
            (stdI64DivRemWrapping dividend divisor)))
        (stdFlagNot
          (stdFlagAnd
            (modelWord64Equal (stdI64ToWord dividend) stdI64MinimumBits)
            (modelWord64Equal (stdI64ToWord divisor) stdU64AllOnes))))))

-- I32 over the U32 division.
def stdU32NegateIf =
  (lambda unrestricted flag : Nat .
    (lambda unrestricted bits : (family ModelWord32) .
      (stdU32Select flag (stdU32SubtractWrapping modelWord32Zero bits) bits)))

def stdI32IsNegative =
  (lambda unrestricted value : (family StdI32) . (stdU32HighBit (stdI32ToWord value)))

def stdI32Negate =
  (lambda unrestricted value : (family StdI32) .
    (stdI32FromWord (stdU32SubtractWrapping modelWord32Zero (stdI32ToWord value))))

def stdI32Magnitude =
  (lambda unrestricted value : (family StdI32) .
    (stdU32NegateIf (stdI32IsNegative value) (stdI32ToWord value)))

def stdI32MinimumBits =
  (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 128))

def stdI32DivRemWrapping =
  (lambda unrestricted dividend : (family StdI32) .
    (lambda unrestricted divisor : (family StdI32) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision (family ModelWord32)) .
          (family StdDivision (family StdI32)))
        (stdU32DivRem (stdI32Magnitude dividend) (stdI32Magnitude divisor))
        (branch
          StdDivisionSucceeded
          quotient
          remainder
          .
          (constructor
            StdDivision
            StdDivisionSucceeded
            (family StdI32)
            (stdI32FromWord
              (stdU32NegateIf
                (stdFlagXor (stdI32IsNegative dividend) (stdI32IsNegative divisor))
                quotient))
            (stdI32FromWord (stdU32NegateIf (stdI32IsNegative dividend) remainder))))
        (branch
          StdDivisionFailed
          error
          .
          (constructor StdDivision StdDivisionFailed (family StdI32) error)))))

def stdI32DivRemChecked =
  (lambda unrestricted dividend : (family StdI32) .
    (lambda unrestricted divisor : (family StdI32) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family StdI32)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family StdI32)
          (constructor StdDivisionErrorCode StdDivisionOverflow))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family StdI32)) .
            (stdI32DivRemWrapping dividend divisor)))
        (stdFlagNot
          (stdFlagAnd
            (stdU32Equal (stdI32ToWord dividend) stdI32MinimumBits)
            (stdU32Equal (stdI32ToWord divisor) stdU32AllOnes))))))

-- I16 and I8 divide as I32 (sign-extend, divide WRAPPING at 32 bits where
-- every 16/8-bit quotient fits, narrow back): the only narrow that drops a
-- bit is signedMinimum / -1, which the wrapping narrow turns back into
-- signedMinimum (the wrap) and the checked API refuses first.
def stdI32ToI16 =
  (lambda unrestricted value : (family StdI32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family StdI16))
      (stdI32ToWord value)
      (branch ModelWord32Value b0 b1 b2 b3 . (stdI16FromU16 (stdU16FromBytes b0 b1)))))

def stdI16DivRemWrapping =
  (lambda unrestricted dividend : (family StdI16) .
    (lambda unrestricted divisor : (family StdI16) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision (family StdI32)) .
          (family StdDivision (family StdI16)))
        (stdI32DivRemWrapping (stdI16ToI32 dividend) (stdI16ToI32 divisor))
        (branch
          StdDivisionSucceeded
          quotient
          remainder
          .
          (constructor
            StdDivision
            StdDivisionSucceeded
            (family StdI16)
            (stdI32ToI16 quotient)
            (stdI32ToI16 remainder)))
        (branch
          StdDivisionFailed
          error
          .
          (constructor StdDivision StdDivisionFailed (family StdI16) error)))))

def stdI16MinimumBits =
  (stdU16FromBytes (byte 0) (byte 128))

def stdU16AllOnes =
  (stdU16FromBytes (byte 255) (byte 255))

def stdI16DivRemChecked =
  (lambda unrestricted dividend : (family StdI16) .
    (lambda unrestricted divisor : (family StdI16) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family StdI16)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family StdI16)
          (constructor StdDivisionErrorCode StdDivisionOverflow))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family StdI16)) .
            (stdI16DivRemWrapping dividend divisor)))
        (stdFlagNot
          (stdFlagAnd
            (stdU16Equal (stdI16ToU16 dividend) stdI16MinimumBits)
            (stdU16Equal (stdI16ToU16 divisor) stdU16AllOnes))))))

def stdI8DivRemWrapping =
  (lambda unrestricted dividend : (family StdI8) .
    (lambda unrestricted divisor : (family StdI8) .
      (eliminate
        StdDivision
        (lambda unrestricted current : (family StdDivision (family StdI32)) .
          (family StdDivision (family StdI8)))
        (stdI32DivRemWrapping (stdI8ToI32 dividend) (stdI8ToI32 divisor))
        (branch
          StdDivisionSucceeded
          quotient
          remainder
          .
          (constructor
            StdDivision
            StdDivisionSucceeded
            (family StdI8)
            (stdI32ToI8 quotient)
            (stdI32ToI8 remainder)))
        (branch
          StdDivisionFailed
          error
          .
          (constructor StdDivision StdDivisionFailed (family StdI8) error)))))

def stdI8DivRemChecked =
  (lambda unrestricted dividend : (family StdI8) .
    (lambda unrestricted divisor : (family StdI8) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdDivision (family StdI8)))
        (constructor
          StdDivision
          StdDivisionFailed
          (family StdI8)
          (constructor StdDivisionErrorCode StdDivisionOverflow))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdDivision (family StdI8)) .
            (stdI8DivRemWrapping dividend divisor)))
        (stdFlagNot
          (stdFlagAnd
            (byte-equal (stdI8ToByte dividend) (byte 128))
            (byte-equal (stdI8ToByte divisor) (byte 255)))))))

-- CHECKED SHIFTS (U32): a count >= the width is an error; the wrapping
-- `stdU32ShiftLeft/Right` (Model.Word32) repeat the one-bit shift `count`
-- times, so a count >= 32 yields ZERO there (stated: NOT the x86-64 `shl`
-- count-masking; a program wanting masking reduces the count itself).
def stdU32ShiftLeftChecked =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted count : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
        (constructor StdOption StdNone (family ModelWord32))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
            (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftLeft value count))))
        (nat-less-than count stdU32NaturalThirtyTwo))))

def stdU32ShiftRightChecked =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted count : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
        (constructor StdOption StdNone (family ModelWord32))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
            (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftRight value count))))
        (nat-less-than count stdU32NaturalThirtyTwo))))