saw-core-rocq: Repair solveUnsafeAssert

[RyanGlScott]

There were two problems:

1. It was never brought into scope when write_rocq_term was used to generate Rocq code due to a missing CryptolPrimitivesForSAWCoreExtra import. We fix this by adding the import to the top of the generated file.
2. The definition of solveUnsafeAssert itself was not properly simplifying proof goals. It is unclear to me if this is a change brought on by more recent versions of Rocq, but in any case, repairing this appears to be a matter of being more precise with unfolds and rewrites.

Fixes #3336.

[RyanGlScott]

Unfortunately, I don't have a great way to add a regression test for this, as the existing saw-core-rocq CI infrastructure doesn't actually typecheck much of the generated code (see #3335). That being said, I have confirmed locally that the original example from #3338 now typechecks after these changes.

[RyanGlScott]

In the absence of more comprehensive testing (#3335), I spot-checked what happens if you typecheck the generated Rocq code under otherTests/saw-core-rocq. Unfortunately, this reveals some additional instances of solveUnsafeAssert bitrot that this patch does not address. There are two distinct types of error messages that this uncovers:

TestRec_NestedField{1,2} from otherTests/saw-core-rocq/test_records.saw

If you apply the following patch:

diff --git a/otherTests/saw-core-rocq/test_records.saw b/otherTests/saw-core-rocq/test_records.saw
index 820082178..6601b1ecc 100644
--- a/otherTests/saw-core-rocq/test_records.saw
+++ b/otherTests/saw-core-rocq/test_records.saw
@@ -39,7 +39,7 @@ let t13 = {{ { t1 | x -> x + 5 }      == { x = 20, y = 20 } }};
 write_rocq_term "TestRec_RelativeUpdate" [] [] "" t13;

 let t14 = {{ { t10 | pt.x = 10 }       == { pt = { x = 10, y = 20 }, size = 100 } }};
-write_rocq_term "TestRec_NestedField1" [] [] "" t14;
+write_rocq_term "TestRec_NestedField1" [] [] "TestRec_NestedField1.v" t14;

 let t15 = {{ { t10 | pt.x -> x + 10 }  == { pt = { x = 25, y = 20 }, size = 100 } }};
-write_rocq_term "TestRec_NestedField2" [] [] "" t15;
+write_rocq_term "TestRec_NestedField2" [] [] "TestRec_NestedField2.v" t15;

Run saw test_records.saw and then run rocq compile -Q ../../saw-core-rocq/rocq/generated/CryptolToRocq CryptolToRocq -Q ../../saw-core-rocq/rocq/handwritten/CryptolToRocq CryptolToRocq TestRec_NestedField1.v, you will get the following error message:

Details

$ saw test_records.saw
<snip>
$ rocq compile -Q ../../saw-core-rocq/rocq/generated/CryptolToRocq CryptolToRocq -Q ../../saw-core-rocq/rocq/handwritten/CryptolToRocq CryptolToRocq TestRec_NestedField1.v
File "./TestRec_NestedField1.v", line 34, characters 1075-1118:
Error:
In environment
var__0 := BinPos.Pos.to_nat (BinNums.xO (BinNums.xO (BinNums.xO BinNums.xH)))
  : CryptolPrimitivesForSAWCore.Num
var__1 := CryptolPrimitivesForSAWCore.seq var__0 bool : Type
var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 :
  CryptolPrimitivesForSAWCore.PLiteral
    (CryptolPrimitivesForSAWCore.seq var__0 bool)
var__3 := RecordTypeCons "y" var__1 RecordTypeNil : Type
var__4 := RecordTypeCons "x" var__1 var__3 : Type
var__5 := CryptolPrimitivesForSAWCore.PEqSeqBool var__0 :
  CryptolPrimitivesForSAWCore.PEq
    (CryptolPrimitivesForSAWCore.seq var__0 bool)
var__6 := RecordTypeCons "size" Integer RecordTypeNil : Type
The term "CryptolPrimitivesForSAWCore.PLiteralInteger" has type
 "CryptolPrimitivesForSAWCore.PLiteral Integer"
while it is expected to have type "Inhabited Integer".

(You get a similar error with TestRec_NestedField2.v.)

TestArith_{Sign,Zero}Extend from otherTests/saw-core-rocq/test_arithmetic.saw

If you apply the following patch:

diff --git a/otherTests/saw-core-rocq/test_arithmetic.saw b/otherTests/saw-core-rocq/test_arithmetic.saw
index 0fab549b8..d888d01b4 100644
--- a/otherTests/saw-core-rocq/test_arithmetic.saw
+++ b/otherTests/saw-core-rocq/test_arithmetic.saw
@@ -30,7 +30,7 @@ let t10 = {{ (8 : [8]) >> 2 }};
 write_rocq_term "TestArith_ShiftRight" [] [] "" t10;

 let t11 = {{ sext`{16} (5 : [8]) }};
-write_rocq_term "TestArith_SignExtend" [] [] "" t11;
+write_rocq_term "TestArith_SignExtend" [] [] "TestArith_SignExtend.v" t11;

 let t12 = {{ zext`{16} (5 : [8]) }};
-write_rocq_term "TestArith_ZeroExtend" [] [] "" t12;
+write_rocq_term "TestArith_ZeroExtend" [] [] "TestArith_ZeroExtend.v" t12;

Run saw test_arithmetic.saw and then run rocq compile -Q ../../saw-core-rocq/rocq/generated/CryptolToRocq CryptolToRocq -Q ../../saw-core-rocq/rocq/handwritten/CryptolToRocq CryptolToRocq TestArith_ZeroExtend.v, you will get the following error message:

Details

$ saw test_arithmetic.saw
<snip>
$ rocq compile -Q ../../saw-core-rocq/rocq/generated/CryptolToRocq CryptolToRocq -Q ../../saw-core-rocq/rocq/handwritten/CryptolToRocq CryptolToRocq TestArith_ZeroExtend.v
File "./TestArith_ZeroExtend.v", line 21, characters 0-788:
Error:
The following term contains unresolved implicit arguments:
  (fun (m n : CryptolPrimitivesForSAWCore.Num)
     (x : CryptolPrimitivesForSAWCore.seq n bool) =>
   let var__0 := CryptolPrimitivesForSAWCore.tcSub m n in
   let var__1 := CryptolPrimitivesForSAWCore.tcAdd var__0 n in
   coerce (CryptolPrimitivesForSAWCore.seq var__1 bool)
     (CryptolPrimitivesForSAWCore.seq m bool)
     (CryptolPrimitivesForSAWCore.seq_cong1 var__1 m bool
        ((match var__1 with
          | CryptolPrimitivesForSAWCore.TCNum _1 =>
              (fun _2 : nat =>
               match var__0 with
               | CryptolPrimitivesForSAWCore.TCNum _3 =>
                   (fun _0 : nat =>
                    match
                      n as n0
                      return
                        (CryptolPrimitivesForSAWCore.seq n0 bool ->
                         CryptolPrimitivesForSAWCore.tcAdd
                           (CryptolPrimitivesForSAWCore.tcSub m n0) n0 =
                         m)
                    with
                    | CryptolPrimitivesForSAWCore.TCNum _4 =>
                        (fun (_5 : nat)
                           (x0 : CryptolPrimitivesForSAWCore.seq _5 bool) =>
                         match
                           m as n0
                           return
                             (CryptolPrimitivesForSAWCore.tcAdd
                                (CryptolPrimitivesForSAWCore.tcSub n0 _5) _5 =
                              n0)
                         with
                         | CryptolPrimitivesForSAWCore.TCNum _6 =>
                             (fun _7 : nat =>
                              eq_ind_r (fun n0 : nat => n0 = _7)
                                (eq_ind_r (fun n0 : nat => n0 + _5 = _7)
                                   (Eq_TCNum (_7 - _5 + _5) _7
                                      (?Goal3@{_3:=_7; _2:=_5; x:=x0; _1:=_2}
                                       :
                                       _7 - _5 + _5 = _7))
                                   (SAWCorePreludeExtra.subNat_sub _7 _5))
                                (SAWCorePreludeExtra.addNat_add
                                   (subNat _7 _5) _5)
                              :
                              CryptolPrimitivesForSAWCore.tcAdd
                                (CryptolPrimitivesForSAWCore.tcSub _7 _5) _5 =
                              _7) _6
                         | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                         end) _4
                    | CryptolPrimitivesForSAWCore.TCInf =>
                        fun
                          x0 : CryptolPrimitivesForSAWCore.seq
                                 CryptolPrimitivesForSAWCore.TCInf bool =>
                        match
                          m as n0
                          return
                            (CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub n0
                                  CryptolPrimitivesForSAWCore.TCInf)
                               CryptolPrimitivesForSAWCore.TCInf =
                             n0)
                        with
                        | CryptolPrimitivesForSAWCore.TCNum _4 =>
                            (fun _5 : nat =>
                             ?Goal@{_2:=_5; x:=x0; _1:=_2}
                             :
                             CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub _5
                                  CryptolPrimitivesForSAWCore.TCInf)
                               CryptolPrimitivesForSAWCore.TCInf =
                             _5) _4
                        | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                        end
                    end x) _3
               | CryptolPrimitivesForSAWCore.TCInf =>
                   match
                     n as n0
                     return
                       (CryptolPrimitivesForSAWCore.seq n0 bool ->
                        CryptolPrimitivesForSAWCore.tcAdd
                          (CryptolPrimitivesForSAWCore.tcSub m n0) n0 =
                        m)
                   with
                   | CryptolPrimitivesForSAWCore.TCNum _3 =>
                       (fun (_0 : nat)
                          (x0 : CryptolPrimitivesForSAWCore.seq _0 bool) =>
                        match
                          m as n0
                          return
                            (CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub n0 _0) _0 =
                             n0)
                        with
                        | CryptolPrimitivesForSAWCore.TCNum _4 =>
                            (fun _5 : nat =>
                             eq_ind_r (fun n0 : nat => n0 = _5)
                               (eq_ind_r (fun n0 : nat => n0 + _0 = _5)
                                  (Eq_TCNum (_5 - _0 + _0) _5
                                     (?Goal4@{_2:=_5; x:=x0; _1:=_2}
                                      :
                                      _5 - _0 + _0 = _5))
                                  (SAWCorePreludeExtra.subNat_sub _5 _0))
                               (SAWCorePreludeExtra.addNat_add
                                  (subNat _5 _0) _0)
                             :
                             CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub _5 _0) _0 =
                             _5) _4
                        | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                        end) _3
                   | CryptolPrimitivesForSAWCore.TCInf =>
                       fun
                         x0 : CryptolPrimitivesForSAWCore.seq
                                CryptolPrimitivesForSAWCore.TCInf bool =>
                       match
                         m as n0
                         return
                           (CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub n0
                                 CryptolPrimitivesForSAWCore.TCInf)
                              CryptolPrimitivesForSAWCore.TCInf =
                            n0)
                       with
                       | CryptolPrimitivesForSAWCore.TCNum _3 =>
                           (fun _0 : nat =>
                            ?Goal0@{x:=x0; _1:=_2}
                            :
                            CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub _0
                                 CryptolPrimitivesForSAWCore.TCInf)
                              CryptolPrimitivesForSAWCore.TCInf =
                            _0) _3
                       | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                       end
                   end x
               end) _1
          | CryptolPrimitivesForSAWCore.TCInf =>
              match var__0 with
              | CryptolPrimitivesForSAWCore.TCNum _1 =>
                  (fun _2 : nat =>
                   match
                     n as n0
                     return
                       (CryptolPrimitivesForSAWCore.seq n0 bool ->
                        CryptolPrimitivesForSAWCore.tcAdd
                          (CryptolPrimitivesForSAWCore.tcSub m n0) n0 =
                        m)
                   with
                   | CryptolPrimitivesForSAWCore.TCNum _3 =>
                       (fun (_0 : nat)
                          (x0 : CryptolPrimitivesForSAWCore.seq _0 bool) =>
                        match
                          m as n0
                          return
                            (CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub n0 _0) _0 =
                             n0)
                        with
                        | CryptolPrimitivesForSAWCore.TCNum _4 =>
                            (fun _5 : nat =>
                             eq_ind_r (fun n0 : nat => n0 = _5)
                               (eq_ind_r (fun n0 : nat => n0 + _0 = _5)
                                  (Eq_TCNum (_5 - _0 + _0) _5
                                     (?Goal5@{_2:=_5; x:=x0; _1:=_2}
                                      :
                                      _5 - _0 + _0 = _5))
                                  (SAWCorePreludeExtra.subNat_sub _5 _0))
                               (SAWCorePreludeExtra.addNat_add
                                  (subNat _5 _0) _0)
                             :
                             CryptolPrimitivesForSAWCore.tcAdd
                               (CryptolPrimitivesForSAWCore.tcSub _5 _0) _0 =
                             _5) _4
                        | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                        end) _3
                   | CryptolPrimitivesForSAWCore.TCInf =>
                       fun
                         x0 : CryptolPrimitivesForSAWCore.seq
                                CryptolPrimitivesForSAWCore.TCInf bool =>
                       match
                         m as n0
                         return
                           (CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub n0
                                 CryptolPrimitivesForSAWCore.TCInf)
                              CryptolPrimitivesForSAWCore.TCInf =
                            n0)
                       with
                       | CryptolPrimitivesForSAWCore.TCNum _3 =>
                           (fun _0 : nat =>
                            ?Goal1@{x:=x0; _1:=_2}
                            :
                            CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub _0
                                 CryptolPrimitivesForSAWCore.TCInf)
                              CryptolPrimitivesForSAWCore.TCInf =
                            _0) _3
                       | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                       end
                   end x) _1
              | CryptolPrimitivesForSAWCore.TCInf =>
                  match
                    n as n0
                    return
                      (CryptolPrimitivesForSAWCore.seq n0 bool ->
                       CryptolPrimitivesForSAWCore.tcAdd
                         (CryptolPrimitivesForSAWCore.tcSub m n0) n0 =
                       m)
                  with
                  | CryptolPrimitivesForSAWCore.TCNum _1 =>
                      (fun (_2 : nat)
                         (x0 : CryptolPrimitivesForSAWCore.seq _2 bool) =>
                       match
                         m as n0
                         return
                           (CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub n0 _2) _2 =
                            n0)
                       with
                       | CryptolPrimitivesForSAWCore.TCNum _3 =>
                           (fun _0 : nat =>
                            eq_ind_r (fun n0 : nat => n0 = _0)
                              (eq_ind_r (fun n0 : nat => n0 + _2 = _0)
                                 (Eq_TCNum (_0 - _2 + _2) _0
                                    (?Goal6@{_1:=_2; x:=x0}
                                     :
                                     _0 - _2 + _2 = _0))
                                 (SAWCorePreludeExtra.subNat_sub _0 _2))
                              (SAWCorePreludeExtra.addNat_add
                                 (subNat _0 _2) _2)
                            :
                            CryptolPrimitivesForSAWCore.tcAdd
                              (CryptolPrimitivesForSAWCore.tcSub _0 _2) _2 =
                            _0) _3
                       | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                       end) _1
                  | CryptolPrimitivesForSAWCore.TCInf =>
                      fun
                        x0 : CryptolPrimitivesForSAWCore.seq
                               CryptolPrimitivesForSAWCore.TCInf bool =>
                      match
                        m as n0
                        return
                          (CryptolPrimitivesForSAWCore.tcAdd
                             (CryptolPrimitivesForSAWCore.tcSub n0
                                CryptolPrimitivesForSAWCore.TCInf)
                             CryptolPrimitivesForSAWCore.TCInf =
                           n0)
                      with
                      | CryptolPrimitivesForSAWCore.TCNum _1 =>
                          (fun _2 : nat =>
                           ?Goal2@{_1:=_2; x:=x0}
                           :
                           CryptolPrimitivesForSAWCore.tcAdd
                             (CryptolPrimitivesForSAWCore.tcSub _2
                                CryptolPrimitivesForSAWCore.TCInf)
                             CryptolPrimitivesForSAWCore.TCInf =
                           _2) _1
                      | CryptolPrimitivesForSAWCore.TCInf => eq_refl
                      end
                  end x
              end
          end
          :
          CryptolPrimitivesForSAWCore.tcAdd var__0 n = m)
         :
         var__1 = m))
     (CryptolPrimitivesForSAWCore.ecCat var__0 n bool
        (CryptolPrimitivesForSAWCore.ecZero
           (CryptolPrimitivesForSAWCore.seq var__0 bool)
           (CryptolPrimitivesForSAWCore.PZeroSeqBool var__0))
        x))
