Merge pull request hacl-star#876 from hacl-star/marina@blake2

blake2: fix a typo in a specification
mamonet · Nov 2, 2023 · 12c5e95 · 12c5e95
2 parents 6872c3c + 5705879
commit 12c5e95
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/specs/Spec.Blake2.fst b/specs/Spec.Blake2.fst
@@ -535,7 +535,7 @@ let blake2s d kk k n = blake2 Blake2S d kk k n
 
 val blake2b:
  d:bytes
- -> kk:size_nat{kk <= 64 /\ (if kk = 0 then length d < pow2 128 else length d + 128 < pow2 64)}
+ -> kk:size_nat{kk <= 64 /\ (if kk = 0 then length d < pow2 128 else length d + 128 < pow2 128)}
  -> k:lbytes kk
  -> nn:size_nat{1 <= nn /\ nn <= 64} ->
  Tot (lbytes nn)