Skip to content

Commit

Permalink
more pattern cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikswamy
nikswamy committed Dec 3, 2023
1 parent 3d55096 commit e37b3a8
Show file tree
Hide file tree
Showing 3 changed files with 102 additions and 180 deletions.
54 changes: 42 additions & 12 deletions src/3d/prelude/EverParse3d.Actions.Base.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,24 +61,54 @@ let disjoint_none_l l =
(disjoint eloc_none l)
(disjointness_trivial)

let conj_disjointess_trivial_unit_left (d:disjointness_pre)
: Lemma
(ensures (disjointness_trivial `conj_disjointness` d) == d)
[SMTPat (disjointness_trivial `conj_disjointness` d)]
let conj_disjointness_trivial_left_unit (d:disjointness_pre)
= FStar.PropositionalExtensionality.apply (disjointness_trivial `conj_disjointness` d) d

let conj_disjointess_trivial_unit_right (d:disjointness_pre)
: Lemma
(ensures (d `conj_disjointness` disjointness_trivial == d))
[SMTPat (d `conj_disjointness` disjointness_trivial)]
let conj_disjointness_trivial_right_unit (d:disjointness_pre)
= FStar.PropositionalExtensionality.apply (d `conj_disjointness` disjointness_trivial) d

let imp_disjointess_idem (d:disjointness_pre)
: Lemma
(ensures (imp_disjointness d d))
[SMTPat (imp_disjointness d d)]
let imp_disjointness_refl (d:disjointness_pre)
= ()

let index_equations ()
= introduce forall d. _
with conj_inv_true_left_unit d;
introduce forall d. _
with conj_inv_true_right_unit d;
introduce forall l. _
with eloc_union_none_right_unit l;
introduce forall l. _
with eloc_union_none_left_unit l;
introduce forall l. _
with disjoint_none_r l;
introduce forall l. _
with disjoint_none_l l;
introduce forall d. _
with conj_disjointness_trivial_left_unit d;
introduce forall d. _
with conj_disjointness_trivial_right_unit d;
introduce forall d. _
with imp_disjointness_refl d;
introduce forall i. _
with inv_implies_refl i;
introduce forall i. _
with inv_implies_true i;
introduce forall i0 i1 i2.
(i0 `inv_implies` i1 /\
i0 `inv_implies` i2) ==>
(i0 `inv_implies` (i1 `conj_inv` i2))
with introduce _ ==> _
with _ . inv_implies_conj i0 i1 i2 () ();
introduce forall l. _
with eloc_includes_none l;
introduce forall l0 l1 l2. (l0 `eloc_includes` l1 /\
l0 `eloc_includes` l2) ==>
(l0 `eloc_includes` (l1 `eloc_union` l2))
with introduce _ ==> _
with _ . eloc_includes_union l0 l1 l2 () ();
introduce forall l. _
with eloc_includes_refl l

let bpointer a = B.pointer a
let ptr_loc #a (x:B.pointer a) : Tot eloc = B.loc_buffer x
let ptr_inv #a (x:B.pointer a) : slice_inv = F.on HS.mem #prop (fun h -> B.live h x /\ True)
Expand Down
61 changes: 57 additions & 4 deletions src/3d/prelude/EverParse3d.Actions.Base.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,17 +64,70 @@ val imp_disjointness (d1 d2:disjointness_pre) : prop
val disjoint_none_r (l:eloc)
: squash (disjoint l eloc_none == disjointness_trivial)
val disjoint_none_l (l:eloc)
: squash (disjoint eloc_none l == disjointness_trivial)

: squash (disjoint eloc_none l == disjointness_trivial)
val conj_disjointness_trivial_left_unit (d:disjointness_pre)
: squash ((disjointness_trivial `conj_disjointness` d) == d)

val conj_disjointness_trivial_right_unit (d:disjointness_pre)
: squash ((d `conj_disjointness` disjointness_trivial) == d)

val imp_disjointness_refl (d:disjointness_pre)
: squash (imp_disjointness d d)

