Claim #63 — Verification of crc::Digest<u32, Table<16>>::finalize (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

crc::Digest<u32, Table<16>>::finalize

Recorded callable · signature and safety not independently recorded.

Tool: Aeneas be86ab0f1989d04944292b345b24c435be3ad10a

This claim has no explanation of its own. Read the report Overview, and treat the formal statement below as authoritative. See Concepts and terminology.

Preconditions

1 <= current algorithm.width <= 32; L in {0,1,16}; arbitrary raw word(s), flags and table; public word-level endpoint contract

Formal statement

CrcPublicWordInstances.digest_finalize32_lane16_spec

for allself : CrcBody.Digest Aeneas.Std.U32 (CrcBody.Table 16#usize) (Aeneas.Std.Array (Aeneas.Std.Array Aeneas.Std.U32 256#usize) 16#usize)

assumehw : 1 ≤ ↑self.crc.algorithm.width ∧ ↑self.crc.algorithm.width ≤ 32

then∃ out, CrcBody.crc32.DigestAU32Table.finalize self = Aeneas.Std.Result.ok out ∧ out.bv = CrcStage2.rawFinalize (↑self.crc.algorithm.width) self.crc.algorithm.refin self.crc.algorithm.refout self.crc.algorithm.xorout.bv self.value.bv

In Lean notation, ↑ denotes an implicit type conversion (coercion).

Complete Lean proposition

∀
  (self :
    CrcBody.Digest.{0, 0, 0} Aeneas.Std.U32
      (CrcBody.Table
        (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
          (@of_decide_eq_true
            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (@id.{0}
              (@Eq.{1} Bool
                (@Decidable.decide
                  (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                  (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                Bool.true)
              (@Eq.refl.{1} Bool Bool.true)))))
      (Aeneas.Std.Array.{0}
        (Aeneas.Std.Array.{0} Aeneas.Std.U32
          (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
            (@of_decide_eq_true
              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
              (@id.{0}
                (@Eq.{1} Bool
                  (@Decidable.decide
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                  Bool.true)
                (@Eq.refl.{1} Bool Bool.true)))))
        (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
          (@of_decide_eq_true
            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
            (@id.{0}
              (@Eq.{1} Bool
                (@Decidable.decide
                  (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                  (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                Bool.true)
              (@Eq.refl.{1} Bool Bool.true))))))
  (hw :
    And
      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
        (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8
          (@CrcBody.crc_catalog.Algorithm.width.{0} Aeneas.Std.U32
            (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
              (CrcBody.Table
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (Aeneas.Std.Array.{0}
                (Aeneas.Std.Array.{0} Aeneas.Std.U32
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                self)))))
      (@LE.le.{0} Nat instLENat
        (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8
          (@CrcBody.crc_catalog.Algorithm.width.{0} Aeneas.Std.U32
            (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
              (CrcBody.Table
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (Aeneas.Std.Array.{0}
                (Aeneas.Std.Array.{0} Aeneas.Std.U32
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                self))))
        (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))),
  @Exists.{1} Aeneas.Std.U32 fun (out : Aeneas.Std.U32) =>
    And
      (@Eq.{1} (Aeneas.Std.Result.{0} Aeneas.Std.U32)
        (@CrcBody.crc32.DigestAU32Table.finalize
          (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
            (@of_decide_eq_true
              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
              (@id.{0}
                (@Eq.{1} Bool
                  (@Decidable.decide
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                  Bool.true)
                (@Eq.refl.{1} Bool Bool.true))))
          self)
        (@Aeneas.Std.Result.ok.{0} Aeneas.Std.U32 out))
      (@Eq.{1} (BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))) (Aeneas.Std.U32.bv out)
        (@CrcStage2.rawFinalize (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))
          (@Aeneas.Std.UScalar.val Aeneas.Std.UScalarTy.U8
            (@CrcBody.crc_catalog.Algorithm.width.{0} Aeneas.Std.U32
              (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                  (CrcBody.Table
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Array.{0}
                    (Aeneas.Std.Array.{0} Aeneas.Std.U32
                      (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (@of_decide_eq_true
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (@id.{0}
                            (@Eq.{1} Bool
                              (@Decidable.decide
                                (@LE.le.{0} Nat instLENat
                                  (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                                (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                              Bool.true)
                            (@Eq.refl.{1} Bool Bool.true)))))
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  self))))
          (@CrcBody.crc_catalog.Algorithm.refin.{0} Aeneas.Std.U32
            (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
              (CrcBody.Table
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (Aeneas.Std.Array.{0}
                (Aeneas.Std.Array.{0} Aeneas.Std.U32
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                self)))
          (@CrcBody.crc_catalog.Algorithm.refout.{0} Aeneas.Std.U32
            (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
              (CrcBody.Table
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (Aeneas.Std.Array.{0}
                (Aeneas.Std.Array.{0} Aeneas.Std.U32
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                self)))
          (Aeneas.Std.U32.bv
            (@CrcBody.crc_catalog.Algorithm.xorout.{0} Aeneas.Std.U32
              (@CrcBody.Crc.algorithm.{0, 0, 0} Aeneas.Std.U32
                (CrcBody.Table
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Array.{0}
                  (Aeneas.Std.Array.{0} Aeneas.Std.U32
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat
                                (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (@CrcBody.Digest.crc.{0, 0, 0} Aeneas.Std.U32
                  (CrcBody.Table
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  (Aeneas.Std.Array.{0}
                    (Aeneas.Std.Array.{0} Aeneas.Std.U32
                      (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (@of_decide_eq_true
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (@id.{0}
                            (@Eq.{1} Bool
                              (@Decidable.decide
                                (@LE.le.{0} Nat instLENat
                                  (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                                (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                                  (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                              Bool.true)
                            (@Eq.refl.{1} Bool Bool.true)))))
                    (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (@of_decide_eq_true
                        (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                          (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                        (@id.{0}
                          (@Eq.{1} Bool
                            (@Decidable.decide
                              (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                              (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                                (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                            Bool.true)
                          (@Eq.refl.{1} Bool Bool.true)))))
                  self))))
          (Aeneas.Std.U32.bv
            (@CrcBody.Digest.value.{0, 0, 0} Aeneas.Std.U32
              (CrcBody.Table
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              (Aeneas.Std.Array.{0}
                (Aeneas.Std.Array.{0} Aeneas.Std.U32
                  (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                    (@of_decide_eq_true
                      (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                        (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                      (@id.{0}
                        (@Eq.{1} Bool
                          (@Decidable.decide
                            (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                            (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))
                              (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                          Bool.true)
                        (@Eq.refl.{1} Bool Bool.true)))))
                (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                  (@of_decide_eq_true
                    (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                      (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                    (@id.{0}
                      (@Eq.{1} Bool
                        (@Decidable.decide
                          (@LE.le.{0} Nat instLENat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize))
                          (Nat.decLe (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))
                            (Aeneas.Std.UScalar.cMax Aeneas.Std.UScalarTy.Usize)))
                        Bool.true)
                      (@Eq.refl.{1} Bool Bool.true)))))
              self))))

Theorem source at recorded commit · Recorded check

Referenced definitions (up to 100 direct references)

CrcBody.Digest
Aeneas.Std.U32 · Aeneas.Std.Scalar.Core
CrcBody.Table
Aeneas.Std.Usize.ofNat · Aeneas.Std.Scalar.Core
OfNat.ofNat · Init.Prelude
Nat · Init.Prelude
instOfNatNat · Init.Prelude
of_decide_eq_true · Init.Prelude
LE.le · Init.Prelude
instLENat · Init.Prelude
Aeneas.Std.UScalar.cMax · Aeneas.Std.Scalar.Core
Aeneas.Std.UScalarTy.Usize · Aeneas.Std.Scalar.Core
Nat.decLe · Init.Prelude
id · Init.Prelude
Eq · Init.Prelude
Bool · Init.Prelude
Decidable.decide · Init.Prelude
Bool.true · Init.Prelude
Eq.refl · Init.Prelude
Aeneas.Std.Array · Aeneas.Std.Array.Array
And · Init.Prelude
Aeneas.Std.UScalar.val · Aeneas.Std.Scalar.Core
Aeneas.Std.UScalarTy.U8 · Aeneas.Std.Scalar.Core
CrcBody.crc_catalog.Algorithm.width
CrcBody.Crc.algorithm
CrcBody.Digest.crc
Exists · Init.Core
Aeneas.Std.Result · Aeneas.Std.Primitives
CrcBody.crc32.DigestAU32Table.finalize
Aeneas.Std.Result.ok · Aeneas.Std.Primitives
BitVec · Init.Prelude
Aeneas.Std.U32.bv · Aeneas.Std.Scalar.Core
CrcStage2.rawFinalize
CrcBody.crc_catalog.Algorithm.refin
CrcBody.crc_catalog.Algorithm.refout
CrcBody.crc_catalog.Algorithm.xorout
CrcBody.Digest.value

Mapping: manual. Translation was not rerun by this recording.

Evidence

https://github.com/keiichiw/crate-proofs/blob/d0358890f8bdc8e72a376d225667ac162f89e3b8/crc/3.4.0/aeneas/profiles/stage2/proofs/Stage2Proofs/WordProtocolInstances.lean#L228-L234

What is trusted

From the report

The results depend on Rust-to-LLBC translation (LLBC is the intermediate representation consumed by Aeneas), Aeneas translation, primitive models, and the Lean kernel. Local bit-reversal definitions are assumed to match Rust's standard operations.

Reference model. The model feeds each byte in input-reflection order, applies output reflection and XOR at the end, and appends no zero block.

The proofs concern the translated program after three transformations used to normalize types and names and make source file references portable. If these transformations changed behavior, the proofs could describe a different program. Structural checks support their correspondence to the original translation, but do not formally prove it:

Type-only normalization lifts the built-in table associated type to the exact array type. An independent checker compares function bodies and permits only the specified type-reference changes; negative guards reject unsupported normalization shapes.
A display-name change preserves indices and operations.
File-name relocation is checked by inverse equality of the complete JSON tree.

These checks are not semantic-preservation or compiler-correctness proofs. The transitive audit permits only propext, Classical.choice, and Quot.sound.

Technical limitations

From the report

Conditions for users. Algorithm fields are public, so Rust types do not rule out invalid widths or out-of-range parameters. The public algorithm field of Crc can be replaced after construction, potentially leaving a stale cache. In addition to the parameter conditions, Table<1> checksum and update require the current table to be coherent with the current algorithm; construction alone does not establish coherence after a change. Table<0> has no cached-table coherence requirement.

Not covered. Table<16> checksum and update over message bytes, custom implementations, other lanes and re-exported dependency APIs are outside this coverage. The proofs do not validate catalogue check or residue values.

The selected executable crate bodies come from the locked crates.io 3.4.0 archive. The existing Rust-to-Lean translation (not rerun in this recording) uses the described transformations and locally authored bit-reversal models; their correspondence to release execution is supported by structural checks and native observations, not a formal equivalence theorem.

Tool limitations

Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.

Updated 2026-10-16 00:00 UTC

Aeneas be86ab0f1989d04944292b345b24c435be3ad10a — version details

Read and join the discussion on the report →