[KIP] - Add a new hook for hashing K terms

Open
#2,568 5 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
32/100
Issue type
Feature
Clarity
Mostly clear
Activity status
Stale
Domain
compilers

Research direction

Start by inspecting the existing LLVM backend support for hashing and how #unparseKORE and Sha3_256 are exposed. Use the proposed #hashK declaration and the KPlutus module uplc-hash.md as reference points. Done means a user-facing hook hashes any K term and the behavior can be validated by replacing #uplcHash in KPlutus.

Written by the indexing model from the issue text.

Description

kip

Motivation

  • Is there a semantics which you are developing which this feature would simplify?

KPlutus - https://github.com/runtimeverification/plutus-core-semantics

  • Is this feature similar to a feature offered by another programming language?

Not that I am aware of.

  • Any other motivation?

It will remove a potential bootleneck at KPlutus that now uses #unparseKORE from K reflection and Sha3_256 functions to hash KPlutus values.

This feature is already present in the LLVM backend. It would only need to be exposed to the user, as far as I know.

Example K Code

Function hashK for instance would receive any K term and return an integer. It could perhaps be declared as

syntax {Sort} Int ::= #hashK(Sort)

I am not sure about the declaration. It was inspired by the declaration of #unparseKORE.

Documentation

Function #hashK produces an integer for any given K term. It may help, for instance, on storing terms on a hash table to represent a heap in a programming language.

Potential Alternatives/Work-arounds

In the KPlutus project we use #unparseKORE and Sha3_256 to implement such a function. Another alternative could be to implement a function that transforms any given KPlutus term into a string and to implement a hash function, all in K.

Testing Approach

This function would could be easily tested in KPlutus simply by rewriting #uplcHash in module uplc-hash.md accordingly or simply replacing the call to #uplcHash by #hashK.

Dominant language
Python
Stars
591
Forks
163
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.