search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
311 stars 48 forks source link

Unexpected crash #416

Open vbgl opened 1 year ago

vbgl commented 1 year ago

The following program makes easycrypt crash.

Current main version (hash add9232): anomaly: File "src/ecUtils.ml", line 233, characters 24-30: Assertion failed Latest release (2022.04): anomaly: File "src/ecUtils.ml", line 226, characters 24-30: Assertion failed

require import AllCore.

type t.
op d : t distr.

module M = {
  proc f() = {
    var k;
    k <$ d;
  }
}.

lemma correct_scheme &q : Pr[ M.f() @ &q : true ] = 1%r.
proof.
  byphoare.
  proc.
  auto => />.
abort.
strub commented 1 year ago

Note: require Distr solves the issue.

oskgo commented 3 months ago

Managed to trigger the same assertion:

require FinType.

op m (f: 'a -> 'b): 'b.

theory T.
clone FinType.FinType as FT.

type wrapper = [wrap of FT.t].

op foo: wrapper = m wrap.

end T.
clone T as T1.

clone T as T2 with
theory FT <- T1.FT,
type wrapper = T1.wrapper,
op foo <= T1.foo.

The fun part is that op m (f: 'a -> 'b): 'b = witness. makes it work.