Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add a Hash interface #98

Open
5 tasks done
marsella opened this issue Jul 26, 2024 · 3 comments · May be fixed by #219
Open
5 tasks done

Add a Hash interface #98

marsella opened this issue Jul 26, 2024 · 3 comments · May be fixed by #219
Assignees
@marsella
Labels
core-utilities good first issue Good for newcomers new-spec Addresses an algorithm that doesn't currently exist

Comments

@marsella
Copy link
Contributor

marsella commented Jul 26, 2024 •
edited
Loading

Many algorithms, like ECDSA, are generic over the hash function they use as long as it satisfies certain properties (e.g. appropriate-length hash output). However, right now there is no unifying interface for hash functions. We should write an interface so that other algorithms can be written generically.

Some useful things we'll want in it, from implementing ECDSA:

  • An accessible hashlen (the length of the output)
  • the Hash function itself
  • I think most hash functions have a constraint on the maximum message size. There should probably be a type constraint as part of the interface that can be used to restrict inputs on functions that call the hash.

There may be other useful things to put in the interface, too.

  • Implement an interface
  • Instantiate it with the SHA2 functions as an example
  • Consider instantiating with other useful hashes as well, or make follow-up issues to do so.
  • Update ECDSA to use the interface (as an example. If this is too hard, make a follow-up issue.)
  • Identify other algorithms that could use it and make follow-up issues.
@marsella marsella mentioned this issue Jul 31, 2024
Merged
marsella added a commit that referenced this issue Aug 1, 2024
@marsella
hash: add first draft of hash interface #98
f64d35d
This was referenced Aug 1, 2024
Open
Merged
@marsella
Copy link
Contributor Author

marsella commented Aug 6, 2024

Notes on the type constraint idea:

  • Interfaces cannot contain generic / fill-in-the-blank constraints. They can contain constraints that must be true for all implementations of the interface
  • A brief pass suggests that many hash functions use the specific constraint that a message must be no more than n bits, for some n. We might be clear to encode this upper bound as a type on the interface and then define the constraint at the interface level (instead of the implementation level).

@weaversa
Copy link
Contributor

weaversa commented Aug 6, 2024

Notes on the type constraint idea:

  • Interfaces cannot contain generic / fill-in-the-blank constraints. They can contain constraints that must be true for all implementations of the interface
  • A brief pass suggests that many hash functions use the specific constraint that a message must be no more than n bits, for some n. We might be clear to encode this upper bound as a type on the interface and then define the constraint at the interface level (instead of the implementation level).

In a recent take we have the following in a parameter block:

  type UpperLimit : #
  hash : {a} (fin a, UpperLimit >= width a) => [a] -> [DigestSize]

This is workable, but I'd love to see an improvement. In the back of my head I've always thought it would be nice if Cryptol could accept type constraints at the parameter level, along with the current values and types (natural numbers).

@marsella marsella mentioned this issue Aug 7, 2024
Closed
3 tasks
This was referenced Aug 20, 2024
Merged
Open
Closed
@mccleeary-galois mccleeary-galois added enhancement New feature or request good first issue Good for newcomers core-utilities labels Aug 29, 2024
@marsella marsella added new-spec Addresses an algorithm that doesn't currently exist and removed enhancement New feature or request labels Aug 29, 2024
@marsella marsella self-assigned this Jan 15, 2025
marsella added a commit that referenced this issue Jan 15, 2025
@marsella
hash: add hash interface #98
d166fd8
marsella added a commit that referenced this issue Jan 15, 2025
@marsella
ecdsa: update to use the hash interface #98
7dd7688 
- Removes all the hardcoded SHA-256 components (including a hardcoded
maximum message width) in ECDSA
- Replaces with the `HashInterface`
- Updates the instantiations to use SHA-256
marsella added a commit that referenced this issue Jan 15, 2025
@marsella
ecdsa: rename p256-sha256 instantiation #98
53d132d 
Renaming now that we could implement ECDSA with other hash functions --
the instantiation name needs to specify which hash is being used!
marsella added a commit that referenced this issue Jan 15, 2025
@marsella
sha3: instantiate HashInterface for SHA3 #98
4f5dab5 
Adds a `fin` constraint to the interface to support truly arbitrary
message lengths in SHA3.
@marsella
Copy link
Contributor Author

Re: the last task. I decided not to search for other use cases at this point. If they arise in our upcoming work we can use the existing hash interface or modify it as necessary.

marsella added a commit that referenced this issue Jan 15, 2025
@marsella
ecdsa: update readme to reflect generic hash #98
40cd5d6
@marsella marsella linked a pull request Jan 15, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@marsella marsella

Labels
core-utilities good first issue Good for newcomers new-spec Addresses an algorithm that doesn't currently exist
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add interface for fixed-length hash functions GaloisInc/cryptol-specs
3 participants
@marsella @weaversa @mccleeary-galois