Skip to content

Add FILE_SHA256 predicate - #369

Open
4Luke4 wants to merge 2 commits into
WeiDUorg:develfrom
4Luke4:agent/add-file-sha256
Open

Add FILE_SHA256 predicate#369
4Luke4 wants to merge 2 commits into
WeiDUorg:develfrom
4Luke4:agent/add-file-sha256

Conversation

@4Luke4

@4Luke4 4Luke4 commented Jul 26, 2026

Copy link
Copy Markdown

Summary

Add a new FILE_SHA256 fileName sha256sum patch-expression predicate as a cryptographically reliable counterpart to FILE_MD5.

  • Add a self-contained, streaming SHA-256 implementation in OCaml.
  • Wire FILE_SHA256 through the AST, evaluator, diagnostic formatter, legacy lexer/parser, and Elkhound grammar.
  • Preserve the established checksum-predicate semantics: evaluated arguments, case-insensitive hexadecimal comparison, and false for missing files.
  • Add regression coverage for lowercase and uppercase valid digests, an invalid digest, and a missing file.
  • Document FILE_SHA256 in the canonical TeX reference and the WeiDU changes file.
  • Correct the existing FILE_MD5 documentation to state that MD5 is cryptographically unreliable and strongly encourage mod authors to use FILE_SHA256 for new checksum checks.

Design

The implementation does not invoke platform-specific checksum utilities and does not add an external OCaml package or runtime dependency.

Files are read in bounded chunks rather than loaded wholly into memory. Input channels are closed on both successful and exceptional paths.

FILE_SHA256 follows the established behavior of FILE_MD5:

  • The filename and expected checksum arguments are evaluated before use.
  • Hexadecimal checksum comparison is case-insensitive.
  • The calculated checksum is written to the log.
  • A missing file evaluates to false.

Documentation

The canonical doc/base.tex reference now documents:

  • FILE_SHA256 fileName sha256sum.
  • Its case-insensitive hexadecimal comparison behavior.
  • Its logging and missing-file semantics.
  • That MD5 is cryptographically unreliable where collision resistance matters.
  • That mod authors are strongly encouraged to use FILE_SHA256 for new checksum checks.
  • That checksum operations on WeiDU inlined files remain undefined.

Validation

  • Compiled the standalone OCaml SHA-256 module and compared its output with Python's hashlib.sha256 for inputs of 0, 1, 3, 55, 56, 63, 64, 65, 127, 128, 129, 65,535, 65,536, 65,537, and 1,000,000 bytes.
  • Completed a full WeiDU make on Ubuntu 22.04 from the proposed implementation commit.
  • Ran git diff --check successfully.
  • Added TP2 regression coverage for:
    • A valid lowercase SHA-256 digest.
    • A valid uppercase SHA-256 digest.
    • An invalid digest.
    • A missing file.
  • Verified that the final branch contains only the intended implementation, parser, documentation, and regression-test files.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant