-spec hchacha20(Key :: chacha20_key(), Nonce :: hchacha20_nonce()) -> hchacha20_block().

Short example of why this works: HChaCha20 = ChaCha20 - State0

Longer example of why this works:

  K  = 256-bit key
  C  = 32-bit counter
  N  = 96-bit nonce
  X  = 128-bit nonce
  || = concatenation
  ++ = 32-bit word little endian addition
  -- = 32-bit word little endian subtraction
 
  ChaCha20(K, C, N) =
      State0 = "expand 32-byte k" || K || C || N
      State1 = Rounds(State0, 10)
      State2 = State1 ++ State2
      return State2
 
  HChaCha20(K, X) =
      State0 = "expand 32-byte k" || K || X
      State1 = Rounds(State0, 10)
      return FirstBits(State1, 128) || LastBits(State1, 128)
 
  # Let's rewrite HChaCha20 to use ChaCha20 with State0 subtraction:
 
  HChaCha20(K, X) =
      C = FirstBits(X, 32)
      N = LastBits(X, 96)
      State0 = "expand 32-byte k" || K || X
      State2 = ChaCha20(K, C, N)
      State1 = State2 -- State0
      return FirstBits(State1, 128) || LastBits(State1, 128)
 
  # Let's further reduce to not use K and use a Mask for blinding:
 
  HChaCha20(K, X) =
      Mask = CSPRNG(512)
      C = FirstBits(X, 32)
      N = LastBits(X, 96)
      KeyStream = ChaCha20(K, C, N) ^ Mask
      State2 = (FirstBits(KeyStream, 128) || LastBits(KeyStream, 128)) ^
          (FirstBits(Mask, 128) || LastBits(Mask, 128))
      State0 = "expand 32-byte k" || X
      State1 = State2 -- State0
      return State1