val index_equations (_:unit)
: Lemma
(ensures (
//true_inv left unit
(forall (d:slice_inv).
{:pattern (true_inv `conj_inv` d)} (true_inv `conj_inv` d) == d) /\
//true_inv right unit
(forall (d:slice_inv).
{:pattern (d `conj_inv` true_inv)} (d `conj_inv` true_inv) == d) /\
//eloc_none left unit
(forall (l:eloc).
{:pattern (l `eloc_union` eloc_none)} (l `eloc_union` eloc_none) == l) /\
//eloc_none right unit
(forall (l:eloc).
{:pattern (eloc_none `eloc_union` l)} (eloc_none `eloc_union` l) == l) /\
//disjoint eloc_none right trivial
(forall (l:eloc).
{:pattern (disjoint l eloc_none)} (disjoint l eloc_none) == disjointness_trivial) /\
//disjoint eloc_none left trivial
(forall (l:eloc).
{:pattern (disjoint eloc_none l)} (disjoint eloc_none l) == disjointness_trivial) /\
//disjointness_pre right unit
(forall (d:disjointness_pre).
{:pattern (conj_disjointness d disjointness_trivial)} (conj_disjointness d disjointness_trivial) == d) /\
//disjointness_pre left unit
(forall (d:disjointness_pre).
{:pattern (conj_disjointness disjointness_trivial d)} (conj_disjointness disjointness_trivial d) == d) /\
//imp_disjointness refl
(forall (d:disjointness_pre).
{:pattern (imp_disjointness d d)} imp_disjointness d d) /\
//inv_implies refl
(forall (i:slice_inv).
{:pattern (inv_implies i i)} inv_implies i i) /\
//inv_implies true_inv right trivial
(forall (i:slice_inv).
{:pattern (inv_implies i true_inv)} inv_implies i true_inv) /\
//inv_implies_conj
(forall (i0 i1 i2:slice_inv).
{:pattern (i0 `inv_implies` (i1 `conj_inv` i2))}
(i0 `inv_implies` i1 /\
i0 `inv_implies` i2) ==>
(i0 `inv_implies` (i1 `conj_inv` i2))) /\
//eloc_includes_none
(forall (l:eloc).
{:pattern (l `eloc_includes` eloc_none)} l `eloc_includes` eloc_none) /\
//eloc_includes_union
(forall (l0 l1 l2:eloc).
{:pattern (l0 `eloc_includes` (l1 `eloc_union` l2))}
(l0 `eloc_includes` l1 /\
l0 `eloc_includes` l2) ==>
(l0 `eloc_includes` (l1 `eloc_union` l2))) /\
//eloc_includes_refl
(forall (l:eloc).
{:pattern (l `eloc_includes` l)} (l `eloc_includes` l))
))

inline_for_extraction
noextract
val bpointer (a: Type0) : Tot Type0
Expand Down
167 changes: 3 additions & 164 deletions src/3d/prelude/EverParse3d.Interpreter.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -580,167 +580,6 @@ type atomic_action
(join_loc l (Some (A.copy_buffer_loc dest)))
true bool

// let _inv_implies_refl (inv: A.slice_inv) : Lemma
// (inv `A.inv_implies` inv)
// [SMTPat (inv `A.inv_implies` inv)]
// = A.inv_implies_refl inv

// let _inv_implies_true (inv0: A.slice_inv) : Lemma
// (inv0 `A.inv_implies` A.true_inv)
// [SMTPat (inv0 `A.inv_implies` A.true_inv)]
// = A.inv_implies_true inv0

// let _inv_implies_conj (inv0 inv1 inv2: A.slice_inv) : Lemma
// (requires (
// inv0 `A.inv_implies` inv1 /\
// inv0 `A.inv_implies` inv2
// ))
// (ensures (
// inv0 `A.inv_implies` (inv1 `A.conj_inv` inv2)
// ))
// [SMTPat (inv0 `A.inv_implies` (inv1 `A.conj_inv` inv2))]
// = A.inv_implies_conj inv0 inv1 inv2 () ()

