Skip to content

Commit 3b97d8f

Browse files
tahina-protahina-pro
committed
various rewrites and other Pulse unification issues
1 parent b9d339c commit 3b97d8f

23 files changed

+846
-106
lines changed

‎src/cbor/pulse/CBOR.Pulse.API.Base.fst‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1154,8 +1154,10 @@ fn mk_map_gen
11541154
let bres = mk_map_gen_by_ref a dest;
11551155
if bres {
11561156
let res = !dest;
1157+
with res' . rewrite mk_map_gen_post vmatch1 vmatch2 a va pv vv res' as mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res);
11571158
Some res
11581159
} else {
1160+
with res' . rewrite mk_map_gen_post vmatch1 vmatch2 a va pv vv res' as mk_map_gen_post vmatch1 vmatch2 a va pv vv None;
11591161
None #t1
11601162
}
11611163
}
@@ -1411,6 +1413,7 @@ fn mk_map_from_ref
14111413
PM.seq_list_match_length (vmatch2 pv) va vv;
14121414
let _ = mk_map_gen a dest;
14131415
let res = !dest;
1416+
with res' . rewrite (mk_map_gen_post vmatch1 vmatch2 a va pv vv res') as (mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res));
14141417
unfold (mk_map_gen_post vmatch1 vmatch2 a va pv vv (Some res));
14151418
res
14161419
}
@@ -1514,8 +1517,10 @@ fn map_get_as_option
15141517
let bres = m x k dest;
15151518
if bres {
15161519
let res = !dest;
1520+
with res' . rewrite map_get_post vmatch x px vx vk res' as map_get_post vmatch x px vx vk (Some res);
15171521
Some res
15181522
} else {
1523+
with res' . rewrite map_get_post vmatch x px vx vk res' as map_get_post vmatch x px vx vk None;
15191524
None #t
15201525
}
15211526
}

‎src/cbor/pulse/CBOR.Pulse.API.Det.Rust.Macros.fst‎

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,13 @@ fn cbor_det_mk_int64'
2020
(v: _)
2121
{
2222
let mty = (if ty = cbor_major_type_uint64 then UInt64 else NegInt64);
23-
cbor_det_mk_int64 mty v
23+
let res = cbor_det_mk_int64 mty v;
24+
with ty' . rewrite cbor_det_match 1.0R
25+
res
26+
(CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CInt64 ty' v)) as cbor_det_match 1.0R
27+
res
28+
(CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CInt64 ty v));
29+
res
2430
}
2531

2632
inline_for_extraction
@@ -32,6 +38,11 @@ fn cbor_det_mk_simple'
3238
{
3339
let Some res = cbor_det_mk_simple_value v;
3440
unfold (cbor_det_mk_simple_value_post v (Some res));
41+
with res' . rewrite cbor_det_match 1.0R
42+
res
43+
res' as cbor_det_match 1.0R
44+
res
45+
(CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CSimple v));
3546
res
3647
}
3748

