Appendix A: Complete Operational Semantics for BSF

This appendix presents the complete set of operational semantics rules for the Bounded Simulation Framework (BSF) used in our case studies. These rules define how arithmetic, boolean, comparison, error propagation, and guard checking operations behave under bounded resource conditions.

Arithmetic Operations

Subtraction

(E-Sub-Zero) ⟨e, R⟩ ⇒ ⟨v, R’⟩ ——————————————

⟨sub(e, 0), R⟩ ⇒ ⟨v, R’+(1,0,0)⟩ (E-Sub-Succ) ⟨e1, R⟩ ⇒ ⟨S(v1), R1⟩ ⟨e2, R1⟩ ⇒ ⟨S(v2), R2⟩

⟨sub(v1, v2), R2⟩ ⇒ ⟨v3, R3⟩ ——————————————

⟨sub(S(e1), S(e2)), R⟩ ⇒ ⟨v3, R3+(1,0,0)⟩ (E-Sub-Under) ⟨e2, R⟩ ⇒ ⟨S(v2), R’⟩ ——————————————

⟨sub(0, S(e2)), R⟩ ⇒ ⟨error(“E102”), R’⟩

Multiplication

(E-Mul-Zero) ⟨e2, R⟩ ⇒ ⟨v2, R’⟩ ——————————————

⟨mul(0, e2), R⟩ ⇒ ⟨0, R’+(1,0,0)⟩ (E-Mul-Succ) ⟨e1, R⟩ ⇒ ⟨S(v1), R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩

⟨mul(v1, v2), R2⟩ ⇒ ⟨v3, R3⟩

⟨add(v2, v3), R3⟩ ⇒ ⟨v4, R4⟩ ————————————————— ⟨mul(S(e1), e2), R⟩ ⇒ ⟨v4, R4+(1,0,0)⟩

Division

(E-Div) ⟨div_safe(e1, e2, 0), R⟩ ⇒ ⟨v, R’⟩

—————————————————————— ⟨div(e1, e2), R⟩ ⇒ ⟨v, R’+(1,0,0)⟩ (E-Div-Guard) steps ≥ max_div_steps

———————————————————— ⟨div_safe(e1, e2, steps), R⟩ ⇒ ⟨error(“E004”), R⟩ (E-Div-Zero) ⟨e2, R⟩ ⇒ ⟨0, R’⟩

———————————————————

⟨div_safe(e1, e2, steps), R⟩ ⇒ ⟨error(“E103”), R’⟩ (E-Div-Base) ⟨e1, R⟩ ⇒ ⟨v1, R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩

lt(v1, v2) = B1

————————————————————— ⟨div_safe(e1, e2, steps), R⟩ ⇒ ⟨0, R2+(1,0,0)⟩ (E-Div-Rec) ⟨e1, R⟩ ⇒ ⟨v1, R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩

(v1, v2) = B0 ∧ v2 ≠ 0 ∧ steps < max_div_steps

⟨sub(v1, v2), R2⟩ ⇒ ⟨v3, R3⟩

⟨div_safe(v3, v2, S( ⟨div_safe(e1, e2, steps), R⟩ ⇒ ⟨S(v4), R4+(1,0,0))

Boolean Operations

(E-And-False) ⟨e1, R⟩ ⇒ ⟨B0, R’⟩

——————————————— ⟨and(e1, e2), R⟩ ⇒ ⟨B0, R’+(1,0,0)⟩ (E-And-True) ⟨e1, R⟩ ⇒ ⟨B1, R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩ —————————————————

⟨and(e1, e2), R⟩ ⇒ ⟨v2, R2+(1,0,0)⟩ (E-Or-True) ⟨e1, R⟩ ⇒ ⟨B1, R’⟩ ———————————————

⟨or(e1, e2), R⟩ ⇒ ⟨B1, R’+(1,0,0)⟩ (E-Or-False) ⟨e1, R⟩ ⇒ ⟨B0, R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩

—————————————————

⟨or(e1, e2), R⟩ ⇒ ⟨v2, R2+(1,0,0)⟩ (E-Not-B0) ⟨e, R⟩ ⇒ ⟨B0, R’⟩

———————————————

⟨not(e), R⟩ ⇒ ⟨B1, R’+(1,0,0)⟩ (E-Not-B1) ⟨e, R⟩ ⇒ ⟨B1, R’⟩

——————————————— ⟨not(e), R⟩ ⇒ ⟨B0, R’+(1,0,0)⟩

Comparison Operations

(E-Eq-Zero) ⟨0, 0⟩ ⇒ ⟨B1, R’+(1,0,0)⟩ (E-Eq-Succ) ⟨e1, R⟩ ⇒ ⟨S(v1), R1⟩ ⟨e2, R1⟩ ⇒ ⟨S(v2), R2⟩

⟨eq(v1, v2), R2⟩ ⇒ ⟨v3, R3⟩ ————————————————————

⟨eq(S(e1), S(e2)), R⟩ ⇒ ⟨v3, R3+(1,0,0)⟩ (E-Eq-Diff) ⟨e1, R⟩ ⇒ ⟨v1, R1⟩

⟨e2, R1⟩ ⇒ ⟨v2, R2⟩ structure(v1) ≠ structure(v2) ———————————————————

⟨eq(e1, e2), R⟩ ⇒ ⟨B0, R2+(1,0,0)⟩

Guard and Error Propagation

(E-Guard-Stack) R.stack_depth ≥ max_stack_dept

——————————————————

⟨e, R⟩ ⇒ ⟨error(“E002”), R⟩ (E-Guard-Nat) depth(S(v)) > max_nat_size ——————————————— ⟨S(e), R⟩ ⇒ ⟨error(“E201”), R⟩ (E-Error-Prop) ⟨e1, R⟩ ⇒ ⟨error(msg), R’⟩

———————————————

⟨op(e1, e2), R⟩ ⇒ ⟨error(msg), R’⟩ These rules form the complete operational semantics required to interpret and evaluate all constructs in the Bounded Simulation Framework while preserving safety, determinism, and finite resource guarantees.