Closed arthurpaulino closed 1 year ago
This PR implements the changes needed to hash the typechecker. So the Lurk code to create proofs of typechecking are modified from this:
(<typechecker code, which is a lambda> <constant hash>)
To this:
((eval (open <typechecker hash>)) <constant hash>)
eval is needed because the typechecker is hashed as a datum.
eval
This PR also removes a potential bug from a double layer of caching, when a cached env has the hash of a constant but the LDON store would not.
This PR implements the changes needed to hash the typechecker. So the Lurk code to create proofs of typechecking are modified from this:
To this:
evalis needed because the typechecker is hashed as a datum.This PR also removes a potential bug from a double layer of caching, when a cached env has the hash of a constant but the LDON store would not.