@@ -49,6 +60,7 @@ fn cbor_det_mk_string0
4960
let mty = (if ty = cbor_major_type_byte_string then ByteString else TextString);
5061
let res = cbor_det_mk_string mty s;
5162
let Some c = res;
63+
with ty' res' . rewrite (cbor_det_mk_string_post ty' s p v res') as (cbor_det_mk_string_post ty s p v (Some c));
5264
unfold (cbor_det_mk_string_post ty s p v (Some c));
5365
c
5466
}
@@ -230,7 +242,7 @@ fn cbor_det_array_iterator_start'
230242
with p' . assert (cbor_det_view_match p' v y);
231243
let Array a = v;
232244
Trade.rewrite_with_trade
233-
(cbor_det_view_match p' v y)
245+
(cbor_det_view_match p' _ y)
234246
(cbor_det_array_match p' a y);
235247
Trade.trans _ _ (cbor_det_match p x y);
236248
let res = cbor_det_array_iterator_start a;
@@ -252,7 +264,7 @@ fn cbor_det_get_array_item'
252264
with p' . assert (cbor_det_view_match p' v y);
253265
let Array a = v;
254266
Trade.rewrite_with_trade
255-
(cbor_det_view_match p' v y)
267+
(cbor_det_view_match p' _ y)
256268
(cbor_det_array_match p' a y);
257269
Trade.trans _ _ (cbor_det_match p x y);
258270
let ores = cbor_det_get_array_item a i;
@@ -295,7 +307,7 @@ fn cbor_det_map_iterator_start'
295307
with p' . assert (cbor_det_view_match p' v y);
296308
let Map a = v;
297309
Trade.rewrite_with_trade
298-
(cbor_det_view_match p' v y)
310+
(cbor_det_view_match p' _ y)
299311
(cbor_det_map_match p' a y);
300312
Trade.trans _ _ (cbor_det_match p x y);
301313
let res = cbor_det_map_iterator_start a;
@@ -326,13 +338,15 @@ ensures
326338
unfold (safe_map_get_post m p' vx vk None);
327339
Trade.elim _ _;
328340
fold (Base.map_get_post_none cbor_det_match x px vx vk);
329-
fold (Base.map_get_post cbor_det_match x px vx vk None)
341+
fold (Base.map_get_post cbor_det_match x px vx vk None);
342+
rewrite (Base.map_get_post cbor_det_match x px vx vk None) as (Base.map_get_post cbor_det_match x px vx vk res)
330343
}
331344
Some x' -> {
332345
unfold (safe_map_get_post m p' vx vk (Some x'));
333346
Trade.trans _ _ (cbor_det_match px x vx);
334347
fold (Base.map_get_post_some cbor_det_match x px vx vk x');
335-
fold (Base.map_get_post cbor_det_match x px vx vk (Some x'))
348+
fold (Base.map_get_post cbor_det_match x px vx vk (Some x'));
349+
rewrite (Base.map_get_post cbor_det_match x px vx vk (Some x')) as (Base.map_get_post cbor_det_match x px vx vk res);
336350
}
337351
}
338352
}
@@ -353,7 +367,7 @@ fn cbor_det_map_get'
353367
with p' . assert (cbor_det_view_match p' x' vx);
354368
let Map m = x';
355369
Trade.rewrite_with_trade
356-
(cbor_det_view_match p' x' vx)
370+
(cbor_det_view_match p' _ vx)
357371
(cbor_det_map_match p' m vx);
358372
Trade.trans _ _ (cbor_det_match px x vx);
359373
let res = cbor_det_map_get m k;

‎src/cbor/pulse/raw/CBOR.Pulse.API.Det.C.fst‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,8 @@ ensures
216216
unfold (mk_map_gen_post vmatch1 vmatch2 s va pv vv None);
217217
S.to_array s;
218218
fold (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest false);
219+
rewrite (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest false)
220+
as (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest bres);
219221
}
220222
Some vres -> {
221223
unfold (mk_map_gen_post vmatch1 vmatch2 s va pv vv (Some vres));
@@ -233,6 +235,8 @@ ensures
233235
Trade.trans_concl_l _ _ _ _;
234236
rewrite each vres as vdest;
235237
fold (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest true);
238+
rewrite (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest true)
239+
as (mk_map_from_array_safe_post vmatch1 vmatch2 a va pv vv vdest bres);
236240
}
237241
}
238242
}

‎src/cbor/pulse/raw/CBOR.Pulse.API.Det.Common.fst‎

Lines changed: 49 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,7 @@ fn cbor_det_parse_valid
180180
let res = Parse.cbor_parse input len;
181181
with v1' . assert (Raw.cbor_match 1.0R res v1');
182182
Classical.forall_intro_2 (cbor_det_parse_aux v (SZ.v len) v1');
183+
rewrite Raw.cbor_match 1.0R res v1' as Raw.cbor_match 1.0R res (SpecRaw.mk_det_raw_cbor (SpecRaw.mk_cbor v1'));
183184
fold (cbor_det_match 1.0R res (SpecRaw.mk_cbor v1'));
184185
rewrite each
185186
Raw.cbor_match 1.0R res v1'
@@ -430,6 +431,10 @@ fn cbor_det_mk_simple_value (_: unit) : mk_simple_t u#0 #_ cbor_det_match
430431
{
431432
let res = Raw.cbor_match_simple_intro v;
432433
SpecRaw.mk_cbor_eq (SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CSimple v)));
434+
rewrite Raw.cbor_match 1.0R res (SpecRaw.Simple v) as Raw.cbor_match 1.0R
435+
res
436+
(SpecRaw.mk_det_raw_cbor (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CSimple
437+
v)));
433438
fold (cbor_det_match 1.0R res (Spec.pack (Spec.CSimple v)));
434439
res
435440
}
@@ -443,6 +448,10 @@ fn cbor_det_mk_int64 (_: unit) : mk_int64_t u#0 #_ cbor_det_match
443448
{
444449
let res = Raw.cbor_match_int_intro ty (SpecRaw.mk_raw_uint64 v);
445450
SpecRaw.mk_cbor_eq (SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CInt64 ty v)));
451+
rewrite Raw.cbor_match 1.0R res (SpecRaw.Int64 ty (SpecRaw.mk_raw_uint64 v)) as Raw.cbor_match 1.0R
452+
res
453+
(SpecRaw.mk_det_raw_cbor (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CInt64
454+
ty v)));
446455
fold (cbor_det_match 1.0R res (Spec.pack (Spec.CInt64 ty v)));
447456
res
448457
}
@@ -469,11 +478,16 @@ fn cbor_det_mk_string (_: unit) : mk_string_t u#0 #_ cbor_det_match
469478
(SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CString ty v)))
470479
(SpecRaw.String ty len64 v);
471480
assert (pure (SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CString ty v)) == SpecRaw.String ty len64 v));
481+
rewrite Raw.cbor_match 1.0R res r as Raw.cbor_match 1.0R
482+
res
483+
(SpecRaw.mk_det_raw_cbor (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CString
484+
ty v)));
472485
fold (cbor_det_match 1.0R res (Spec.pack (Spec.CString ty v)));
473486
rewrite each
474487
Raw.cbor_match 1.0R res r
475488
as
476489
cbor_det_match 1.0R res (SpecRaw.mk_cbor r);
490+
rewrite each (SpecRaw.mk_cbor r) as (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CString ty v));
477491
res
478492
}
479493

