Skip to content

Commit a8da761

Browse files
johnzl-777johnzl-777
committed
try to merge in latest work
2 parents 4920273 + 0958f24 commit a8da761

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+2227
-881
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: 8 additions & 5 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,11 +13,11 @@ 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",
20-
"pyqrack-cpu~=1.69.1",
20+
"pyqrack-cpu>=1.70.4",
2121
]
2222

2323
[project.optional-dependencies]
@@ -40,10 +40,10 @@ cirq = [
4040
"qpsolvers[clarabel]>=4.7.0",
4141
]
4242
pyqrack-opencl = [
43-
"pyqrack~=1.69.1",
43+
"pyqrack>=1.70.4",
4444
]
4545
pyqrack-cuda = [
46-
"pyqrack-cuda~=1.69.1",
46+
"pyqrack-cuda>=1.70.4",
4747
]
4848
stim = [
4949
"stim>=1.15.0",
@@ -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/analysis/address/analysis.py‎

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,20 @@ class AddressAnalysis(Forward[Address]):
1818
keys = ("qubit.address",)
1919
_const_prop: const.Propagate
2020
lattice = Address
21-
next_address: int = field(init=False)
21+
_next_address: int = field(init=False)
22+
23+
# NOTE: the following are properties so we can hook into the setter in FidelityAnalysis
24+
@property
25+
def next_address(self) -> int:
26+
return self._next_address
27+
28+
@next_address.setter
29+
def next_address(self, value: int):
30+
self._next_address = value
2231

2332
def initialize(self):
2433
super().initialize()
25-
self.next_address: int = 0
34+
self.next_address = 0
2635
self._const_prop = const.Propagate(self.dialects)
2736
self._const_prop.initialize()
2837
return self
@@ -127,7 +136,9 @@ def run_lattice(
127136
case _:
128137
return Address.top()
129138

130-
def get_const_value(self, addr: Address, typ: Type[T]) -> T | None:
139+
def get_const_value(
140+
self, addr: Address, typ: Type[T] | tuple[Type[T], ...]
141+
) -> T | None:
131142
if not isinstance(addr, ConstResult):
132143
return None
133144

‎src/bloqade/analysis/address/impls.py‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -366,16 +366,22 @@ def for_loop(
366366
if iter_type is None:
367367
return interp_.eval_fallback(frame, stmt)
368368

369+
body_values = {}
369370
for value in iterable:
370371
with interp_.new_frame(stmt, has_parent_access=True) as body_frame:
371372
loop_vars = interp_.frame_call_region(
372373
body_frame, stmt, stmt.body, value, *loop_vars
373374
)
374375

376+
for ssa, val in body_frame.entries.items():
377+
body_values[ssa] = body_values.setdefault(ssa, val).join(val)
378+
375379
if loop_vars is None:
376380
loop_vars = ()
377381

378382
elif isinstance(loop_vars, interp.ReturnValue):
383+
frame.set_values(body_frame.entries.keys(), body_frame.entries.values())
379384
return loop_vars
380385

386+
frame.set_values(body_values.keys(), body_values.values())
381387
return loop_vars

0 commit comments

Comments
 (0)