More precisely:
- ?Goal: Cannot infer an existential variable of type
  "CryptolPrimitivesForSAWCore.TCInf = _2" in
  environment:
  _2 : nat
  x : CryptolPrimitivesForSAWCore.seq CryptolPrimitivesForSAWCore.TCInf bool
  _0, _1 : nat
- ?Goal0: Cannot infer an existential variable of type
  "CryptolPrimitivesForSAWCore.TCInf = _0" in
  environment:
  _0 : nat
  x : CryptolPrimitivesForSAWCore.seq CryptolPrimitivesForSAWCore.TCInf bool
  _1 : nat
- ?Goal1: Cannot infer an existential variable of type
  "CryptolPrimitivesForSAWCore.TCInf = _0" in
  environment:
  _0 : nat
  x : CryptolPrimitivesForSAWCore.seq CryptolPrimitivesForSAWCore.TCInf bool
  _1 : nat
- ?Goal2: Cannot infer an existential variable of type
  "CryptolPrimitivesForSAWCore.TCInf = _1" in
  environment:
  _1 : nat
  x : CryptolPrimitivesForSAWCore.seq CryptolPrimitivesForSAWCore.TCInf bool
- ?Goal3: Cannot infer an existential variable of type
  "_3 - _2 + _2 = _3" in
  environment:
  _3, _2 : nat
  x : CryptolPrimitivesForSAWCore.seq _2 bool
  _0, _1 : nat
