Merge pull request #870 from hacspec/countones

count-ones post-condition
hacspec · Sep 2, 2024 · 3b38e61 · 3b38e61
2 parents b285b13 + d8d9c0f
commit 3b38e61
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -45,7 +45,7 @@ val impl__u128__pow: u128 -> u32 -> u128
 val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> (Math.Lemmas.pow2_lt_compat 15 (v exponent); result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent)))}
 val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}
 
-val impl__u8__count_ones: u8 -> u32
+val impl__u8__count_ones: u8 -> r:u32{v r <= 8}
 
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError