From f1ad5b5500c3f95e0e602a9585fc0efcdfe1948a Mon Sep 17 00:00:00 2001
From: adelaett <90894311+adelaett@users.noreply.github.com>
Date: Wed, 17 Apr 2024 15:19:27 +0200
Subject: [PATCH] adding template for symbolic continuation-based semantics

---
 theories/mini.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/theories/mini.v b/theories/mini.v
index 9a7e127..952caa8 100644
--- a/theories/mini.v
+++ b/theories/mini.v
@@ -159,3 +159,42 @@ Inductive cred: state -> state -> Prop :=
       (mode_cont (CBinopL op v1 :: kappa) sigma (RValue v2))
       (mode_cont kappa sigma (RValue v))
 .
+
+(* [AD: Add typing rules], but check where it is used. It was in boolean  conditions. Soundness and completeness was proved using all inputs that satisfy path constrains, it is a valid execution for the concrete semantics. We need to have some typing constrains here to check the path constraints are well-formed. 
+
+It might be better to directly separate what the well-formeness and pathc onstraints, and the correctness of the typing.
+
+*)
+
+
+
+
+(******************************************************************************)
+(* Continuation-Based Symbolic Semantics                                      *)
+(******************************************************************************)
+
+(** Possible to include here the path constraints (?) *)
+Inductive sstate : Type :=.
+
+Inductive scred: sstate -> sstate -> Prop :=.
+
+Inductive srefine: state -> sstate -> Prop :=.
+
+
+Theorem scred_sound:
+  forall ss1 ss2,
+    scred ss1 ss2 ->
+      forall s1,
+        srefine s1 ss1 ->
+        exists s2, srefine s2 ss2 /\ cred s1 s2.
+Abort.
+
+
+(** This theorem might not be true under resonable conditions. *)
+Theorem scred_complete:
+  forall s1 s2,
+    cred s1 s2 ->
+      forall ss1,
+        srefine s1 ss1 ->
+        exists ss2, srefine s2 ss2 /\ scred ss1 ss2.
+Abort.