↝*-irr-cont postulate is false

[dsheets]

trafficstars

↝*-irr-cont postulated at https://github.com/jmlowenthal/agda-c/blob/348c56754376fd3a901f75ebb93d39402fae3cb3/src/C/Semantics/SmallStep/Properties/Program/Equivalence.agda#L45 is false due to the non-monotonicity of reductions over continuations.

Here is a counterexample:

𝒮 nop [while true then s] E ↝* 𝒮 s [while true then s] E by ↝-nop ↝-while ↝-if-true ↝-seq but despite that 𝒮 nop [] E cannot ↝* 𝒮 s [] E.

↝-irr-cont is fine because all continuation-preserving single steps are continuation agnostic.

I don't see ↝*-irr-cont in use anywhere so I'm not sure what impact its falsification has.

[dsheets]

I believe that a modified ↝*-irr-cont : ∀ { x y : Statement } { k' E E' e } → 𝒮 x [] E ~[ e ]↝* 𝒮 y [] E' → (𝒮 x k' E) ~[ e ]↝* (𝒮 y k' E') should be demanded of inhabitants of Semantics. Roughly speaking, this means that valid interpretations must demonstrate that "reduction sequences unreliant on continuation structure admit any continuation structure". Nothing in the Semantics laws prevents extrajudicial reductions on magical statements that inspect their own continuations and change their behavior depending on the structure of future statements.

[dsheets]

https://github.com/jmlowenthal/agda-c/blob/348c56754376fd3a901f75ebb93d39402fae3cb3/src/C/Semantics/SmallStep/Properties/Program/Equivalence.agda#L46 becomes trivial to prove with this new ↝*-irr-cont.

It would seem that ↝-irr-cont and ↝*-irr-cont are then independent as the former asserts that any single reduction preserving its continuation is unreliant on that continuation whereas the latter asserts that any composition of reductions admitting an empty continuation can admit any continuation (but crucially not the converse due to divergence).

[jmlowenthal]

Good find, thanks @dsheets! Feel free to post a PR if you're working on a solve.