This type lists the allowed alternatives for “gate”; its constructors are the cases that downstream code must handle.
inductive Gate where
| oneQubit (name : String) (target : Nat)
| rotationY (target : Nat) (angleLabel : String)
| rotationZ (target : Nat) (angleLabel : String)
| cnot (control target : Nat)
| swap (left right : Nat)
| multiControlled (controls : List (Nat × Bool)) (body : Gate)
| oracleCall (name : String)
deriving Repr, DecidableEq
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “circuit”.
abbrev Circuit := List Gate
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”. Conservative elementary-resource estimate for the current IR.
def resource : Gate -> Resource
| oneQubit _ _ => Resource.ofCounts 1 0 0
| rotationY _ _ => Resource.ofCounts 1 0 0
| rotationZ _ _ => Resource.ofCounts 1 0 0
| cnot _ _ => Resource.ofCounts 0 1 0
| swap _ _ => Resource.ofCounts 0 3 0
| oracleCall _ => Resource.ofCountsWithDepth 0 0 1 0 1
| multiControlled controls body =>
body.resource + Resource.ofCounts
(16 * controls.length) (12 * controls.length) controls.length
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “circuit layer”. A layer is a list of gates intended to be scheduled in parallel.
abbrev CircuitLayer := List Gate
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource (layer : CircuitLayer) : Resource :=
layer.foldl (fun acc gate => Resource.parallel acc gate.resource) 0
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “layered circuit”. A layered circuit is the schedule used for depth comparisons.
abbrev LayeredCircuit := List CircuitLayer
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource : LayeredCircuit → Resource
| [] => 0
| layer :: rest => CircuitLayer.resource layer + resource rest
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “depth”.
def depth (circuit : LayeredCircuit) : Nat :=
(resource circuit).depth
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource : Circuit -> Resource
| [] => 0
| gate :: rest => Gate.resource gate + resource rest
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “resource nil”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem resource_nil : resource [] = 0 := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “resource cons”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem resource_cons (gate : Gate) (rest : Circuit) :
resource (gate :: rest) = Gate.resource gate + resource rest := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “depth”.
def depth (circuit : Circuit) : Nat :=
(resource circuit).depth
commit-pinned source · Verso Blueprint panel