Cogent Refinement Proofs fail for RISC-V architecture

[gteege]

When setting L4V_ARCH to RISCV64 instead of ARM, isabelle fails to build the session CogentCRefinement. The Cogent version was commit 7f8b944c... of Oct 29th. The error occurs in theory Value_Relation.thy The error message is:

*** Type unification failed: Clash of types "_ bit0" and "1"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  (=) uv :: (char list, unit, 32 word) uval \<Rightarrow> bool
*** Operand:   UPtr (ptr_val x) repr :: (char list, unit, 64 word) uval
*** 
*** Coercion Inference:
*** 
*** Local coercion insertion on the operand failed:
*** Clash of types "_ bit0" and "1"
*** 
*** Now trying to infer coercions globally.
*** 
*** Coercion inference failed:
*** weak unification of subtype constraints fails
*** Clash of types "1" and "_ bit0"
*** 
*** At command "definition" (line 109 of ".../cogent/c-refinement/Value_Relation.thy")

[vjackson725]

I have made changes to the proofs (commit 90f9d19) that should fix this. Could you test this on your code and see if this change helps. Thanks.

[gteege]

Yes, it seems to help, I was now able to build the CogentCRefinement session for architecture RISCV64. Thanks for fixing it.

[gteege]

A similar problem now occurs later in AllRefine.thy (which I could not test before). I am using commit 65b5724ef4a of April 8th in master branch with builtin arrays enabled. The Cogent program is a very simple test program:

f: U32 -> U32
f i = i+1

g: U32 -> U32
g i = f (i+1)

The error message is:

*** Type unification failed: Clash of types "1" and "_ bit0"
*** 
*** Failed to meet type constraint:
*** 
*** Term:  abs_upd_val ::
***   unit
***   \<Rightarrow> 'b \<Rightarrow> char list
***                                  \<Rightarrow> Cogent.type list
***          \<Rightarrow> sigil
***                        \<Rightarrow> 32 word set
***                                      \<Rightarrow> 32 word set
***              \<Rightarrow> bool
*** Type:
***   unit
***   \<Rightarrow> 'b \<Rightarrow> char list
***                                  \<Rightarrow> Cogent.type list
***          \<Rightarrow> sigil
***                        \<Rightarrow> 64 word set
***                                      \<Rightarrow> 64 word set
***              \<Rightarrow> bool
*** 
*** Coercion Inference:
*** 
*** Local coercion insertion on the operand failed:
*** Clash of types "1" and "_ bit0"
*** 
*** Now trying to infer coercions globally.
*** 
*** Coercion inference failed:
*** weak unification of subtype constraints fails
*** Clash of types "_ bit0" and "1"
*** 
*** At command "locale" (line 79 of ".../Test_simple_AllRefine.thy")