Skip to content

Commit 21f4af0

Browse files
didriklundbergdidriklundberg
committed
Copying the fixes to IPSec example too
1 parent 13509a4 commit 21f4af0

File tree

2 files changed

+169
-159
lines changed

2 files changed

+169
-159
lines changed

‎hol/symb_exec/example_ipsec/basicScript.sml‎

Lines changed: 87 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -256,10 +256,10 @@ val basic_actx = ``([arch_block_inp;
256256
F; F; F; T],32));
257257
e_v
258258
(v_bit
259-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
260-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
261-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
262-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],
259+
([F; F; F; F; F; F; F; F;
260+
F; F; F; F; F; F; F; F;
261+
F; F; F; F; F; F; F; F;
262+
F; F; F; F; F; F; F; F],
263263
32))])))
264264
(stmt_ass (lval_varname (varn_name "notify_soft"))
265265
(e_v (v_bool F))))
@@ -336,7 +336,7 @@ val basic_actx = ``([arch_block_inp;
336336
(stmt_seq
337337
(stmt_ass lval_null
338338
(e_call (funn_name "send_to_controller")
339-
[e_v (v_bool F); e_v (v_bool ARB);
339+
[e_v (v_bool F); e_v (v_bool F);
340340
e_v
341341
(v_bit
342342
([F; F; F; F; F; F; F; F; F; F; F; F; F; F;
@@ -346,7 +346,7 @@ val basic_actx = ``([arch_block_inp;
346346
(stmt_seq
347347
(stmt_ass lval_null
348348
(e_call (funn_name "send_to_controller")
349-
[e_v (v_bool F); e_v (v_bool ARB);
349+
[e_v (v_bool F); e_v (v_bool F);
350350
e_v
351351
(v_bit
352352
([F; F; F; F; F; F; F; F; F; F; F; F; F;
@@ -1117,116 +1117,116 @@ val basic_actx = ``([arch_block_inp;
11171117
v1model_input_f
11181118
(v_struct
11191119
[("cpu_header",
1120-
v_header ARB
1120+
v_header F
11211121
[("zeros",
11221122
v_bit
1123-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1124-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1125-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1126-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1127-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1128-
ARB; ARB; ARB; ARB],64));
1123+
([F; F; F; F; F; F; F; F; F; F; F; F;
1124+
F; F; F; F; F; F; F; F; F; F; F; F;
1125+
F; F; F; F; F; F; F; F; F; F; F; F;
1126+
F; F; F; F; F; F; F; F; F; F; F; F;
1127+
F; F; F; F; F; F; F; F; F; F; F; F;
1128+
F; F; F; F],64));
11291129
("reason",
11301130
v_bit
1131-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1132-
ARB; ARB; ARB; ARB],16));
1131+
([F; F; F; F; F; F; F; F; F; F; F; F;
1132+
F; F; F; F],16));
11331133
("port",
11341134
v_bit
1135-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1136-
ARB; ARB; ARB; ARB],16));
1135+
([F; F; F; F; F; F; F; F; F; F; F; F;
1136+
F; F; F; F],16));
11371137
("timestamp",
11381138
v_bit
1139-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1140-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1141-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1142-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],
1139+
([F; F; F; F; F; F; F; F; F; F; F; F;
1140+
F; F; F; F; F; F; F; F; F; F; F; F;
1141+
F; F; F; F; F; F; F; F; F; F; F; F;
1142+
F; F; F; F; F; F; F; F; F; F; F; F],
11431143
48))]);
11441144
("ethernet",
1145-
v_header ARB
1145+
v_header F
11461146
[("dstAddr",
11471147
v_bit
1148-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1149-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1150-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1151-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],
1148+
([F; F; F; F; F; F; F; F; F; F; F; F;
1149+
F; F; F; F; F; F; F; F; F; F; F; F;
1150+
F; F; F; F; F; F; F; F; F; F; F; F;
1151+
F; F; F; F; F; F; F; F; F; F; F; F],
11521152
48));
11531153
("srcAddr",
11541154
v_bit
1155-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1156-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1157-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1158-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],
1155+
([F; F; F; F; F; F; F; F; F; F; F; F;
1156+
F; F; F; F; F; F; F; F; F; F; F; F;
1157+
F; F; F; F; F; F; F; F; F; F; F; F;
1158+
F; F; F; F; F; F; F; F; F; F; F; F],
11591159
48));
11601160
("etherType",
11611161
v_bit
1162-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1163-
ARB; ARB; ARB; ARB],16))]);
1162+
([F; F; F; F; F; F; F; F; F; F; F; F;
1163+
F; F; F; F],16))]);
11641164
("ipv4",
1165-
v_header ARB
1166-
[("version",v_bit ([ARB; ARB; ARB; ARB],4));
1167-
("ihl",v_bit ([ARB; ARB; ARB; ARB],4));
1168-
("diffserv",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
1165+
v_header F
1166+
[("version",v_bit ([F; F; F; F],4));
1167+
("ihl",v_bit ([F; F; F; F],4));
1168+
("diffserv",v_bit ([F; F; F; F; F; F; F; F],8));
11691169
("totalLen",
11701170
v_bit
1171-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1172-
ARB; ARB; ARB; ARB],16));
1171+
([F; F; F; F; F; F; F; F; F; F; F; F;
1172+
F; F; F; F],16));
11731173
("identification",
11741174
v_bit
1175-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1176-
ARB; ARB; ARB; ARB],16));
1177-
("flags",v_bit ([ARB; ARB; ARB],3));
1175+
([F; F; F; F; F; F; F; F; F; F; F; F;
1176+
F; F; F; F],16));
1177+
("flags",v_bit ([F; F; F],3));
11781178
("fragOffset",
11791179
v_bit
1180-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1181-
ARB],13));
1182-
("ttl",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
1183-
("protocol",v_bit ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],8));
1180+
([F; F; F; F; F; F; F; F; F; F; F; F;
1181+
F],13));
1182+
("ttl",v_bit ([F; F; F; F; F; F; F; F],8));
1183+
("protocol",v_bit ([F; F; F; F; F; F; F; F],8));
11841184
("hdrChecksum",
11851185
v_bit
1186-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1187-
ARB; ARB; ARB; ARB],16));
1186+
([F; F; F; F; F; F; F; F; F; F; F; F;
1187+
F; F; F; F],16));
11881188
("srcAddr",
11891189
v_bit
1190-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1191-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1192-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],32));
1190+
([F; F; F; F; F; F; F; F; F; F; F; F;
1191+
F; F; F; F; F; F; F; F; F; F; F; F;
1192+
F; F; F; F; F; F; F; F],32));
11931193
("dstAddr",
11941194
v_bit
1195-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1196-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1197-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],32))]);
1195+
([F; F; F; F; F; F; F; F; F; F; F; F;
1196+
F; F; F; F; F; F; F; F; F; F; F; F;
1197+
F; F; F; F; F; F; F; F],32))]);
11981198
("esp",
1199-
v_header ARB
1199+
v_header F
12001200
[("spi",
12011201
v_bit
1202-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1203-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1204-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],32));
1202+
([F; F; F; F; F; F; F; F; F; F; F; F;
1203+
F; F; F; F; F; F; F; F; F; F; F; F;
1204+
F; F; F; F; F; F; F; F],32));
12051205
("sequenceNumber",
12061206
v_bit
1207-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1208-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1209-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],32))])],
1207+
([F; F; F; F; F; F; F; F; F; F; F; F;
1208+
F; F; F; F; F; F; F; F; F; F; F; F;
1209+
F; F; F; F; F; F; F; F],32))])],
12101210
v_struct
12111211
[("intrinsic_metadata",
12121212
v_struct
12131213
[("ingress_global_timestamp",
12141214
v_bit
1215-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1216-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1217-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1218-
ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB],
1215+
([F; F; F; F; F; F; F; F; F; F; F; F;
1216+
F; F; F; F; F; F; F; F; F; F; F; F;
1217+
F; F; F; F; F; F; F; F; F; F; F; F;
1218+
F; F; F; F; F; F; F; F; F; F; F; F],
12191219
48))]);
12201220
("user_metadata",
12211221
v_struct
1222-
[("spd_mark",v_bit ([ARB; ARB; ARB; ARB],4));
1223-
("bypass",v_bool ARB)]);
1222+
[("spd_mark",v_bit ([F; F; F; F],4));
1223+
("bypass",v_bool F)]);
12241224
("esp_meta",
12251225
v_struct
12261226
[("payloadLength",
12271227
v_bit
1228-
([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB;
1229-
ARB; ARB; ARB; ARB],16))])]),v1model_output_f,
1228+
([F; F; F; F; F; F; F; F; F; F; F; F;
1229+
F; F; F; F],16))])]),v1model_output_f,
12301230
v1model_copyin_pbl,v1model_copyout_pbl,v1model_apply_table_f,
12311231
[("header",NONE,
12321232
[("isValid",[("this",d_in)],header_is_valid);
@@ -1250,21 +1250,21 @@ val basic_actx = ``([arch_block_inp;
12501250
[("emit",[("this",d_in); ("data",d_in)],v1model_packet_out_emit)]);
12511251
("register",
12521252
SOME
1253-
([("this",d_out); ("size",d_none); ("targ1",d_in)],register_construct),
1254-
[("read",[("this",d_in); ("result",d_out); ("index",d_in)],register_read);
1253+
([("this",d_out); ("size",d_none); ("targ1",d_in)],register_construct random_oracle),
1254+
[("read",[("this",d_in); ("result",d_out); ("index",d_in)],register_read random_oracle);
12551255
("write",[("this",d_in); ("index",d_in); ("value",d_in)],register_write)]);
12561256
("ipsec_crypt",SOME ([("this",d_out)],ipsec_crypt_construct),
12571257
[("decrypt_aes_ctr",
12581258
[("this",d_in); ("ipv4",d_inout); ("esp",d_inout); ("standard_metadata",d_inout);
1259-
("key",d_in); ("key_hmac",d_in)],ipsec_crypt_decrypt_aes_ctr);
1259+
("key",d_in); ("key_hmac",d_in)],ipsec_crypt_decrypt_aes_ctr random_oracle);
12601260
("encrypt_aes_ctr",
12611261
[("this",d_in); ("ipv4",d_inout); ("esp",d_inout); ("key",d_in); ("key_hmac",d_in)],
1262-
ipsec_crypt_encrypt_aes_ctr);
1262+
ipsec_crypt_encrypt_aes_ctr random_oracle);
12631263
("encrypt_null",[("this",d_in); ("ipv4",d_inout); ("esp",d_inout)],
1264-
ipsec_crypt_encrypt_null);
1264+
ipsec_crypt_encrypt_null random_oracle);
12651265
("decrypt_null",
12661266
[("this",d_in); ("ipv4",d_inout); ("esp",d_inout); ("standard_metadata",d_inout)],
1267-
ipsec_crypt_decrypt_null)])],
1267+
ipsec_crypt_decrypt_null random_oracle)])],
12681268
[("NoAction",
12691269
stmt_seq
12701270
(stmt_cond (e_var (varn_name "from_table"))
@@ -1278,14 +1278,15 @@ val basic_actx = ``([arch_block_inp;
12781278
([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
12791279
F; F; F; F; F; F; F; F; F; F; F; F; F; F],32)))]))
12801280
stmt_empty) (stmt_seq stmt_empty (stmt_ret (e_v v_bot))),
1281-
[("from_table",d_in); ("hit",d_in)])]):v1model_ascope actx``;
1281+
[("from_table",d_in); ("hit",d_in)])],v1model_get_oracle_index,
1282+
v1model_set_oracle_index,random_oracle):v1model_ascope actx``;
12821283

