BPStep

formal source

  76  else none
  77
  78/-- A (single) backpropagation step relation with guarded rules. -/
  79inductive BPStep {n} (φ : CNF n) (H : XORSystem n) : BPState n → BPState n → Prop
  80  | xor_push
  81      {s : BPState n}
  82      (X : XORConstraint n)
  83      (v : Var n)
  84      (b : Bool)
  85      (hX : X ∈ H)
  86      (hmiss : xorMissing s.assign X = some (v, b))
  87      : BPStep φ H s { assign := setVar s.assign v b }
  88  | clause_unit
  89      {s : BPState n}
  90      (C : Clause n)
  91      (v : Var n)
  92      (b : Bool)
  93      (hC : C ∈ φ.clauses)
  94      (hmiss : clauseUnit s.assign C = some (v, b))
  95      : BPStep φ H s { assign := setVar s.assign v b }
  96  -- Additional gate placeholders (to be refined with circuit semantics):
  97  | and_one  {s : BPState n} : BPStep φ H s s
  98  | and_zero {s : BPState n} : BPStep φ H s s
  99  | or_one   {s : BPState n} : BPStep φ H s s
 100  | or_zero  {s : BPState n} : BPStep φ H s s
 101  | not_flip {s : BPState n} : BPStep φ H s s
 102  | wire_prop {s : BPState n} : BPStep φ H s s
 103
 104/-- Predicate: state is complete (all variables determined). -/
 105def complete {n} (s : BPState n) : Prop :=
 106  ∀ v, (s.assign v).isSome = true
 107
 108/-- Predicate: state is consistent with φ ∧ H (semantic notion). -/
 109def consistent {n} (s : BPState n) (φ : CNF n) (H : XORSystem n) : Prop :=