pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs
Other
237 stars 42 forks source link

HOL4 Can't Prove Termination of log2 #449

Closed mmalvarez closed 7 years ago

mmalvarez commented 7 years ago

When I try to build the generated *Script.sml files with HOL4, HOL4 fails on evmScript.sml (translation of evm.lem).

At first glance it seems like the issue is that HOL4's termination/totality checker is not as smart as Isabelle's and so can't prove the termination of log2. Since the failing HOL4 sources are themselves automatically generated from Lem, I'm not sure what the right fix here is (i.e., whether there's any hope of fixing this in Lem or if we'll have to patch the generated code).

The error is as follows:


Holmake: Linking evmScript.uo to produce theory-builder executable
<<HOL message: Created theory "evm">>
Saved definition __ "sintFromW256_def"
Saved definition __ "uint_def"
Saved definition __ "absnat_def"
Saved definition __ "byteFromNat_def"
Saved definition __ "w256_of_bl_def"
Saved definition __ "w256_to_address_def"
Saved definition __ "address_to_w256_def"
Saved definition __ "w256_to_byte_def"
Saved definition __ "byte_to_w256_def"
Saved definition __ "word_rsplit256_def"
Saved definition __ "get_byte_def"
Initial goal:

∃R. WF R ∧ ∀x. ¬(x ≤ 1) ⇒ R (x / 2) x

<<HOL warning: GrammarDeltas.revise_data:
  Grammar-deltas:
    overload_on("log2")
  invalidated by DelConstant(evm$log2)>>

Exception raised at TotalDefn.Define:
between line 111, character 2 and line 113, character 39:
at TotalDefn.defnDefine:

Unable to prove termination!

Try using "TotalDefn.tDefine <name> <quotation> <tac>".
pirapira commented 7 years ago

I was able to reproduce the issue.

pirapira commented 7 years ago

If there is an equivalent function in the HOL4 library, I could do something like:

declare hol target_rep function log2 = `library.log2`

EDIT: I found LOG2.

mmalvarez commented 7 years ago

Thanks!