- ?Goal4: Cannot infer an existential variable of type
  "_2 - _0 + _0 = _2" in
  environment:
  _2, _0 : nat
  x : CryptolPrimitivesForSAWCore.seq _0 bool
  _1 : nat
- ?Goal5: Cannot infer an existential variable of type
  "_2 - _0 + _0 = _2" in
  environment:
  _2, _0 : nat
  x : CryptolPrimitivesForSAWCore.seq _0 bool
  _1 : nat
- ?Goal6: Cannot infer an existential variable of type
  "_0 - _1 + _1 = _0" in
  environment:
  _0, _1 : nat
  x : CryptolPrimitivesForSAWCore.seq _1 bool

(You get similar errors with TestArith_SignExtend.v.)

---

I'll mark this PR as a draft until I figure out what to do about these.

[RyanGlScott]

Having taking a closer look at the causes of these type errors, I think it would be best to leave each of these as future work, as they aren't easily resolvable by simply changing the definition of solveUnsafeAssert.

TestRec_NestedField{1,2} from otherTests/saw-core-rocq/test_records.saw

This failure is completely unrelated to solveUnsafeAssert, as far as I can tell. I've opened #3339 to track this.

TestArith_{Sign,Zero}Extend from otherTests/saw-core-rocq/test_arithmetic.saw

When typechecking the generated code for the zext function, solveUnsafeAssert gets stuck when attempting to solve a proposition of the following type:

forall (m n : Num), tcAdd (tcSub m n) n = m.

That lemma doesn't hold in general if m < n or if n = TCInf. We know from the Cryptol type of zext that these cases should not happen:

zext : {m, n} (fin m, m >= n) => [n] -> [m]

However, SAWCore does not currently preserve Cryptol's fin or (>=) constraints during translation, which means that Rocq has no way of knowing this. There is ongoing work to change this (see #3202), so it would be best to revisit this problem once we have access to the necessary constraints in Rocq.

Besides zext, the sext, scarry, and sborrow functions from the Cryptol prelude also exhibit similar issues. While we wait for #3202 to land, it may be worth considering special-casing the translation for these functions to make them typecheck. I've opened #3340 to track this idea.