Merge pull request #105 from SkyLabsAI/paolo/missing-opacity

cassert/vector specs: add missing opacity/knowledge

Author: pgiarrusso-sl

rocq-brick-libstdcpp/proof/cassert/spec.v

@@ -33,6 +33,8 @@ Section with_cpp.
 
   Definition specs :=
     assert_fail_spec ** assert_rtn_spec.
+  #[global] Hint Opaque specs : typeclass_instances sl_opacity.
+  #[only(knowledge)] derive specs.
 End with_cpp.
 
 NES.End std.cassert.

rocq-brick-libstdcpp/proof/vector/spec.v

@@ -368,6 +368,8 @@ NES.Begin std.
           iter_op_pre_inc const ty alloc_ty **
           iter_op_eq const ty alloc_ty **
           iter_op_ne const ty alloc_ty.
+        #[global] Hint Opaque specs : typeclass_instances sl_opacity.
+        #[only(knowledge)] derive specs.
 
       End iter.
       #[global] Existing Instance iterator_has_rep.
@@ -767,6 +769,8 @@ NES.Begin std.
           size **
           MaybeConst begin_spec **
           MaybeConst end_spec.
+        #[global] Hint Opaque specs : typeclass_instances sl_opacity.
+        #[only(knowledge)] derive specs.
 
       End specs.
 

rocq-brick-libstdcpp/test/vector/test_cpp_proof.v

@@ -294,6 +294,7 @@ Section with_cpp.
     Proof using MOD.
       rewrite /std.vector.specs.
       rewrite /std.vector.iterator.specs.
+      rewrite /std.cassert.specs.
       work.
     Qed.