OAI/Computability/QuantumFactoring/BoundedStack.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.stackEncoding line 19

   Source documentation

   A fixed-capacity little-endian word stack. No dynamic address or unbounded list is part of the corresponding Boolean network.

   def stackEncoding (s w : ℕ) (xs : List (Basis w)) : Basis (s*w) := fun j =>
   …

   Mentions: OAI.ExactQuantumFactoring.Basis

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.block_stackEncoding line 23
3. def OAI.ExactQuantumFactoring.BitArithmetic.stackPop line 29

   Source documentation

   Pop the top, padding the empty end with zero.

   def stackPop (s w : ℕ) : BooleanNetwork (s*w) (s*w) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

4. def OAI.ExactQuantumFactoring.BitArithmetic.stackPush line 35

   Source documentation

   Push a word; the last slot is dropped. Capacity is verified separately in controller invariants, rather than silently growing the physical width.

   def stackPush {k s w : ℕ} (a : BooleanNetwork k w) (v : BooleanNetwork k (s*w)) :
       BooleanNetwork k (s*w) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

5. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPop_value line 40
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPush_value line 49
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.block_ext line 56
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPop_encoding line 62
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPush_encoding line 77
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPop_count line 89
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.stackPush_count line 103