Merge pull request #70 from ku-sldg/json-depth-new

Modifying JSON Encoding

src/Attestation_Session.v

@@ -36,9 +36,9 @@ Global Instance Jsonifiable_Attestation_Session `{Jsonifiable (MapC Plc UUID), J
 eapply Build_Jsonifiable with 
   (to_JSON := (fun v => 
                 JSON_Object [
-                  ("Session_Plc", InJSON_String (to_string (Session_Plc v)));
-                  ("Plc_Mapping", InJSON_Object (to_JSON (Plc_Mapping v)));
-                  ("PubKey_Mapping", InJSON_Object (to_JSON (PubKey_Mapping v)))])) 
+                  ("Session_Plc", JSON_String (to_string (Session_Plc v)));
+                  ("Plc_Mapping", to_JSON (Plc_Mapping v));
+                  ("PubKey_Mapping", to_JSON (PubKey_Mapping v))])) 
   (from_JSON := (fun j =>
     match (JSON_get_string "Session_Plc" j), (JSON_get_Object "Plc_Mapping" j), (JSON_get_Object "PubKey_Mapping" j) with
     | resultC plc, resultC plc_map, resultC pub_map =>

src/Concrete_Extractables.v

@@ -1,4 +1,4 @@
-Require Import Manifest JSON Manifest_JSON Attestation_Session.
+Require Import Manifest JSON Manifest_JSON Attestation_Session Term_Defs JSON_Core.
 Require Import List.
 Import ListNotations.
 
@@ -17,3 +17,11 @@ Definition concrete_Jsonifiable_Attestation_Session : Jsonifiable Attestation_Se
 solve [typeclasses eauto].
 Defined.
 
+Definition concrete_Jsonifiable_Term : Jsonifiable Term.
+solve [typeclasses eauto].
+Defined.
+
+Definition concrete_Jsonifiable_Evidence : Jsonifiable Evidence.
+solve [typeclasses eauto].
+Defined.
+

src/Extraction_Cvm_Cake.v

@@ -36,4 +36,6 @@ Separate Extraction
     run_demo_client_AM concrete_Jsonifiable_Manifest
     concrete_Jsonifiable_ASP_Compat_MapT
     concrete_Jsonifiable_Attestation_Session
+    concrete_Jsonifiable_Term
+    concrete_Jsonifiable_Evidence
     Jsonifiable_Evidence_Plc_list Jsonifiable_Term_Plc_list.

src/Interface_JSON.v

@@ -8,12 +8,12 @@ Global Instance Jsonifiable_ProtocolRunRequest `{Jsonifiable Term,
 eapply Build_Jsonifiable with
 (to_JSON := fun req =>
   JSON_Object 
-    [(STR_TYPE, (InJSON_String STR_REQUEST));
-    (STR_ACTION, (InJSON_String STR_RUN));
-    (STR_ATTEST_SESS, (InJSON_Object (to_JSON (prreq_att_sess req))));
-    (STR_REQ_PLC, (InJSON_String (to_string (prreq_req_plc req))));
-    (STR_TERM, (InJSON_Object (to_JSON (prreq_term req)))); 
-    (STR_RAWEV, (InJSON_Object (to_JSON (prreq_rawev req))))])
+    [(STR_TYPE, (JSON_String STR_REQUEST));
+    (STR_ACTION, (JSON_String STR_RUN));
+    (STR_ATTEST_SESS, (to_JSON (prreq_att_sess req)));
+    (STR_REQ_PLC, (JSON_String (to_string (prreq_req_plc req))));
+    (STR_TERM, (to_JSON (prreq_term req))); 
+    (STR_RAWEV, (to_JSON (prreq_rawev req)))])
 (from_JSON := (fun j =>
   temp_att_sess <- JSON_get_Object STR_ATTEST_SESS j ;;
   temp_term <- JSON_get_Object STR_TERM j ;;
@@ -33,10 +33,10 @@ Global Instance Jsonifiable_ProtocolRunResponse `{Jsonifiable RawEv}: Jsonifiabl
 eapply Build_Jsonifiable with
 (to_JSON := fun resp =>
   JSON_Object 
-    [(STR_TYPE, (InJSON_String STR_RESPONSE));
-    (STR_ACTION, (InJSON_String STR_RUN));
-    (STR_SUCCESS, (InJSON_Boolean (prresp_success resp)));
-    (STR_PAYLOAD, (InJSON_Object (to_JSON (prresp_ev resp))))])
+    [(STR_TYPE, (JSON_String STR_RESPONSE));
+    (STR_ACTION, (JSON_String STR_RUN));
+    (STR_SUCCESS, (JSON_Boolean (prresp_success resp)));
+    (STR_PAYLOAD, (to_JSON (prresp_ev resp)))])
 (from_JSON := (fun resp =>
   temp_success <- JSON_get_bool STR_SUCCESS resp ;;
   temp_ev <- JSON_get_Object STR_PAYLOAD resp ;;
@@ -50,9 +50,9 @@ Global Instance Jsonifiable_ProtocolNegotiateRequest `{Jsonifiable Term}: Jsonif
 eapply Build_Jsonifiable with
 (to_JSON := fun req =>
   JSON_Object 
-    [(STR_TYPE, (InJSON_String STR_REQUEST));
-    (STR_ACTION, (InJSON_String STR_NEGOTIATE));
-    (STR_TERM, (InJSON_Object (to_JSON (pnreq_term req))))])
+    [(STR_TYPE, (JSON_String STR_REQUEST));
+    (STR_ACTION, (JSON_String STR_NEGOTIATE));
+    (STR_TERM, (to_JSON (pnreq_term req)))])
 (from_JSON := (fun j =>
   temp_term <- JSON_get_Object STR_TERM j ;;
 
@@ -65,10 +65,10 @@ Global Instance Jsonifiable_ProtocolNegotiateResponse `{Jsonifiable Term}: Jsoni
 eapply Build_Jsonifiable with
 (to_JSON := fun resp =>
   JSON_Object 
-    [(STR_TYPE, (InJSON_String STR_RESPONSE));
-    (STR_ACTION, (InJSON_String STR_NEGOTIATE));
-    (STR_SUCCESS, (InJSON_Boolean (pnresp_success resp)));
-    (STR_PAYLOAD, (InJSON_Object (to_JSON (pnresp_term resp))))])
+    [(STR_TYPE, (JSON_String STR_RESPONSE));
+    (STR_ACTION, (JSON_String STR_NEGOTIATE));
+    (STR_SUCCESS, (JSON_Boolean (pnresp_success resp)));
+    (STR_PAYLOAD, (to_JSON (pnresp_term resp)))])
 (from_JSON := (fun resp =>
   temp_success <- JSON_get_bool STR_SUCCESS resp ;;
   temp_term <- JSON_get_Object STR_PAYLOAD resp ;;
@@ -82,13 +82,13 @@ Global Instance Jsonifiable_ProtocolAppraiseRequest `{Jsonifiable Term, Jsonifia
 eapply Build_Jsonifiable with
 (to_JSON := fun req =>
   JSON_Object [
-    (STR_TYPE, (InJSON_String STR_REQUEST));
-    (STR_ACTION, (InJSON_String STR_APPRAISE));
-    (STR_ATTEST_SESS, (InJSON_Object (to_JSON (pareq_att_sess req))));
-    (STR_TERM, (InJSON_Object (to_JSON (pareq_term req))));
-    (STR_REQ_PLC, (InJSON_String (to_string (pareq_plc req))));
-    (STR_EVIDENCE, (InJSON_Object (to_JSON (pareq_evidence req))));
-    (STR_RAWEV, (InJSON_Object (to_JSON (pareq_ev req))))])
+    (STR_TYPE, (JSON_String STR_REQUEST));
+    (STR_ACTION, (JSON_String STR_APPRAISE));
+    (STR_ATTEST_SESS, (to_JSON (pareq_att_sess req)));
+    (STR_TERM, (to_JSON (pareq_term req)));
+    (STR_REQ_PLC, (JSON_String (to_string (pareq_plc req))));
+    (STR_EVIDENCE, (to_JSON (pareq_evidence req)));
+    (STR_RAWEV, (to_JSON (pareq_ev req)))])
 (from_JSON := (fun j =>
   temp_att_sess <- JSON_get_Object STR_ATTEST_SESS j ;;
   temp_term <- JSON_get_Object STR_TERM j ;;
@@ -109,10 +109,10 @@ Global Instance Jsonifiable_ProtocolAppraiseResponse `{Jsonifiable AppResultC}:
 eapply Build_Jsonifiable with
 (to_JSON := fun resp =>
   JSON_Object [
-    (STR_TYPE, (InJSON_String STR_RESPONSE));
-    (STR_ACTION, (InJSON_String STR_APPRAISE));
-    (STR_SUCCESS, (InJSON_Boolean (paresp_success resp)));
-    (STR_PAYLOAD, (InJSON_Object (to_JSON (paresp_result resp))))])
+    (STR_TYPE, (JSON_String STR_RESPONSE));
+    (STR_ACTION, (JSON_String STR_APPRAISE));
+    (STR_SUCCESS, (JSON_Boolean (paresp_success resp)));
+    (STR_PAYLOAD, (to_JSON (paresp_result resp)))])
 (from_JSON := (fun resp =>
   temp_success <- JSON_get_bool STR_SUCCESS resp ;;
   temp_result <- JSON_get_Object STR_PAYLOAD resp ;;
@@ -126,18 +126,18 @@ Global Instance Jsonifiable_ASPRunRequest `{Jsonifiable RawEv, Jsonifiable ASP_A
 eapply Build_Jsonifiable with
 (to_JSON := fun req =>
   JSON_Object [
-    (STR_TYPE, (InJSON_String STR_REQUEST));
-    (STR_ACTION, (InJSON_String STR_ASP_RUN));
-    (STR_ASP_ID, (InJSON_String (to_string (asprreq_asp_id req))));
-    (STR_ASP_ARGS, (InJSON_Object (to_JSON (asprreq_asp_args req))));
-    (STR_TARG_PLC, (InJSON_String (to_string (asprreq_targ_plc req))));
-    (STR_TARG, (InJSON_String (to_string (asprreq_targ req))));
-    (STR_RAWEV, (InJSON_Object (to_JSON (asprreq_rawev req))))])
+    (STR_TYPE, (JSON_String STR_REQUEST));
+    (STR_ACTION, (JSON_String STR_ASP_RUN));
+    (STR_ASP_ID, (JSON_String (to_string (asprreq_asp_id req))));
+    (STR_ASP_ARGS, (to_JSON (asprreq_asp_args req)));
+    (STR_ASP_PLC, (JSON_String (to_string (asprreq_targ_plc req))));
+    (STR_ASP_TARG_ID, (JSON_String (to_string (asprreq_targ req))));
+    (STR_RAWEV, (to_JSON (asprreq_rawev req)))])
 (from_JSON := (fun j =>
   temp_asp_id <- JSON_get_string STR_ASP_ID j ;;
   temp_asp_args <- JSON_get_Object STR_ASP_ARGS j ;;
-  temp_targ_plc <- JSON_get_string STR_TARG_PLC j ;;
-  temp_targ <- JSON_get_string STR_TARG j ;;
+  temp_targ_plc <- JSON_get_string STR_ASP_PLC j ;;
+  temp_targ <- JSON_get_string STR_ASP_TARG_ID j ;;
   temp_ev <- JSON_get_Object STR_RAWEV j ;;
 
   asp_id <- from_string temp_asp_id ;;
@@ -153,10 +153,10 @@ Global Instance Jsonifiable_ASPRunResponse `{Jsonifiable RawEv}: Jsonifiable ASP
 eapply Build_Jsonifiable with
 (to_JSON := fun resp =>
   JSON_Object 
-    [(STR_TYPE, (InJSON_String STR_RESPONSE));
-    (STR_ACTION, (InJSON_String STR_ASP_RUN));
-    (STR_SUCCESS, (InJSON_Boolean (asprresp_success resp)));
-    (STR_PAYLOAD, (InJSON_Object (to_JSON (asprresp_rawev resp))))])
+    [(STR_TYPE, (JSON_String STR_RESPONSE));
+    (STR_ACTION, (JSON_String STR_ASP_RUN));
+    (STR_SUCCESS, (JSON_Boolean (asprresp_success resp)));
+    (STR_PAYLOAD, (to_JSON (asprresp_rawev resp)))])
 (from_JSON := (fun resp =>
   temp_success <- JSON_get_bool STR_SUCCESS resp ;;
   temp_rawev <- JSON_get_Object STR_PAYLOAD resp ;;
@@ -168,5 +168,5 @@ Defined.
 (* Error Response *)
 Definition ErrorResponseJSON (msg: string): JSON :=
   JSON_Object 
-    [(STR_SUCCESS, InJSON_Boolean false);
-    (STR_PAYLOAD, (InJSON_String msg))].
+    [(STR_SUCCESS, JSON_Boolean false);
+    (STR_PAYLOAD, (JSON_String msg))].

src/Interface_Strings_Vars.v

@@ -20,8 +20,9 @@ Definition STR_RESPONSE : string := "RESPONSE".
 Definition STR_ATTEST_SESS : string := "ATTESTATION_SESSION".
 
 (* ASP String Admits *)
+Definition STR_ASP : string := "ASP".
 Definition STR_ASP_RUN : string := "ASP_RUN".
 Definition STR_ASP_ID : string := "ASP_ID".
 Definition STR_ASP_ARGS : string := "ASP_ARGS".
-Definition STR_TARG_PLC : string := "TARG_PLC".
-Definition STR_TARG : string := "TARG".
+Definition STR_ASP_PLC : string := "ASP_PLC".
+Definition STR_ASP_TARG_ID : string := "ASP_TARG_ID".

src/JSON.v

@@ -46,15 +46,13 @@ Definition JSON_get_Object (key : string) (js : JSON) : ResultT JSON string :=
   match js with
   | JSON_Object m => 
       match map_get m key with
-      | Some ijs => 
-          match ijs with
-          | InJSON_Object v => resultC v
-          | _ => errC "JSON_get_Object: NOT AN OBJECT"
-          end
-      | None => errC "JSON_get_Object: KEY NOT FOUND"
+      | Some v => resultC v 
+      | None => errC ("JSON_get_Object: KEY NOT FOUND : " ++ key)
       end
+  | _ => errC "JSON_get_Object: NOT AN OBJECT"
   end.
 
+(*
 Fixpoint JSON_map_get_Object_rec_safe (key : string) (js_map : MapC string InnerJSON) : ResultT JSON string :=
   match js_map with
   | [] => errC ("NO OBJECT """ ++ key ++ """")
@@ -66,44 +64,30 @@ Fixpoint JSON_map_get_Object_rec_safe (key : string) (js_map : MapC string Inner
             end)
       else JSON_map_get_Object_rec_safe key js_map'
   end.
-
-Definition JSON_get_Array (key : string) (js : JSON) : ResultT (list InnerJSON) string :=
-  match js with
-  | JSON_Object m => 
-      match map_get m key with
-      | Some ijs => 
-          match ijs with
-          | InJSON_Array v => resultC v
-          | _ => errC errStr_json_get_array_not_an_array
-          end
-      | None => errC errStr_json_get_array_key_not_found
-      end
+*)
+
+Definition JSON_get_Array (key : string) (js : JSON) : ResultT (list JSON) string :=
+  match JSON_get_Object key js with
+  | resultC (JSON_Array v) => resultC v
+  | resultC js' => errC ("Key: '" ++ key ++ "' yields '" ++ (JSON_to_string js') ++ "' which is not an array")
+  | _ => errC ("Could not find key: '" ++ key ++ "' in Json object: '" ++
+    (JSON_to_string js) ++ "'")
   end.
 
 Definition JSON_get_string (key : string) (js : JSON) : ResultT string string :=
-  match js with
-  | JSON_Object m => 
-      match map_get m key with
-      | Some ijs => 
-          match ijs with
-          | InJSON_String v => resultC v
-          | _ => errC errStr_json_get_string_not_a_string
-          end
-      | None => errC errStr_json_get_string_key_not_found
-      end
+  match JSON_get_Object key js with
+  | resultC (JSON_String v) => resultC v
+  | resultC js' => errC ("Key: '" ++ key ++ "' yields '" ++ (JSON_to_string js') ++ "' which is not a string")
+  | _ => errC ("Could not find key: '" ++ key ++ "' in Json object: '" ++
+    (JSON_to_string js) ++ "'")
   end.
 
 Definition JSON_get_bool (key : string) (js : JSON) : ResultT bool string :=
-  match js with
-  | JSON_Object m => 
-      match map_get m key with
-      | Some ijs => 
-          match ijs with
-          | InJSON_Boolean v => resultC v
-          | _ => errC errStr_json_get_bool_not_a_bool
-          end
-      | None => errC errStr_json_get_bool_key_not_found
-      end
+  match (JSON_get_Object key js) with
+  | resultC (JSON_Boolean v) => resultC v
+  | resultC js' => errC ("Key: '" ++ key ++ "' yields '" ++ (JSON_to_string js') ++ "' which is not a bool")
+  | _ => errC ("Could not find key: '" ++ key ++ "' in Json object: '" ++
+    (JSON_to_string js) ++ "'")
   end.
 
 (* Lemma canonical_serialization_string : forall (js : JSON) (a : string), 
@@ -115,36 +99,46 @@ Proof.
 Qed. *)
 
 (* The Pair JSONIFIABLE Class *)
-Definition pair_to_JSON_Array {A B : Type} `{Stringifiable A, Stringifiable B} (v : (A * B)) : InnerJSON :=
-  InJSON_Array [InJSON_String (to_string (fst v)); InJSON_String (to_string (snd v))].
+Definition str_pair_to_JSON {A B : Type} `{Stringifiable A, Stringifiable B} (v : (A * B)) : JSON :=
+  JSON_Array [JSON_String (to_string (fst v)); JSON_String (to_string (snd v))].
 
-Definition InnerJSON_to_pair {A B : Type} `{Stringifiable A, Stringifiable B} (js : InnerJSON) : ResultT (A * B) string :=
+Definition str_pair_from_JSON {A B : Type} `{Stringifiable A, Stringifiable B} (js : JSON) : ResultT (A * B) string :=
   match js with
-  | InJSON_Array [InJSON_String a; InJSON_String b] =>
+  | JSON_Array [JSON_String a; JSON_String b] =>
       match (from_string a), (from_string b) with
       | resultC a, resultC b => resultC (a, b)
       | _, _ => errC errStr_json_to_pair
       end
   | _ => errC errStr_json_to_pair
   end.
 
+Global Instance Jsonifiable_str_pair {A B : Type} `{Stringifiable A, Stringifiable B} : Jsonifiable (A * B).
+eapply Build_Jsonifiable with 
+  (to_JSON := str_pair_to_JSON)
+  (from_JSON := str_pair_from_JSON).
+simpl_json.
+Defined.
+
+(* The List JSONIFIABLE Class *)
+
 Definition map_serial_serial_to_JSON {A B : Type} `{Stringifiable A, Stringifiable B, EqClass A} (m : MapC A B) : JSON :=
   JSON_Object (
-    map (fun '(k, v) => (to_string k, InJSON_String (to_string v))) m).
+    map (fun '(k, v) => (to_string k, JSON_String (to_string v))) m).
 
 Definition map_serial_serial_from_JSON {A B : Type} `{Stringifiable A, Stringifiable B, EqClass A} (js : JSON) : ResultT (MapC A B) string :=
   match js with
   | JSON_Object m => 
       result_map 
         (fun '(k, v) => 
             match v with
-            | InJSON_String v' =>
+            | JSON_String v' =>
               match (from_string k), (from_string v') with
               | resultC k', resultC v' => resultC (k', v')
-              | _, _ => errC "Error in map_serial_serial_from_JSON"
+              | _, _ => errC "Error in map_serial_serial_from_JSON:  key/value pair not both Strings"
               end
-            | _ => errC "Error in map_serial_serial_from_JSON"
+            | _ => errC "Error in map_serial_serial_from_JSON:  value not a JSON String"
             end) m
+  | _ => errC "Error in map_serial_serial_from_JSON:  JSON map not a JSON Object"
   end.
 
 Lemma canonical_jsonification_map_serial_serial : forall {A B} `{Stringifiable A, Stringifiable B, EqClass A} (m : MapC A B),
@@ -168,19 +162,20 @@ Global Instance jsonifiable_map_serial_serial (A B : Type) `{Stringifiable A, Eq
     canonical_jsonification := canonical_jsonification_map_serial_serial;
   }.
 
+(*
 Global Instance jsonifiable_map_serial_json (A B : Type) `{Stringifiable A, EqClass A, Jsonifiable B} : Jsonifiable (MapC A B). 
 eapply Build_Jsonifiable with (
   to_JSON := (fun m => JSON_Object (
                       map (fun '(k, v) => 
-                            (to_string k, InJSON_Object (to_JSON v))
+                            (to_string k, JSON_Object (to_JSON v))
                           ) m))) 
   (from_JSON := (fun js =>   
                     match js with
                     | JSON_Object m => 
                         result_map 
                           (fun '(k, v) => 
                               match v with
-                              | InJSON_Object v' =>
+                              | JSON_Object v' =>
                                 match (from_string k), (from_JSON v') with
                                 | resultC k', resultC v' => resultC (k', v')
                                 | _, _ => errC "Error in jsonifiable_map_serial_json"
@@ -195,6 +190,7 @@ try rewrite canonical_stringification in *;
 repeat find_injection; simpl in *; 
 try find_rewrite; eauto; try congruence.
 Defined.
+*)
 
 Close Scope string_scope.
 
@@ -257,7 +253,7 @@ Fixpoint map_flatten {A B C : Type} `{EqClass A, EqClass B}
   | ((k1, k2), v) :: m' => (k1,k2,v) :: map_flatten m'
   end.
 
-Fixpoint result_map_pairs {A B C : Type} `{EqClass A, EqClass B} (f : InnerJSON -> ResultT ((A * B) * C) string) (l : list InnerJSON)
+Fixpoint result_map_pairs {A B C : Type} `{EqClass A, EqClass B} (f : JSON -> ResultT ((A * B) * C) string) (l : list JSON)
     : ResultT (MapC (A * B) C) string :=
   match l with
   | [] => resultC []
@@ -272,15 +268,15 @@ Fixpoint result_map_pairs {A B C : Type} `{EqClass A, EqClass B} (f : InnerJSON
       end
   end.
 
-Definition map_pair_to_InnerJSON_string {A B C : Type} `{Stringifiable A, EqClass A, EqClass B, Stringifiable B, Stringifiable C} (m : MapC (A * B) C) : list InnerJSON :=
-  List.map (fun '(k1, k2, v) => InJSON_Array [InJSON_String (to_string k1); InJSON_String (to_string k2); InJSON_String (to_string v)]) (map_flatten m).
+Definition map_pair_to_InnerJSON_string {A B C : Type} `{Stringifiable A, EqClass A, EqClass B, Stringifiable B, Stringifiable C} (m : MapC (A * B) C) : list JSON :=
+  List.map (fun '(k1, k2, v) => JSON_Array [JSON_String (to_string k1); JSON_String (to_string k2); JSON_String (to_string v)]) (map_flatten m).
 
-Definition InnerJson_string_to_map_pair {A B C : Type} `{Stringifiable A, EqClass A, EqClass B, Stringifiable B, Stringifiable C} (js : list InnerJSON) 
+Definition InnerJson_string_to_map_pair {A B C : Type} `{Stringifiable A, EqClass A, EqClass B, Stringifiable B, Stringifiable C} (js : list JSON) 
     : ResultT (MapC (A * B) C) string :=
   result_map_pairs 
     (fun js' => 
         match js' with
-        | InJSON_Array [InJSON_String k1; InJSON_String k2; InJSON_String v] =>
+        | JSON_Array [JSON_String k1; JSON_String k2; JSON_String v] =>
           match (from_string k1), (from_string k2), (from_string v) with
           | resultC k1, resultC k2, resultC v => resultC ((k1, k2), v)
           | _, _, _ => errC errStr_json_to_map