Preserve more Cryptol numeric predicates in SAWCore types by brianhuffman · Pull Request #3202 · GaloisInc/saw-script

brianhuffman · 2026-04-27T22:53:35Z

Previously the Cryptol-to-SAWCore translation erased all Cryptol numeric type constraints (fin, ==, >=, !=, prime) during translation to SAWCore. With this PR, the type-level numeric constraints fin, ==, >= and != are preserved as SAWCore predicates.

This offers multiple benefits:

It removes many calls to error functions within Cryptol.sawcore
With fewer calls to error, we rely less on "inhabited sort" constraints in the Rocq backend
It now becomes theoretically possible to prove properties of polymorphic functions with constraints like 4 >= n by enumeration of cases.

brianhuffman · 2026-04-30T18:07:38Z

The SAW-exercises test is failing on a call to w4_unint_z3 where the function to be uninterpreted has a polymorphic type with a fin constraint. The way I'd like for this to work is actually very similar to how uninterpreted higher-order functions would work (#906). So I might put this PR on hold until that is done.

RyanGlScott · 2026-05-18T18:52:22Z

+Ltac solveUnsafeAssumePGEq :=
+  reflexivity.
+
+Ltac solveUnsafeAssumePNeq :=
+  reflexivity.


I'm somewhat surprised that reflexivity is enough to solver some of the trickier type-level inequality constraints that appear in Cryptol type signatures. I would have figured that something more sophisticated (e.g., lia) would have been required!

It's not. I only expect reflexivity to be able to discharge constraints on concrete type arguments. It appears that the SAW test suite doesn't require anything more than that at the moment, but as soon as we exercise it a bit harder, I'm sure we'll need to replace it with something more sophisticated.

Also, at that point I'll need to recruit someone with much more experience with Ltac programming than I have.

I'm a bit surprised that there's nothing in the test suite currently that requires anything more sophisticated than just reflexivity. Surely it shouldn't be that difficult to cook up a test case where this falls over?

In any case, I'm still worried about this, as I think that this could technically constitute a regression in saw-core-rocq's ability to translate definitions involving type-level equality/inequality constraints. One possible solution here: since the names of these tactics involve the word "unsafe", perhaps they should just fall back on the admit tactic if reflexivity/lia/etc. isn't enough to solve the current goal?

Changing these to try contradiction; try discriminate; auto; try lia would increase the set of things they work on automatically without costing much.

Some things are never going to work automatically, like exponents, and if I understand properly the idea is to have ltac generate the translated term in the middle of a bunch of other stuff, in which case using admit is the only simple way to make it not just croak when loading it.

I think that the current implementation of solveUnsafeAssert may actually suffice for solveUnsafeAssume{PFin,PGEq,PNeq} as well. I suspect that most {PFin,PGEq,PNeq} proof goals will involve equality proofs over type-level numbers, which is exactly what solveUnsafeAssert is designed to solve. The only additions that we might need to make are to teach solveUnsafeAssertStep how to "unfold" certain operations when applied to TCNum arguments. For instance, you'll note the following cases in solveUnsafeAssertStep:

saw-script/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v

Lines 53 to 57 in 023c846

| [ |- context [ addNat ?m ?n ] ] => rewrite (addNat_add m n)

| [ |- context [ mulNat ?m ?n ] ] => rewrite (mulNat_mul m n)

| [ |- context [ subNat ?m ?n ] ] => rewrite (subNat_sub m n)

| [ |- context [ maxNat ?m ?n ] ] => rewrite (maxNat_max m n)

| [ |- context [ minNat ?m ?n ] ] => rewrite (minNat_min m n)

These exist so that we can unfold proof goals about Nums to proof goals about nats, the latter of which the lia tactic is excellent at solving. We may want to add an additional equalNat_eqb case to help simplify PNeq proof goals:

Theorem equalNat_eqb : forall x y, equalNat x y = Nat.eqb x y.

And an additional ltNat_ltb case to help simplify PGeq proof goals:

Theorem ltNat_ltb : forall x y, ltNat x y = Nat.ltb x y.

