In this file we prove the equivalence between a recursive and an iterative compilation function for extended has. The specs use the iterative implementation, which is more efficient and mirrors the Rust implementation, but the proofs rely on the equivalence with the recursive implementation (which mimics the recursive compilation of the desugared form of extended-has).

The only public theorem, at the end of this module, is:

compileExtHasAttr_eq_compileExtHasAttrRec (...) :
  compileExtHasAttr t as εs = compileExtHasAttrRec t as εs

def Cedar.SymCC.compileExtHasAttrRec (t : Term) (as : List Spec.Attr) (εs : SymEntities) : Result Term

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.compileExtHasAttrRec t [] εs = pure (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true)).some
• Cedar.SymCC.compileExtHasAttrRec t [a] εs = do let __do_lift ← Cedar.SymCC.compileHasAttr (Cedar.SymCC.Factory.option.get t) a εs Except.ok (Cedar.SymCC.Factory.ifSome t __do_lift)

theorem Cedar.Thm.compileExtHasAttr_eq_compileExtHasAttrRec (t : SymCC.Term) (as : List Spec.Attr) (εs : SymCC.SymEntities) : SymCC.compileExtHasAttr t as εs = SymCC.compileExtHasAttrRec t as εs