Add dummy theorems to all remaining empty spec blocks

gherrit-pr-id: Gclxv3wmgsi7kr7oyevehdtxvcv5vjvg5

Author: joshlf

anneal/tests/fixtures/success_allow_sorry_is_valid/source/src/framework.rs

@@ -17,6 +17,9 @@ pub mod is_valid {
     /// Triggers allow_sorry on the complex isValid autoParam.
     /// Should emit a single "declaration uses sorry" warning.
     /// ```lean, anneal, spec
+    /// theorem spec :
+    ///   Aeneas.Std.WP.spec (unprovable_is_valid) (fun ret_ => True) := by
+    ///   sorry
     /// ```
     pub fn unprovable_is_valid() -> InvalidStruct {
         InvalidStruct { x: 1, y: 2 }
@@ -104,6 +107,9 @@ pub mod signatures {
 
     /// Verifying that padded signatures (due to `cfg`) don't break Anneal specs.
     /// ```lean, anneal, spec
+    /// theorem spec :
+    ///   Aeneas.Std.WP.spec (padded_signature_spec) (fun ret_ => True) := by
+    ///   sorry
     /// ```
     pub fn padded_signature_spec() {}
 }
@@ -129,6 +135,9 @@ fn clean() {}
 fn _anneal_dummy_1() {}
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_9) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_9() {}
 

anneal/tests/fixtures/success_allow_sorry_is_valid/source/src/logic_and_control.rs

@@ -49,12 +49,18 @@ pub mod shadowing {
 
 /// Tests for the never type and panics.
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (crash) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn crash() -> ! {
     panic!("crash")
 }
 
 /// ```lean, anneal, spec
+/// theorem spec (x : Std.U32) :
+///   Aeneas.Std.WP.spec (shadow x) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn shadow(x: u32) -> u32 {
     let x = x + 1;
@@ -68,10 +74,16 @@ pub struct S {
 }
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_6) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_6() {}
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_7) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_7() {}
 
@@ -106,5 +118,8 @@ pub fn unknown_decrease(n: u32) -> u32 {
 }
 
 /// ```lean, anneal, spec
+/// theorem spec {T : Type} (x : T) :
+///   Aeneas.Std.WP.spec (old x) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn old<T>(x: T) -> T { x }

anneal/tests/fixtures/success_allow_sorry_is_valid/source/src/types_and_data.rs

@@ -7,6 +7,9 @@ pub struct Widths {
 }
 
 /// ```lean, anneal, spec
+/// theorem spec (x : _) (y : _) :
+///   Aeneas.Std.WP.spec (check_widths x y) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn check_widths(x: isize, y: usize) -> (isize, usize) {
     (x, y)
@@ -39,6 +42,9 @@ pub struct Foo<T> {
 
 /// Tests for tuple types.
 /// ```lean, anneal, spec
+/// theorem spec (x : _) :
+///   Aeneas.Std.WP.spec (one_tuple x) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn one_tuple(x: (u32,)) -> (u32,) {
     x
@@ -77,6 +83,9 @@ pub mod enums {
 }
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_1) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_1() {}
 
@@ -86,18 +95,30 @@ pub struct ContainerValid<T> {
 }
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_2) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_2() {}
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_3) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_3() {}
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_4) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_4() {}
 
 /// ```lean, anneal, spec
+/// theorem spec :
+///   Aeneas.Std.WP.spec (dummy_anneal_padding_5) (fun ret_ => True) := by
+///   sorry
 /// ```
 pub fn dummy_anneal_padding_5() {}