Skip to content

Commit 591f0e6

Browse files
dranovdranov
committed
feat: counter-example view in verification results
1 parent 6f706bf commit 591f0e6

File tree

2 files changed

+195
-157
lines changed

2 files changed

+195
-157
lines changed

‎ProofWidgets/Demos/VerificationResults.lean‎

Lines changed: 94 additions & 151 deletions
Original file line numberDiff line numberDiff line change
@@ -17,245 +17,188 @@ def exampleResults : Json := json% {"vcs":
1717
"dischargers":
1818
[{"time": 28,
1919
"status": "proven",
20+
"result": {"time": 28, "status": "proven", "data": null},
2021
"name": "initializer_doesNotThrow_0",
2122
"id": 0}]},
2223
"status": "proven",
2324
"name": "initializer_doesNotThrow",
24-
"metadata":
25-
{"stmtDerivedFrom": ["Invariants", "initializer", "Assumptions"],
26-
"property": "doesNotThrow",
27-
"kind": "primary",
28-
"action": "initializer"},
25+
"metadata": {"property": "doesNotThrow", "kind": "primary", "action": "initializer"},
2926
"id": 0},
3027
{"timing":
31-
{"totalTime": 506,
32-
"successfulDischargerTime": 506,
28+
{"totalTime": 330,
29+
"successfulDischargerTime": 330,
3330
"successfulDischargerId": 0,
3431
"dischargers":
35-
[{"time": 506,
32+
[{"time": 330,
3633
"status": "proven",
34+
"result": {"time": 330, "status": "proven", "data": {"unsatCores": [[]], "kind": "unsat"}},
3735
"name": "initializer_single_leader_0",
3836
"id": 0}]},
3937
"status": "proven",
4038
"name": "initializer_single_leader",
41-
"metadata":
42-
{"stmtDerivedFrom":
43-
["Invariants", "initializer", "Assumptions", "single_leader"],
44-
"property": "single_leader",
45-
"kind": "primary",
46-
"action": "initializer"},
39+
"metadata": {"property": "single_leader", "kind": "primary", "action": "initializer"},
4740
"id": 1},
4841
{"timing":
49-
{"totalTime": 100,
50-
"successfulDischargerTime": 100,
42+
{"totalTime": 82,
43+
"successfulDischargerTime": 82,
5144
"successfulDischargerId": 0,
5245
"dischargers":
53-
[{"time": 100,
46+
[{"time": 82,
5447
"status": "proven",
48+
"result": {"time": 82, "status": "proven", "data": null},
5549
"name": "initializer_leader_greatest_0",
5650
"id": 0}]},
5751
"status": "proven",
5852
"name": "initializer_leader_greatest",
59-
"metadata":
60-
{"stmtDerivedFrom":
61-
["leader_greatest", "Invariants", "initializer", "Assumptions"],
62-
"property": "leader_greatest",
63-
"kind": "primary",
64-
"action": "initializer"},
53+
"metadata": {"property": "leader_greatest", "kind": "primary", "action": "initializer"},
6554
"id": 2},
6655
{"timing":
67-
{"totalTime": 568,
68-
"successfulDischargerTime": 568,
56+
{"totalTime": 90,
57+
"successfulDischargerTime": 90,
6958
"successfulDischargerId": 0,
7059
"dischargers":
71-
[{"time": 568,
60+
[{"time": 90,
7261
"status": "proven",
62+
"result": {"time": 90, "status": "proven", "data": null},
7363
"name": "initializer_inv_1_0",
7464
"id": 0}]},
7565
"status": "proven",
7666
"name": "initializer_inv_1",
77-
"metadata":
78-
{"stmtDerivedFrom": ["Invariants", "initializer", "Assumptions", "inv_1"],
79-
"property": "inv_1",
80-
"kind": "primary",
81-
"action": "initializer"},
67+
"metadata": {"property": "inv_1", "kind": "primary", "action": "initializer"},
8268
"id": 3},
8369
{"timing":
84-
{"totalTime": 92,
85-
"successfulDischargerTime": 92,
70+
{"totalTime": 368,
71+
"successfulDischargerTime": 368,
8672
"successfulDischargerId": 0,
8773
"dischargers":
88-
[{"time": 92, "status": "proven", "name": "initializer_inv_2_0", "id": 0}]},
89-
"status": "proven",
90-
"name": "initializer_inv_2",
91-
"metadata":
92-
{"stmtDerivedFrom": ["Invariants", "initializer", "Assumptions", "inv_2"],
93-
"property": "inv_2",
94-
"kind": "primary",
95-
"action": "initializer"},
96-
"id": 4},
97-
{"timing":
98-
{"totalTime": 544,
99-
"successfulDischargerTime": 544,
100-
"successfulDischargerId": 0,
101-
"dischargers":
102-
[{"time": 544,
74+
[{"time": 368,
10375
"status": "proven",
76+
"result": {"time": 368, "status": "proven", "data": {"unsatCores": [[]], "kind": "unsat"}},
10477
"name": "send_doesNotThrow_0",
10578
"id": 0}]},
10679
"status": "proven",
10780
"name": "send_doesNotThrow",
108-
"metadata":
109-
{"stmtDerivedFrom": ["send", "Invariants", "Assumptions"],
110-
"property": "doesNotThrow",
111-
"kind": "primary",
112-
"action": "send"},
113-
"id": 5},
81+
"metadata": {"property": "doesNotThrow", "kind": "primary", "action": "send"},
82+
"id": 4},
11483
{"timing":
115-
{"totalTime": 644,
116-
"successfulDischargerTime": 644,
84+
{"totalTime": 413,
85+
"successfulDischargerTime": 413,
11786
"successfulDischargerId": 0,
11887
"dischargers":
119-
[{"time": 644,
88+
[{"time": 413,
12089
"status": "proven",
90+
"result":
91+
{"time": 413, "status": "proven", "data": {"unsatCores": [["_uniq.60168", "_uniq.60329"]], "kind": "unsat"}},
12192
"name": "send_single_leader_0",
12293
"id": 0}]},
12394
"status": "proven",
12495
"name": "send_single_leader",
125-
"metadata":
126-
{"stmtDerivedFrom": ["send", "Invariants", "Assumptions", "single_leader"],
127-
"property": "single_leader",
128-
"kind": "primary",
129-
"action": "send"},
130-
"id": 6},
96+
"metadata": {"property": "single_leader", "kind": "primary", "action": "send"},
97+
"id": 5},
13198
{"timing":
132-
{"totalTime": 605,
133-
"successfulDischargerTime": 605,
99+
{"totalTime": 391,
100+
"successfulDischargerTime": 391,
134101
"successfulDischargerId": 0,
135102
"dischargers":
136-
[{"time": 605,
103+
[{"time": 391,
137104
"status": "proven",
105+
"result":
106+
{"time": 391, "status": "proven", "data": {"unsatCores": [["_uniq.60109", "_uniq.60242"]], "kind": "unsat"}},
138107
"name": "send_leader_greatest_0",
139108
"id": 0}]},
140109
"status": "proven",
141110
"name": "send_leader_greatest",
142-
"metadata":
143-
{"stmtDerivedFrom": ["send", "leader_greatest", "Invariants", "Assumptions"],
144-
"property": "leader_greatest",
145-
"kind": "primary",
146-
"action": "send"},
147-
"id": 7},
111+
"metadata": {"property": "leader_greatest", "kind": "primary", "action": "send"},
112+
"id": 6},
148113
{"timing":
149-
{"totalTime": 675,
150-
"successfulDischargerTime": 675,
114+
{"totalTime": 423,
115+
"successfulDischargerTime": 423,
151116
"successfulDischargerId": 0,
152117
"dischargers":
153-
[{"time": 675, "status": "proven", "name": "send_inv_1_0", "id": 0}]},
118+
[{"time": 423,
119+
"status": "proven",
120+
"result":
121+
{"time": 423,
122+
"status": "proven",
123+
"data": {"unsatCores": [["_uniq.61147", "_uniq.61278", "_uniq.61281"]], "kind": "unsat"}},
124+
"name": "send_inv_1_0",
125+
"id": 0}]},
154126
"status": "proven",
155127
"name": "send_inv_1",
156-
"metadata":
157-
{"stmtDerivedFrom": ["send", "Invariants", "Assumptions", "inv_1"],
158-
"property": "inv_1",
159-
"kind": "primary",
160-
"action": "send"},
161-
"id": 8},
162-
{"timing":
163-
{"totalTime": 641,
164-
"successfulDischargerTime": 641,
165-
"successfulDischargerId": 0,
166-
"dischargers":
167-
[{"time": 641, "status": "proven", "name": "send_inv_2_0", "id": 0}]},
168-
"status": "proven",
169-
"name": "send_inv_2",
170-
"metadata":
171-
{"stmtDerivedFrom": ["send", "Invariants", "Assumptions", "inv_2"],
172-
"property": "inv_2",
173-
"kind": "primary",
174-
"action": "send"},
175-
"id": 9},
128+
"metadata": {"property": "inv_1", "kind": "primary", "action": "send"},
129+
"id": 7},
176130
{"timing":
177-
{"totalTime": 603,
178-
"successfulDischargerTime": 603,
131+
{"totalTime": 412,
132+
"successfulDischargerTime": 412,
179133
"successfulDischargerId": 0,
180134
"dischargers":
181-
[{"time": 603,
135+
[{"time": 412,
182136
"status": "proven",
137+
"result": {"time": 412, "status": "proven", "data": {"unsatCores": [[]], "kind": "unsat"}},
183138
"name": "recv_doesNotThrow_0",
184139
"id": 0}]},
185140
"status": "proven",
186141
"name": "recv_doesNotThrow",
187-
"metadata":
188-
{"stmtDerivedFrom": ["recv", "Invariants", "Assumptions"],
189-
"property": "doesNotThrow",
190-
"kind": "primary",
191-
"action": "recv"},
192-
"id": 10},
142+
"metadata": {"property": "doesNotThrow", "kind": "primary", "action": "recv"},
143+
"id": 8},
193144
{"timing":
194-
{"totalTime": 514,
195-
"successfulDischargerTime": 514,
145+
{"totalTime": 432,
146+
"successfulDischargerTime": 432,
196147
"successfulDischargerId": 0,
197148
"dischargers":
198-
[{"time": 514,
149+
[{"time": 432,
199150
"status": "proven",
151+
"result":
152+
{"time": 432,
153+
"status": "proven",
154+
"data":
155+
{"unsatCores": [["_uniq.62433", "_uniq.62592", "_uniq.62628", "_uniq.62629", "_uniq.62768"]], "kind": "unsat"}},
200156
"name": "recv_single_leader_0",
201157
"id": 0}]},
202158
"status": "proven",
203159
"name": "recv_single_leader",
204-
"metadata":
205-
{"stmtDerivedFrom": ["recv", "Invariants", "Assumptions", "single_leader"],
206-
"property": "single_leader",
207-
"kind": "primary",
208-
"action": "recv"},
209-
"id": 11},
160+
"metadata": {"property": "single_leader", "kind": "primary", "action": "recv"},
161+
"id": 9},
210162
{"timing":
211-
{"totalTime": 477,
212-
"successfulDischargerTime": 477,
163+
{"totalTime": 408,
164+
"successfulDischargerTime": 408,
213165
"successfulDischargerId": 0,
214166
"dischargers":
215-
[{"time": 477,
167+
[{"time": 408,
216168
"status": "proven",
169+
"result":
170+
{"time": 408,
171+
"status": "proven",
172+
"data": {"unsatCores": [["_uniq.61954", "_uniq.61955", "_uniq.62093"]], "kind": "unsat"}},
217173
"name": "recv_leader_greatest_0",
218174
"id": 0}]},
219175
"status": "proven",
220176
"name": "recv_leader_greatest",
221-
"metadata":
222-
{"stmtDerivedFrom": ["recv", "leader_greatest", "Invariants", "Assumptions"],
223-
"property": "leader_greatest",
224-
"kind": "primary",
225-
"action": "recv"},
226-
"id": 12},
177+
"metadata": {"property": "leader_greatest", "kind": "primary", "action": "recv"},
178+
"id": 10},
227179
{"timing":
228-
{"totalTime": 559,
229-
"successfulDischargerTime": 559,
230-
"successfulDischargerId": 0,
180+
{"totalTime": 311,
181+
"successfulDischargerTime": null,
182+
"successfulDischargerId": null,
231183
"dischargers":
232-
[{"time": 559, "status": "proven", "name": "recv_inv_1_0", "id": 0}]},
233-
"status": "proven",
184+
[{"time": 311,
185+
"status": "disproven",
186+
"result":
187+
{"time": 311,
188+
"status": "disproven",
189+
"data":
190+
{"kind": "sat",
191+
"counterexamples": [{"model": {"values": 8, "sorts": 1}, "html": {"text": "no model"}}]}},
192+
"name": "recv_inv_1_0",
193+
"id": 0}]},
194+
"status": "disproven",
234195
"name": "recv_inv_1",
235-
"metadata":
236-
{"stmtDerivedFrom": ["recv", "Invariants", "Assumptions", "inv_1"],
237-
"property": "inv_1",
238-
"kind": "primary",
239-
"action": "recv"},
240-
"id": 13},
241-
{"timing":
242-
{"totalTime": 518,
243-
"successfulDischargerTime": 518,
244-
"successfulDischargerId": 0,
245-
"dischargers":
246-
[{"time": 518, "status": "proven", "name": "recv_inv_2_0", "id": 0}]},
247-
"status": "proven",
248-
"name": "recv_inv_2",
249-
"metadata":
250-
{"stmtDerivedFrom": ["recv", "Invariants", "Assumptions", "inv_2"],
251-
"property": "inv_2",
252-
"kind": "primary",
253-
"action": "recv"},
254-
"id": 14}],
255-
"totalVCs": 15,
256-
"totalTime": 7074,
257-
"totalSolved": 15,
258-
"totalDischarged": 15}
196+
"metadata": {"property": "inv_1", "kind": "primary", "action": "recv"},
197+
"id": 11}],
198+
"totalVCs": 12,
199+
"totalTime": 3688,
200+
"totalSolved": 11,
201+
"totalDischarged": 12}
259202

260203

261204
instance : Lean.Server.RpcEncodable Unit where

0 commit comments

Comments
 (0)