Note that there is more work that could be done in order to teach solveUnsafeAssert how to use PFin/PGeq/PNeq as assumptions, not just as goals to prove. Doing so would be necessary in order to make the generated Rocq code for zext typecheck, for instance (see #3340). That being said, I don't want to scope-creep this PR more, so I'm happy leave that as future work.

My vote for the moment would be to merge this with minimal changes in the Rocq stuff and then fix it separately, if only to minimize conflicts with what I'm already doing in there.

brianhuffman · 2026-05-19T01:22:35Z

It looks like the only remaining CI failures are caused by #3254. As soon as that's fixed, I should be able to rebase and mark this PR as ready.

brianhuffman · 2026-05-29T21:22:52Z

With PR #3252, issue #3254 is now fixed, and after rebasing all the tests are now passing.

RyanGlScott · 2026-06-03T14:05:57Z

+FalseProp_elim : (a : sort 1) -> FalseProp -> a;
+FalseProp_elim a =
+  Eq__rec Bool True
+  (\ (y : Bool) (_ : Eq Bool True y) ->
+    Bool#rec2 (\ (_ : Bool) -> sort 1) TrueProp a y)
+  TrueI
+  False;


Perhaps this definition should be moved to saw-core/prelude/Prelude.sawcore, alongside the definition of FalseProp itself?

RyanGlScott · 2026-06-03T14:14:35Z

 isErasedPC :: C.PC -> Bool
 isErasedPC pc =


Is your eventual goal here to remove all of the True cases in this function? If so, would it be worth filing follow-up issues for the remaining True cases (e.g., PPrime)?

Yes, that's a good idea. I'd like to preserve PPrime and PValidFloat eventually. I'll have to check with @yav, but I suspect that we should never see PHas, PAnd, or PTrue for fully type-checked Cryptol modules; I think Cryptol guarantees that these are always gone by the time type checking finishes. So it's probably reasonable for cryptol-saw-core to panic on those.

PHas should not appear after type checking, as we should report a type error if we can't simplify it.

However, I think there might be situations where And and True end up in the code. They are generated when we apply substitutions to constraints, and that ends up simplifying the constraints. The reason is that when we do this on already generalized code, it is important that we don't change the number of constraints, as this would change the "API" to the function (i.e., we'd have to also update all call sites). So if a constraint is completely simplified it stays there but becomes true. Otoh, if a constraint ends up simplifying to multiple "simpler" constraints", those are joined with "and", so we still have a single composite constraint.

I haven't tried it, but I think it might happen if you have a functor with a type parameter and then instantiate it with some concrete type.

RyanGlScott · 2026-06-03T14:18:28Z

 Definition maxNat := Nat.max.
 Definition Nat__rec := nat_rect.

+Definition ltNat_0_right (n : nat) : ltNat n Zero = false := eq_refl.


Out of curiosity, why is it beneficial to manually define this in Rocq?

We can't translate the SAW definition of ltNat_0_right directly to Rocq, because it's proved by induction on Nat (i.e. using Nat#ind) and Rocq's nat type isn't defined the same way. Providing a special translation for ltNat_0_right was much easier than writing a Rocq translation rule for Nat#ind. (As mentioned in the comment thread for #1606, the Rocq backend doesn't even have hooks yet for adding translation rules for recursors.)

I would have thought it would translate to N and not nat, and then it would mostly align...

Ah, OK! It might be worth leaving a comment explaining why the choice to special-case this was made, as it wasn't obvious to me until reading this explanation.

Translating Nat to N instead of nat seems like it would be the right thing to do. I think the main thing in the way is our translation of the Vec type: We are currently using a Rocq library with a vector type indexed by nat, so we'd need to find a replacement with a vector type indexed by N.

There are not a whole lot of bitvector libraries, unfortunately. I have one of my own half done (ongoing personal project since before the pandemic) but it's not really done enough to post in public, let alone use.

We should be translating to N rather than nat, but apparently we don't. That's going to need to be its own big breaking change.

I agree. Perhaps we should open an issue about moving from nat to N. (I'd do so myself, although I'm not sure I've fully thought through all of the implications of what this change would bring about.)

I made #3355.

RyanGlScott · 2026-06-03T14:22:15Z

+Ltac solveUnsafeAssumePGEq :=
+  reflexivity.
+
+Ltac solveUnsafeAssumePNeq :=
+  reflexivity.


I'm a bit surprised that there's nothing in the test suite currently that requires anything more sophisticated than just reflexivity. Surely it shouldn't be that difficult to cook up a test case where this falls over?

In any case, I'm still worried about this, as I think that this could technically constitute a regression in saw-core-rocq's ability to translate definitions involving type-level equality/inequality constraints. One possible solution here: since the names of these tactics involve the word "unsafe", perhaps they should just fall back on the admit tactic if reflexivity/lia/etc. isn't enough to solve the current goal?

sauclovian-g · 2026-06-04T00:20:44Z

 Definition maxNat := Nat.max.
 Definition Nat__rec := nat_rect.

+Definition ltNat_0_right (n : nat) : ltNat n Zero = false := eq_refl.


I would have thought it would translate to N and not nat, and then it would mostly align...

sauclovian-g · 2026-06-04T00:34:22Z

+Ltac solveUnsafeAssumePGEq :=
+  reflexivity.
+
+Ltac solveUnsafeAssumePNeq :=
+  reflexivity.


Changing these to try contradiction; try discriminate; auto; try lia would increase the set of things they work on automatically without costing much.

Some things are never going to work automatically, like exponents, and if I understand properly the idea is to have ltac generate the translated term in the middle of a bunch of other stuff, in which case using admit is the only simple way to make it not just croak when loading it.

sauclovian-g · 2026-06-04T00:53:01Z



-Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool :=
+Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin m) (_P1 : CryptolPrimitivesForSAWCore.PGeq m n) (_P2 : CryptolPrimitivesForSAWCore.PGeq n (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool :=


Same for these

`PEqual` is no longer one of the "erased" proposition types in the Cryptol importer, which means that any Cryptol function whose type schema includes a numeric equality constraint will now have that constraint as an argument in its SAWCore type.

This is just for completeness, as `PTrue` should never actually show up in any type-checked Cryptol terms.

`PGeq` is no longer one of the "erased" proposition types in the Cryptol importer, which means that any Cryptol function whose type schema includes a numeric inequality constraint will now have that constraint as an argument in its SAWCore type.

Any Cryptol function whose type schema includes a numeric inequality constraint will now have that constraint as an argument in its SAWCore type.

Any cryptol function whose type includes a `fin` constraint will now have that constraint as an argument in its SAWCore type.

This exercises the import of all Cryptol numeric sequence primitives.

It is replaced by three proposition-specific constants that have actual definitions: * `unsafeAssumePFin` * `unsafeAssumePGeq` * `unsafeAssumePNeq` When evaluated, each of these will force evaluation of its numeric arguments and call `error` if the proposition does not evaluate to true. This ensures that uninterpreted functions will work properly when they have `fin` or inequality constraints.

Also support this lemma in the saw-core-rocq backend.

Rocq did not allow the old `PFin` definition (as an indexed datatype) to be eliminated to a non-Prop type.

If `PFin n` is defined as `Eq Num n PFin -> FalseProp`, then this turns any function with a `PFin` constraint into a higher-order function, causing problems with uninterpreted functions.

Now they are handled consistently with the other `unsafeAssert` primitives already present in the SAWCore prelude.

Courtesy of Ryan Scott.

Cryptol.sawcore has changed.

RyanGlScott · 2026-08-11T18:01:10Z

This PR will need to resolve the merge conflicts that came about as a result of otherTests/saw-core-rocq's reorganization in #3361.

brianhuffman force-pushed the bh/cryptol-preserve-props branch 3 times, most recently from a91522a to dd64670 Compare April 30, 2026 14:22

brianhuffman force-pushed the bh/cryptol-preserve-props branch 3 times, most recently from 6bdb5ae to 48c5597 Compare May 16, 2026 00:27

RyanGlScott reviewed May 18, 2026

View reviewed changes

brianhuffman force-pushed the bh/cryptol-preserve-props branch from 435f2d9 to 6fb9c2d Compare May 29, 2026 18:52

brianhuffman marked this pull request as ready for review May 29, 2026 21:22

brianhuffman requested review from RyanGlScott, chathhorn-galois and sauclovian-g June 1, 2026 20:27

RyanGlScott reviewed Jun 3, 2026

View reviewed changes

brianhuffman force-pushed the bh/cryptol-preserve-props branch from 6fb9c2d to 7176fa6 Compare June 4, 2026 00:30

sauclovian-g reviewed Jun 4, 2026

View reviewed changes

brianhuffman force-pushed the bh/cryptol-preserve-props branch from 7176fa6 to 1f5cc3f Compare June 4, 2026 03:52

RyanGlScott reviewed Jun 4, 2026

View reviewed changes

Comment thread crux-mir-comp/src/Mir/Cryptol.hs Outdated

Comment thread cryptol-saw-core/saw/Cryptol.sawcore Outdated

Comment thread cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs Outdated

This was referenced Jul 10, 2026

saw-core-rocq: Repair solveUnsafeAssert #3338

Merged

saw-core-rocq: Generated code for zext, sext, scarry, and sborrow does not typecheck #3340

Open

RyanGlScott mentioned this pull request Jul 21, 2026

cryptol-saw-core: Panic when importing numeric constraint guard with prime constraint #3352

Open

brianhuffman force-pushed the bh/cryptol-preserve-props branch 2 times, most recently from c3624e2 to a7725fc Compare July 23, 2026 17:51

brianhuffman added 5 commits July 23, 2026 10:51

cryptol-saw-core: Mark constraint PTrue as not erased.

77bda42

This is just for completeness, as `PTrue` should never actually show up in any type-checked Cryptol terms.

cryptol-saw-core: Keep neq (!=) constraints in Cryptol types.

970a336

Any Cryptol function whose type schema includes a numeric inequality constraint will now have that constraint as an argument in its SAWCore type.

cryptol-saw-core: Keep fin constraints in Cryptol types.

d55cc42

Any cryptol function whose type includes a `fin` constraint will now have that constraint as an argument in its SAWCore type.

brianhuffman added 12 commits July 23, 2026 10:51

cryptol-saw-core: Add SAWCore proofs for PFin rules.

9d96979

intTests: Add new regression test test_cryptol_fromto.

d1cfdb1

This exercises the import of all Cryptol numeric sequence primitives.

saw-core: Move lemma ltNat_0_right into Prelude.sawcore.

fe4c3ae

Also support this lemma in the saw-core-rocq backend.

cryptol-saw-core: Reimplement PFin to make Rocq export happy.

7346696

Rocq did not allow the old `PFin` definition (as an indexed datatype) to be eliminated to a non-Prop type.

cryptol-saw-core: Redefine PFin again without using a Pi type.

8eacc15

If `PFin n` is defined as `Eq Num n PFin -> FalseProp`, then this turns any function with a `PFin` constraint into a higher-order function, causing problems with uninterpreted functions.

saw-central: Make llvm_ffi_setup work with numeric type constraints.

a0ebb6f

cryptol-saw-core: Use unsafeAssert instead of declaring new axioms.

0b98359

saw-core-rocq: Translate unsafeAssume variants using Ltac.

e6838d2

Now they are handled consistently with the other `unsafeAssert` primitives already present in the SAWCore prelude.

crux-mir-comp: Generate proof terms to discharge numeric constraints.

bd7b281

cryptol-saw-core: Add proof of PFin_downward_closed.

2107a0e

Courtesy of Ryan Scott.

saw-core-rocq-tests: Update expected outputs.

544f692

Cryptol.sawcore has changed.

brianhuffman force-pushed the bh/cryptol-preserve-props branch from a7725fc to 544f692 Compare July 23, 2026 19:56

brianhuffman mentioned this pull request Aug 3, 2026

Add a new vector / bitvector library for the Rocq exporter #3360

Draft

	\| [ \|- context [ addNat ?m ?n ] ] => rewrite (addNat_add m n)
	\| [ \|- context [ mulNat ?m ?n ] ] => rewrite (mulNat_mul m n)
	\| [ \|- context [ subNat ?m ?n ] ] => rewrite (subNat_sub m n)
	\| [ \|- context [ maxNat ?m ?n ] ] => rewrite (maxNat_max m n)
	\| [ \|- context [ minNat ?m ?n ] ] => rewrite (minNat_min m n)



		Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool :=
		Definition sext (m : CryptolPrimitivesForSAWCore.Num) (n : CryptolPrimitivesForSAWCore.Num) (_P : CryptolPrimitivesForSAWCore.PFin m) (_P1 : CryptolPrimitivesForSAWCore.PGeq m n) (_P2 : CryptolPrimitivesForSAWCore.PGeq n (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH))) (x : CryptolPrimitivesForSAWCore.seq n Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq m Init.Datatypes.bool :=

Uh oh!

Conversation

brianhuffman commented Apr 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

brianhuffman commented Apr 30, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

brianhuffman commented May 19, 2026

Uh oh!

brianhuffman commented May 29, 2026

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yav Jun 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RyanGlScott commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

brianhuffman commented Apr 27, 2026 •

edited

Loading

yav Jun 4, 2026 •

edited

Loading