Skip to content

Commit a7faa8d

Browse files
tcochran-queratcochran-quera
committed
Merge branch 'main' into tcochran-measure_and_reset
merge main.
2 parents c9468bf + 2d1bc01 commit a7faa8d

File tree

182 files changed

+5126
-2115
lines changed

Some content is hidden

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

182 files changed

+5126
-2115
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ jobs:
4343
token: ${{ secrets.CODECOV_TOKEN }} # required
4444
- name: Archive code coverage results
4545
if: matrix.python-version == '3.12'
46-
uses: actions/upload-artifact@v4
46+
uses: actions/upload-artifact@v5
4747
with:
4848
name: code-coverage-report
4949
path: coverage.xml
@@ -55,7 +55,7 @@ jobs:
5555
steps:
5656
- uses: actions/checkout@v5
5757
- name: download covearge
58-
uses: actions/download-artifact@v5
58+
uses: actions/download-artifact@v6
5959
with:
6060
name: code-coverage-report
6161
- name: check coverage

‎.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@v5
16+
- uses: chartboost/ruff-action@v1
17+
with:
18+
args: check --select="D"
19+
src: src/

‎.github/workflows/release.yml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ jobs:
1919
- name: Build distribution 📦
2020
run: uv build
2121
- name: Store the distribution packages
22-
uses: actions/upload-artifact@v4
22+
uses: actions/upload-artifact@v5
2323
with:
2424
name: python-package-distributions
2525
path: dist/
@@ -39,7 +39,7 @@ jobs:
3939

4040
steps:
4141
- name: Download all the dists
42-
uses: actions/download-artifact@v5
42+
uses: actions/download-artifact@v6
4343
with:
4444
name: python-package-distributions
4545
path: dist/
@@ -60,12 +60,12 @@ jobs:
6060

6161
steps:
6262
- name: Download all the dists
63-
uses: actions/download-artifact@v5
63+
uses: actions/download-artifact@v6
6464
with:
6565
name: python-package-distributions
6666
path: dist/
6767
- name: Sign the dists with Sigstore
68-
uses: sigstore/gh-action-sigstore-python@v3.0.1
68+
uses: sigstore/gh-action-sigstore-python@v3.1.0
6969
with:
7070
inputs: >-
7171
./dist/*.tar.gz

‎.pre-commit-config.yaml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ repos:
77
- id: check-yaml
88
args: ['--unsafe']
99
- id: end-of-file-fixer
10+
exclude: .*\.stim$
1011
- id: trailing-whitespace
1112
- repo: https://github.com/pycqa/isort
1213
rev: 6.0.1

‎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.8.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.17.30",
16+
"kirin-toolchain>=0.21.0,<0.23.0",
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/__init__.py‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
from . import impls as impls
22
from .lattice import (
3+
Bottom as Bottom,
34
Address as Address,
4-
NotQubit as NotQubit,
5+
Unknown as Unknown,
56
AddressReg as AddressReg,
6-
AnyAddress as AnyAddress,
7-
AddressWire as AddressWire,
7+
UnknownReg as UnknownReg,
8+
ConstResult as ConstResult,
89
AddressQubit as AddressQubit,
9-
AddressTuple as AddressTuple,
10+
PartialIList as PartialIList,
11+
PartialTuple as PartialTuple,
12+
UnknownQubit as UnknownQubit,
13+
PartialLambda as PartialLambda,
1014
)
1115
from .analysis import AddressAnalysis as AddressAnalysis

0 commit comments

Comments
 (0)