search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

CorresProof fails in the dargent branch for a cogent program without layout #361

Closed amblafont closed 4 years ago

amblafont commented 4 years ago

Consider the following cogent program

main : U32 -> U32
main aa = aa + 1

Then the generated CorresProof theory file fails in the dargent branch, but not in the master branch. I have noticed that the generated Cogent expression in TypeProof is not the same for these two branches. In master branch, it is : Let (Var 0) (Let (Lit (LU32 1)) (Prim (Plus U32) [Var 1, Var 0])), whereas in the failing dargent branch, it is Let (Var 0) (Prim (Plus U32) [Var 0, Lit (LU32 1)]).

I edited the TypeProof theory file generated in the dargent branch to replace the cogent expression with the one from master, but CorresProff still fails.

Also, CorresProof works fine in the dargent branch for the following program:

main : U32 -> U32
main aa = aa + aa
amblafont commented 4 years ago

This is fixed in the master branch (in which the dargent branch was merged)