1use omena_cascade::{
8 BoxLonghandInputV0, LayerFlattenInputV0, LonghandMergeInputV0, ScopeFlattenInputV0,
9 StaticSupportsAssumptionV0, StaticSupportsEvalVerdictV0, evaluate_static_supports_condition,
10 prove_box_shorthand_combination, prove_layer_flatten_candidate, prove_longhand_merge,
11 prove_scope_flatten_candidate,
12};
13use omena_evidence_graph::{
14 EvidenceDemandEdgeV0, EvidenceGraphBuildErrorV0, EvidenceGraphV0, EvidenceNodeKeyV0,
15 EvidenceNodeSeedV0, FamilyStampV0, GuaranteeKindV0, LedgerDischargeWitnessV0,
16 ObligationFamilyIdV0, ProseObligationProvenanceV0, build_evidence_graph_from_edges_v0,
17};
18use omena_refinement_trait::RefinementVerdictV0;
19use serde::Serialize;
20
21pub mod discharge_ledger;
22pub mod fuzz;
23
24pub use discharge_ledger::{
25 DISCHARGE_LEDGER_PRODUCT_V1, DISCHARGE_LEDGER_SCHEMA_VERSION_V1, DischargeLedgerLookupStatusV0,
26 DischargeLedgerLookupV0, DischargeLedgerVerdictV0, discharge_ledger_cell_key_v0,
27 lookup_discharge_ledger_entry_v0,
28};
29pub use fuzz::{
30 SmtBisimulationFuzzCaseV0, SmtBisimulationFuzzReportV0, run_smt_bisimulation_fuzz_case_v0,
31 run_smt_bisimulation_fuzz_seed_corpus_v0, smt_bisimulation_fuzz_case_v0,
32};
33
34pub const SMT_SCHEMA_VERSION_V0: &str = "0";
35pub const SMT_LAYER_MARKER_V0: &str = "smt-cascade-verification";
36pub const SMT_FEATURE_GATE_V0: &str = "smt-stub";
37const REWRITE_PROOF_INPUT_EVIDENCE_QUERY_V0: &str = "omena-cascade-proof.transform-rewrite-input";
38const CASCADE_PROOF_RECORD_EVIDENCE_QUERY_V0: &str = "omena-cascade-proof.cascade-proof-record";
39const CASCADE_PROOF_EVIDENCE_EDGE_KIND_V0: &str = "cascade-proof-evidence";
40pub const TRANSFORM_REWRITE_PROOF_INPUT_OBLIGATION_FAMILY_V0: ObligationFamilyIdV0 =
41 ObligationFamilyIdV0::CascadeObligationDeclaration;
42
43fn prose_obligation_family_stamp(provenance: &[String]) -> FamilyStampV0 {
44 let Some(prose_provenance) = ProseObligationProvenanceV0::from_provenance_labels(provenance)
45 else {
46 unreachable!("prose evidence seeds include an obligation provenance label")
47 };
48 FamilyStampV0::prose_obligation_discharged(&prose_provenance)
49}
50
51const CASCADE_SMT_SPEC_MATERIAL_V0: &str = "\
52schema=0\n\
53theory=cascade-smt-theory-v0\n\
54encoding=canonical-smt-input-v0\n\
55default-backend=stub-propositional\n\
56opt-in-backend=smt-z3-qf-lia-layer-inversion\n\
57obligations=box-shorthand-combination,scope-flatten-candidate,layer-flatten-candidate,static-supports-condition\n\
58";
59
60#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
61#[serde(rename_all = "camelCase")]
62pub struct CanonicalSmtInputV0 {
63 pub schema_version: &'static str,
64 pub product: &'static str,
65 pub layer_marker: &'static str,
66 pub feature_gate: &'static str,
67 pub obligation_id: String,
68 pub l1_primitive: &'static str,
69 pub canonical_terms: Vec<String>,
70 pub smtlib2_script: String,
71}
72
73pub fn canonical_smt_input_v0(
74 obligation_id: impl Into<String>,
75 l1_primitive: &'static str,
76 canonical_terms: Vec<String>,
77) -> CanonicalSmtInputV0 {
78 let smtlib2_script = canonical_smtlib2_script_v0(&canonical_terms);
79 CanonicalSmtInputV0 {
80 schema_version: SMT_SCHEMA_VERSION_V0,
81 product: "omena-smt.canonical-input",
82 layer_marker: SMT_LAYER_MARKER_V0,
83 feature_gate: SMT_FEATURE_GATE_V0,
84 obligation_id: obligation_id.into(),
85 l1_primitive,
86 canonical_terms,
87 smtlib2_script,
88 }
89}
90
91pub fn canonical_smt_input_with_script_v0(
92 obligation_id: impl Into<String>,
93 l1_primitive: &'static str,
94 canonical_terms: Vec<String>,
95 smtlib2_script: String,
96) -> CanonicalSmtInputV0 {
97 CanonicalSmtInputV0 {
98 schema_version: SMT_SCHEMA_VERSION_V0,
99 product: "omena-smt.canonical-input",
100 layer_marker: SMT_LAYER_MARKER_V0,
101 feature_gate: SMT_FEATURE_GATE_V0,
102 obligation_id: obligation_id.into(),
103 l1_primitive,
104 canonical_terms,
105 smtlib2_script,
106 }
107}
108
109pub fn canonical_smtlib2_script_v0(canonical_terms: &[String]) -> String {
110 let mut script = String::from("(set-logic QF_UF)\n");
111 for term in canonical_terms {
112 if let Some((name, value)) = canonical_requirement_parts_v0(term) {
113 let symbol = smtlib2_named_assertion_symbol_v0(name);
114 let atom = if value { "true" } else { "false" };
115 script.push_str(&format!("(assert (! {atom} :named {symbol}))\n"));
116 } else {
117 let comment = smtlib2_comment_v0(term);
118 script.push_str(&format!("; {comment}\n"));
119 }
120 }
121 script
122}
123
124pub fn canonical_requirement_value_v0(term: &str) -> Option<bool> {
125 canonical_requirement_parts_v0(term).map(|(_, value)| value)
126}
127
128pub fn canonical_input_has_unknown_v0(input: &CanonicalSmtInputV0) -> bool {
129 input
130 .canonical_terms
131 .iter()
132 .any(|term| term.starts_with("unknown:"))
133}
134
135fn canonical_requirement_parts_v0(term: &str) -> Option<(&str, bool)> {
136 let (name, value) = term.strip_prefix("require:")?.rsplit_once('=')?;
137 match value {
138 "true" => Some((name, true)),
139 "false" => Some((name, false)),
140 _ => None,
141 }
142}
143
144fn smtlib2_named_assertion_symbol_v0(name: &str) -> String {
145 let mut symbol = String::from("req_");
146 for ch in name.chars() {
147 if ch.is_ascii_alphanumeric() {
148 symbol.push(ch);
149 } else {
150 symbol.push('_');
151 }
152 }
153 symbol
154}
155
156fn smtlib2_comment_v0(term: &str) -> String {
157 term.chars()
158 .map(|ch| match ch {
159 '\n' | '\r' => ' ',
160 _ => ch,
161 })
162 .collect()
163}
164
165#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
166#[serde(rename_all = "camelCase")]
167pub enum SmtBackendKindV0 {
168 Stub,
169 Z3,
170}
171
172#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
173#[serde(rename_all = "camelCase")]
174pub enum SmtBackendSatResultV0 {
175 Sat,
176 Unsat,
177 Unknown,
178}
179
180#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
181#[serde(rename_all = "camelCase")]
182pub struct SmtBackendCheckV0 {
183 pub schema_version: &'static str,
184 pub product: &'static str,
185 pub layer_marker: &'static str,
186 pub feature_gate: &'static str,
187 pub backend: SmtBackendKindV0,
188 pub obligation_id: String,
189 pub formula_count: usize,
190 pub sat_result: SmtBackendSatResultV0,
191 pub model_available: bool,
192}
193
194pub trait SmtBackendV0 {
195 fn backend_kind(&self) -> SmtBackendKindV0;
196
197 fn quantifier_elimination_tactic(&self) -> Option<&'static str> {
198 None
199 }
200
201 fn check_canonical_input_v0(&self, input: &CanonicalSmtInputV0) -> SmtBackendCheckV0 {
202 let sat_result = if canonical_input_has_unknown_v0(input) {
203 SmtBackendSatResultV0::Unknown
204 } else if input
205 .canonical_terms
206 .iter()
207 .all(|term| canonical_requirement_value_v0(term).unwrap_or(true))
208 {
209 SmtBackendSatResultV0::Sat
210 } else {
211 SmtBackendSatResultV0::Unsat
212 };
213 SmtBackendCheckV0 {
214 schema_version: SMT_SCHEMA_VERSION_V0,
215 product: "omena-smt.backend-check",
216 layer_marker: SMT_LAYER_MARKER_V0,
217 feature_gate: SMT_FEATURE_GATE_V0,
218 backend: self.backend_kind(),
219 obligation_id: input.obligation_id.clone(),
220 formula_count: input.canonical_terms.len(),
221 sat_result,
222 model_available: matches!(sat_result, SmtBackendSatResultV0::Sat),
223 }
224 }
225}
226
227#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
228#[serde(rename_all = "camelCase")]
229pub struct StubSmtBackendV0 {
230 pub schema_version: &'static str,
231 pub product: &'static str,
232 pub layer_marker: &'static str,
233 pub feature_gate: &'static str,
234}
235
236impl Default for StubSmtBackendV0 {
237 fn default() -> Self {
238 Self {
239 schema_version: SMT_SCHEMA_VERSION_V0,
240 product: "omena-smt.backend.stub",
241 layer_marker: SMT_LAYER_MARKER_V0,
242 feature_gate: SMT_FEATURE_GATE_V0,
243 }
244 }
245}
246
247impl SmtBackendV0 for StubSmtBackendV0 {
248 fn backend_kind(&self) -> SmtBackendKindV0 {
249 SmtBackendKindV0::Stub
250 }
251}
252
253#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
254#[serde(rename_all = "camelCase")]
255pub enum SmtVerdictV0 {
256 Accepted,
257 Rejected,
258 Unknown,
259}
260
261#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
262#[serde(rename_all = "camelCase")]
263pub struct CascadeSMTProofV0 {
264 pub schema_version: &'static str,
265 pub product: &'static str,
266 pub layer_marker: &'static str,
267 pub feature_gate: &'static str,
268 pub obligation_id: String,
269 pub backend: SmtBackendKindV0,
270 pub verdict: SmtVerdictV0,
271 pub l1_primitive: &'static str,
272 pub l1_accepted: Option<bool>,
273 pub canonical_input: CanonicalSmtInputV0,
274 pub solver_check: SmtBackendCheckV0,
275 pub refinement_verdict: Option<RefinementVerdictV0>,
276 pub cascade_spec_digest: [u8; 32],
277}
278
279impl CascadeSMTProofV0 {
280 pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
281 EvidenceNodeKeyV0::new(
282 CASCADE_PROOF_RECORD_EVIDENCE_QUERY_V0,
283 self.obligation_id.clone(),
284 )
285 }
286
287 pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
288 let provenance = vec![
289 ["obligation:", self.obligation_id.as_str()].concat(),
290 ["primitive:", self.l1_primitive].concat(),
291 ["featureGate:", self.feature_gate].concat(),
292 ];
293 let lookup = lookup_discharge_ledger_entry_v0(&self.canonical_input);
294 if let Some(seed) = ledger_backed_cascade_proof_seed_v0(
295 self.evidence_node_key(),
296 provenance.clone(),
297 &lookup,
298 ) {
299 return seed;
300 }
301 let family_stamp = prose_obligation_family_stamp(&provenance);
302 EvidenceNodeSeedV0::with_family(
303 self.evidence_node_key(),
304 provenance,
305 GuaranteeKindV0::for_label_less_family(),
306 family_stamp,
307 )
308 }
309
310 pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
311 build_evidence_graph_from_edges_v0(
312 [self.evidence_node_seed()],
313 [EvidenceDemandEdgeV0::new(
314 CASCADE_PROOF_RECORD_EVIDENCE_QUERY_V0,
315 self.evidence_node_key(),
316 CASCADE_PROOF_EVIDENCE_EDGE_KIND_V0,
317 )],
318 )
319 }
320}
321
322#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
323#[serde(rename_all = "camelCase")]
324pub struct TransformRewriteProofInputV0 {
325 pub schema_version: &'static str,
326 pub product: &'static str,
327 pub pass_id: String,
328 pub cascade_obligation_declared: bool,
329 pub provenance_recomputed: bool,
330 pub provenance_preserved: bool,
331 pub contains_bogus_or_trivia: bool,
332 pub stable_post_semantic_ir: bool,
333}
334
335impl TransformRewriteProofInputV0 {
336 pub fn new(
337 pass_id: impl Into<String>,
338 obligation_family: ObligationFamilyIdV0,
339 provenance_recomputed: bool,
340 provenance_preserved: bool,
341 contains_bogus_or_trivia: bool,
342 stable_post_semantic_ir: bool,
343 ) -> Self {
344 let cascade_obligation_declared = obligation_family.declares_cascade_obligation();
345 Self {
346 schema_version: SMT_SCHEMA_VERSION_V0,
347 product: "omena-cascade-proof.transform-rewrite-input",
348 pass_id: pass_id.into(),
349 cascade_obligation_declared,
350 provenance_recomputed,
351 provenance_preserved,
352 contains_bogus_or_trivia,
353 stable_post_semantic_ir,
354 }
355 }
356
357 pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
358 EvidenceNodeKeyV0::new(REWRITE_PROOF_INPUT_EVIDENCE_QUERY_V0, self.pass_id.clone())
359 }
360
361 pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
362 let provenance = vec![
363 ["pass:", self.pass_id.as_str()].concat(),
364 [
365 "cascadeObligationDeclared:",
366 self.cascade_obligation_declared.to_string().as_str(),
367 ]
368 .concat(),
369 [
370 "provenanceRecomputed:",
371 self.provenance_recomputed.to_string().as_str(),
372 ]
373 .concat(),
374 [
375 "provenancePreserved:",
376 self.provenance_preserved.to_string().as_str(),
377 ]
378 .concat(),
379 ];
380 let family_stamp = prose_obligation_family_stamp(&provenance);
381 EvidenceNodeSeedV0::with_family(
382 self.evidence_node_key(),
383 provenance,
384 GuaranteeKindV0::for_label_less_family(),
385 family_stamp,
386 )
387 }
388
389 pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
390 build_evidence_graph_from_edges_v0(
391 [self.evidence_node_seed()],
392 [EvidenceDemandEdgeV0::new(
393 REWRITE_PROOF_INPUT_EVIDENCE_QUERY_V0,
394 self.evidence_node_key(),
395 CASCADE_PROOF_EVIDENCE_EDGE_KIND_V0,
396 )],
397 )
398 }
399}
400
401fn ledger_backed_cascade_proof_seed_v0(
402 key: EvidenceNodeKeyV0,
403 mut provenance: Vec<String>,
404 lookup: &DischargeLedgerLookupV0,
405) -> Option<EvidenceNodeSeedV0> {
406 if !lookup.can_apply_family_stamp() {
407 return None;
408 }
409 let witness = LedgerDischargeWitnessV0::from_discharge_cell_key_v0(&lookup.cell_key)?;
410 provenance.push(["dischargeCell:", lookup.cell_key.as_str()].concat());
411 Some(EvidenceNodeSeedV0::with_family(
412 key,
413 provenance,
414 GuaranteeKindV0::for_label_less_family(),
415 FamilyStampV0::ledger_backed_obligation_discharge(&witness),
416 ))
417}
418
419pub fn cascade_spec_digest_v0() -> [u8; 32] {
420 *blake3::hash(CASCADE_SMT_SPEC_MATERIAL_V0.as_bytes()).as_bytes()
421}
422
423fn cascade_smt_proof_v0<B: SmtBackendV0>(
424 canonical_input: CanonicalSmtInputV0,
425 backend: &B,
426 l1_primitive: &'static str,
427 l1_accepted: Option<bool>,
428) -> CascadeSMTProofV0 {
429 let solver_check = backend.check_canonical_input_v0(&canonical_input);
430 CascadeSMTProofV0 {
431 schema_version: SMT_SCHEMA_VERSION_V0,
432 product: "omena-smt.cascade-proof",
433 layer_marker: SMT_LAYER_MARKER_V0,
434 feature_gate: SMT_FEATURE_GATE_V0,
435 obligation_id: canonical_input.obligation_id.clone(),
436 backend: backend.backend_kind(),
437 verdict: smt_verdict_from_backend_check_v0(solver_check.sat_result),
438 l1_primitive,
439 l1_accepted,
440 canonical_input,
441 solver_check,
442 refinement_verdict: None,
443 cascade_spec_digest: cascade_spec_digest_v0(),
444 }
445}
446
447fn smt_verdict_from_backend_check_v0(sat_result: SmtBackendSatResultV0) -> SmtVerdictV0 {
448 match sat_result {
449 SmtBackendSatResultV0::Sat => SmtVerdictV0::Accepted,
450 SmtBackendSatResultV0::Unsat => SmtVerdictV0::Rejected,
451 SmtBackendSatResultV0::Unknown => SmtVerdictV0::Unknown,
452 }
453}
454
455pub fn smt_prove_box_shorthand_combination_v0<B: SmtBackendV0>(
456 shorthand_property: &str,
457 longhands: &[BoxLonghandInputV0],
458 backend: &B,
459) -> CascadeSMTProofV0 {
460 let proof = prove_box_shorthand_combination(shorthand_property, longhands);
461 let canonical_input =
462 canonical_box_shorthand_combination_input_v0(shorthand_property, longhands);
463 cascade_smt_proof_v0(
464 canonical_input,
465 backend,
466 "prove_box_shorthand_combination",
467 Some(proof.accepted),
468 )
469}
470
471pub fn smt_prove_longhand_merge_v0<B, S>(
472 shorthand_property: &str,
473 expected_longhands: &[S],
474 longhands: &[LonghandMergeInputV0],
475 backend: &B,
476) -> CascadeSMTProofV0
477where
478 B: SmtBackendV0,
479 S: AsRef<str>,
480{
481 let proof = prove_longhand_merge(shorthand_property, expected_longhands, longhands);
482 let canonical_input =
483 canonical_longhand_merge_input_v0(shorthand_property, expected_longhands, longhands);
484 cascade_smt_proof_v0(
485 canonical_input,
486 backend,
487 "prove_longhand_merge",
488 Some(proof.accepted),
489 )
490}
491
492pub fn smt_prove_scope_flatten_candidate_v0<B: SmtBackendV0>(
493 input: ScopeFlattenInputV0,
494 backend: &B,
495) -> CascadeSMTProofV0 {
496 let canonical_input = canonical_scope_flatten_candidate_input_v0(&input);
497 let proof = prove_scope_flatten_candidate(input);
498 cascade_smt_proof_v0(
499 canonical_input,
500 backend,
501 "prove_scope_flatten_candidate",
502 Some(proof.accepted),
503 )
504}
505
506pub fn smt_prove_layer_flatten_candidate_v0<B: SmtBackendV0>(
507 input: LayerFlattenInputV0,
508 backend: &B,
509) -> CascadeSMTProofV0 {
510 let canonical_input = canonical_layer_flatten_candidate_input_v0(&input);
511 let proof = prove_layer_flatten_candidate(input);
512 cascade_smt_proof_v0(
513 canonical_input,
514 backend,
515 "prove_layer_flatten_candidate",
516 Some(proof.accepted),
517 )
518}
519
520pub fn smt_evaluate_static_supports_condition_v0<B: SmtBackendV0>(
521 condition: &str,
522 assumption: StaticSupportsAssumptionV0,
523 backend: &B,
524) -> CascadeSMTProofV0 {
525 let witness = evaluate_static_supports_condition(condition, assumption);
526 let l1_accepted = match witness.verdict {
527 StaticSupportsEvalVerdictV0::AlwaysTrue => Some(true),
528 StaticSupportsEvalVerdictV0::AlwaysFalse => Some(false),
529 StaticSupportsEvalVerdictV0::Unknown => None,
530 };
531 cascade_smt_proof_v0(
532 canonical_static_supports_condition_input_v0(&witness.verdict),
533 backend,
534 "evaluate_static_supports_condition",
535 l1_accepted,
536 )
537}
538
539pub fn smt_verify_transform_rewrite_candidate_v0<B: SmtBackendV0>(
540 input: &TransformRewriteProofInputV0,
541 backend: &B,
542) -> CascadeSMTProofV0 {
543 cascade_smt_proof_v0(
544 canonical_transform_rewrite_candidate_input_v0(input),
545 backend,
546 "verify_transform_rewrite_candidate",
547 Some(
548 input.cascade_obligation_declared
549 && input.provenance_recomputed
550 && input.provenance_preserved
551 && !input.contains_bogus_or_trivia
552 && input.stable_post_semantic_ir,
553 ),
554 )
555}
556
557fn canonical_box_shorthand_combination_input_v0(
558 shorthand_property: &str,
559 longhands: &[BoxLonghandInputV0],
560) -> CanonicalSmtInputV0 {
561 let expected = smt_box_shorthand_longhands_v0(shorthand_property);
562 let canonical_order = expected.is_some_and(|expected| {
563 longhands.len() == expected.len()
564 && longhands
565 .iter()
566 .zip(expected.iter())
567 .all(|(actual, expected)| actual.property == *expected)
568 });
569 canonical_smt_input_v0(
570 "box-shorthand-combination",
571 "prove_box_shorthand_combination",
572 vec![
573 smt_require_term_v0("supported-shorthand-property", expected.is_some()),
574 smt_require_term_v0("canonical-longhand-quartet", canonical_order),
575 smt_require_term_v0(
576 "no-important-longhand",
577 longhands.iter().all(|longhand| !longhand.important),
578 ),
579 smt_require_term_v0(
580 "no-empty-longhand-value",
581 longhands.iter().all(|longhand| !longhand.value.is_empty()),
582 ),
583 smt_require_term_v0(
584 "adjacent-source-order",
585 longhands
586 .windows(2)
587 .all(|pair| pair[1].source_order == pair[0].source_order + 1),
588 ),
589 ],
590 )
591}
592
593fn canonical_longhand_merge_input_v0<S>(
594 shorthand_property: &str,
595 expected_longhands: &[S],
596 longhands: &[LonghandMergeInputV0],
597) -> CanonicalSmtInputV0
598where
599 S: AsRef<str>,
600{
601 let canonical_order = !expected_longhands.is_empty()
602 && longhands.len() == expected_longhands.len()
603 && longhands
604 .iter()
605 .zip(expected_longhands.iter())
606 .all(|(actual, expected)| actual.property == expected.as_ref());
607 canonical_smt_input_v0(
608 "longhand-merge",
609 "prove_longhand_merge",
610 vec![
611 smt_require_term_v0("supported-merge-family", !expected_longhands.is_empty()),
612 smt_require_term_v0("canonical-longhand-order", canonical_order),
613 smt_require_term_v0(
614 "no-important-longhand",
615 longhands.iter().all(|longhand| !longhand.important),
616 ),
617 smt_require_term_v0(
618 "no-empty-longhand-value",
619 longhands.iter().all(|longhand| !longhand.value.is_empty()),
620 ),
621 smt_require_term_v0(
622 "adjacent-source-order",
623 longhands
624 .windows(2)
625 .all(|pair| pair[1].source_order == pair[0].source_order + 1),
626 ),
627 format!("merge-family:{shorthand_property}"),
628 ],
629 )
630}
631
632fn canonical_scope_flatten_candidate_input_v0(input: &ScopeFlattenInputV0) -> CanonicalSmtInputV0 {
633 canonical_smt_input_v0(
634 "scope-flatten-candidate",
635 "prove_scope_flatten_candidate",
636 vec![
637 smt_require_term_v0("no-limit-selector", input.limit_selector.is_none()),
638 smt_require_term_v0("root-scope", input.root_selector.trim() == ":root"),
639 smt_require_term_v0("no-peer-scope", input.peer_scope_count == 0),
640 smt_require_term_v0(
641 "no-competing-unscoped-rule",
642 input.competing_unscoped_rule_count == 0,
643 ),
644 smt_require_term_v0("not-inside-layer", !input.inside_layer),
645 ],
646 )
647}
648
649fn canonical_layer_flatten_candidate_input_v0(input: &LayerFlattenInputV0) -> CanonicalSmtInputV0 {
650 canonical_smt_input_v0(
651 "layer-flatten-candidate",
652 "prove_layer_flatten_candidate",
653 vec![
654 smt_require_term_v0("closed-bundle", input.closed_bundle),
655 smt_require_term_v0("no-peer-layer", input.peer_layer_count == 0),
656 smt_require_term_v0("no-unlayered-rule", input.unlayered_rule_count == 0),
657 smt_require_term_v0(
658 "no-important-declaration",
659 input.important_declaration_count == 0,
660 ),
661 ],
662 )
663}
664
665fn canonical_static_supports_condition_input_v0(
666 verdict: &StaticSupportsEvalVerdictV0,
667) -> CanonicalSmtInputV0 {
668 let canonical_terms = match verdict {
669 StaticSupportsEvalVerdictV0::AlwaysTrue => {
670 vec![smt_require_term_v0("supports-condition-known-true", true)]
671 }
672 StaticSupportsEvalVerdictV0::AlwaysFalse => {
673 vec![smt_require_term_v0("supports-condition-known-true", false)]
674 }
675 StaticSupportsEvalVerdictV0::Unknown => vec!["unknown:supports-condition".to_string()],
676 };
677 canonical_smt_input_v0(
678 "static-supports-condition",
679 "evaluate_static_supports_condition",
680 canonical_terms,
681 )
682}
683
684fn canonical_transform_rewrite_candidate_input_v0(
685 input: &TransformRewriteProofInputV0,
686) -> CanonicalSmtInputV0 {
687 canonical_smt_input_v0(
688 "transform-rewrite-candidate",
689 "verify_transform_rewrite_candidate",
690 vec![
691 format!("pass:{}", input.pass_id),
692 smt_require_term_v0(
693 "cascade-obligation-declared",
694 input.cascade_obligation_declared,
695 ),
696 smt_require_term_v0("provenance-recomputed", input.provenance_recomputed),
697 smt_require_term_v0("provenance-preserved", input.provenance_preserved),
698 smt_require_term_v0("no-bogus-or-trivia", !input.contains_bogus_or_trivia),
699 smt_require_term_v0("stable-post-semantic-ir", input.stable_post_semantic_ir),
700 ],
701 )
702}
703
704fn smt_require_term_v0(name: &str, value: bool) -> String {
705 format!("require:{name}={value}")
706}
707
708fn smt_box_shorthand_longhands_v0(shorthand_property: &str) -> Option<[&'static str; 4]> {
709 match shorthand_property {
710 "margin" => Some(["margin-top", "margin-right", "margin-bottom", "margin-left"]),
711 "padding" => Some([
712 "padding-top",
713 "padding-right",
714 "padding-bottom",
715 "padding-left",
716 ]),
717 "border-color" => Some([
718 "border-top-color",
719 "border-right-color",
720 "border-bottom-color",
721 "border-left-color",
722 ]),
723 "border-style" => Some([
724 "border-top-style",
725 "border-right-style",
726 "border-bottom-style",
727 "border-left-style",
728 ]),
729 "border-width" => Some([
730 "border-top-width",
731 "border-right-width",
732 "border-bottom-width",
733 "border-left-width",
734 ]),
735 "scroll-margin" => Some([
736 "scroll-margin-top",
737 "scroll-margin-right",
738 "scroll-margin-bottom",
739 "scroll-margin-left",
740 ]),
741 "scroll-padding" => Some([
742 "scroll-padding-top",
743 "scroll-padding-right",
744 "scroll-padding-bottom",
745 "scroll-padding-left",
746 ]),
747 _ => None,
748 }
749}
750
751#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
752#[serde(rename_all = "camelCase")]
753pub struct LayerInversionDeclarationV0 {
754 pub schema_version: &'static str,
755 pub product: &'static str,
756 pub layer_marker: &'static str,
757 pub feature_gate: &'static str,
758 pub declaration_id: String,
759 pub layer_rank: i64,
760 pub source_order: i64,
761}
762
763pub fn layer_inversion_declaration_v0(
764 declaration_id: impl Into<String>,
765 layer_rank: i64,
766 source_order: i64,
767) -> LayerInversionDeclarationV0 {
768 LayerInversionDeclarationV0 {
769 schema_version: SMT_SCHEMA_VERSION_V0,
770 product: "omena-smt.layer-inversion-declaration",
771 layer_marker: SMT_LAYER_MARKER_V0,
772 feature_gate: SMT_FEATURE_GATE_V0,
773 declaration_id: declaration_id.into(),
774 layer_rank,
775 source_order,
776 }
777}
778
779#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
780#[serde(rename_all = "camelCase")]
781pub struct LayerFlattenInversionVerdictV0 {
782 pub schema_version: &'static str,
783 pub product: &'static str,
784 pub layer_marker: &'static str,
785 pub feature_gate: &'static str,
786 pub backend: SmtBackendKindV0,
787 pub inversion_exists: bool,
788 pub verdict: SmtVerdictV0,
789 pub canonical_input: CanonicalSmtInputV0,
790 pub sat_result: SmtBackendSatResultV0,
791}
792
793impl LayerFlattenInversionVerdictV0 {
794 pub fn evidence_node_key(&self) -> EvidenceNodeKeyV0 {
795 EvidenceNodeKeyV0::new(
796 CASCADE_PROOF_RECORD_EVIDENCE_QUERY_V0,
797 self.canonical_input.obligation_id.clone(),
798 )
799 }
800
801 pub fn evidence_node_seed(&self) -> EvidenceNodeSeedV0 {
802 let provenance = vec![
803 ["obligation:", self.canonical_input.obligation_id.as_str()].concat(),
804 ["primitive:", self.canonical_input.l1_primitive].concat(),
805 ["featureGate:", self.feature_gate].concat(),
806 ];
807 let lookup = lookup_discharge_ledger_entry_v0(&self.canonical_input);
808 if let Some(seed) = ledger_backed_cascade_proof_seed_v0(
809 self.evidence_node_key(),
810 provenance.clone(),
811 &lookup,
812 ) {
813 return seed;
814 }
815 let family_stamp = prose_obligation_family_stamp(&provenance);
816 EvidenceNodeSeedV0::with_family(
817 self.evidence_node_key(),
818 provenance,
819 GuaranteeKindV0::for_label_less_family(),
820 family_stamp,
821 )
822 }
823
824 pub fn evidence_graph(&self) -> Result<EvidenceGraphV0, EvidenceGraphBuildErrorV0> {
825 build_evidence_graph_from_edges_v0(
826 [self.evidence_node_seed()],
827 [EvidenceDemandEdgeV0::new(
828 CASCADE_PROOF_RECORD_EVIDENCE_QUERY_V0,
829 self.evidence_node_key(),
830 CASCADE_PROOF_EVIDENCE_EDGE_KIND_V0,
831 )],
832 )
833 }
834}
835
836pub fn canonical_layer_flatten_inversion_input_v0(
837 declarations: &[LayerInversionDeclarationV0],
838) -> CanonicalSmtInputV0 {
839 let declarations = canonicalize_layer_inversion_declarations_v0(declarations);
840 let mut script = String::from("(set-logic QF_LIA)\n");
841 for (index, declaration) in declarations.iter().enumerate() {
842 script.push_str(&format!("(declare-const rank_{index} Int)\n"));
843 script.push_str(&format!("(declare-const source_{index} Int)\n"));
844 script.push_str(&format!(
845 "(assert (= rank_{index} {}))\n",
846 smtlib2_int_v0(declaration.layer_rank)
847 ));
848 script.push_str(&format!(
849 "(assert (= source_{index} {}))\n",
850 smtlib2_int_v0(declaration.source_order)
851 ));
852 }
853
854 let mut inversion_clauses = Vec::new();
855 for a in 0..declarations.len() {
856 for b in 0..declarations.len() {
857 if a == b {
858 continue;
859 }
860 inversion_clauses.push(format!(
861 "(and (> rank_{a} rank_{b}) (> source_{b} source_{a}))"
862 ));
863 }
864 }
865
866 let inversion_assertion = match inversion_clauses.len() {
867 0 => "false".to_string(),
868 1 => inversion_clauses.remove(0),
869 _ => format!("(or {})", inversion_clauses.join(" ")),
870 };
871 script.push_str(&format!(
872 "(assert (! {inversion_assertion} :named cascade_layer_flatten_inversion))\n"
873 ));
874
875 let canonical_terms = declarations
876 .iter()
877 .map(|declaration| {
878 format!(
879 "decl:{}:rank={}:source={}",
880 declaration.declaration_id, declaration.layer_rank, declaration.source_order
881 )
882 })
883 .collect();
884
885 canonical_smt_input_with_script_v0(
886 "layer-flatten-cascade-inversion",
887 "prove_layer_flatten_candidate",
888 canonical_terms,
889 script,
890 )
891}
892
893pub fn canonicalize_layer_inversion_declarations_v0(
894 declarations: &[LayerInversionDeclarationV0],
895) -> Vec<LayerInversionDeclarationV0> {
896 let mut layer_ranks = declarations
897 .iter()
898 .map(|declaration| declaration.layer_rank)
899 .collect::<Vec<_>>();
900 layer_ranks.sort_unstable();
901 layer_ranks.dedup();
902 let mut source_orders = declarations
903 .iter()
904 .map(|declaration| declaration.source_order)
905 .collect::<Vec<_>>();
906 source_orders.sort_unstable();
907 source_orders.dedup();
908
909 declarations
910 .iter()
911 .enumerate()
912 .map(|(index, declaration)| {
913 layer_inversion_declaration_v0(
914 format!("decl-{index}"),
915 ordinal_coordinate(declaration.layer_rank, &layer_ranks),
916 ordinal_coordinate(declaration.source_order, &source_orders),
917 )
918 })
919 .collect()
920}
921
922fn ordinal_coordinate(value: i64, ordered_values: &[i64]) -> i64 {
923 let index = ordered_values
924 .binary_search(&value)
925 .unwrap_or_else(|index| index) as i64;
926 index - (ordered_values.len().saturating_sub(1) as i64 / 2)
927}
928
929pub fn smt_check_layer_flatten_inversion_v0<B: SmtBackendV0>(
930 declarations: &[LayerInversionDeclarationV0],
931 backend: &B,
932) -> LayerFlattenInversionVerdictV0 {
933 let canonical_input = canonical_layer_flatten_inversion_input_v0(declarations);
934 let check = backend.check_canonical_input_v0(&canonical_input);
935 let inversion_exists = matches!(check.sat_result, SmtBackendSatResultV0::Sat);
936 let verdict = match check.sat_result {
937 SmtBackendSatResultV0::Sat => SmtVerdictV0::Rejected,
938 SmtBackendSatResultV0::Unsat => SmtVerdictV0::Accepted,
939 SmtBackendSatResultV0::Unknown => SmtVerdictV0::Unknown,
940 };
941 LayerFlattenInversionVerdictV0 {
942 schema_version: SMT_SCHEMA_VERSION_V0,
943 product: "omena-smt.layer-flatten-inversion",
944 layer_marker: SMT_LAYER_MARKER_V0,
945 feature_gate: SMT_FEATURE_GATE_V0,
946 backend: backend.backend_kind(),
947 inversion_exists,
948 verdict,
949 canonical_input,
950 sat_result: check.sat_result,
951 }
952}
953
954fn smtlib2_int_v0(value: i64) -> String {
955 if value < 0 {
956 format!("(- {})", value.unsigned_abs())
957 } else {
958 value.to_string()
959 }
960}
961
962#[cfg(test)]
963mod tests {
964 use super::*;
965 use omena_cascade::{
966 StaticSupportsEvalVerdictV0, evaluate_static_supports_condition,
967 prove_box_shorthand_combination, prove_layer_flatten_candidate,
968 prove_scope_flatten_candidate,
969 };
970 use omena_evidence_graph::GuaranteeFamilyV0;
971
972 fn accepted_verdict(accepted: bool) -> SmtVerdictV0 {
973 if accepted {
974 SmtVerdictV0::Accepted
975 } else {
976 SmtVerdictV0::Rejected
977 }
978 }
979
980 #[test]
981 fn default_backend_matches_l1_box_shorthand_verdict() {
982 let backend = StubSmtBackendV0::default();
983 let proof = smt_prove_box_shorthand_combination_v0(
984 "margin",
985 &[
986 BoxLonghandInputV0 {
987 property: "margin-top".to_string(),
988 value: "1px".to_string(),
989 important: false,
990 source_order: 1,
991 },
992 BoxLonghandInputV0 {
993 property: "margin-right".to_string(),
994 value: "1px".to_string(),
995 important: false,
996 source_order: 2,
997 },
998 BoxLonghandInputV0 {
999 property: "margin-bottom".to_string(),
1000 value: "1px".to_string(),
1001 important: false,
1002 source_order: 3,
1003 },
1004 BoxLonghandInputV0 {
1005 property: "margin-left".to_string(),
1006 value: "1px".to_string(),
1007 important: false,
1008 source_order: 4,
1009 },
1010 ],
1011 &backend,
1012 );
1013 assert_eq!(proof.schema_version, "0");
1014 assert_eq!(proof.verdict, SmtVerdictV0::Accepted);
1015 assert_eq!(proof.backend, SmtBackendKindV0::Stub);
1016 assert!(
1017 proof
1018 .canonical_input
1019 .smtlib2_script
1020 .contains("(set-logic QF_UF)")
1021 );
1022 }
1023
1024 #[test]
1025 fn transform_rewrite_verification_runs_backend_check() {
1026 let backend = StubSmtBackendV0::default();
1027 let proof_input = TransformRewriteProofInputV0::new(
1028 "rule-deduplication",
1029 ObligationFamilyIdV0::CascadeObligationDeclaration,
1030 true,
1031 true,
1032 false,
1033 true,
1034 );
1035 let proof = smt_verify_transform_rewrite_candidate_v0(&proof_input, &backend);
1036
1037 assert_eq!(proof.verdict, SmtVerdictV0::Accepted);
1038 assert_eq!(proof.l1_primitive, "verify_transform_rewrite_candidate");
1039 assert_eq!(
1040 proof.canonical_input.obligation_id,
1041 "transform-rewrite-candidate"
1042 );
1043 assert!(
1044 proof
1045 .canonical_input
1046 .canonical_terms
1047 .contains(&"require:provenance-recomputed=true".to_string())
1048 );
1049 assert!(
1050 proof
1051 .canonical_input
1052 .canonical_terms
1053 .contains(&"require:no-bogus-or-trivia=true".to_string())
1054 );
1055 }
1056
1057 #[test]
1058 fn proof_style_bisimulation_invariant_holds_for_all_l1_primitives() {
1059 let backend = StubSmtBackendV0::default();
1060 let longhands = vec![
1061 BoxLonghandInputV0 {
1062 property: "margin-top".to_string(),
1063 value: "1px".to_string(),
1064 important: false,
1065 source_order: 1,
1066 },
1067 BoxLonghandInputV0 {
1068 property: "margin-right".to_string(),
1069 value: "1px".to_string(),
1070 important: false,
1071 source_order: 2,
1072 },
1073 BoxLonghandInputV0 {
1074 property: "margin-bottom".to_string(),
1075 value: "1px".to_string(),
1076 important: false,
1077 source_order: 3,
1078 },
1079 BoxLonghandInputV0 {
1080 property: "margin-left".to_string(),
1081 value: "1px".to_string(),
1082 important: false,
1083 source_order: 4,
1084 },
1085 ];
1086 let l1_box = prove_box_shorthand_combination("margin", &longhands);
1087 let l3_box = smt_prove_box_shorthand_combination_v0("margin", &longhands, &backend);
1088 assert_eq!(l3_box.verdict, accepted_verdict(l1_box.accepted));
1089
1090 let scope_input = ScopeFlattenInputV0 {
1091 root_selector: ":root".to_string(),
1092 limit_selector: None,
1093 scoped_rule_count: 1,
1094 peer_scope_count: 0,
1095 competing_unscoped_rule_count: 0,
1096 inside_layer: false,
1097 };
1098 let l1_scope = prove_scope_flatten_candidate(scope_input.clone());
1099 let l3_scope = smt_prove_scope_flatten_candidate_v0(scope_input, &backend);
1100 assert_eq!(l3_scope.verdict, accepted_verdict(l1_scope.accepted));
1101
1102 let layer_input = LayerFlattenInputV0 {
1103 layer_name: Some("components".to_string()),
1104 layer_rule_count: 1,
1105 peer_layer_count: 0,
1106 unlayered_rule_count: 0,
1107 important_declaration_count: 0,
1108 closed_bundle: true,
1109 };
1110 let l1_layer = prove_layer_flatten_candidate(layer_input.clone());
1111 let l3_layer = smt_prove_layer_flatten_candidate_v0(layer_input, &backend);
1112 assert_eq!(l3_layer.verdict, accepted_verdict(l1_layer.accepted));
1113 }
1114
1115 #[test]
1116 fn static_supports_smt_equivalence_tracks_l1_verdict_shape() {
1117 let backend = StubSmtBackendV0::default();
1118 let l1 = evaluate_static_supports_condition(
1119 "(display: grid)",
1120 StaticSupportsAssumptionV0::ModernBrowser,
1121 );
1122 let l3 = smt_evaluate_static_supports_condition_v0(
1123 "(display: grid)",
1124 StaticSupportsAssumptionV0::ModernBrowser,
1125 &backend,
1126 );
1127
1128 assert_eq!(l1.verdict, StaticSupportsEvalVerdictV0::AlwaysTrue);
1129 assert_eq!(l3.verdict, SmtVerdictV0::Accepted);
1130 assert_eq!(l3.l1_primitive, "evaluate_static_supports_condition");
1131 }
1132
1133 #[test]
1134 fn smt_bisimulation_fuzz_seed_corpus_covers_fixture_shapes() {
1135 let report = run_smt_bisimulation_fuzz_seed_corpus_v0(128);
1136 assert_eq!(report.schema_version, "0");
1137 assert_eq!(report.fixture_suite, "m3-cascade-proof-fixtures");
1138 assert_eq!(report.checked_obligation_count, 128 * 4);
1139 assert_eq!(report.l1_l3_mismatch_count, 0);
1140 assert!(report.passed);
1141 }
1142
1143 #[test]
1144 fn smt_bisimulation_fuzz_case_is_a_schema_zero_contract() {
1145 let case = smt_bisimulation_fuzz_case_v0(42);
1146 assert_eq!(case.schema_version, "0");
1147 assert_eq!(case.layer_marker, "smt-cascade-verification");
1148 assert_eq!(case.feature_gate, "smt-stub");
1149 assert_eq!(case.seed, 42);
1150 }
1151
1152 #[test]
1153 fn rewrite_proof_input_evidence_graph_preserves_public_shape() -> Result<(), serde_json::Error>
1154 {
1155 let input = TransformRewriteProofInputV0::new(
1156 "number-compression",
1157 ObligationFamilyIdV0::CascadeObligationDeclaration,
1158 true,
1159 true,
1160 false,
1161 true,
1162 );
1163
1164 let before = serde_json::to_value(&input)?;
1165 let graph = input
1166 .evidence_graph()
1167 .map_err(|_| serde::ser::Error::custom("input edge must target its node"))?;
1168 let after = serde_json::to_value(&input)?;
1169
1170 assert_eq!(before, after);
1171 assert_eq!(graph.nodes.len(), 1);
1172 assert_eq!(graph.nodes[0].key.input_identity, "number-compression");
1173 assert_eq!(graph.nodes[0].guarantee, GuaranteeKindV0::Floor);
1174 assert_eq!(
1175 graph.nodes[0].earned_via(),
1176 GuaranteeFamilyV0::ProseObligationDischarged
1177 );
1178 assert!(
1179 graph.nodes[0]
1180 .provenance
1181 .iter()
1182 .any(|item| item == "provenancePreserved:true")
1183 );
1184 Ok(())
1185 }
1186
1187 #[test]
1188 fn rewrite_proof_input_family_derivation_preserves_legacy_json_contract()
1189 -> Result<(), serde_json::Error> {
1190 for (pass_id, family, expected_declared) in [
1191 (
1192 "number-compression",
1193 ObligationFamilyIdV0::CascadeObligationDeclaration,
1194 true,
1195 ),
1196 ("print-css", ObligationFamilyIdV0::CascadeSafetyFloor, false),
1197 ] {
1198 let input =
1199 TransformRewriteProofInputV0::new(pass_id, family, true, false, false, true);
1200
1201 assert_eq!(
1202 serde_json::to_value(&input)?,
1203 serde_json::json!({
1204 "schemaVersion": "0",
1205 "product": "omena-cascade-proof.transform-rewrite-input",
1206 "passId": pass_id,
1207 "cascadeObligationDeclared": expected_declared,
1208 "provenanceRecomputed": true,
1209 "provenancePreserved": false,
1210 "containsBogusOrTrivia": false,
1211 "stablePostSemanticIr": true,
1212 })
1213 );
1214 assert_eq!(
1215 serde_json::to_value(input.evidence_node_seed())?,
1216 serde_json::json!({
1217 "key": {
1218 "queryIdentity": REWRITE_PROOF_INPUT_EVIDENCE_QUERY_V0,
1219 "inputIdentity": pass_id,
1220 },
1221 "provenance": [
1222 format!("pass:{pass_id}"),
1223 format!("cascadeObligationDeclared:{expected_declared}"),
1224 "provenanceRecomputed:true",
1225 "provenancePreserved:false",
1226 ],
1227 "guarantee": "floor",
1228 "earnedVia": "proseObligationDischarged",
1229 })
1230 );
1231 }
1232
1233 Ok(())
1234 }
1235
1236 #[test]
1237 fn cascade_proof_record_evidence_graph_preserves_public_shape() -> Result<(), serde_json::Error>
1238 {
1239 let backend = StubSmtBackendV0::default();
1240 let proof = smt_verify_transform_rewrite_candidate_v0(
1241 &TransformRewriteProofInputV0::new(
1242 "number-compression",
1243 ObligationFamilyIdV0::CascadeObligationDeclaration,
1244 true,
1245 true,
1246 false,
1247 true,
1248 ),
1249 &backend,
1250 );
1251
1252 let before = serde_json::to_value(&proof)?;
1253 let graph = proof
1254 .evidence_graph()
1255 .map_err(|_| serde::ser::Error::custom("proof edge must target its node"))?;
1256 let after = serde_json::to_value(&proof)?;
1257
1258 assert_eq!(before, after);
1259 assert_eq!(graph.nodes.len(), 1);
1260 assert_eq!(graph.nodes[0].key.input_identity, proof.obligation_id);
1261 assert_eq!(graph.nodes[0].guarantee, GuaranteeKindV0::Floor);
1262 assert_eq!(
1263 graph.nodes[0].earned_via(),
1264 GuaranteeFamilyV0::ProseObligationDischarged
1265 );
1266 assert!(
1267 graph.nodes[0]
1268 .provenance
1269 .iter()
1270 .any(|item| item == "primitive:verify_transform_rewrite_candidate")
1271 );
1272 Ok(())
1273 }
1274
1275 #[test]
1276 fn cascade_proof_record_uses_ledger_family_on_matching_cell() -> Result<(), serde_json::Error> {
1277 let backend = StubSmtBackendV0::default();
1278 let longhands = vec![
1279 LonghandMergeInputV0 {
1280 property: "margin-top".to_string(),
1281 value: "1px".to_string(),
1282 important: false,
1283 source_order: 1,
1284 },
1285 LonghandMergeInputV0 {
1286 property: "margin-right".to_string(),
1287 value: "1px".to_string(),
1288 important: false,
1289 source_order: 2,
1290 },
1291 LonghandMergeInputV0 {
1292 property: "margin-bottom".to_string(),
1293 value: "1px".to_string(),
1294 important: false,
1295 source_order: 3,
1296 },
1297 LonghandMergeInputV0 {
1298 property: "margin-left".to_string(),
1299 value: "1px".to_string(),
1300 important: false,
1301 source_order: 4,
1302 },
1303 ];
1304 let proof = smt_prove_longhand_merge_v0(
1305 "margin",
1306 &["margin-top", "margin-right", "margin-bottom", "margin-left"],
1307 &longhands,
1308 &backend,
1309 );
1310 let graph = proof
1311 .evidence_graph()
1312 .map_err(|_| serde::ser::Error::custom("proof edge must target its node"))?;
1313
1314 assert_eq!(graph.nodes.len(), 1);
1315 assert_eq!(graph.nodes[0].guarantee, GuaranteeKindV0::Floor);
1316 assert_eq!(
1317 graph.nodes[0].earned_via(),
1318 GuaranteeFamilyV0::LedgerBackedObligationDischarge
1319 );
1320 assert!(
1321 graph.nodes[0]
1322 .provenance
1323 .iter()
1324 .any(|item| item.starts_with("dischargeCell:"))
1325 );
1326 Ok(())
1327 }
1328}