Frame
Difficulty: moderate — 4 definitions, 1 abbreviations, 0 lemmas, 5 theorems, 0 examples.
Frame.crc
Frame.crc (poly bits : List Bool) : List Bool
Show details
fun poly bits => Frame.crcFrom✝ poly (List.replicate poly.length false) bits
Complexity: 25 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Bool, List, List.length, List.replicate
Frame
Frame (poly : List Bool) (n k : ℕ) : Type
Show details
| Frame.mk : {poly : List Bool} → {n k : ℕ} → (Fin n → Bit) → (Fin k → Bit) → Frame poly n k
Outer dependencies: (none)
Inner dependencies: Bit
instNonemptyFrame
instNonemptyFrame {poly : List Bool} {n k : ℕ} : Nonempty (Frame poly n k)
instNormFrame
instNormFrame {poly : List Bool} {n k : ℕ} : Norm (Frame poly n k)
Show details
fun {poly} {n k} => { norm := fun e => ‖e.payload‖ + ‖e.check‖ }
Complexity: 91 (size of the value term)
Outer dependencies: Frame
Inner dependencies: Bit, instNormBit, instNormForallFin_computerNetworks
Frame.make
Frame.make (poly : List Bool) (n : ℕ) (payload : Fin n → Bit) : Frame poly n poly.length
Show details
fun poly n payload => { payload := payload, check := fun i => (Frame.crc poly (List.ofFn fun j => payload j))[↑i]?.getD false }
Complexity: 101 (size of the value term)
Inner dependencies: Frame.crc
Lean core dependencies: Bool, Fin, List, List.length, List.ofFn, Nat, Option.getD
Used by: Frame.make_valid
Frame.valid
Frame.valid (poly : List Bool) {n : ℕ} (e : Frame poly n poly.length) : Prop
Show details
fun poly {n} e => ∀ (i : Fin poly.length), e.check i = (Frame.crc poly (List.ofFn fun j => e.payload j))[↑i]?.getD false
Complexity: 125 (size of the value term)
Outer dependencies: Frame
Lean core dependencies: Bool, Eq, Fin, List, List.length, List.ofFn, Nat, Option.getD
Frame.make_valid
Frame.make_valid (poly : List Bool) (n : ℕ) (payload : Fin n → Bit) : Frame.valid poly (Frame.make poly n payload)
Show details
fun poly n payload x => rfl
Complexity: 45 (size of the value term)
Dependencies: Bit, Frame.make, Frame.valid
Used by: (none)
Frame.crc_detects_single_bit_flip
Frame.crc_detects_single_bit_flip (poly : List Bool) (hpoly : poly.any id = true) (bits : List Bool) (i : Fin bits.length) : Frame.crc poly (bits.set ↑i !bits[i]) ≠ Frame.crc poly bits
Show details
fun poly hpoly bits i => Frame.crcFrom_detects_single_bit_flip✝ poly hpoly (List.replicate poly.length false) (of_eq_true (Eq.trans (congrFun' (congrArg Eq List.length_replicate) poly.length) (eq_self poly.length))) bits i
Complexity: 227 (size of the value term)
Dependencies: Frame.crc
Lean core dependencies: Bool, Bool.not, Decidable.byContradiction, Eq, Eq.trans, Fin, List, List.any, List.length, List.length_replicate, List.replicate, List.set, Nat, Ne, Not, True, congrArg, congrFun', eq_self, id, of_eq_true
Used by: (none)
Frame.crc32Ethernet
Frame.crc32Ethernet (n : ℕ) (hn : n % 8 = 0) (payload : Fin n → Bool) : List Bool
Show details
fun n hn payload => List.map not (Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (List.ofFn (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)))).reverse
Complexity: 151 (size of the value term)
Outer dependencies: (none)
Mathlib dependencies: Equiv.Perm
Lean core dependencies: Bool, Bool.not, Eq, Fin, Function.comp, List, List.map, List.ofFn, List.replicate, List.reverse, Nat
Frame.crc32Ethernet_detects_single_bit_flip
Frame.crc32Ethernet_detects_single_bit_flip (n : ℕ) (hn : n % 8 = 0) (payload : Fin n → Bool) (i : Fin n) : Frame.crc32Ethernet n hn (Function.update payload i !payload i) ≠ Frame.crc32Ethernet n hn payload
Show details
fun n hn payload i heq => have hraw := have h1 := List.map_injective_iff.mpr (fun x y => Bool.casesOn (motive := fun t => x = t → (!x) = !y → x = y) x (fun h => Eq.ndrec (motive := fun x => (!x) = !y → x = y) (Bool.casesOn (motive := fun t => y = t → (!false) = !y → false = y) y (fun h => Eq.ndrec (motive := fun y => (!false) = !y → false = y) (of_eq_true (Eq.trans (implies_congr (Eq.trans (congr (congrArg Eq Bool.not_false) Bool.not_false) (eq_self true)) (eq_self false)) imp_self._simp_1)) (Eq.symm h)) (fun h => Eq.ndrec (motive := fun y => (!false) = !y → false = y) (of_eq_true (Eq.trans (implies_congr (Eq.trans (congr (congrArg Eq Bool.not_false) Bool.not_true) Bool.true_eq_false) Bool.false_eq_true) imp_self._simp_1)) (Eq.symm h)) (Eq.refl y)) (Eq.symm h)) (fun h => Eq.ndrec (motive := fun x => (!x) = !y → x = y) (Bool.casesOn (motive := fun t => y = t → (!true) = !y → true = y) y (fun h => Eq.ndrec (motive := fun y => (!true) = !y → true = y) (of_eq_true (Eq.trans (implies_congr (Eq.trans (congr (congrArg Eq Bool.not_true) Bool.not_false) Bool.false_eq_true) Bool.true_eq_false) imp_self._simp_1)) (Eq.symm h)) (fun h => Eq.ndrec (motive := fun y => (!true) = !y → true = y) (of_eq_true (Eq.trans (implies_congr (Eq.trans (congr (congrArg Eq Bool.not_true) Bool.not_true) (eq_self false)) (eq_self true)) imp_self._simp_1)) (Eq.symm h)) (Eq.refl y)) (Eq.symm h)) (Eq.refl x)) heq; id (Eq.mp (congr (congrArg Eq (List.reverse_reverse (Frame.crcFrom✝ Frame.crc32EthernetPoly✝ [true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true] (List.ofFn ((Function.update payload i !payload i) ∘ ⇑(Frame.reflectEquiv✝ n hn)))))) (List.reverse_reverse (Frame.crcFrom✝ Frame.crc32EthernetPoly✝ [true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true] (List.ofFn (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)))))) (congrArg List.reverse h1)); have hcomp := have this := Function.update_comp_equiv payload (Frame.reflectEquiv✝ n hn) i !payload i; Eq.mp (congrArg (fun _a => (Function.update payload i !payload i) ∘ ⇑(Frame.reflectEquiv✝ n hn) = Function.update (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)) (_a i) !payload i) (Frame.reflectEquiv_symm✝ n hn)) this; let bits := List.ofFn (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)); have hbits := rfl; have hlen := of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congrArg List.length hbits) List.length_ofFn)) n) (eq_self n)); let j := Fin.cast (Eq.symm hlen) ((Frame.reflectEquiv✝ n hn) i); have hjdef := rfl; have hjval := rfl; have hval := of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (GetElem.getElem.congr_simp bits (List.ofFn (payload ∘ Frame.reflectIndex✝ n hn)) hbits j j (Eq.refl j) (id (Decidable.byContradiction fun a => Frame.crc32Ethernet_detects_single_bit_flip._proof_1_2 n hn payload i hlen hjval a))) (Eq.trans (Eq.trans (GetElem.getElem.congr_simp (List.ofFn (payload ∘ Frame.reflectIndex✝ n hn)) (List.ofFn (payload ∘ Frame.reflectIndex✝ n hn)) (Eq.refl (List.ofFn (payload ∘ Frame.reflectIndex✝ n hn))) (↑j) (↑(Frame.reflectIndex✝ n hn i)) hjval (hbits ▸ Eq.refl j ▸ id (Decidable.byContradiction fun a => Frame.crc32Ethernet_detects_single_bit_flip._proof_1_2 n hn payload i hlen hjval a))) (List.getElem_ofFn (hjval ▸ hbits ▸ Eq.refl j ▸ id (Decidable.byContradiction fun a => Frame.crc32Ethernet_detects_single_bit_flip._proof_1_2 n hn payload i hlen hjval a)))) (congrArg payload (Frame.reflectIndex_involutive✝ n hn i))))) (payload i)) (eq_self (payload i))); Frame.crcFrom_detects_single_bit_flip✝ Frame.crc32EthernetPoly✝ Frame.crc32EthernetPoly_any✝ (List.replicate 32 true) (of_eq_true (Eq.trans (congr (congrArg Eq (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd ⋯) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) (Eq.trans (congrArg List.length (Eq.trans List.ofFn_succ (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 31))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 31 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 30))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 30 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 29))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 29 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 28))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 28 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 27))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 27 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 26))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 26 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 25))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 25 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 24))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 24 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 23))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 23 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 22))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 22 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 21))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 21 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 20))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 20 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 19))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 19 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 18))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 18 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 17))) (Eq.trans (Eq.trans (congrArg List.ofFn (funext fun i => congrArg (Nat.testBit 79764919) (Nat.Simproc.sub_add_eq_comm 17 (↑i) 1))) List.ofFn_succ) (congr (congrArg List.cons (congrArg (Nat.testBit 79764919) (tsub_zero 16))) (Eq.trans (Eq.trans (congrArg List.ofFn ⋯) List.ofFn_succ) (congr (congrArg List.cons ⋯) (Eq.trans ⋯ ⋯)))))))))))))))))))))))))))))))))))) (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd ⋯) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1)) 1))) (eq_self 32))) bits j (Eq.mp (congrArg (fun _a => Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (bits.set ↑j !_a) = Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) bits) (Eq.symm hval)) (Eq.mp (congrArg (fun _a => Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (bits.set _a !payload i) = Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) bits) (Eq.symm hjval)) (Eq.mp (congrArg (fun _a => Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (_a.set ↑((Frame.reflectEquiv✝ n hn) i) !payload i) = Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) _a) (have this := rfl; this)) (Eq.mp (congrArg (fun _a => Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) _a = Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (List.ofFn (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)))) (Frame.ofFn_update✝ (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)) ((Frame.reflectEquiv✝ n hn) i) !payload i)) (Eq.mp (congrArg (fun _a => Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (List.ofFn _a) = Frame.crcFrom✝ Frame.crc32EthernetPoly✝ (List.replicate 32 true) (List.ofFn (payload ∘ ⇑(Frame.reflectEquiv✝ n hn)))) hcomp) hraw)))))
Complexity: 158893 (size of the value term)
Dependencies: Frame.crc32Ethernet
Mathlib dependencies: Equiv, Equiv.Perm, Equiv.symm, Function.update, Function.update_comp_equiv, List.map_injective_iff, tsub_self, tsub_zero, zero_add
Lean core dependencies: Bool, Bool.false_eq_true, Bool.not, Bool.not_false, Bool.not_true, Bool.true_eq_false, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.symm, Eq.trans, False, Fin, Fin.cast, Fin.succ, Fin.val_eq_zero, Function.Injective, Function.comp, Int, Int.add_one_le_of_lt, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, List, List.getElem_ofFn, List.length, List.length_ofFn, List.map, List.ofFn, List.ofFn_succ, List.ofFn_zero, List.replicate, List.reverse, List.reverse_reverse, List.set, Nat, Nat.Simproc.sub_add_eq_comm, Nat.cast, Nat.le_of_not_lt, Nat.testBit, Nat.testBit_zero, Ne, Not, True, congr, congrArg, congrFun', decide_true, eq_self, funext, id, implies_congr, le_of_le_of_eq, of_decide_eq_true, of_eq_true, rfl
Used by: (none)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.