fact: Definition asm_step_new_stack (stack mem : list Z) (i : assembly) : list Z := match i with | push v => v :: stack | pop => tl stack | add => match stack with a :: b :: s => (a + b)%Z :: s | _ => nil end | cmp => match stack with a :: b :: s => Z.b2z(a <=? b)%Z :: s | _ => nil end | load n => nth n mem 0%Z :: stack | store n => tl stack | goto n => stack | branch n => tl stack end.
imports: ZArith Arith List syntax little Lia