Remove 'rewritingSharedContext' and related code. #2684

brianhuffman · 2025-10-07T15:31:11Z

sauclovian-g · 2025-10-07T20:29:31Z

Not looking super promising :-(

brianhuffman · 2025-10-13T20:19:30Z

I just force-pushed to 3e21b62: Instead of removing everything all at once, I'm now going to try removing a few rules at a time. I'm starting with the rules to remove coerce, since these are not (and should not be) part of the type system's convertibility relation.

brianhuffman · 2025-10-14T05:12:21Z

Removing the coerce rewrites causes test_hash_table to time out; all other integration tests pass. Investigating test_hash_table has revealed multiple other problems, including #2708 and #2709.

Both of the rewriter conversions `remove_coerce` and `remove_unsafeCoerce` were blatantly type-unsafe. Fortunately neither was ever used.

Neither of the conversions `remove_ident_coerce` and `remove_ident_unsafeCoerce` needed to be a conversion: Both of these are expressible as ordinary rewrite rules, so we don't need either of them as conversions.

Such reductions can cause types on Pi binders to be rewritten, so that they no longer match the types annotated on occurrences of the bound variable. This in turn can cause type checking to fail, as one of the enforced invariants is that all 'Variable' subterms in the scope of a lambda or Pi should have a type that matches exactly.

brianhuffman · 2025-10-24T18:39:13Z

Removing bvConversions has caused test0001 to start timing out. (Previously it took around 8 seconds on CI.) I'll have to try to debug this.

Rewriting with basic_ss includes bvConversions.

brianhuffman · 2025-10-25T00:56:46Z

Remove vecConversions has caused test_sawscript_builtins to fail. The problem is with eval_list:

sawscript> print (eval_list {{ [True, False] }})
[at 2 Bool 0b10 0,at 2 Bool 0b10 1]

The test expects it to print out [True, False].

Now it will immediately return the list of elements instead of applying the SAWCore 'at' function to the whole list. Previously this relied on a rewritingSharedContext with vecConversions to simplify; this is no longer necessary.

sauclovian-g · 2025-10-25T02:58:51Z

Woo, it ran!

brianhuffman · 2025-10-25T13:53:52Z

Removing the rewritingSharedContext from buildTopLevelEnv, even with an empty simpset, seems to have broken test_yosys_compositional. This is probably because rewritingSharedContext also reduces pair and record redexes no matter what, even with no rewrite rules. I probably just need to add a call to scWhnf in one of the Yosys commands.

EDIT: It turns out scWhnf is not what we want, because it unfolds constant definitions. We at least need to evaluate record redexes.

This is an adaptation to the removal of rewritingSharedContext, which used to perform tuple and record reductions as terms were built.

RyanGlScott · 2025-10-25T15:35:05Z

cryptol-saw-core/src/CryptolSAWCore/Simpset.hs

      case nameInfo (defName d) of
        ModuleIdentifier ident -> ident `elem` excludedNames
        ImportedName{} -> True
+    idents = ["Prelude.coerce_same", "Prelude.unsafeCoerce_same"]


I know that cryptol_ss is already a bit ad hoc, but it is interesting that we need to specifically add identifiers from the SAWCore prelude, not cryptol-saw-core's prelude, in order to make things work. This raises a number of questions when I read it:

What determines which identifiers to add to cryptol_ss? The SAW user manual entry gives the impression that it contains primarily Cryptol-specific rules, but clearly there's more to it than that.

Would these be better suited for basic_ss than cryptol_ss? I'm not actually sure if cryptol_ss is a superset of basic_ss, however.

Would it be worth documenting in more detail what cryptol_ss/basic_ss contain in the SAW user manual?

The purpose of cryptol_ss is to be able to take a SAWCore term translated from Cryptol, and reduce it down to basic SAWCore operations and types from the SAWCore prelude. One of the things that cryptol-saw-core does is to insert coercions to handle situations where e.g. symbolic array size types are equal (according to the Cryptol type checker) but not syntactically identical. We rely on coerce_same and unsafeCoerce_same to eliminate such coercions once the size types have been instantiated and reduced to literals.

I'll add some comments to that effect.

See d035e7c.

RyanGlScott · 2025-10-25T15:39:42Z

otherTests/saw-core/Tests/Rewriter.hs

-    let sc = rewritingSharedContext sc0 ss
-    natType <- scNatType sc0
+    ss <- scSimpset sc [] eqs [] :: IO (Simpset ())
+    -- let sc = rewritingSharedContext sc0 ss


Remove this comment?

RyanGlScott · 2025-10-25T15:43:13Z

saw-core/src/SAWCore/SharedTerm.hs

 emptyAppCache :: AppCache
 emptyAppCache = emptyTFM

 -- | Return term for application using existing term in cache if it is available.


This isn't your fault (the comment was like this before the PR), but I have a hard time parsing this sentence. I think some extra speech articles would help. Should this say something like "Return a term for an application, using an existing term in the cache if it is available"?

See new haddocks in a1aa91c.

This makes it so that client code can't break the SharedContext abstraction by updating the 'scTermF' field.

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 6a38e31 to 3e21b62 Compare October 13, 2025 20:17

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 3e21b62 to 3f428c2 Compare October 22, 2025 23:12

brianhuffman added 9 commits October 24, 2025 08:01

Remove ident_coerce conversions from rewritingSharedContext.

3ae94ec

saw-core: Remove remove_coerce rewriter conversions.

a1fab4e

Both of the rewriter conversions `remove_coerce` and `remove_unsafeCoerce` were blatantly type-unsafe. Fortunately neither was ever used.

saw-core: Remove remove_ident_coerce rewriter conversions.

7e477d3

Neither of the conversions `remove_ident_coerce` and `remove_ident_unsafeCoerce` needed to be a conversion: Both of these are expressible as ordinary rewrite rules, so we don't need either of them as conversions.

cryptol-saw-core: Add coerce_same to cryptol simpset.

32b55dc

Remove Cryptol.seq rewrites from default rewritingSharedContext.

60559c1

Update expected output for test2049.

f68409e

Update expected output for test_llvm_errors.

36d9999

Update expected output for test_sawscript_builtins.

adcb05f

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 4a7252f to c138999 Compare October 24, 2025 15:16

brianhuffman added 2 commits October 24, 2025 08:21

Remove tuple/record conversions from default rewritingSharedContext.

7e87f2a

Remove bvConversions from default rewritingSharedContext.

5854c65

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 08050c7 to 5854c65 Compare October 24, 2025 17:54

brianhuffman added 2 commits October 24, 2025 12:02

intTests: Adapt test0001 to the removal of bvConversions.

53c7e97

Rewriting with basic_ss includes bvConversions.

Remove vecConversions from default rewritingSharedContext.

f1b3c04

brianhuffman added 2 commits October 24, 2025 18:09

Remove natConversions from default rewritingSharedContext.

95d55df

saw-script: Stop using rewritingSharedContext in buildTopLevelEnv.

2d66b92

saw-central/yosys: Reduce selectors in 'buildTheorem'.

4557435

This is an adaptation to the removal of rewritingSharedContext, which used to perform tuple and record reductions as terms were built.

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 01c6aa6 to 66ef819 Compare October 25, 2025 14:59

brianhuffman marked this pull request as ready for review October 25, 2025 15:23

brianhuffman requested review from RyanGlScott and sauclovian-g October 25, 2025 15:24

RyanGlScott reviewed Oct 25, 2025

View reviewed changes

brianhuffman added 3 commits October 26, 2025 08:55

otherTests: Update Tests/Rewriter.hs to avoid rewritingSharedContext.

55e10c2

saw-core: Remove rewritingSharedContext. Fixes #2676.

df3b7f9

saw-core: Redefine field accessor 'scTermF' as a normal function.

4bce8d3

This makes it so that client code can't break the SharedContext abstraction by updating the 'scTermF' field.

brianhuffman force-pushed the bh/no-rewriting-shared-context branch from 81a605e to 4bce8d3 Compare October 26, 2025 15:56

brianhuffman added 2 commits October 26, 2025 09:00

saw-core: Rewrite haddock comment for 'scTermF'.

a1aa91c

cryptol-saw-core: Add haddock comments for mkCryptolSimpset.

d035e7c

RyanGlScott approved these changes Oct 27, 2025

View reviewed changes

brianhuffman merged commit b6ad666 into master Oct 27, 2025
37 checks passed

brianhuffman deleted the bh/no-rewriting-shared-context branch October 27, 2025 12:20

This was referenced Oct 27, 2025

saw-core: Rename function 'scInstantiateExt' to 'scInstantiate'. #2746

Merged

rewriteSharedTermConvertibility: rewrite terms without breaking type safety #2750

Draft

Remove 'rewritingSharedContext' and related code. #2684

Remove 'rewritingSharedContext' and related code. #2684

Uh oh!

Conversation

brianhuffman commented Oct 7, 2025

Uh oh!

sauclovian-g commented Oct 7, 2025

Uh oh!

brianhuffman commented Oct 13, 2025

Uh oh!

brianhuffman commented Oct 14, 2025

Uh oh!

brianhuffman commented Oct 24, 2025

Uh oh!

brianhuffman commented Oct 25, 2025

Uh oh!

sauclovian-g commented Oct 25, 2025

Uh oh!

brianhuffman commented Oct 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

RyanGlScott Oct 25, 2025

Choose a reason for hiding this comment

Uh oh!

brianhuffman Oct 26, 2025

Choose a reason for hiding this comment

Uh oh!

brianhuffman Oct 26, 2025

Choose a reason for hiding this comment

Uh oh!

RyanGlScott Oct 25, 2025

Choose a reason for hiding this comment

Uh oh!

RyanGlScott Oct 25, 2025

Choose a reason for hiding this comment

Uh oh!

brianhuffman Oct 26, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

brianhuffman commented Oct 25, 2025 •

edited

Loading