1from __future__ import annotations
2
3import json
4import logging
5from dataclasses import dataclass
6from typing import TYPE_CHECKING, Any, Final
7
8from ..cterm import CSubst, CTerm, build_claim
9from ..kast.inner import KApply, KInner, Subst
10from ..kast.manip import extract_lhs, extract_rhs, flatten_label
11from ..prelude.k import GENERATED_TOP_CELL
12from ..prelude.kbool import BOOL, FALSE, TRUE
13from ..prelude.ml import is_bottom, is_top, mlAnd, mlEquals, mlEqualsFalse, mlEqualsTrue
14from ..utils import ensure_dir_path
15from .proof import FailureInfo, Proof, ProofStatus, ProofSummary, Prover
16
17if TYPE_CHECKING:
18 from collections.abc import Iterable, Mapping
19 from pathlib import Path
20
21 from ..kast.inner import KSort
22 from ..kast.outer import KClaim, KDefinition
23 from ..kcfg import KCFGExplore
24 from ..ktool.kprint import KPrint
25
26_LOGGER: Final = logging.getLogger(__name__)
27
28
[docs]
29@dataclass(frozen=True)
30class ImpliesProofStep:
31 proof: ImpliesProof
32
33
[docs]
34@dataclass
35class ImpliesProofResult:
36 csubst: CSubst | None
37 simplified_antecedent: KInner | None
38 simplified_consequent: KInner | None
39
40
[docs]
41class ImpliesProof(Proof[ImpliesProofStep, ImpliesProofResult]):
42 antecedent: KInner
43 consequent: KInner
44 bind_universally: bool
45 simplified_antecedent: KInner | None
46 simplified_consequent: KInner | None
47 csubst: CSubst | None
48
49 def __init__(
50 self,
51 id: str,
52 antecedent: KInner,
53 consequent: KInner,
54 bind_universally: bool = False,
55 simplified_antecedent: KInner | None = None,
56 simplified_consequent: KInner | None = None,
57 csubst: CSubst | None = None,
58 proof_dir: Path | None = None,
59 subproof_ids: Iterable[str] = (),
60 admitted: bool = False,
61 ):
62 super().__init__(id=id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
63 self.antecedent = antecedent
64 self.consequent = consequent
65 self.bind_universally = bind_universally
66 self.simplified_antecedent = simplified_antecedent
67 self.simplified_consequent = simplified_consequent
68 self.csubst = csubst
69
[docs]
70 def get_steps(self) -> list[ImpliesProofStep]:
71 if not self.can_progress:
72 return []
73 return [ImpliesProofStep(self)]
74
[docs]
75 def commit(self, result: ImpliesProofResult) -> None:
76 proof_type = type(self).__name__
77 if isinstance(result, ImpliesProofResult):
78 self.csubst = result.csubst
79 self.simplified_antecedent = result.simplified_antecedent
80 self.simplified_consequent = result.simplified_consequent
81 _LOGGER.info(f'{proof_type} finished {self.id}: {self.status}')
82 else:
83 raise ValueError(f'Incorrect result type, expected ImpliesProofResult: {result}')
84
85 @property
86 def own_status(self) -> ProofStatus:
87 if self.admitted:
88 return ProofStatus.PASSED
89 if self.simplified_antecedent is None or self.simplified_consequent is None:
90 return ProofStatus.PENDING
91 if self.csubst is None:
92 return ProofStatus.FAILED
93 return ProofStatus.PASSED
94
95 @property
96 def can_progress(self) -> bool:
97 return self.simplified_antecedent is None or self.simplified_consequent is None
98
[docs]
99 def write_proof_data(self, subproofs: bool = False) -> None:
100 super().write_proof_data()
101 if not self.proof_dir:
102 return
103 ensure_dir_path(self.proof_dir)
104 ensure_dir_path(self.proof_dir / self.id)
105 proof_path = self.proof_dir / self.id / 'proof.json'
106 if not self.up_to_date:
107 proof_json = json.dumps(self.dict)
108 proof_path.write_text(proof_json)
109 _LOGGER.info(f'Updated proof file {self.id}: {proof_path}')
110
[docs]
111 @classmethod
112 def from_dict(cls: type[ImpliesProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> ImpliesProof:
113 id = dct['id']
114 antecedent = KInner.from_dict(dct['antecedent'])
115 consequent = KInner.from_dict(dct['consequent'])
116 simplified_antecedent = (
117 KInner.from_dict(dct['simplified_antecedent']) if 'simplified_antecedent' in dct else None
118 )
119 simplified_consequent = (
120 KInner.from_dict(dct['simplified_consequent']) if 'simplified_consequent' in dct else None
121 )
122 csubst = CSubst.from_dict(dct['csubst']) if 'csubst' in dct else None
123 subproof_ids = dct['subproof_ids']
124 admitted = dct.get('admitted', False)
125 return ImpliesProof(
126 id,
127 antecedent,
128 consequent,
129 simplified_antecedent=simplified_antecedent,
130 simplified_consequent=simplified_consequent,
131 csubst=csubst,
132 admitted=admitted,
133 subproof_ids=subproof_ids,
134 proof_dir=proof_dir,
135 )
136
137 @property
138 def dict(self) -> dict[str, Any]:
139 dct = super().dict
140 dct['type'] = 'ImpliesProof'
141 dct['antecedent'] = self.antecedent.to_dict()
142 dct['consequent'] = self.consequent.to_dict()
143 if self.simplified_antecedent is not None:
144 dct['simplified_antecedent'] = self.simplified_antecedent.to_dict()
145 if self.simplified_consequent is not None:
146 dct['simplified_consequent'] = self.simplified_consequent.to_dict()
147 if self.csubst is not None:
148 dct['csubst'] = self.csubst.to_dict()
149 return dct
150
151
[docs]
152class EqualityProof(ImpliesProof):
153 def __init__(
154 self,
155 id: str,
156 lhs_body: KInner,
157 rhs_body: KInner,
158 sort: KSort,
159 constraints: Iterable[KInner] = (),
160 simplified_constraints: KInner | None = None,
161 simplified_equality: KInner | None = None,
162 csubst: CSubst | None = None,
163 proof_dir: Path | None = None,
164 subproof_ids: Iterable[str] = (),
165 admitted: bool = False,
166 ):
167 antecedent = mlAnd(constraints)
168 consequent = mlEquals(lhs_body, rhs_body, arg_sort=sort, sort=GENERATED_TOP_CELL)
169 super().__init__(
170 id,
171 antecedent,
172 consequent,
173 bind_universally=True,
174 simplified_antecedent=simplified_constraints,
175 simplified_consequent=simplified_equality,
176 csubst=csubst,
177 proof_dir=proof_dir,
178 subproof_ids=subproof_ids,
179 admitted=admitted,
180 )
181 _LOGGER.warning(
182 'Building an EqualityProof that has known soundness issues: See https://github.com/runtimeverification/haskell-backend/issues/3605.'
183 )
184
[docs]
185 @staticmethod
186 def read_proof_data(proof_dir: Path, id: str) -> EqualityProof:
187 proof_path = proof_dir / id / 'proof.json'
188 if Proof.proof_data_exists(id, proof_dir):
189 proof_dict = json.loads(proof_path.read_text())
190 return EqualityProof.from_dict(proof_dict, proof_dir)
191
192 raise ValueError(f'Could not load Proof from file {id}: {proof_path}')
193
[docs]
194 @staticmethod
195 def from_claim(claim: KClaim, defn: KDefinition, proof_dir: Path | None = None) -> EqualityProof:
196 claim_body = defn.add_sort_params(claim.body)
197 sort = defn.sort_strict(claim_body)
198 lhs_body = extract_lhs(claim_body)
199 rhs_body = extract_rhs(claim_body)
200 if not (claim.ensures is None or claim.ensures == TRUE):
201 raise ValueError(f'Cannot convert claim to EqualityProof due to non-trival ensures clause {claim.ensures}')
202 constraints = [mlEquals(TRUE, c, arg_sort=BOOL) for c in flatten_label('_andBool_', claim.requires)]
203 return EqualityProof(claim.label, lhs_body, rhs_body, sort, constraints=constraints, proof_dir=proof_dir)
204
205 @property
206 def equality(self) -> KApply:
207 assert type(self.consequent) is KApply
208 return self.consequent
209
210 @property
211 def lhs_body(self) -> KInner:
212 return self.equality.args[0]
213
214 @property
215 def rhs_body(self) -> KInner:
216 return self.equality.args[1]
217
218 @property
219 def sort(self) -> KSort:
220 return self.equality.label.params[0]
221
222 @property
223 def constraint(self) -> KInner:
224 return self.antecedent
225
226 @property
227 def constraints(self) -> list[KInner]:
228 return flatten_label('#And', self.constraint)
229
230 @property
231 def simplified_constraints(self) -> KInner | None:
232 return self.simplified_antecedent
233
234 @property
235 def simplified_equality(self) -> KInner | None:
236 return self.simplified_consequent
237
[docs]
238 @classmethod
239 def from_dict(cls: type[EqualityProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> EqualityProof:
240 implies_proof = ImpliesProof.from_dict(dct, proof_dir=proof_dir)
241 assert type(implies_proof.consequent) is KApply
242 return EqualityProof(
243 id=implies_proof.id,
244 lhs_body=implies_proof.consequent.args[0],
245 rhs_body=implies_proof.consequent.args[1],
246 sort=implies_proof.consequent.label.params[0],
247 constraints=flatten_label('#And', implies_proof.antecedent),
248 simplified_constraints=implies_proof.simplified_antecedent,
249 simplified_equality=implies_proof.simplified_consequent,
250 csubst=implies_proof.csubst,
251 proof_dir=implies_proof.proof_dir,
252 subproof_ids=implies_proof.subproof_ids,
253 admitted=implies_proof.admitted,
254 )
255
256 @property
257 def dict(self) -> dict[str, Any]:
258 dct = super().dict
259 dct['type'] = 'EqualityProof'
260 return dct
261
[docs]
262 def pretty(self, kprint: KPrint) -> Iterable[str]:
263 lines = [
264 f'LHS: {kprint.pretty_print(self.lhs_body)}',
265 f'RHS: {kprint.pretty_print(self.rhs_body)}',
266 f'Constraints: {kprint.pretty_print(mlAnd(self.constraints))}',
267 f'Equality: {kprint.pretty_print(self.equality)}',
268 ]
269 if self.simplified_constraints:
270 lines.append(f'Simplified constraints: {kprint.pretty_print(self.simplified_constraints)}')
271 if self.simplified_equality:
272 lines.append(f'Simplified equality: {kprint.pretty_print(self.simplified_equality)}')
273 if self.csubst is not None:
274 lines.append(f'Implication csubst: {self.csubst}')
275 lines.append(f'Status: {self.status}')
276 return lines
277
278 @property
279 def summary(self) -> EqualitySummary:
280 return EqualitySummary(self.id, self.status, self.admitted)
281
282
[docs]
283@dataclass(frozen=True)
284class EqualitySummary(ProofSummary):
285 id: str
286 status: ProofStatus
287 admitted: bool
288
289 @property
290 def lines(self) -> list[str]:
291 return [
292 f'EqualityProof: {self.id}',
293 f' status: {self.status}',
294 f' admitted: {self.admitted}',
295 ]
296
297
[docs]
298class RefutationProof(ImpliesProof):
299 def __init__(
300 self,
301 id: str,
302 pre_constraints: Iterable[KInner],
303 last_constraint: KInner,
304 simplified_antecedent: KInner | None = None,
305 simplified_consequent: KInner | None = None,
306 csubst: CSubst | None = None,
307 proof_dir: Path | None = None,
308 subproof_ids: Iterable[str] = (),
309 admitted: bool = False,
310 ):
311 antecedent = mlAnd(mlEqualsTrue(c) for c in pre_constraints)
312 consequent = mlEqualsFalse(last_constraint)
313 super().__init__(
314 id,
315 antecedent,
316 consequent,
317 bind_universally=True,
318 simplified_antecedent=simplified_antecedent,
319 simplified_consequent=simplified_consequent,
320 csubst=csubst,
321 subproof_ids=subproof_ids,
322 proof_dir=proof_dir,
323 admitted=admitted,
324 )
325 _LOGGER.warning(
326 'Building a RefutationProof that has known soundness issues: See https://github.com/runtimeverification/haskell-backend/issues/3605.'
327 )
328
[docs]
329 @staticmethod
330 def read_proof_data(proof_dir: Path, id: str) -> RefutationProof:
331 proof_path = proof_dir / id / 'proof.json'
332 if Proof.proof_data_exists(id, proof_dir):
333 proof_dict = json.loads(proof_path.read_text())
334 return RefutationProof.from_dict(proof_dict, proof_dir)
335
336 raise ValueError(f'Could not load Proof from file {id}: {proof_path}')
337
338 @property
339 def pre_constraints(self) -> list[KInner]:
340 return flatten_label('#And', self.antecedent)
341
342 @property
343 def last_constraint(self) -> KInner:
344 assert type(self.consequent) is KApply
345 return self.consequent.args[1]
346
347 @property
348 def simplified_constraints(self) -> KInner | None:
349 return self.simplified_antecedent
350
[docs]
351 @classmethod
352 def from_dict(cls: type[RefutationProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> RefutationProof:
353 implies_proof = ImpliesProof.from_dict(dct, proof_dir=proof_dir)
354 assert type(implies_proof.consequent) is KApply
355 return RefutationProof(
356 id=implies_proof.id,
357 pre_constraints=flatten_label('#And', implies_proof.antecedent),
358 last_constraint=implies_proof.consequent.args[1],
359 simplified_antecedent=implies_proof.simplified_antecedent,
360 simplified_consequent=implies_proof.simplified_consequent,
361 csubst=implies_proof.csubst,
362 proof_dir=implies_proof.proof_dir,
363 subproof_ids=implies_proof.subproof_ids,
364 admitted=implies_proof.admitted,
365 )
366
367 @property
368 def dict(self) -> dict[str, Any]:
369 dct = super().dict
370 dct['type'] = 'RefutationProof'
371 return dct
372
373 @property
374 def summary(self) -> RefutationSummary:
375 return RefutationSummary(self.id, self.status)
376
[docs]
377 def pretty(self, kprint: KPrint) -> Iterable[str]:
378 lines = [
379 f'Constraints: {kprint.pretty_print(mlAnd(self.pre_constraints))}',
380 f'Last constraint: {kprint.pretty_print(self.last_constraint)}',
381 ]
382 if self.csubst is not None:
383 lines.append(f'Implication csubst: {self.csubst}')
384 lines.append(f'Status: {self.status}')
385 return lines
386
[docs]
387 def to_claim(self, claim_id: str) -> tuple[KClaim, Subst]:
388 return build_claim(
389 claim_id,
390 init_config=self.last_constraint,
391 final_config=FALSE,
392 init_constraints=self.pre_constraints,
393 final_constraints=[],
394 )
395
396
[docs]
397@dataclass(frozen=True)
398class RefutationSummary(ProofSummary):
399 id: str
400 status: ProofStatus
401
402 @property
403 def lines(self) -> list[str]:
404 return [
405 f'RefutationProof: {self.id}',
406 f' status: {self.status}',
407 ]
408
409
[docs]
410class ImpliesProver(Prover[ImpliesProof, ImpliesProofStep, ImpliesProofResult]):
411 proof: ImpliesProof
412 kcfg_explore: KCFGExplore
413 assume_defined: bool
414
[docs]
415 def close(self) -> None:
416 self.kcfg_explore.cterm_symbolic._kore_client.close()
417
418 def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore, assume_defined: bool = False):
419 self.kcfg_explore = kcfg_explore
420 self.proof = proof
421 self.assume_defined = assume_defined
422
[docs]
423 def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
424 proof_type = type(step.proof).__name__
425 _LOGGER.info(f'Attempting {proof_type} {step.proof.id}')
426
427 if step.proof.status is not ProofStatus.PENDING:
428 _LOGGER.info(f'{proof_type} finished {step.proof.id}: {step.proof.status}')
429 return []
430
431 # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e.
432 # "LHS equals RHS under these constraints"
433 simplified_antecedent, _ = self.kcfg_explore.cterm_symbolic.kast_simplify(step.proof.antecedent)
434 simplified_consequent, _ = self.kcfg_explore.cterm_symbolic.kast_simplify(step.proof.consequent)
435 _LOGGER.debug(f'Simplified antecedent: {self.kcfg_explore.pretty_print(simplified_antecedent)}')
436 _LOGGER.debug(f'Simplified consequent: {self.kcfg_explore.pretty_print(simplified_consequent)}')
437
438 csubst: CSubst | None = None
439
440 if is_bottom(simplified_antecedent):
441 _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {step.proof.id}')
442 csubst = CSubst(Subst({}), ())
443
444 elif is_top(simplified_consequent):
445 _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {step.proof.id}')
446 csubst = CSubst(Subst({}), ())
447
448 else:
449 # TODO: we should not be forced to include the dummy configuration in the antecedent and consequent
450 dummy_config = self.kcfg_explore.cterm_symbolic._definition.empty_config(sort=GENERATED_TOP_CELL)
451 _result = self.kcfg_explore.cterm_symbolic.implies(
452 antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]),
453 consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]),
454 bind_universally=step.proof.bind_universally,
455 assume_defined=self.assume_defined,
456 )
457 result = _result.csubst
458 if result is not None:
459 csubst = result
460
461 _LOGGER.info(f'{proof_type} finished {step.proof.id}: {step.proof.status}')
462 return [
463 ImpliesProofResult(
464 csubst=csubst, simplified_antecedent=simplified_antecedent, simplified_consequent=simplified_consequent
465 )
466 ]
467
[docs]
468 def init_proof(self, proof: ImpliesProof) -> None:
469 pass
470
[docs]
471 def failure_info(self, proof: ImpliesProof) -> FailureInfo:
472 # TODO add implementation
473 return FailureInfo()