Email Gateway (Dec 02 2020 at 15:46): Email Gateway (Dec 02 2020 at 15:46):From: David Kretzmer <david.k@posteo.de>
Dear all,
I have formalized a virtual machine roughly in the following way:
(* Executes a single instruction in the given state and returns the new
state. Returns None if the end of the program has been reached. *)
fun exec_instr :: "state ⇒ state option" where
"exec_instr s = ..."
(* Now define the transitive closure for exec_instr *)
inductive exec :: "state ⇒ state ⇒ bool" where
refl: "exec s s" |
trans: "⟦Some s'' = exec_instr s; exec s'' s'⟧ ⟹ exec s s'"
The semantics for individual instructions is implemented by
exec_instr, and complete executions can be performed by the inductive
predicate exec.
Code generation works, but execution of exec becomes increasingly
slower the more instructions are executed. If in the generated code I
call exec_instr directly, execution time for one example dropped from
roughly 10s to 0.2s.
I use the inductive predicate in the formalization because I don't want
to specify an upper bound on the number of steps to execute. Is there a
way to instruct the code generator to generate code for exec that
calls exec_instr directly without the indirection caused by
Predicate.bind and Predicate.apply, which seem to be responsible for
most of the slowdown?
Best regards,
David
Email Gateway (Dec 02 2020 at 16:34):From: Peter Lammich <lammich@in.tum.de>
You could use a tail-recursive function
partial_function (tailrec) execf where
"execf s = (case exec_instr s of None ⇒ s | Some s' ⇒ execf s')"
thm execf.simps
declare execf.simps[code]
execf will execute the program until it terminates.
Email Gateway (Dec 02 2020 at 16:37):From: Peter Lammich <lammich@in.tum.de>
and that's the relation of execf to your exec relation:
lemma "exec s s' ⟹ exec_instr s' = None ⟹ execf s = s'"
apply (induction rule: exec.induct)
apply (subst execf.simps)
apply (auto split: option.split)
apply (subst execf.simps)
apply (auto split: option.split)
done
Email Gateway (Dec 03 2020 at 10:10):From: David Kretzmer <david.k@posteo.de>
This indeed gives the same performance as the handwritten version!
Having proven the equivalence between exec and execf for complete
executions I can use exec for proves and execf for code generation,
in case this turns out to be more convenient.
Thank you very much!
David
Last updated: Jan 04 2025 at 20:18 UTC