Skip to content

Commit 6755015

Browse files
david-pldavid-pl
authored
Merge branch 'main' into david/592-3-fidelity-analysis
2 parents 8767fc3 + 8fa9d04 commit 6755015

File tree

32 files changed

+908
-688
lines changed

32 files changed

+908
-688
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ jobs:
1919
python-version: ["3.10", "3.11", "3.12"]
2020

2121
steps:
22-
- uses: actions/checkout@v5
22+
- uses: actions/checkout@v6
2323
- name: Install uv
2424
uses: astral-sh/setup-uv@v7
2525
with:
@@ -53,7 +53,7 @@ jobs:
5353
needs: build
5454
if: github.event.pull_request
5555
steps:
56-
- uses: actions/checkout@v5
56+
- uses: actions/checkout@v6
5757
- name: download covearge
5858
uses: actions/download-artifact@v6
5959
with:

‎.github/workflows/docstrings.yml‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
name: Docstrings
2+
on:
3+
pull_request:
4+
push:
5+
branches:
6+
- main
7+
concurrency:
8+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
9+
cancel-in-progress: true
10+
11+
jobs:
12+
docstrings:
13+
runs-on: ubuntu-latest
14+
steps:
15+
- uses: actions/checkout@v6
16+
- uses: chartboost/ruff-action@v1
17+
with:
18+
args: check --select="D"
19+
src: src/

‎.github/workflows/isort.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ jobs:
1212
build:
1313
runs-on: ubuntu-latest
1414
steps:
15-
- uses: actions/checkout@v5
15+
- uses: actions/checkout@v6
1616
- uses: isort/isort-action@v1
1717
with:
1818
sortPaths: "src" # only sort files in the src directory

‎.github/workflows/lint.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ jobs:
1212
ruff:
1313
runs-on: ubuntu-latest
1414
steps:
15-
- uses: actions/checkout@v5
15+
- uses: actions/checkout@v6
1616
- uses: chartboost/ruff-action@v1
1717
black:
1818
runs-on: ubuntu-latest
1919
steps:
20-
- uses: actions/checkout@v5
20+
- uses: actions/checkout@v6
2121
- uses: psf/black@stable

‎.github/workflows/release.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ jobs:
88
runs-on: ubuntu-latest
99

1010
steps:
11-
- uses: actions/checkout@v5
11+
- uses: actions/checkout@v6
1212
- name: Install uv
1313
uses: astral-sh/setup-uv@v7
1414
with:

‎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

‎pyproject.toml‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[project]
22
name = "bloqade-circuit"
3-
version = "0.10.0-DEV"
3+
version = "0.11.0-DEV"
44
description = "The software development toolkit for neutral atom arrays."
55
readme = "README.md"
66
authors = [
@@ -13,7 +13,7 @@ requires-python = ">=3.10"
1313
dependencies = [
1414
"numpy>=1.22.0",
1515
"scipy>=1.13.1",
16-
"kirin-toolchain~=0.21.0",
16+
"kirin-toolchain~=0.22.2",
1717
"rich>=13.9.4",
1818
"pydantic>=1.3.0,<2.11.0",
1919
"pandas>=2.2.3",
@@ -116,6 +116,9 @@ dummy-variable-rgx = "^(_+|(_+[a-zA-Z0-9_]*[a-zA-Z0-9]+?))$"
116116
[tool.coverage.run]
117117
include = ["src/bloqade/*"]
118118

119+
[tool.ruff.lint.pydocstyle]
120+
convention = "google"
121+
119122
[tool.pytest.ini_options]
120123
testpaths = "test/"
121124
filterwarnings = [

‎src/bloqade/cirq_utils/lowering.py‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -282,8 +282,6 @@ def generic_visit(self, state: lowering.State[cirq.Circuit], node: CirqNode):
282282
)
283283
raise lowering.BuildError(f"Cannot lower {node}")
284284

285-
# return self.visit_Operation(state, node)
286-
287285
def lower_literal(self, state: lowering.State[cirq.Circuit], value) -> ir.SSAValue:
288286
raise lowering.BuildError("Literals not supported in cirq circuit")
289287

@@ -658,3 +656,10 @@ def visit_AsymmetricDepolarizingChannel(
658656
probabilities, controls=control_qarg, targets=target_qarg
659657
)
660658
)
659+
660+
def visit_ResetChannel(
661+
self, state: lowering.State[cirq.Circuit], node: cirq.ResetChannel
662+
):
663+
qubits = self.lower_qubit_getindices(state, node.qubits)
664+
stmt = qubit.stmts.Reset(qubits)
665+
return state.current_frame.push(stmt)

‎src/bloqade/gemini/__init__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
from .groups import logical as logical
1+
from .dialects import logical as logical

0 commit comments

Comments
 (0)