// let _eloc_includes_none (l1:A.eloc) : Lemma
// (l1 `A.eloc_includes` A.eloc_none)
// [SMTPat (l1 `A.eloc_includes` A.eloc_none)]
// = A.eloc_includes_none l1

// let _eloc_includes_union (l0: A.eloc) (l1 l2: A.eloc) : Lemma
// (requires (
// l0 `A.eloc_includes` l1 /\
// l0 `A.eloc_includes` l2
// ))
// (ensures (
// l0 `A.eloc_includes` (l1 `A.eloc_union` l2)
// ))
// [SMTPat (l0 `A.eloc_includes` (l1 `A.eloc_union` l2))]
// = A.eloc_includes_union l0 l1 l2 () ()

// let _eloc_includes_refl (l: A.eloc) : Lemma
// (l `A.eloc_includes` l)
// [SMTPat (l `A.eloc_includes` l)]
// = A.eloc_includes_refl l


let index_equations ()
: Lemma
(ensures (
(forall (d:A.slice_inv).
{:pattern (A.true_inv `A.conj_inv` d)} (A.true_inv `A.conj_inv` d) == d) /\
(forall (d:A.slice_inv).
{:pattern (d `A.conj_inv` A.true_inv)} (d `A.conj_inv` A.true_inv) == d) /\
(forall (l:A.eloc).
{:pattern (l `A.eloc_union` A.eloc_none)} (l `A.eloc_union` A.eloc_none) == l) /\
(forall (l:A.eloc).
{:pattern (A.eloc_none `A.eloc_union` l)} (A.eloc_none `A.eloc_union` l) == l) /\
(forall (l:A.eloc).
{:pattern (A.disjoint l A.eloc_none)} (A.disjoint l A.eloc_none) == A.disjointness_trivial) /\
(forall (l:A.eloc).
{:pattern (A.disjoint A.eloc_none l)} (A.disjoint A.eloc_none l) == A.disjointness_trivial) /\
(forall (d:A.disjointness_pre).
{:pattern (A.conj_disjointness d A.disjointness_trivial)} (A.conj_disjointness d A.disjointness_trivial) == d) /\
(forall (d:A.disjointness_pre).
{:pattern (A.conj_disjointness A.disjointness_trivial d)} (A.conj_disjointness A.disjointness_trivial d) == d) /\
(forall (d:A.disjointness_pre).
{:pattern (A.imp_disjointness d d)} A.imp_disjointness d d) /\
(forall (i:A.slice_inv).
{:pattern (A.inv_implies i i)} A.inv_implies i i) /\
(forall (i:A.slice_inv).
{:pattern (A.inv_implies i A.true_inv)} A.inv_implies i A.true_inv) /\
//inv_implies_conj
(forall (i0 i1 i2:A.slice_inv).
{:pattern (i0 `A.inv_implies` (i1 `A.conj_inv` i2))}
(i0 `A.inv_implies` i1 /\
i0 `A.inv_implies` i2) ==>
(i0 `A.inv_implies` (i1 `A.conj_inv` i2))) /\
//eloc_includes_none
(forall (l:A.eloc).
{:pattern (l `A.eloc_includes` A.eloc_none)} l `A.eloc_includes` A.eloc_none) /\
//eloc_includes_union
(forall (l0 l1 l2:A.eloc).
{:pattern (l0 `A.eloc_includes` (l1 `A.eloc_union` l2))}
(l0 `A.eloc_includes` l1 /\
l0 `A.eloc_includes` l2) ==>
(l0 `A.eloc_includes` (l1 `A.eloc_union` l2))) /\
//eloc_includes_refl
(forall (l:A.eloc).
{:pattern (l `A.eloc_includes` l)} (l `A.eloc_includes` l))
))
= introduce forall d. _
with A.conj_inv_true_left_unit d;
introduce forall d. _
with A.conj_inv_true_right_unit d;
introduce forall l. _
with A.eloc_union_none_right_unit l;
introduce forall l. _
with A.eloc_union_none_left_unit l;
introduce forall l. _
with A.disjoint_none_r l;
introduce forall l. _
with A.disjoint_none_l l;
introduce forall d. _
with A.conj_disjointness_trivial_left_unit d;
introduce forall d. _
with A.conj_disjointness_trivial_right_unit d;
introduce forall d. _
with A.imp_disjointness_refl d;
introduce forall i. _
with A.inv_implies_refl i;
introduce forall i. _
with A.inv_implies_true i;
introduce forall i0 i1 i2.
(i0 `A.inv_implies` i1 /\
i0 `A.inv_implies` i2) ==>
(i0 `A.inv_implies` (i1 `A.conj_inv` i2))
with introduce _ ==> _
with _ . A.inv_implies_conj i0 i1 i2 () ();
introduce forall l. _
with A.eloc_includes_none l;
introduce forall l0 l1 l2. (l0 `A.eloc_includes` l1 /\
l0 `A.eloc_includes` l2) ==>
(l0 `A.eloc_includes` (l1 `A.eloc_union` l2))
with introduce _ ==> _
with _ . A.eloc_includes_union l0 l1 l2 () ();
introduce forall l. _
with A.eloc_includes_refl l