12831284
val basic_astate = ``((0,[],[],0,[],[("parseError",v_bit (fixwidth 32 (n2v 0),32))],
1284-
[("spd",spd_tbl); ("forward",forward_tbl); ("sad_decrypt",sad_decrypt_tbl); ("sad_encrypt",sad_encrypt_tbl)]),
1285+
[("spd",spd_tbl); ("forward",forward_tbl); ("sad_decrypt",sad_decrypt_tbl); ("sad_encrypt",sad_encrypt_tbl)], 0),
12851286
[[(varn_name "gen_apply_result",
12861287
v_struct
1287-
[("hit",v_bool ARB); ("miss",v_bool ARB);
1288-
("action_run",v_bit (REPLICATE 32 ARB,32))],NONE)]],
1288+
[("hit",v_bool F); ("miss",v_bool T);
1289+
("action_run",v_bit (REPLICATE 32 F,32))],NONE)]],
12891290
arch_frame_list_empty,status_running):v1model_ascope astate``;
12901291

12911292
(********************)
@@ -1300,7 +1301,10 @@ val input = rhs $ concl $ EVAL “^eth_input ++ (^ipv4_input ++ ^esp_input)”;
13001301
val basic_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [(^input,0)] ^basic_astate”;
13011302

13021303
val ctx = basic_actx;
1303-
val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_ctx" (mk_eq(mk_var("basic_ctx", type_of ctx), ctx));
1304+
val ctx_name = "basic_ctx"
1305+
val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn ctx_name (mk_eq(mk_comb (mk_var (ctx_name, mk_fun_ty “:random_oracle” (type_of ctx)), “random_oracle:random_oracle”), ctx))
1306+
val ctx_data = def_thm ctx_def
1307+
13041308

13051309

13061310
(* Additional parts of the context relevant only to symbolic execution *)
@@ -1371,6 +1375,9 @@ val postcond =
13711375

13721376
val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def, p4_symb_execTheory.get_packet_def, p4_symb_execTheory.packet_dropped_def, p4_v1modelTheory.v1model_is_drop_port_def];
13731377

1378+
(* TODO: ??? *)
1379+
val postcond_simpset = pure_ss
1380+
13741381
val time_start = Time.now();
13751382

13761383
(* Commit 7463b72:
@@ -1382,7 +1389,7 @@ Single thread yields
13821389
Finished rewriting step theorems to contract format in 0s, trying to unify contracts...
13831390
Finished unification of all contracts in 170s." (19m, 11s)
13841391
*)
1385-
val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms;
1392+
val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty ctx_data (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset;
13861393
val _ = print (String.concat ["Total time consumption: ",
13871394
(LargeInt.toString $ Time.toMilliseconds ((Time.now()) - time_start)),
13881395
" ms\n"]);

0 commit comments

Comments
 (0)