The SAWCore.Rewriter library provides a dubious feature called rewritingSharedContext: It creates a SharedContext in which the rewriter is applied to every subterm as it is built:

This feature is incompatible with the idea of having a trusted SAWCore kernel with certified terms and proofs (#49), because it can break type safety: Even if it is not used with unsound rewrite rules, the rewriter is free to transform an input term into one that is not convertible according to the SAW type system.

The rewritingSharedContext feature is made possible because scTermF (which is the basis of all term-forming operations in SAW) is simply a field in the SharedContext record, and can be replaced by arbitrary code later on.

This is a huge backdoor into any SAWCore proof kernel we might try to implement. We cannot have a trusted SAWCore kernel until this is changed and scTermF is given a fixed definition.