search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 8 forks source link

Update dependency: ext/k #313

Closed rv-jenkins closed 2 years ago

sskeirik commented 2 years ago

@ehildenb So, after updating to the latest frontend/kore/z3 combo, one of our tests is failing because of the new frontend check for smt-lemma usage that ensures that all terms in the rule have smtlib or smt-hook attributes. We have a rule of the form:

sskeirik commented 2 years ago

@ehildenb So, with the latest frontend/kore/z3 combo, our proof tests are broken because they fail the new smt-lemma checks. One broken rule is in in tests/proofs/lemmas.md file which is imported by all proof tests, though only some of them make use of this rule:

rule size(_ ;; _:InternalList)  >Int 0 => true [simplification, smt-lemma]

It seems to be failing on the first anonymous variable, but that variable has a very general type, which would seem to require adding a ton of annotations to our codebase. I wonder whether there is a better way.

There are also five other rules in the tests/proofs/multisig-spec.md file which will need to be fixed:

  syntax Int ::= numValidSigs(sigs: InternalList, keys: InternalList) [function, smtlib(numValidSigs)]
  rule numValidSigs([ Some #Signature(_) ] ;; Sigs, [ #Key(_) ] ;; Keys) => 1 +Int numValidSigs(Sigs, Keys) [simplification, smt-lemma]
  rule numValidSigs([ None ] ;; Sigs, _K ;; Keys) => numValidSigs(Sigs, Keys) [simplification, smt-lemma]
  rule numValidSigs(_, .InternalList) => 0 [simplification, smt-lemma]
  rule numValidSigs(_, _) >=Int 0 => true [simplification, smt-lemma]
  rule N:Int +Int ( 1 +Int numValidSigs(L0,L)) => (N:Int +Int 1) +Int numValidSigs(L0,L) [simplification, smt-lemma]

I am not too familiar with smt-lemma, so I would like help with the general process of fixing this kind of problem.

sskeirik commented 2 years ago

So, locally, the test suite passed with the following tests disabled (representing 7 out of 57 proof tests and out of 400+ of total tests):

If it passes CI, I will file issues for these tests and merge the update.