We managed to symbolically evaluate some PlutusIR programs, but the interface needs work. If we are to rely on pirouette during our audits, we need to be able to easily run it over a validator. I can imagine that something that looks like the following would work:
pirouettePIR ::
TypedValidator a ->
AssumeProve PlutusIR ->
Assertion
pirouettePIR val condition =
let pir = Pl.getPir val
env@(PrtUnorderedDefs decls main) = _transformAndTr pir
in assertIncorrectnessLogic env (proveAny _stoppingCond) $ IncorrectnessLogicParams
{ ipTarget = main,
ipTargetType = [pir| Bool |],
ipCondition = condition
}
There are a few discrepancies that should be investigated and taken care of, though. For example:
The main term in a PrtUnorderedDefs is never used and can't be referred to. Maybe we should change PirouetteReadDefs to exclute that main term. It would certainly make things cleaner
When writing the condition, we will likely need to rely on existing definitions or plut in a set of auxiliary definitions. Do we need a pirouette-specific plutus prelude? For instance, say the validator is the auction validator, we might want to say that a "bid" never loses that thread token. How do we write this in:
cond :: AssumeProve PlutusIR
cond = ( [pir| \(res : Bool) (dat : Datum) (red : Redeemer) (ctx : ScriptContext) . res && isBid red |]
:==>: [pir| \res dat red ctx . exists out in continuingOuts ctx such that ... |])
As we can see, that will get really difficult really fast, we need to find a way to write these properties with ease.
We managed to symbolically evaluate some PlutusIR programs, but the interface needs work. If we are to rely on pirouette during our audits, we need to be able to easily run it over a validator. I can imagine that something that looks like the following would work:
There are a few discrepancies that should be investigated and taken care of, though. For example:
mainterm in aPrtUnorderedDefsis never used and can't be referred to. Maybe we should changePirouetteReadDefsto exclute that main term. It would certainly make things cleanercondition, we will likely need to rely on existing definitions or plut in a set of auxiliary definitions. Do we need a pirouette-specific plutus prelude? For instance, say the validator is the auction validator, we might want to say that a "bid" never loses that thread token. How do we write this in:As we can see, that will get really difficult really fast, we need to find a way to write these properties with ease.