Examples.lean

1 import CircuitObstructions.CutComparison
2 
3 /-! Constructive witnesses and a refuted target-only shortcut. -/
4 namespace CircuitObstructions.Examples
5 
6 inductive WorkWire where
7   | left | right | scratch | target
8   deriving DecidableEq, Repr
9 
10 def andBoundary : Boundary (Bool × Bool) WorkWire where
11   encode x y
12     | .left => x.1
13     | .right => x.2
14     | .scratch => false
15     | .target => y
16   target := .target
17   target_eq := by intros; rfl
18 
19 def andCompute : Circuit WorkWire :=
20   [.toffoli .left .right .scratch (by decide) (by decide) (by decide)]
21 
22 def andCopy : Circuit WorkWire := [.cnot .scratch .target (by decide)]
23 
24 def andOracle : Circuit WorkWire := andCompute ++ andCopy ++ andCompute
25 
26 /-- Explicit dirty-workspace compute/copy/uncompute oracle for conjunction. -/
27 theorem andOracle_restores :
28     Restores andBoundary andOracle (fun x => x.1 && x.2) := by
29   intro x y
30   rcases x with ⟨a, b⟩
31   cases a <;> cases b <;> cases y <;> funext i <;> cases i <;> rfl
32 
33 theorem andOracle_toffoli_count : toffoliCount andOracle = 2 := rfl
34 
35 /-- The scratch bit need not be zero between the endpoints. -/
36 theorem and_scratch_can_be_dirty :
37     run andCompute (andBoundary.encode (true, true) false) .scratch = true := rfl
38 
39 /-- Every cut of this explicit circuit is an instance of the universal C01 theorem. -/
40 theorem andOracle_every_cut (k : Nat) (x : Bool × Bool) :
41     (x.1 && x.2) = true ↔
42       ∃ i, packet andBoundary (andOracle.take k) (andOracle.drop k) x i = true :=
43   every_index_cut andBoundary andOracle (fun x => x.1 && x.2) andOracle_restores k x
44 
45 inductive SwapWire where
46   | data | target
47   deriving DecidableEq, Repr
48 
49 def swapBoundary : Boundary Bool SwapWire where
50   encode x y
51     | .data => x
52     | .target => y
53   target := .target
54   target_eq := by intros; rfl
55 
56 def swapCircuit : Circuit SwapWire :=
57   [.cnot .data .target (by decide),
58    .cnot .target .data (by decide),
59    .cnot .data .target (by decide)]
60 
61 def swapSuffix : Circuit SwapWire := [.not .data] ++ swapCircuit
62 
63 def outputActiveOracle : Circuit SwapWire := swapCircuit ++ swapSuffix
64 
65 /-- The target is genuinely used as a control in a restored oracle. -/
66 theorem outputActiveOracle_restores :
67     Restores swapBoundary outputActiveOracle (fun _ => true) := by
68   intro x y
69   cases x <;> cases y <;> funext i <;> cases i <;> rfl
70 
71 theorem outputActiveOracle_length : outputActiveOracle.length = 7 := rfl
72 
73 theorem outputActiveOracle_toffoli_count : toffoliCount outputActiveOracle = 0 := rfl
74 
75 /-- At this cut the discrepancy is in the data wire, not in the named target. -/
76 theorem moved_discrepancy_data (x : Bool) :
77     packet swapBoundary swapCircuit swapSuffix x .data = true := by
78   cases x <;> rfl
79 
80 theorem moved_discrepancy_target (x : Bool) :
81     packet swapBoundary swapCircuit swapSuffix x .target = false := by
82   cases x <;> rfl
83 
84 /-- A concrete refutation of replacing the complete register comparison by target-only comparison. -/
85 theorem target_only_reconstruction_is_false :
86     ¬ (∀ x : Bool, packet swapBoundary swapCircuit swapSuffix x .target = true) := by
87   intro h
88   have hh := h false
89   rw [moved_discrepancy_target] at hh
90   contradiction
91 
92 /-- Dropping target separation permits a vacuous endpoint equation for the wrong function. -/
93 theorem degenerate_encoding_control :
94     let bad : Bool → State SwapWire := fun _ _ => false
95     (∀ y, run ([] : Circuit SwapWire) (bad y) = bad (Bool.xor y true)) ∧
96     (∀ i, Bool.xor (bad false i) (bad false i) = false) := by
97   constructor <;> intros <;> rfl
98 
99 end CircuitObstructions.Examples

Back to source controls