Model.Word32

A logical shift is division/multiplication by 2^amount followed by the word conversion, rather than amount separate carry traversals. The width guard is lazy: amounts >= 32 return zero without computing their power. On the bounded u64 runtime lane the largest admitted multiplication is (2^32 - 1) * 2^31 < 2^63, so no host overflow precedes truncation. Keeping the one-bit operations independent also leaves a byte-lane reference for the full shift tests. The Baguette realize profile run-430189202 motivated this change; equality of emitted bytes still needs artifact qualification.

285def modelWord32ShiftRight =
286  (lambda unrestricted value : (family ModelWord32) .
287    (lambda unrestricted amount : Nat .
288      (app
289        (nat-eliminate
290          (lambda unrestricted current : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
291          (lambda unrestricted unit : Nat . modelWord32Zero)
292          (lambda unrestricted predecessor : Nat .
293            (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
294              (lambda unrestricted unit : Nat .
295                (modelWord32FromNaturalTruncated
296                  (naturalDivideUnchecked (modelWord32ToNatural value) (naturalPowerOfTwo amount))))))
297          (naturalLess amount modelWord32NaturalThirtyTwo))
298        zero)))