Open DavePearce opened 7 years ago
UPDATE: this version where I've replaced bool
with int
does indeed verify:
define invertByte_loopinvariant_51(int[] bits, int i, int[] ret) is:
forall(int j):
if:
(0 <= j) && (j < i)
then:
ret[j] == -(bits[j])
assert "loop invariant not restored":
forall(int[] bits, int[] before, int[] after, int i):
if:
invertByte_loopinvariant_51(bits, i, before)
after == before[i:=-(bits[i])]
then:
invertByte_loopinvariant_51(bits, i+1, after)
The generated proof is also quite large:
130. exists(int[] bits, int[] before, int[] after, int i).(((invertByte_loo ()
141. exists(int[] bits, int[] before, int[] after, int i).((invertB (Simp 130)
140. (invertByte_loopinvariant_51(bits, i, before) && (after == (Exists-E 141)
136. invertByte_loopinvariant_51(bits, i, before) && (after == bef (And-E 140)
139. !invertByte_loopinvariant_51(bits, 1 + i, after) (And-E 140)
116. invertByte_loopinvariant_51(bits, i, before) (And-E 136)
135. after == before[i:=-1 * bits[i]] (And-E 136)
178. forall(int j).(((((0 >= (j + 1)) || ((j + 1) >= (i + 1)))) (Macro-I 116)
180. !invertByte_loopinvariant_51(bits, 1 + i, before[i:=-1 * b (Eq-S 139,135)
195. forall(int j).(((0 >= (1 + j)) || (j >= i)) || (0 == (before[j (Simp 178)
213. exists(int j).((((((j + 1) >= (0 + 1)) && (((1 + i) + 1) >= (Macro-I 180)
225. exists(int j).(((j >= 0) && (i >= j)) && (0 != (bits[j] + befo (Simp 213)
224. ((j >= 0) && (i >= j)) && (0 != (bits[j] + before[i:=-1 * (Exists-E 225)
221. (j >= 0) && (i >= j) (And-E 224)
223. 0 != (bits[j] + before[i:=-1 * bits[i]][j]) (And-E 224)
219. j >= 0 (And-E 221)
220. i >= j (And-E 221)
239. ((i == j) && (0 != (bits[j] + (-1 * bits[i])))) || ((i != (ArrInd-C 223)
256. ((i == j) && (bits[i] != bits[j])) || ((i != j) && (0 != (befo (Simp 239)
┌──────────────────────────────────────────────────────────────────────────────┐
│ 252. (i == j) && (bits[i] != bits[j]) (Or-E 256) │
│ 230. i == j (And-E 252) │
│ 251. bits[i] != bits[j] (And-E 252) │
│ 275. bits[j] != bits[j] (Eq-S 251,230) │
│ 106. false (Simp 275) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 255. (i != j) && (0 != (before[j] + bits[j])) (Or-E 256) │
│ 234. i != j (And-E 255) │
│ 254. 0 != (before[j] + bits[j]) (And-E 255) │
│ 281. (j >= (i + 1)) || (i >= (j + 1)) (Neq-C 234) │
│ 285. ((before[j] + bits[j]) >= (0 + 1)) || (0 >= ((before[j] + b (Neq-C 254) │
│ 299. (j >= (1 + i)) || (i >= (1 + j)) (Simp 281) │
│ 303. ((before[j] + bits[j]) >= 1) || (0 >= (1 + before[j] + bits[ (Simp 285) │
│┌─────────────────────────────────────────────────────────────────────────────┤
││ 296. j >= (1 + i) (Or-E 299) │
││ 323. (-1 + j) >= j (Ieq-I 296,220) │
││ 106. false (Simp 323) │
│├─────────────────────────────────────────────────────────────────────────────┤
││ 298. i >= (1 + j) (Or-E 299) │
││┌────────────────────────────────────────────────────────────────────────────┤
│││ 300. (before[j] + bits[j]) >= 1 (Or-E 303) │
│││ 331. ((0 >= (1 + j)) || (j >= i)) || (0 == (before[j] + (Forall-I 195,300) │
│││┌───────────────────────────────────────────────────────────────────────────┤
││││ 329. (0 >= (1 + j)) || (j >= i) (Or-E 331) │
││││┌──────────────────────────────────────────────────────────────────────────┤
│││││ 327. 0 >= (1 + j) (Or-E 329) │
│││││ 346. -1 >= 0 (Ieq-I 327,219) │
│││││ 106. false (Simp 346) │
││││├──────────────────────────────────────────────────────────────────────────┤
│││││ 328. j >= i (Or-E 329) │
│││││ 348. j >= (1 + j) (Ieq-I 328,298) │
│││││ 106. false (Simp 348) │
││││└──────────────────────────────────────────────────────────────────────────┤
│││├───────────────────────────────────────────────────────────────────────────┤
││││ 330. 0 == (before[j] + bits[j]) (Or-E 331) │
││││ 355. (before[j] + (-1 * before[j])) >= 1 (Eq-S 300,330) │
││││ 106. false (Simp 355) │
│││└───────────────────────────────────────────────────────────────────────────┤
││├────────────────────────────────────────────────────────────────────────────┤
│││ 302. 0 >= (1 + before[j] + bits[j]) (Or-E 303) │
│││ 331. ((0 >= (1 + j)) || (j >= i)) || (0 == (before[j] + (Forall-I 195,302) │
│││┌───────────────────────────────────────────────────────────────────────────┤
││││ 329. (0 >= (1 + j)) || (j >= i) (Or-E 331) │
││││┌──────────────────────────────────────────────────────────────────────────┤
│││││ 327. 0 >= (1 + j) (Or-E 329) │
│││││ 346. -1 >= 0 (Ieq-I 327,219) │
│││││ 106. false (Simp 346) │
││││├──────────────────────────────────────────────────────────────────────────┤
│││││ 328. j >= i (Or-E 329) │
│││││ 348. j >= (1 + j) (Ieq-I 328,298) │
│││││ 106. false (Simp 348) │
││││└──────────────────────────────────────────────────────────────────────────┤
│││├───────────────────────────────────────────────────────────────────────────┤
││││ 330. 0 == (before[j] + bits[j]) (Or-E 331) │
││││ 357. 0 >= (1 + before[j] + (-1 * before[j])) (Eq-S 302,330) │
││││ 106. false (Simp 357) │
│││└───────────────────────────────────────────────────────────────────────────┤
││└────────────────────────────────────────────────────────────────────────────┤
│└─────────────────────────────────────────────────────────────────────────────┤
└──────────────────────────────────────────────────────────────────────────────┘
Why is this proof so large?
The following fails for reasons unknown:
The (somewhat ridiculous) proof for this is:
The generation of
207. (true != bits[j]) != before[i:=true != bits[i]][j]
is somewhat suspect.