OAI/Computability/QuantumFactoring/AIGCompiler.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.AIGCompiler.graphWire line 18
  2. def OAI.ExactQuantumFactoring.AIGCompiler.faninNet line 20
  3. lemma OAI.ExactQuantumFactoring.AIGCompiler.fanin_count line 24
  4. lemma OAI.ExactQuantumFactoring.AIGCompiler.fanin_eval line 40
  5. def OAI.ExactQuantumFactoring.AIGCompiler.nodeNet line 45
  6. lemma OAI.ExactQuantumFactoring.AIGCompiler.node_count line 51
  7. def OAI.ExactQuantumFactoring.AIGCompiler.nodeDenote line 62
  8. lemma OAI.ExactQuantumFactoring.AIGCompiler.node_eval line 65
  9. def OAI.ExactQuantumFactoring.AIGCompiler.nodeStep line 82
  10. def OAI.ExactQuantumFactoring.AIGCompiler.partialGraph line 85
  11. lemma OAI.ExactQuantumFactoring.AIGCompiler.graph_count line 90
  12. lemma OAI.ExactQuantumFactoring.AIGCompiler.graph_input line 99
  13. lemma OAI.ExactQuantumFactoring.AIGCompiler.graph_value line 110
  14. theorem OAI.ExactQuantumFactoring.AIGCompiler.graph_correct line 133

    Source documentation

    The circuit interpreter's own, already verified, AIG semantics is preserved by a retained-trace network of at most five nodes per AIG declaration.

    theorem graph_correct (x : Fin (n+g.decls.size) → Bool) (j : Fin g.decls.size) :
    (partialGraph g g.decls.size le_rfl).eval x (graphWire g j) =
      nodeDenote g (fun i => x (i.castAdd g.decls.size)) j :=
…

    Mentions: OAI.ExactQuantumFactoring.AIGCompiler.partialGraph, OAI.ExactQuantumFactoring.AIGCompiler.graphWire, OAI.ExactQuantumFactoring.AIGCompiler.nodeDenote

  15. def OAI.ExactQuantumFactoring.AIGCompiler.compile line 140

    Source documentation

    Compile designated references of an AIG, starting only with its input bits. All graph slots and their retained evaluation traces are genuine ancillas.

    def compile {m : ℕ} (refs : Fin m → AIG.Ref g) : BooleanNetwork n m :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  16. lemma OAI.ExactQuantumFactoring.AIGCompiler.compile_count line 144
  17. lemma OAI.ExactQuantumFactoring.AIGCompiler.compile_correct line 152
  18. def OAI.ExactQuantumFactoring.AIGCompiler.compileVec line 163

    Source documentation

    The whole output BitVec of a native, already verified, arithmetic bitblaster is now a Boolean network with a linear overhead in its AIG graph size.

    def compileVec {w : ℕ} (refs : AIG.RefVec g w) : BooleanNetwork n w :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  19. lemma OAI.ExactQuantumFactoring.AIGCompiler.compileVec_correct line 166
  20. lemma OAI.ExactQuantumFactoring.AIGCompiler.compileVec_count line 170