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