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
89
90
91
92
|
#!/usr/bin/python3
# The purpose of this file is to assist with reverse-engineering addition
# chains from imperative code. One would find an implementation with a good
# addition chain, translate the code to python (vim macros are your friends),
# and replace the middle section of this file with the addition chain. This
# script prints back-indices in the format that AdditionChainExponentiation.v
# accepts.
values = [1]
chain = []
def mul(x,y):
i = values.index(x)
j = values.index(y)
assert values[i] + values[j] == x+y
chain.insert(0, (i, j))
values.insert(0, x+y)
return x+y
def sqr(x):
return mul(x,x)
### ==== cut here ==== ###
z = 1
z2 = sqr(z) # 2
t1 = sqr(z2) # 4
t0 = sqr(t1) # 8
z9 = mul(t0, z) # 9
z11 = mul(z9, z2) # 11
t0 = sqr(z11) # 22
z2_5_0 = mul(t0, z9) # 2^5 - 2^0 = 31 = 22 + 9
t0 = sqr(z2_5_0) # 2^6 - 2^1
t1 = sqr(t0) # 2^7 - 2^2
t0 = sqr(t1) # 2^8 - 2^3
t1 = sqr(t0) # 2^9 - 2^4
t0 = sqr(t1) # 2^10 - 2^5
z2_10_0 = mul(t0, z2_5_0) # 2^10 - 2^0
t0 = sqr(z2_10_0) # 2^11 - 2^1
t1 = sqr(t0) # 2^12 - 2^2
for i in range(2, 10, 2): # 2^20 - 2^10
t0 = sqr(t1)
t1 = sqr(t0)
z2_20_0 = mul(t1, z2_10_0) # 2^20 - 2^0
t0 = sqr(z2_20_0) # 2^21 - 2^1
t1 = sqr(t0) # 2^22 - 2^1
for i in range(2, 20, 2): # 2^40 - 2^20
t0 = sqr(t1)
t1 = sqr(t0)
z2_40_0 = mul(t1, z2_20_0) # 2^40 - 2^0
t0 = sqr(z2_40_0) # 2^41 - 2^1
t1 = sqr(t0) # 2^42 - 2^2
for i in range(2, 10, 2): # 2^50 - 2^10
t0 = sqr(t1)
t1 = sqr(t0)
z2_50_0 = mul(t1, z2_10_0) # 2^50 - 2^0
t0 = sqr(z2_50_0) # 2^51 - 2^1
t1 = sqr(t0) # 2^52 - 2^2
for i in range(2, 50, 2): # 2^100 - 2^50
t0 = sqr(t1)
t1 = sqr(t0)
z2_100_0 = mul(t1, z2_50_0) # 2^100 - 2^0
t0 = sqr(z2_100_0) # 2^101 - 2^1
t1 = sqr(t0) # 2^102 - 2^2
for i in range(2, 100, 2): # 2^200 - 2^100
t0 = sqr(t1)
t1 = sqr(t0)
z2_200_0 = mul(t1, z2_100_0) # 2^200 - 2^0
t0 = sqr(z2_200_0) # 2^201 - 2^1
t1 = sqr(t0) # 2^202 - 2^2
for i in range(2, 50, 2): # 2^250 - 2^50
t0 = sqr(t1)
t1 = sqr(t0)
t0 = mul(t1, z2_50_0) # 2^250 - 2^0
t1 = sqr(t0) # 2^251 - 2^1
t0 = sqr(t1) # 2^252 - 2^2
t1 = sqr(t0) # 2^253 - 2^3
t0 = sqr(t1) # 2^254 - 2^4
t1 = sqr(t0) # 2^255 - 2^5
t0 = mul(t1, z11) # 2^255 - 21
### ==== cut here ==== ###
print (list(reversed(chain)))
|
