Theory Sign_Regression

theory Sign_Regression
  imports
    "Voblint_Analysis_Sign.Sign_Transfer"
begin

section ‹Sign regression assertions›

text ‹
  Build-checked regression assertions for the Sign domain, moved out of the core
  theories. Each lemma evaluates a Sign operation on concrete values; nothing cites them.
›

subsection ‹Executable equality-narrowing tests›

text ‹
  Representative @{const inv_eq_sign} cases, directly matching the behavioral
  examples from the design: the true branch always meets, and the false
  branch narrows exactly when one operand is exactly @{term SZero} and the
  other's sign bounds it away from zero on one side.
›

lemma inv_eq_sign_true_meets: "inv_eq_sign True SNonNeg SNonPos = (SZero, SZero)"
  by eval

lemma inv_eq_sign_false_zero_zero_unreachable:
  "inv_eq_sign False SZero SZero = (SBot, SBot)"
  by eval

lemma inv_eq_sign_false_nonneg_zero_narrows_pos:
  "inv_eq_sign False SNonNeg SZero = (SPos, SZero)"
  by eval

lemma inv_eq_sign_false_zero_nonneg_narrows_pos:
  "inv_eq_sign False SZero SNonNeg = (SZero, SPos)"
  by eval

lemma inv_eq_sign_false_nonpos_zero_narrows_neg:
  "inv_eq_sign False SNonPos SZero = (SNeg, SZero)"
  by eval

lemma inv_eq_sign_false_zero_nonpos_narrows_neg:
  "inv_eq_sign False SZero SNonPos = (SZero, SNeg)"
  by eval

text ‹Neither operand is exactly @{term SZero}: the conservative identity fallback.›
lemma inv_eq_sign_false_unrepresentable_identity:
  "inv_eq_sign False SPos SPos = (SPos, SPos)"
  by eval

text ‹@{term SBot} on either side stays bottom-consistent.›
lemma inv_eq_sign_false_bot_consistent:
  "inv_eq_sign False SBot SZero = (SBot, SBot)"
  by eval

subsection ‹Executable end-to-end bfilter tests›

text ‹
  Pins ‹bfilter_sign› on ‹x = 0› over an ‹SNonNeg› store: the true branch
  narrows ‹x› to ‹SZero›, the false branch to ‹SPos›.
›

definition test_env_nonneg_eq :: "sign abs_state" where
  "test_env_nonneg_eq = (λ_. STop)((STR ''x'') := SNonNeg)"

text ‹@{text ‹x = 0›} known true meets ‹x›'s bound with @{term SZero}.›
lemma bfilter_sign_eq_true_narrows:
  "bfilter_sign (Eq (V (STR ''x'')) (N 0)) True test_env_nonneg_eq (STR ''x'') = SZero"
  unfolding test_env_nonneg_eq_def by eval

text ‹@{text ‹x != 0›} known true (i.e. the guard @{text ‹x = 0›} is false) on
  @{term SNonNeg} narrows to @{term SPos}: the disequality narrowing
  @{const inv_eq_sign} supplies.›
lemma bfilter_sign_eq_false_narrows_to_pos:
  "bfilter_sign (Eq (V (STR ''x'')) (N 0)) False test_env_nonneg_eq (STR ''x'') = SPos"
  unfolding test_env_nonneg_eq_def by eval

subsection ‹Executable classification tests›

text ‹
  Pins ‹sign_classify_check›'s three verdicts, including the ‹Not› case and
  nested ‹And›/‹Or› recursion.
›

text ‹One state per test, built as an override of an otherwise-unconstrained
  (‹STop›) environment, so each test exercises exactly the comparison it names.›

definition test_env_pos :: "sign abs_state" where
  "test_env_pos = (λ_. STop)((STR ''x'') := SPos)"

lemma sign_classify_less_proved:
  "sign_classify_check (Less (N 0) (V (STR ''x''))) test_env_pos = Check_Proved"
  unfolding test_env_pos_def by eval

lemma sign_classify_less_refuted:
  "sign_classify_check (Less (V (STR ''x'')) (N 0)) test_env_pos = Check_Refuted"
  unfolding test_env_pos_def by eval

lemma sign_classify_eq_unknown:
  "sign_classify_check (Eq (V (STR ''x'')) (N 1)) test_env_pos = Check_Unknown"
  unfolding test_env_pos_def by eval

text ‹Negation: ‹!(x < 0)› is provable under ‹SNonNeg›, going through
  ‹check_query›'s ‹Not› case (‹map_option HOL.Not› on the un-negated
  ‹x < 0› query) rather than a one-sided reading of the positive answer.›

definition test_env_nonneg :: "sign abs_state" where
  "test_env_nonneg = (λ_. STop)((STR ''x'') := SNonNeg)"

lemma sign_classify_not_proved:
  "sign_classify_check (Not (Less (V (STR ''x'')) (N 0))) test_env_nonneg = Check_Proved"
  unfolding test_env_nonneg_def by eval

text ‹Nested ‹And›/‹Or›: proved through the ‹And› branch alone, and unknown
  when neither branch resolves.›

definition test_env_nested_proved :: "sign abs_state" where
  "test_env_nested_proved = (λ_. STop)((STR ''x'') := SPos, (STR ''y'') := SPos)"

lemma sign_classify_nested_proved:
  "sign_classify_check
     (Or (And (Less (N 0) (V (STR ''x''))) (Less (N 0) (V (STR ''y'')))) (Eq (V (STR ''z'')) (N 1)))
     test_env_nested_proved = Check_Proved"
  unfolding test_env_nested_proved_def by eval

definition test_env_nested_unknown :: "sign abs_state" where
  "test_env_nested_unknown = (λ_. STop)((STR ''x'') := SNonNeg, (STR ''y'') := SPos)"

lemma sign_classify_nested_unknown:
  "sign_classify_check
     (Or (And (Less (N 0) (V (STR ''x''))) (Less (N 0) (V (STR ''y'')))) (Eq (V (STR ''z'')) (N 1)))
     test_env_nested_unknown = Check_Unknown"
  unfolding test_env_nested_unknown_def by eval

end