This definition gives the library's named construction or computation for “primitive basis le equiv”. Convert named primitive bits to a flat little-endian matrix index.
def primitiveBasisLEEquiv : (q : Nat) -> PrimitiveBasis q ≃ Fin (gridSize q)
| 0 =>
{ toFun := fun _ => ⟨0, by decide⟩
invFun := fun _ => Fin.elim0
left_inv := fun bits => funext fun wire => Fin.elim0 wire
right_inv := fun index => by fin_cases index; rfl }
| q + 1 =>
(Fin.consEquiv (fun _ : Fin (q + 1) => Fin 2)).symm
|>.trans (Equiv.prodCongr (Equiv.refl (Fin 2)) (primitiveBasisLEEquiv q))
|>.trans (Equiv.prodComm (Fin 2) (Fin (gridSize q)))
|>.trans finProdFinEquiv
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le equiv zero apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem primitiveBasisLEEquiv_zero_apply (bits : PrimitiveBasis 0) :
(primitiveBasisLEEquiv 0 bits).val = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le equiv succ value”; the hypotheses and conclusion in the code panel fix its exact scope. The recursive equation makes the little-endian convention inspectable.
theorem primitiveBasisLEEquiv_succ_value (q : Nat)
(bits : PrimitiveBasis (q + 1)) :
(primitiveBasisLEEquiv (q + 1) bits).val =
(bits 0).val + 2 *
(primitiveBasisLEEquiv q (fun wire => bits wire.succ)).val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le equiv six value”; the hypotheses and conclusion in the code panel fix its exact scope. Six-wire expansion used by the fixed Robin executable benchmark.
theorem primitiveBasisLEEquiv_six_value (bits : PrimitiveBasis 6) :
(primitiveBasisLEEquiv 6 bits).val =
(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val +
8 * (bits 3).val + 16 * (bits 4).val + 32 * (bits 5).val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “primitive bits 3 le”. Explicit inverse used by finite three-wire compiler proofs.
def primitiveBits3LE (index : Fin 8) : PrimitiveBasis 3
| 0 => ⟨index.val % 2, by omega⟩
| 1 => ⟨(index.val / 2) % 2, by omega⟩
| _ => ⟨(index.val / 4) % 2, by omega⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le equiv three symm”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem primitiveBasisLEEquiv_three_symm (index : Fin 8) :
(primitiveBasisLEEquiv 3).symm index = primitiveBits3LE index := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “primitive bits 3 le without”.
def primitiveBits3LEWithout (target : Fin 3) (index : Fin 8) : Nat :=
match target.val with
| 0 => index.val / 2
| 1 => index.val % 2 + 2 * (index.val / 4)
| _ => index.val % 4
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “split primitive wire primitive bits 3 le context eq”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem splitPrimitiveWire_primitiveBits3LE_context_eq
(target : Fin 3) (left right : Fin 8) :
(splitPrimitiveWire target (primitiveBits3LE left)).2 =
(splitPrimitiveWire target (primitiveBits3LE right)).2 ↔
primitiveBits3LEWithout target left =
primitiveBits3LEWithout target right := by
commit-pinned source · Verso Blueprint panel