• Top
    • Documentation
    • Books
      • Cert.pl
      • Community-books
      • Project-dir-alist
      • Bookdata
      • Book-hash
      • Uncertified-books
      • Sysfile
      • Show-books
      • Best-practices
      • Books-reference
      • Where-do-i-place-my-book
      • Books-tour
        • Include-book
        • Certify-book
        • Certificate
          • Checksum
          • Portcullis
          • Book-name
          • Book-example
          • Book-contents
          • Keep
      • Recursion-and-induction
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Certificate

    Checksum

    Assigning ``often unique'' integers to files and objects

    See book-hash for a discussion of how ACL2 can use checksums (though not by default) to increase security in the books mechanism.

    A checksum is an integer in some fixed range computed from the printed representation of an object, e.g., the sum, modulo 2**32, of the ascii codes of all the characters in the printed representation.

    Ideally, you would like the checksum of an object to be uniquely associated with that object, like a fingerprint. It could then be used as a convenient way to recognize the object in the future: you could remember the checksum (which is relatively small) and when an object is presented to you and alleged to be the special one you could compute its checksum and see if indeed it was. Alas, there are many more objects than checksums (after all, each checksum is an object, and then there's t). So you try to design a checksum algorithm that maps similar looking objects far apart, in the hopes that corruptions and counterfeits — which appear to be similar to the object — have different checksums. Nevertheless, the best you can do is a many-to-one map. If an object with a different checksum is presented, you can be positive it is not the special object. But if an object with the same checksum is presented, you have no grounds for positive identification.

    The basic checksum algorithm in ACL2 is called check-sum-obj, which computes the checksum of an ACL2 object. Roughly speaking, we scan the print representation of the object and, for each character encountered, we multiply the ascii code of the character times its position in the stream (modulo a certain prime) and then add (modulo a certain prime) that into the running sum. This is inaccurate in many senses (for example, we don't always use the ascii code and we see numbers as though they were printed in base 127) but indicates the basic idea.