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
79
80
81
82
83
84
85
86
87
88
|
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[4]) * (uint64_t)UINT8_C(0x13));
uint64_t x2 = (x1 * (uint64_t)0x2);
uint64_t x3 = ((arg1[4]) * (uint64_t)0x2);
uint64_t x4 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
uint64_t x5 = (x4 * (uint64_t)0x2);
uint64_t x6 = ((arg1[3]) * (uint64_t)0x2);
uint64_t x7 = ((arg1[2]) * (uint64_t)0x2);
uint64_t x8 = ((arg1[1]) * (uint64_t)0x2);
uint512 x9 = ((uint512)((uint128)(arg1[4]) * (arg1[4])) << 204);
uint128 x10 = ((uint128)(arg1[3]) * x2);
uint256 x11 = ((uint256)((uint128)(arg1[3]) * (arg1[3])) << 102);
uint128 x12 = ((uint128)(arg1[2]) * x2);
uint128 x13 = ((uint128)(arg1[2]) * x5);
uint128 x14 = ((uint128)(arg1[2]) * (arg1[2]));
uint128 x15 = ((uint128)(arg1[1]) * x2);
uint128 x16 = ((uint128)(arg1[1]) * x6);
uint128 x17 = ((uint128)(arg1[1]) * x7);
uint128 x18 = ((uint128)(arg1[1]) * (arg1[1]));
uint128 x19 = ((uint128)(arg1[0]) * x3);
uint128 x20 = ((uint128)(arg1[0]) * x6);
uint128 x21 = ((uint128)(arg1[0]) * x7);
uint128 x22 = ((uint128)(arg1[0]) * x8);
uint128 x23 = ((uint128)(arg1[0]) * (arg1[0]));
uint128 x24 = (x23 + (x15 + x13));
uint64_t x25 = (uint64_t)(x24 >> 51);
uint64_t x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff));
uint512 x27 = (x19 + (x16 + (x14 + (x11 + x9))));
uint128 x28 = (x20 + x17);
uint128 x29 = (x21 + (x18 + x10));
uint128 x30 = (x22 + x12);
uint128 x31 = (x25 + x30);
uint64_t x32 = (uint64_t)(x31 >> 51);
uint64_t x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff));
uint128 x34 = (x32 + x29);
uint64_t x35 = (uint64_t)(x34 >> 51);
uint64_t x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff));
uint128 x37 = (x35 + x28);
uint64_t x38 = (uint64_t)(x37 >> 51);
uint64_t x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff));
uint512 x40 = (x38 + x27);
uint512 x41 = (x40 >> 51);
uint64_t x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff));
uint512 x43 = (x41 * (uint512)UINT8_C(0x13));
uint512 x44 = (x26 + x43);
uint256 x45 = (uint256)(x44 >> 51);
uint64_t x46 = (uint64_t)(x44 & UINT64_C(0x7ffffffffffff));
uint256 x47 = (x45 + x33);
uint256 x48 = (x47 >> 51);
uint64_t x49 = (uint64_t)(x47 & UINT64_C(0x7ffffffffffff));
uint256 x50 = (x48 + x36);
out1[0] = x46;
out1[1] = x49;
out1[2] = x50;
out1[3] = x39;
out1[4] = x42;
}
with input bounds (Some [Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664], Some [0x0 ~> 0x1a666666666664]], tt).
|
