ProofFastAppend.shq: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
Lines 511-514 of lawful-bytes@0.1.1.0/proof_fast_append.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&start_line=511&end_line=514

import Base

# The shift of append.w is 8 * (q & 3).
law shq:
  for +q: U32
  {U32.to_nat(((q .&. 3 : U32) << 3n : U32)) == Nat.mul(8n, U32.to_nat((q .&. 3 : U32))) : Nat}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=and3_lt
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&name=shq2