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.

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

[New module system] Incorrect IR after module insantiation #1450

Closed
yav opened this issue Oct 12, 2022 · 2 comments
Closed

[New module system] Incorrect IR after module insantiation #1450

yav opened this issue Oct 12, 2022 · 2 comments
Assignees
Labels
bug Something not working correctly importing instantiations

Comments

@yav
Copy link
Member

yav commented Oct 12, 2022

To reproduce:

  1. Checkout cryptol-specs
  2. Start cryptol
  3. :set coreLint=on
  4. :load Primitive/Keyless/Hash/SHA2/SHA512.cry

This needs more investigation, but the cause might due to the fact that when we instantiate a module we substitute concrete types into the schemas of some things. This might cause certain predicates in the qualified types to become True and thus disappear, but then the underlying term is incorrect because it expects evidence for something which is now gone.

@yav yav changed the title Incorrect IR after module insantiation [New module system] Incorrect IR after module insantiation Oct 12, 2022
@yav
Copy link
Member Author

yav commented Oct 12, 2022

The comment above describes the problem. Here is a smaller example to reproduce it:

submodule F where
  parameter
    type n : #

  f : (2 < n) => ()
  f = ()

submodule M = submodule F where
  type n = 8
Main> :set debug=on
Main> :r
Loading module Cryptol
Loading module Main
module Main
import Cryptol
  
/* Not recursive */
Main::M::f : ()
Main::M::f = \(True) -> ()

@yav
Copy link
Member Author

yav commented Oct 12, 2022

There's also an issue if we change the above example to instantiate F with 1 in which case the predicate would become False. Apparently coreLint does not like that, so we need to investigate why that is.

@yav yav self-assigned this Oct 13, 2022
@yav yav added bug Something not working correctly importing instantiations labels Oct 13, 2022
@yav yav closed this as completed Oct 20, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly importing instantiations
Projects
None yet
Development

No branches or pull requests

1 participant