Skip to content

Commit d93a18b

Browse files
Durbatuluk1701Durbatuluk1701
authored
Merge pull request #63 from ku-sldg/json-depth-new
Corresponding change on CakeML Side for new JSON Encoding
2 parents 507ecd5 + 1f766f9 commit d93a18b

24 files changed

+2247
-1479
lines changed

‎CMakeLists.txt‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,13 +56,15 @@ get_files(copland_am_src
5656
stubs/BS.sml
5757

5858
extracted/ErrorStringConstants.cml
59+
extracted/Interface_Strings_Vars.cml
5960
extracted/Maps.cml
6061
extracted/JSON_Type.cml
6162

6263
stubs/JSON_Admits.sml
6364

6465
extracted/JSON.cml
6566
extracted/Term_Defs_Core.cml
67+
extracted/JSON_Core.cml
6668

6769
stubs/Params_Admits.sml
6870
stubs/Manifest_Admits.sml
@@ -71,7 +73,6 @@ get_files(copland_am_src
7173
extracted/Manifest_Set.cml
7274
extracted/Manifest.cml
7375
extracted/Attestation_Session.cml
74-
extracted/Interface_Strings_Vars.cml
7576
extracted/Interface_Types.cml
7677
extracted/Interface_JSON.cml
7778
extracted/ErrorStMonad_Coq.cml

‎apps/evidence_to_json/CMakeLists.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ get_files(evidenceToJson_src
1111
../../extracted/Maps.cml
1212
../../extracted/JSON_Type.cml
1313
../../extracted/ErrorStringConstants.cml
14+
../../extracted/Interface_Strings_Vars.cml
1415

1516
../../stubs/JSON_Admits.sml
1617
../../stubs/Stringifiable_Class_Admits.sml
@@ -20,6 +21,7 @@ get_files(evidenceToJson_src
2021
../../stubs/BS.sml
2122

2223
../../extracted/Term_Defs_Core.cml
24+
../../extracted/JSON_Core.cml
2325

2426
../../stubs/Params_Admits.sml
2527

‎apps/evidence_to_json/evidence_to_json.sml‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,15 @@
22

33
fun write_evidence_to_file (term : coq_Evidence) (filename : string) =
44
let
5-
val (Build_Jsonifiable to_JSON _) = coq_Jsonifiable_Evidence
5+
val (Build_Jsonifiable to_JSON _) = (coq_Jsonifiable_Evidence
6+
(jsonifiable_map_serial_serial
7+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
8+
coq_Stringifiable_ID_Type) coq_Jsonifiable_FWD
9+
coq_Jsonifiable_nat
10+
(coq_Jsonifiable_ASP_Params
11+
(jsonifiable_map_serial_serial
12+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
13+
coq_Stringifiable_ID_Type)))
614
val coq_json = to_JSON term
715
val json_str = coq_JSON_to_string coq_json
816
in

‎apps/manifest_generator/CMakeLists.txt‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,18 +12,19 @@ get_files(manGen_src
1212
../../extracted/Maps.cml
1313
../../extracted/JSON_Type.cml
1414
../../extracted/ErrorStringConstants.cml
15+
../../extracted/Interface_Strings_Vars.cml
1516
../../stubs/JSON_Admits.sml
1617
../../stubs/Stringifiable_Class_Admits.sml
1718
../../extracted/JSON.cml
1819
../../stubs/BS.sml
1920
../../extracted/Term_Defs_Core.cml
21+
../../extracted/JSON_Core.cml
2022
../../stubs/Params_Admits.sml
2123
../../extracted/Term_Defs.cml
2224
../../extracted/ErrorStMonad_Coq.cml
2325
../../stubs/Manifest_Admits.sml
2426
../../extracted/Manifest_Set.cml
2527
../../extracted/Manifest.cml
26-
../../extracted/Interface_Strings_Vars.cml
2728
../../extracted/Attestation_Session.cml
2829
../../extracted/Anno_Term_Defs.cml
2930
../../extracted/Interface_Types.cml

‎apps/manifest_generator/manifest_generator.sml‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,15 @@ structure ManGen_CLI_Utils = struct
3535
case (cakeML_JSON_to_coq_JSON js) of
3636
Coq_errC c => Coq_errC c
3737
| Coq_resultC js =>
38-
let val (Build_Jsonifiable _ from_JSON) = (coq_Jsonifiable_Evidence_Plc_list coq_Jsonifiable_Evidence)
38+
let val (Build_Jsonifiable _ from_JSON) = (coq_Jsonifiable_Evidence_Plc_list (coq_Jsonifiable_Evidence
39+
(jsonifiable_map_serial_serial
40+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
41+
coq_Stringifiable_ID_Type) coq_Jsonifiable_FWD
42+
coq_Jsonifiable_nat
43+
(coq_Jsonifiable_ASP_Params
44+
(jsonifiable_map_serial_serial
45+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
46+
coq_Stringifiable_ID_Type))))
3947
(* NOTE: We have to tell it the jsonifiable class for evidence in case there would be multiple ways to jsonify evidence *)
4048
in
4149
from_JSON js
@@ -54,7 +62,7 @@ structure ManGen_CLI_Utils = struct
5462
case (cakeML_JSON_to_coq_JSON js) of
5563
Coq_errC c => Coq_errC c
5664
| Coq_resultC js =>
57-
let val (Build_Jsonifiable _ from_JSON) = (coq_Jsonifiable_Term_Plc_list coq_Jsonifiable_Term)
65+
let val (Build_Jsonifiable _ from_JSON) = (coq_Jsonifiable_Term_Plc_list concrete_Jsonifiable_Term)
5866
(* NOTE: Same as above for evidence, we have to tell it the jsonifiable class for Terms in case there would be multiple ways *)
5967
in
6068
from_JSON js

‎apps/term_to_json/CMakeLists.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ get_files(termToJson_src
1414
../../extracted/Maps.cml
1515
../../extracted/JSON_Type.cml
1616
../../extracted/ErrorStringConstants.cml
17+
../../extracted/Interface_Strings_Vars.cml
1718

1819
../../stubs/JSON_Admits.sml
1920
../../stubs/Stringifiable_Class_Admits.sml
@@ -23,6 +24,7 @@ get_files(termToJson_src
2324
../../stubs/BS.sml
2425

2526
../../extracted/Term_Defs_Core.cml
27+
../../extracted/JSON_Core.cml
2628

2729
../../stubs/Params_Admits.sml
2830

‎apps/term_to_json/term_to_json.sml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,12 @@
22

33
fun write_term_to_file (term : coq_Term) (filename : string) =
44
let
5-
val (Build_Jsonifiable to_JSON _) = coq_Jsonifiable_Term
5+
val (Build_Jsonifiable to_JSON _) = (coq_Jsonifiable_Term
6+
(coq_Jsonifiable_ASP coq_Jsonifiable_FWD
7+
(coq_Jsonifiable_ASP_Params
8+
(jsonifiable_map_serial_serial
9+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
10+
coq_Stringifiable_ID_Type))) coq_Jsonifiable_Split)
611
val coq_json = to_JSON term
712
val json_str = coq_JSON_to_string coq_json
813
in

‎extracted/AM_Json_Interfaces.cml‎

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,13 @@ fun handle_AM_request_JSON conf js nonceVal =
2424
(case (op=) req_type coq_STR_RUN of
2525
True =>
2626
(case let val Build_Jsonifiable _ from_JSON =
27-
coq_Jsonifiable_ProtocolRunRequest coq_Jsonifiable_Term
27+
coq_Jsonifiable_ProtocolRunRequest
28+
(coq_Jsonifiable_Term
29+
(coq_Jsonifiable_ASP coq_Jsonifiable_FWD
30+
(coq_Jsonifiable_ASP_Params
31+
(jsonifiable_map_serial_serial
32+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
33+
coq_Stringifiable_ID_Type))) coq_Jsonifiable_Split)
2834
coq_Jsonifiable_RawEv
2935
(coq_Jsonifiable_Attestation_Session
3036
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
@@ -53,8 +59,22 @@ fun handle_AM_request_JSON conf js nonceVal =
5359
True =>
5460
(case let val Build_Jsonifiable _ from_JSON =
5561
coq_Jsonifiable_ProtocolAppraiseRequest
56-
coq_Jsonifiable_Term coq_Jsonifiable_RawEv
57-
coq_Jsonifiable_Evidence
62+
(coq_Jsonifiable_Term
63+
(coq_Jsonifiable_ASP coq_Jsonifiable_FWD
64+
(coq_Jsonifiable_ASP_Params
65+
(jsonifiable_map_serial_serial
66+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
67+
coq_Stringifiable_ID_Type)))
68+
coq_Jsonifiable_Split) coq_Jsonifiable_RawEv
69+
(coq_Jsonifiable_Evidence
70+
(jsonifiable_map_serial_serial
71+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
72+
coq_Stringifiable_ID_Type) coq_Jsonifiable_FWD
73+
coq_Jsonifiable_nat
74+
(coq_Jsonifiable_ASP_Params
75+
(jsonifiable_map_serial_serial
76+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
77+
coq_Stringifiable_ID_Type)))
5878
(coq_Jsonifiable_Attestation_Session
5979
(jsonifiable_map_serial_serial
6080
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
@@ -74,9 +94,11 @@ fun handle_AM_request_JSON conf js nonceVal =
7494
let val Build_Jsonifiable to_JSON _ =
7595
coq_Jsonifiable_ProtocolAppraiseResponse
7696
(coq_Jsonifiable_AppResultC
77-
(jsonifiable_map_serial_serial
78-
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
79-
coq_Stringifiable_ID_Type))
97+
(coq_Jsonifiable_ASP_Params
98+
(jsonifiable_map_serial_serial
99+
coq_Stringifiable_ID_Type coq_Eq_Class_ID_Type
100+
coq_Stringifiable_ID_Type))
101+
coq_Jsonifiable_Split coq_Jsonifiable_RawEv)
80102
in
81103
to_JSON app_resp0 end) end)
82104
| False => coq_ErrorResponseJSON "Invalid request type")))

‎extracted/Attestation_Session.cml‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,16 +21,14 @@ datatype coq_Session_Config =
2121
coq_MapC coq_Jsonifiable -> coq_Attestation_Session coq_Jsonifiable **)
2222

2323
fun coq_Jsonifiable_Attestation_Session h h0 =
24-
Build_Jsonifiable (fn v => JSON_Object (("Session_Plc", (InJSON_String
24+
Build_Jsonifiable (fn v => JSON_Object (("Session_Plc", (JSON_String
2525
(let val Build_Stringifiable to_string _ = coq_Stringifiable_ID_Type in
2626
to_string (let val Coq_mkAtt_Sess session_Plc _ _ = v in session_Plc end) end))) :: (("Plc_Mapping",
27-
(InJSON_Object
2827
(let val Build_Jsonifiable to_JSON _ = h in
29-
to_JSON (let val Coq_mkAtt_Sess _ plc_Mapping _ = v in plc_Mapping end) end))) :: (("PubKey_Mapping",
30-
(InJSON_Object
28+
to_JSON (let val Coq_mkAtt_Sess _ plc_Mapping _ = v in plc_Mapping end) end)) :: (("PubKey_Mapping",
3129
(let val Build_Jsonifiable to_JSON _ = h0 in
3230
to_JSON
33-
(let val Coq_mkAtt_Sess _ _ pubKey_Mapping = v in pubKey_Mapping end) end))) :: []))))
31+
(let val Coq_mkAtt_Sess _ _ pubKey_Mapping = v in pubKey_Mapping end) end)) :: []))))
3432
(fn j =>
3533
case coq_JSON_get_string "Session_Plc" j of
3634
Coq_errC _ => Coq_errC "Error in parsing Attestation_Session"

‎extracted/Client_AM.cml‎

Lines changed: 25 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,13 @@ fun am_sendReq req_plc att_sess t uuid e =
66
let val req = Coq_mkPRReq att_sess t req_plc e in
77
let val js =
88
let val Build_Jsonifiable to_JSON _ =
9-
coq_Jsonifiable_ProtocolRunRequest coq_Jsonifiable_Term
10-
coq_Jsonifiable_RawEv
9+
coq_Jsonifiable_ProtocolRunRequest
10+
(coq_Jsonifiable_Term
11+
(coq_Jsonifiable_ASP coq_Jsonifiable_FWD
12+
(coq_Jsonifiable_ASP_Params
13+
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
14+
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type)))
15+
coq_Jsonifiable_Split) coq_Jsonifiable_RawEv
1116
(coq_Jsonifiable_Attestation_Session
1217
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
1318
coq_Eq_Class_ID_Type coq_Stringifiable_UUUID)
@@ -39,8 +44,20 @@ fun am_sendReq_app uuid att_sess t p e ev =
3944
let val req = Coq_mkPAReq att_sess t p e ev in
4045
let val js =
4146
let val Build_Jsonifiable to_JSON _ =
42-
coq_Jsonifiable_ProtocolAppraiseRequest coq_Jsonifiable_Term
43-
coq_Jsonifiable_RawEv coq_Jsonifiable_Evidence
47+
coq_Jsonifiable_ProtocolAppraiseRequest
48+
(coq_Jsonifiable_Term
49+
(coq_Jsonifiable_ASP coq_Jsonifiable_FWD
50+
(coq_Jsonifiable_ASP_Params
51+
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
52+
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type)))
53+
coq_Jsonifiable_Split) coq_Jsonifiable_RawEv
54+
(coq_Jsonifiable_Evidence
55+
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
56+
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type)
57+
coq_Jsonifiable_FWD coq_Jsonifiable_nat
58+
(coq_Jsonifiable_ASP_Params
59+
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
60+
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type)))
4461
(coq_Jsonifiable_Attestation_Session
4562
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
4663
coq_Eq_Class_ID_Type coq_Stringifiable_UUUID)
@@ -56,8 +73,10 @@ fun am_sendReq_app uuid att_sess t p e ev =
5673
(case let val Build_Jsonifiable _ from_JSON =
5774
coq_Jsonifiable_ProtocolAppraiseResponse
5875
(coq_Jsonifiable_AppResultC
59-
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
60-
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type))
76+
(coq_Jsonifiable_ASP_Params
77+
(jsonifiable_map_serial_serial coq_Stringifiable_ID_Type
78+
coq_Eq_Class_ID_Type coq_Stringifiable_ID_Type))
79+
coq_Jsonifiable_Split coq_Jsonifiable_RawEv)
6180
in
6281
from_JSON js_res end of
6382
Coq_errC msg => Coq_errC msg

0 commit comments

Comments
 (0)