@@ -505,11 +519,18 @@ fn cbor_det_mk_tagged (_: unit) : mk_tagged_t #_ cbor_det_match
505519
(SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CTagged tag v')))
506520
(SpecRaw.Tagged tag64 w');
507521
assert (pure (SpecRaw.mk_det_raw_cbor (Spec.pack (Spec.CTagged tag v')) == SpecRaw.Tagged tag64 w'));
522+
rewrite Raw.cbor_match 1.0R res (SpecRaw.Tagged tag64 w') as
523+
Raw.cbor_match 1.0R
524+
res
525+
(SpecRaw.mk_det_raw_cbor (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CTagged
526+
tag v')));
508527
fold (cbor_det_match 1.0R res (Spec.pack (Spec.CTagged tag v')));
509528
rewrite each
510529
Raw.cbor_match 1.0R res r
511530
as
512531
cbor_det_match 1.0R res (SpecRaw.mk_cbor r);
532+
rewrite each (SpecRaw.mk_cbor (SpecRaw.Tagged tag64 w')) as
533+
(CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CTagged tag v'));
513534
res
514535
}
515536

@@ -553,6 +574,9 @@ decreases v
553574
SM.seq_list_match_cons_intro_trade (Seq.head c) (mk_det_raw_cbor (List.Tot.hd v)) (Seq.tail c) (List.Tot.map mk_det_raw_cbor (List.Tot.tl v)) (Raw.cbor_match p);
554575
Trade.trans _ _ (SM.seq_list_match c v (cbor_det_match p));
555576
rewrite each Seq.cons (Seq.head c) (Seq.tail c) as c;
577+
rewrite each (mk_det_raw_cbor (List.Tot.Base.hd v) ::
578+
List.Tot.Base.map mk_det_raw_cbor (List.Tot.Base.tl v))
579+
as List.Tot.Base.map mk_det_raw_cbor v;
556580
();
557581
}
558582
}
@@ -594,12 +618,19 @@ fn cbor_det_mk_array (_: unit) : mk_array_t #_ cbor_det_match
594618
with r. assert Raw.cbor_match 1.0R res r;
595619
Trade.trans_concl_r _ _ _ _;
596620
Spec.unpack_pack (Spec.CArray vv);
621+
rewrite Raw.cbor_match 1.0R res r
622+
as
623+
Raw.cbor_match 1.0R
624+
res
625+
(SpecRaw.mk_det_raw_cbor (CBOR.Spec.API.Type.pack (CBOR.Spec.API.Type.CArray
626+
vv)));
597627
fold (cbor_det_match 1.0R res (Spec.pack (Spec.CArray vv)));
598628
rewrite
599629
each
600630
Raw.cbor_match 1.0R res r
601631
as
602632
cbor_det_match 1.0R res v';
633+
rewrite each Ghost.reveal v' as (Spec.pack (Spec.CArray vv));
603634
res
604635
}
605636

@@ -698,6 +729,11 @@ decreases v
698729
SM.seq_list_match_cons_intro_trade (Seq.head c) (SpecRaw.mk_det_raw_cbor_map_entry (List.Tot.hd v)) (Seq.tail c) (List.Tot.map SpecRaw.mk_det_raw_cbor_map_entry (List.Tot.tl v)) (Raw.cbor_match_map_entry p);
699730
Trade.trans _ _ (SM.seq_list_match c v (cbor_det_map_entry_match p));
700731
rewrite each Seq.cons (Seq.head c) (Seq.tail c) as c;
732+
rewrite each (SpecRaw.mk_det_raw_cbor_map_entry (List.Tot.Base.hd v) ::
733+
List.Tot.Base.map SpecRaw.mk_det_raw_cbor_map_entry
734+
(List.Tot.Base.tl v)) as (
735+
List.Tot.Base.map SpecRaw.mk_det_raw_cbor_map_entry
736+
(v));
701737
();
702738
}
703739
}
@@ -723,7 +759,8 @@ fn cbor_det_mk_map_entry
723759
Trade.rewrite_with_trade
724760
(Raw.cbor_match_map_entry 1.0R res (SpecRaw.mk_det_raw_cbor vk, SpecRaw.mk_det_raw_cbor vv))
725761
(cbor_det_map_entry_match 1.0R res (Ghost.reveal vk, Ghost.reveal vv));
726-
Trade.trans (cbor_det_map_entry_match 1.0R res (Ghost.reveal vk, Ghost.reveal vv)) _ _;
762+
CBOR.Pulse.Raw.Iterator.trade_trans_nounify (cbor_det_map_entry_match 1.0R res (Ghost.reveal vk, Ghost.reveal vv)) _ (Raw.cbor_match_map_entry 1.0R
763+
res _) _;
727764
Trade.trans_concl_l (cbor_det_map_entry_match 1.0R res (Ghost.reveal vk, Ghost.reveal vv)) _ _ _;
728765
Trade.trans_concl_r (cbor_det_map_entry_match 1.0R res (Ghost.reveal vk, Ghost.reveal vv)) _ _ _;
729766
res
@@ -853,6 +890,9 @@ decreases v
853890
SM.seq_list_match_cons_intro_trade (Seq.head c) (mk_cbor_map_entry (List.Tot.hd v)) (Seq.tail c) (List.Tot.map mk_cbor_map_entry (List.Tot.tl v)) (cbor_det_map_entry_match p);
854891
Trade.trans _ _ (SM.seq_list_match c v (Raw.cbor_match_map_entry p));
855892
rewrite each Seq.cons (Seq.head c) (Seq.tail c) as c;
893+
rewrite each (mk_cbor_map_entry (List.Tot.Base.hd v) ::
894+
List.Tot.Base.map mk_cbor_map_entry (List.Tot.Base.tl v)) as (
895+
List.Tot.Base.map mk_cbor_map_entry (v));
856896
();
857897
}
858898
}
@@ -1788,13 +1828,17 @@ ensures
17881828
Trade.elim _ _;
17891829
fold (map_get_post_none cbor_det_match x px vx vk);
17901830
fold (map_get_post cbor_det_match x px vx vk None);
1831+
rewrite (map_get_post cbor_det_match x px vx vk None)
1832+
as (map_get_post cbor_det_match x px vx vk res);
17911833
();
17921834
}
17931835
Some x' -> {
17941836
unfold (cbor_det_map_get_invariant false px x vx vk m p' i (Some x'));
17951837
unfold (cbor_det_map_get_invariant_some px x vx vk m x');
17961838
fold (map_get_post_some cbor_det_match x px vx vk x');
17971839
fold (map_get_post cbor_det_match x px vx vk (Some x'));
1840+
rewrite (map_get_post cbor_det_match x px vx vk (Some x'))
1841+
as (map_get_post cbor_det_match x px vx vk res);
17981842
}
17991843
}
18001844
}
@@ -1833,6 +1877,8 @@ fn cbor_det_map_get (_: unit)
18331877
pure (cont == cont')
18341878
{
18351879
with gb gi gres . assert (cbor_det_map_get_invariant gb px x vx vk m p' gi gres);
1880+
rewrite (cbor_det_map_get_invariant gb px x vx vk m p' gi gres)
1881+
as (cbor_det_map_get_invariant gb px x vx vk m p' gi None);
18361882
unfold (cbor_det_map_get_invariant gb px x vx vk m p' gi None);
18371883
unfold (cbor_det_map_get_invariant_none gb px x vx vk m p' gi);
18381884
let entry = cbor_det_map_iterator_next () pi;
@@ -1859,6 +1905,7 @@ fn cbor_det_map_get (_: unit)
18591905
List.Tot.assoc_mem (Ghost.reveal vk) l';
18601906
pcont := false;
18611907
fold (cbor_det_map_get_invariant_none false px x vx vk m p' gi');
1908+
assert (pts_to pres None);
18621909
fold (cbor_det_map_get_invariant false px x vx vk m p' gi' None);
18631910
} else {
18641911
Trade.elim_hyp_l _ _ (cbor_det_match px x vx);
@@ -1870,6 +1917,7 @@ fn cbor_det_map_get (_: unit)
18701917
let cont = not is_empty;
18711918
pcont := cont;
18721919
fold (cbor_det_map_get_invariant_none cont px x vx vk m p' i');
1920+
assert (pts_to pres None);
18731921
fold (cbor_det_map_get_invariant cont px x vx vk m p' i' None);
18741922
}
18751923
};

‎src/cbor/pulse/raw/CBOR.Pulse.API.Det.Rust.fst‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,7 @@ ensures exists* p' .
272272
let s = cbor_det_get_string () c;
273273
with p' v' . assert (pts_to s #p' v');
274274
fold (cbor_det_string_match ty p' s v);
275-
fold (cbor_det_view_match p' (String k s) v);
275+
rewrite (cbor_det_string_match ty p' s v) as (cbor_det_view_match p' (String k s) v);
276276
intro
277277
(Trade.trade
278278
(cbor_det_view_match p' (String k s) v)
@@ -282,13 +282,14 @@ ensures exists* p' .
282282
fn _
283283
{
284284
unfold (cbor_det_view_match p' (String k s) v);
285-
unfold (cbor_det_string_match ty p' s v);
285+
with ty . unfold (cbor_det_string_match ty p' s v);
286286
};
287287
Trade.trans _ _ (cbor_det_match p c v);
288288
String k s
289289
}
290290
else if (ty = cbor_major_type_array) {
291291
let res : cbor_det_array = { array = c };
292+
rewrite Det.cbor_det_match p c v as Det.cbor_det_match p res.array v;
292293
fold (cbor_det_array_match p res v);
293294
fold (cbor_det_view_match p (Array res) v);
294295
intro
@@ -301,11 +302,13 @@ ensures exists* p' .
301302
{
302303
unfold (cbor_det_view_match p (Array res) v);
303304
unfold (cbor_det_array_match p res v);
305+
rewrite Det.cbor_det_match p res.array v as Det.cbor_det_match p c v;
304306
};
305307
Array res
306308
}
307309
else if (ty = cbor_major_type_map) {
308310
let res : cbor_det_map = { map = c };
311+
rewrite Det.cbor_det_match p c v as Det.cbor_det_match p res.map v;
309312
fold (cbor_det_map_match p res v);
310313
fold (cbor_det_view_match p (Map res) v);
311314
intro
@@ -318,6 +321,7 @@ ensures exists* p' .
318321
{
319322
unfold (cbor_det_view_match p (Map res) v);
320323
unfold (cbor_det_map_match p res v);
324+
rewrite Det.cbor_det_match p res.map v as Det.cbor_det_match p c v;
321325
};
322326
Map res
323327
}
@@ -337,6 +341,7 @@ ensures exists* p' .
337341
{
338342
unfold (cbor_det_view_match p' (Tagged tag payload) v);
339343
unfold (cbor_det_tagged_match p' tag payload v);
344+
with v_ . rewrite Det.cbor_det_match p' payload v_ as Det.cbor_det_match p' payload v'
340345
};
341346
Trade.trans _ _ (cbor_det_match p c v);
342347
Tagged tag payload
@@ -573,12 +578,14 @@ ensures
573578
unfold (map_get_post_none cbor_det_match x.map px vx vk);
574579
Trade.elim _ _;
575580
fold (safe_map_get_post x px vx vk None);
581+
rewrite (safe_map_get_post x px vx vk None) as (safe_map_get_post x px vx vk res)
576582
}
577583
Some res' -> {
578584
unfold (map_get_post cbor_det_match x.map px vx vk (Some res'));
579585
unfold (map_get_post_some cbor_det_match x.map px vx vk res');
580586
Trade.trans _ _ (cbor_det_map_match px x vx);
581587
fold (safe_map_get_post x px vx vk (Some res'));
588+
rewrite (safe_map_get_post x px vx vk (Some res')) as (safe_map_get_post x px vx vk res)
582589
}
583590
}
584591
}

0 commit comments

Comments
 (0)