Hstep : step1 env (Callstate (Ctypes.Internal f_add) [Vint x; Vint y] Kstop m) t1 s2 Hstar : Smallstep.star step2 env s2 t2 (Returnstate (Vint z) Kstop m') In other words, to “go” from a Callstate of f_add to a Returnstate, there is a first step from a Callstate to a state s2, then a succession of steps to go from s2 to a Returnstate.
Lemma f_add_spec ( env : genv ) ( t : Events.trace ) ( m m' : Memory.Mem.mem ) ( v : val ) ( y z : int ) ( trace : Smallstep.star step2 env ( Callstate ( Ctypes.Internal f_add ) [ Vint x ; Vint y ] Kstop m ) t ( Returnstate ( Vint z ) Kstop : z = add x y. )