Implement the information flow logic described in Winter, Coughlin, Smith 2021 at CSF and for BASIL in https://github.com/UQ-PAC/BASIL/blob/main/docs/iflogic-encoding.pdf
- It should lower the
Gamma/Classification intrinsics to concrete ghost state and function applications
- It requires slight generalisation from the literature to fully cover our IR structures. Notably we specify classifications of memory/maps as functions from keys to booleans. We may want to simplify some type system stuff to make that reasoning easier; or have some integration with the memory lowering pass. We do want cell-precise reasoning about arrays and records.
- When unspecified assume a default gamma.
Break the feature up into the following layers:
Implement the information flow logic described in Winter, Coughlin, Smith 2021 at CSF and for BASIL in https://github.com/UQ-PAC/BASIL/blob/main/docs/iflogic-encoding.pdf
Gamma/Classification intrinsics to concrete ghost state and function applicationsBreak the feature up into the following layers: