Z3 cross layer consistency

The check is z3_cross_layer_consistency. It is VERIFY-stage. Default severity is warning. It loads every requirement that consumes comparable input data_constraint variables and walks traces.satisfies. For each comparable parent and child it asks Z3 two questions: does the child partition imply the parent partition, and do the satisfying children cover the parent partition without sibling overlap inside it. Unrelated domains are skipped. Similar names are not aliases. It does not rewrite the YAML. It does not prove the Go. It does not call Kind2.

The single-layer partition hop stays on data constraints complete. That hop is whether the cases you already named on one requirement are disjoint and complete. This hop is whether those cases still mean the same domain after a child claims the parent. The count of authored rows the encoder actually lowered stays on data constraint Z3 coverage. The subject-closed hop stays on Z3 properties verified.

Each child can look fine on its own. The Jama cell still names a parent. Reviewers signed the English in another tool. A completeness hop is green because the child's own cases still partition. That child can already reject values the parent still allows. Other VERIFY hops miss this because they never walk parent to child on the same parameters.

The expensive miss is a programme that treats the satisfies cell as the contract. The parent requirement stayed active. The child requirement stayed active. The child's invalid-port region is larger. This hop is the gate that prints the parent and child ids and the counterexample.

# SYS-REQ-410  invalid when port > 65535
# SW-REQ-881   traces.satisfies: [SYS-REQ-410]
#              invalid when port < 0 || port > 65535
# a presence-only satisfies hop
# pass. the child still names the parent
# proof audit --check z3_cross_layer_consistency
# [VERIFY] z3_cross_layer_consistency
# child_not_imply_parent
# parent SYS-REQ-410 child SW-REQ-881
# counterexample port=-1
# WARNING
# proof help z3_cross_layer_consistency

The fix is a product decision, not a rewrite of Go. Narrow the child, broaden the parent, add a missing child that covers the leftover region, drop the satisfies link if the child is not the same domain, or author data_constraint_mapping only when the same input has two names. Do not infer aliases from similar names. Then re-run VERIFY.

proof audit --check z3_cross_layer_consistency --verbose
proof workflow check --stage verify --only z3_cross_layer_consistency --verbose
proof help z3_cross_layer_consistency

The teaching graph is still one parent that rejects port > 65535 and one child that also rejects negatives. Close it by matching the two partitions, covering the leftover region, dropping the link, or mapping two names of the same input. Do not delete the YAML. Do not invent a second SYS-REQ. Zero comparable pairs is a pass, not a proved decomposition. Unrelated domains are skipped. Proof does not infer aliases from similar names. A cross_layer_optional: true variable skips every finding kind on that name.

# SYS-REQ-410 kept. SW-REQ-881 invalid when port > 65535
# proof audit --check z3_cross_layer_consistency
# child partition implies parent
# children cover parent
# VERIFY may move on. pass sits on a matching domain

The single-layer hop stays on data constraints complete. The skip-count hop stays on data constraint Z3 coverage. The subject-closed hop stays on Z3 properties verified. The rewrite hop stays on characterization testing and mirrors. Jama still authors. Proof vs Jama.

Warning when a child partition does not imply the parent, when children fail to cover the parent, when siblings overlap inside the parent, or when coverage or overlap is unknown. Default severity does not fail the merge. You can still advance. Zero comparable pairs is a pass, not a complete parent-to-child domain. The hop compares exact parameter and domain signatures. It does not guess that request_rate is current_user_rate. Author data_constraint_mapping if the names differ on purpose. A cross_layer_optional: true declaration on a variable skips sibling_partition_overlap, child_not_imply_parent, parent_not_covered_by_children, coverage_unknown, and overlap_unknown on that name. Use it when siblings share a trigger and refine different aspects. The hop does not write the satisfies list. It does not add a shall. It does not write a description. It does not prove the Go. It does not run Kind2. It does not measure independence. It does not say every authored row was lowered. That hop is data constraint Z3 coverage. A quiet hop is not a proof that Jama's shall matches the Go, only that every in-scope comparable pair currently implies and covers. We have not scored this floor against a frozen Jama pack or a VectorCAST corpus. The loss is named, not scored.

The single-layer hop stays on data constraints complete. The rewrite hop stays on characterization testing and mirrors. The engagement stays on software correctness audit. Jama still authors.

What is Z3 cross layer consistency? Same question. Same URL.

Is this data constraints complete? No. That hop is whether one requirement's cases are disjoint and complete. This hop is whether a child partition still implies its parent. See data constraints complete.

Is this data constraint Z3 coverage? No. That hop is whether the encoder lowered every authored row. This hop is whether the lowered parent and child still agree. See data constraint Z3 coverage.

Is this Z3 properties verified? No. That hop is whether each Z3 subject closed on its own YAML. This hop is parent and child across a satisfies link. See Z3 properties verified.

Is this Z3 on one function? No. That hop is a lemma on a helper. This hop is data-constraint partitions. See Z3/Kind2 on one function.

Does a similar name map automatically? No. Proof does not infer aliases. Author data_constraint_mapping keyed by parent id.

Does an unrelated domain fail this hop? No. The check is conservative. Unrelated signatures are skipped.

Does sibling overlap always mean a bad spec? No. Siblings can share a trigger and refine different aspects. Flag the trigger with cross_layer_optional: true on the variable, not on the requirement.

Does a quiet hop prove the named child is the right decomposition? No. The hop observes comparable partitions. It does not score the sentence.

Does a quiet hop prove the Go matches the shall? No. The hop observes Z3 partitions. It does not prove the Go.

Does a broader child fail the merge? No by default. The check keeps warning severity. You can still advance.

Is zero comparable pairs a complete decomposition? No. Zero comparable pairs is a pass of this hop, not a parent-to-child domain.

Is this characterization testing? No. That page is rewrite-with-a-ledger. This hop is a child partition that does not imply its parent. See characterization testing and mirrors.

Is Proof an LDRA alternative for the instrument? No. LDRA still owns the avionics toolchain. Proof vs LDRA.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.