GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
14 stars 3 forks source link

Pate.Ground.groundMacawEndCase breaks the abstract boundary of MacawBlockEndType #196

Closed danmatichuk closed 5 months ago

danmatichuk commented 2 years ago

To define Pate.Ground.groundMacawEndCase as a pure function, the abstraction boundary of 'MacawBlockEndType is partially violated. We would like to abstract away the specific encoding of 'MacawBlockEndType', but the only function from macaw for interpreting it is 'Macaw.Symbolic.blockEndCase'

Ideally we could break up MacawBlockEndType into its components and define a pure function in Macaw: GroundValue MacawBlockEndType -> MacawBlockEndCase

danmatichuk commented 2 years ago

Subsumed by #277