Skip to content

Commit 5cc87e7

Browse files
david-pldavid-pl
authored
Merge branch 'main' into david/docstrings-ci
2 parents d900247 + fd9b87e commit 5cc87e7

File tree

2 files changed

+166
-0
lines changed

2 files changed

+166
-0
lines changed

‎proofs/QubitValidation.v‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
From Stdlib Require Import List String Bool.
2+
From Stdlib Require Import Structures.OrderedTypeEx.
3+
From Stdlib Require Import FSets.FSetList.
4+
From Stdlib Require Import FSets.FSetFacts.
5+
From Stdlib Require Import FSets.FSetProperties.
6+
7+
Import ListNotations.
8+
Open Scope string_scope.
9+
10+
Module StringSet := FSetList.Make(String_as_OT).
11+
Module SSF := FSetFacts.WFacts(StringSet).
12+
Module SSP := FSetProperties.Properties(StringSet).
13+
14+
15+
Definition elt := string.
16+
Definition set := StringSet.t.
17+
18+
(*
19+
QubitValidation lattice for control-flow must/may analysis.
20+
21+
Semantics for control flow:
22+
- Bottom: proven safe / never occurs (most precise)
23+
- Must s: definitely occurs on ALL execution paths with violations s
24+
- May s: possibly occurs on SOME execution paths with violations s
25+
- Top: unknown / no information (least precise)
26+
27+
Lattice ordering (more precise --> less precise):
28+
Bottom ⊑ Must s ⊑ May s ⊑ Top
29+
Bottom ⊑ May s ⊑ Top
30+
31+
Key properties:
32+
- Must s ⊔ Bottom = May s (happens on some paths, not all)
33+
- Must s1 ⊔ Must s2 = Must (s1 ∪ s2) (union of violations on all paths)
34+
- May s1 ⊔ May s2 = May (s1 ∪ s2) (union of potential violations)
35+
36+
This models control-flow analysis where we track:
37+
- Which violations definitely happen (Must)
38+
- Which violations might happen (May)
39+
- When we've proven safety (Bottom)
40+
- When we lack information (Top)
41+
*)
42+
Inductive QubitValidation : Type :=
43+
| Bottom : QubitValidation
44+
| Must : set -> QubitValidation
45+
| May : set -> QubitValidation
46+
| Top : QubitValidation.
47+
48+
Definition subsetb_prop (a b : set) : Prop := StringSet.Subset a b.
49+
50+
Definition join (x y : QubitValidation) : QubitValidation :=
51+
match x, y with
52+
| Bottom, Bottom => Bottom
53+
| Bottom, Must v => May v
54+
| Bottom, May v => May v
55+
| Bottom, Top => Top
56+
57+
| Must vx, Bottom => May vx
58+
| Must vx, Must vy => Must (StringSet.union vx vy)
59+
| Must vx, May vy => May (StringSet.union vx vy)
60+
| Must _, Top => Top
61+
62+
| May vx, Bottom => May vx
63+
| May vx, Must vy => May (StringSet.union vx vy)
64+
| May vx, May vy => May (StringSet.union vx vy)
65+
| May _, Top => Top
66+
67+
| Top, _ => Top
68+
end.
69+
70+
Definition validation_eq (x y : QubitValidation) : bool :=
71+
match x, y with
72+
| Bottom, Bottom => true
73+
| Top, Top => true
74+
| Must a, Must b => StringSet.equal a b
75+
| May a, May b => StringSet.equal a b
76+
| _, _ => false
77+
end.
78+
79+
Definition subseteq (x y : QubitValidation) : Prop :=
80+
match x, y with
81+
| Bottom, _ => True
82+
| Must vx, Must vy => subsetb_prop vx vy
83+
| Must vx, May vy => subsetb_prop vx vy
84+
| Must _, Top => True
85+
| May vx, May vy => subsetb_prop vx vy
86+
| May _, Top => True
87+
| Top, Top => True
88+
| _, _ => False
89+
end.
90+
91+
Definition QV_equiv (x y : QubitValidation) : Prop :=
92+
match x, y with
93+
| Bottom, Bottom => True
94+
| Top, Top => True
95+
| Must a, Must b => StringSet.Equal a b
96+
| May a, May b => StringSet.Equal a b
97+
| _, _ => False
98+
end.
99+
100+
Lemma set_equal_bool_iff : forall a b,
101+
StringSet.equal a b = true <-> StringSet.Equal a b.
102+
Proof.
103+
intros a b. split.
104+
- intros Heq. apply StringSet.equal_2. assumption.
105+
- intros H. apply StringSet.equal_1. assumption.
106+
Qed.
107+
108+
Theorem union_commutative_bool : forall a b,
109+
StringSet.equal (StringSet.union a b) (StringSet.union b a) = true.
110+
Proof.
111+
intros. apply StringSet.equal_1. apply SSP.union_sym.
112+
Qed.
113+
114+
Theorem inter_commutative_bool : forall a b,
115+
StringSet.equal (StringSet.inter a b) (StringSet.inter b a) = true.
116+
Proof.
117+
intros. apply StringSet.equal_1. apply SSP.inter_sym.
118+
Qed.
119+
120+
Theorem join_commutative : forall x y,
121+
QV_equiv (join x y) (join y x).
122+
Proof.
123+
intros x y. destruct x; destruct y;
124+
try simpl; try auto; try apply SSP.equal_refl.
125+
- unfold QV_equiv. simpl. apply SSP.union_sym.
126+
- unfold QV_equiv. simpl. apply SSP.union_sym.
127+
- unfold QV_equiv. simpl. apply SSP.union_sym.
128+
- unfold QV_equiv. simpl. apply SSP.union_sym.
129+
Qed.
130+
131+
Lemma join_upper_bound : forall x y,
132+
subseteq x (join x y) /\ subseteq y (join x y).
133+
Proof.
134+
intros x y. destruct x; destruct y.
135+
- split. unfold subseteq. auto. unfold subseteq. auto.
136+
- split. unfold subseteq. auto. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. assumption.
137+
- split. unfold subseteq. auto. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. assumption.
138+
- split. unfold subseteq. auto. unfold subseteq. simpl. auto.
139+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. assumption. unfold subseteq. auto.
140+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_2. assumption.
141+
unfold subseteq. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_3. assumption.
142+
- split. unfold subseteq. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_2. assumption.
143+
unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_3. assumption.
144+
- split. unfold subseteq. simpl. auto. unfold subseteq. simpl. auto.
145+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. assumption. unfold subseteq. auto.
146+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_2. assumption.
147+
unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_3. assumption.
148+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_2. assumption.
149+
unfold subseteq. simpl. simpl. unfold subsetb_prop. intros x Hin. apply StringSet.union_3. assumption.
150+
- split. unfold subseteq. simpl. auto. unfold subseteq. simpl. auto.
151+
- split. unfold subseteq. simpl. simpl. unfold subsetb_prop. auto. unfold subseteq. auto.
152+
- split. unfold subseteq. simpl. auto. unfold subseteq. simpl. auto.
153+
- split. unfold subseteq. simpl. auto. unfold subseteq. simpl. auto.
154+
- split. unfold subseteq. simpl. auto. unfold subseteq. simpl. auto.
155+
Qed.
156+
157+
Theorem join_associative : forall x y z,
158+
QV_equiv (join (join x y) z) (join x (join y z)).
159+
Proof.
160+
intros x y z.
161+
destruct x; destruct y; destruct z; simpl;
162+
unfold QV_equiv; simpl; try reflexivity;
163+
try apply SSP.equal_refl; try apply SSP.union_assoc.
164+
Qed.

‎proofs/_CoqProject‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
-Q . proofs
2+
QubitValidation.v

0 commit comments

Comments
 (0)