1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
check_args
/* Autogenerated */
/* curve description: 25519 */
/* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */
/* n = 5 (from "5") */
/* s = 0x8000000000000000000000000000000000000000000000000000000000000000 (from "2^255") */
/* c = [(1, 19)] (from "1,19") */
/* machine_wordsize = 64 (from "64") */
#include <stdint.h>
typedef unsigned char fiat_25519_uint1;
typedef signed char fiat_25519_int1;
typedef signed __int128 fiat_25519_int128;
typedef unsigned __int128 fiat_25519_uint128;
In fiat_25519_carry_square:
Computed bounds (Some [Some [0x0 ~> 0x7ffffffffffff], Some [0x0 ~> 0x7ffffffffffff], Some [0x0 ~> 0x19dd1eb851eb806ae147ae147b7ff47ae147ae01a], Some [0x0 ~> 0x7ffffffffffff], Some [0x0 ~> 0x7ffffffffffff]]) are not tight enough (expected bounds not looser than (Some [Some [0x0 ~> 0x8cccccccccccc], Some [0x0 ~> 0x8cccccccccccc], Some [0x0 ~> 0x8cccccccccccc], Some [0x0 ~> 0x8cccccccccccc], Some [0x0 ~> 0x8cccccccccccc]])).
The bounds [0x0 ~> 0x19dd1eb851eb806ae147ae147b7ff47ae147ae01a] are looser than the expected bounds [0x0 ~> 0x8cccccccccccc]
When doing bounds analysis on the syntax tree:
/*
* Input Bounds:
* arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* Output Bounds:
* out1: None
*/
void f(uint256 out1[5], const uint64_t arg1[5]) {
uint64_t x1 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
uint64_t x2 = (x1 * (uint64_t)0x2);
uint64_t x3 = ((arg1[1]) * (uint64_t)0x2);
uint64_t x4 = ((arg1[0]) * (uint64_t)0x2);
uint512 x5 = ((uint512)((uint128)(arg1[4]) * (arg1[4])) << 204);
uint128 x6 = ((uint128)(arg1[3]) * x2);
uint256 x7 = ((uint256)((uint128)(arg1[3]) * (arg1[3])) << 102);
uint128 x8 = ((uint128)(arg1[2]) * (arg1[2]));
uint128 x9 = ((uint128)(arg1[1]) * x3);
uint128 x10 = ((uint128)(arg1[1]) * x3);
uint128 x11 = ((uint128)(arg1[1]) * (arg1[1]));
uint128 x12 = ((uint128)(arg1[0]) * x4);
uint128 x13 = ((uint128)(arg1[0]) * x4);
uint128 x14 = ((uint128)(arg1[0]) * x4);
uint128 x15 = ((uint128)(arg1[0]) * x4);
uint128 x16 = ((uint128)(arg1[0]) * (arg1[0]));
uint128 x17 = (x16 + (x15 + (x14 + (x13 + x12))));
uint64_t x18 = (uint64_t)(x17 >> 51);
uint64_t x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff));
uint512 x20 = (x8 + (x7 + x5));
uint128 x21 = (x11 + (x10 + x9));
uint128 x22 = (x18 + x6);
uint64_t x23 = (uint64_t)(x22 >> 51);
uint64_t x24 = (uint64_t)(x22 & UINT64_C(0x7ffffffffffff));
uint128 x25 = (x23 + x21);
uint64_t x26 = (uint64_t)(x25 >> 51);
uint64_t x27 = (uint64_t)(x25 & UINT64_C(0x7ffffffffffff));
uint8_t x28 = (uint8_t)(x26 >> 51);
uint64_t x29 = (x26 & UINT64_C(0x7ffffffffffff));
uint512 x30 = (x28 + x20);
uint512 x31 = (x30 >> 51);
uint64_t x32 = (uint64_t)(x30 & UINT64_C(0x7ffffffffffff));
uint512 x33 = (x31 * (uint512)UINT8_C(0x13));
uint512 x34 = (x19 + x33);
uint256 x35 = (uint256)(x34 >> 51);
uint64_t x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff));
uint256 x37 = (x35 + x24);
uint256 x38 = (x37 >> 51);
uint64_t x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff));
uint256 x40 = (x38 + x27);
out1[0] = x36;
out1[1] = x39;
out1[2] = x40;
out1[3] = x29;
out1[4] = x32;
}
with input bounds (Some [Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664]], tt).
|