// let inv_true_unit_left (d:A.slice_inv)
// : Lemma
// (ensures (A.true_inv `A.conj_inv` d) == d)
// [SMTPat (A.true_inv `A.conj_inv` d)]
// = A.conj_inv_true_left_unit d

// let inv_true_unit_right (d:A.slice_inv)
// : Lemma
// (ensures (d `A.conj_inv` A.true_inv) == d)
// [SMTPat (d `A.conj_inv` A.true_inv)]
// = A.conj_inv_true_right_unit d

// let loc_none_unit_right (d:A.eloc)
// : Lemma
// (ensures (d `A.eloc_union` A.eloc_none == d))
// [SMTPat (d `A.eloc_union` A.eloc_none)]
// = A.eloc_union_none_right_unit d

// let loc_none_unit_left (d:A.eloc)
// : Lemma
// (ensures (A.eloc_none `A.eloc_union` d == d))
// [SMTPat (A.eloc_none `A.eloc_union` d)]
// = A.eloc_union_none_left_unit d

// let disjoint_none_r (l:A.eloc)
// : Lemma (A.disjoint l A.eloc_none == A.disjointness_trivial)
// [SMTPat (A.disjoint l A.eloc_none)]
// = A.disjoint_none_r l

// let disjoint_none_l (l:A.eloc)
// : Lemma (A.disjoint A.eloc_none l == A.disjointness_trivial)
// [SMTPat (A.disjoint A.eloc_none l)]
// = A.disjoint_none_l l

(* Denotation of atomic_actions as A.action *)
[@@specialize]
Expand Down Expand Up @@ -770,7 +609,7 @@ let atomic_action_as_action
| Action_call c ->
c
| Action_probe_then_validate #nz #wk #k #_hr #inv #l dt src len dest probe ->
index_equations();
A.index_equations();
let v = dtyp_as_validator dt in
A.probe_then_validate v src len dest probe

Expand Down Expand Up @@ -815,7 +654,7 @@ let rec action_as_action
(a:action i d l b t)
: Tot (A.action (interp_inv i) (interp_disj d) (interp_loc l) b t)
(decreases a)
= index_equations();
= A.index_equations();
match a with
| Atomic_action a ->
atomic_action_as_action a
Expand Down Expand Up @@ -1286,7 +1125,7 @@ let rec as_validator
(interp_loc loc)
b)
(decreases t)
= index_equations();
= A.index_equations();
match t
returns Tot (
A.validate_with_action_t #nz #wk #pk #(as_type t)
Expand Down

0 comments on commit e37b3a8

Please sign in to comment.