Closed rtjoa closed 1 month ago
Add a mechanized formal semantics for eggcc IR*, as well as proofs of:
(If pred in then else)
(If pred in (Ctx (InThen pred in) then) (Ctx (InElse pred in) else)
(Ctx a (PureOp e))
(PureOp (Ctx a e))
(Ctx a (If pred in then else))
(If (Ctx a pred) (Ctx a in) then else)
(Ctx a (DoWhile in pred out))
(DoWhile (Ctx a in) pred out)
(Ctx (InThen pred (Const c)) Arg)
(Ctx (InThen pred (Const c)) (Const c))
*See here for more explanation of the modeled IR/semantics, which are more general (context nodes, arbitrary pure ops) than those actually used in eggcc now: https://uw-cse.slack.com/archives/C06CH261JM9/p1718175743886959
Add a mechanized formal semantics for eggcc IR*, as well as proofs of:
(If pred in then else)is equivalent to(If pred in (Ctx (InThen pred in) then) (Ctx (InElse pred in) else)(Ctx a (PureOp e))is equivalent to(PureOp (Ctx a e))(Ctx a (If pred in then else))is equivalent to(If (Ctx a pred) (Ctx a in) then else)(Ctx a (DoWhile in pred out))is equivalent to(DoWhile (Ctx a in) pred out)(Ctx (InThen pred (Const c)) Arg)is equivalent to(Ctx (InThen pred (Const c)) (Const c))*See here for more explanation of the modeled IR/semantics, which are more general (context nodes, arbitrary pure ops) than those actually used in eggcc now: https://uw-cse.slack.com/archives/C06CH261JM9/p1718175743886959