the CI isn't passing anymore. Btw, now we could merge on main directly to avoid having to sync all the time

The CI isn't passing because, in this branch, the implementation of PreLiquidation is out of date with the harness which has been removed in newer branches. Said newer branches are blocking because a verification is failing. The Certora team should provide assistance on the failing task. I'll tidy up all of this so that we can merge this branch.

Said newer branches are blocking because a verification is failing. The Certora team should provide assistance on the failing task.

What's the task that is blocking ?

I think you can merge main into this branch anyway right ? No need to wait to resolve other failures

@QGarchery

What's the task that is blocking ?

The goal that is failing is the property that shows that a pre-liquidation is created iff the market exists in the PR #37 .

I think you can merge main into this branch anyway right ? No need to wait to resolve other failures

The branch main has been merged in this branch, this is not the issue. Perhaps the situation is unclear.

As talked over with @MathisGD, this branch is meant as a develop branch that lives in parallel to the solidity development. This helps me maintaining a clean setup and to stay close to upstream branches whilst syncing with upstream changes only when they are somewhat stable. That means that fixes with respect to upstream changes are done in branches that target colin@verif/setup, namely #37. You may think of it as a the principal branch of the verification to target pull requests.

If you want to me adopt another workflow just let me know which are your recommendations to organize the work. I chose this as there was no given workflow or recommended setup.

I was probably unclear when we discussed this, but this isn't what I had in mind. To me now we should merge this branch in main. This has the benefit of making it clear for other devs and you that we are introducing a change that's breaking the verification, and avoid you to have to merge main in this branch all the time.

The parallel branch was for when the code wasn't even on main, so having the verif in the same PR would have been weird.

Does that work for you?

Sure! I'll fix this so we can merge it then.

@MathisGD and @QGarchery CI is fixed in 7463846.