1 files changed, 17 insertions, 0 deletions
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
new file mode 100644
index 000000000..239bd6b71
--- /dev/null
+++ b/src/Assembly/Conversion.v
@@ -0,0 +1,17 @@
+
+Require Export Language.
+
+Module Type Conversion (A B: Language).
+
+  Parameter convertProgram: forall (x: A.Params) (y: B.Params),
+    A.Program x -> option (B.Program y).
+  Parameter convertState: forall (x: A.Params) (y: B.Params),
+    B.State y -> option (A.State x).
+
+  Axiom convert_spec: forall pa pb a a' b b' prog prog',
+    convertProgram pa pb prog = Some prog' ->
+    convertState pa pb a = Some a' ->
+    convertState pa pb b = Some b' ->
+    B.evaluatesTo pb prog' a b <-> A.evaluatesTo pa prog a' b'.
+
+End Conversion.