synthesis: add metrics snapshot secret examples

Author: geroldsteiner67

rust/modality/src/cmds/synthesize.rs

@@ -515,6 +515,8 @@ const FORMULA_EXAMPLE_GROUPS: &[FormulaExampleGroup] = &[
             r#"always([+PURGE_CRASH_DUMPS] true -> eventually(<+NOTIFY_RUNTIME_OWNER> true))"#,
             r#"always([+TRACE_EXPORT_SECRET_LEAKED] true -> (<+PURGE_TRACE_EXPORTS> true | <+REVOKE_TRACE_EXPOSED_CREDENTIALS> true))"#,
             r#"always([+PURGE_TRACE_EXPORTS] true -> eventually(<+NOTIFY_TRACING_OWNER> true))"#,
+            r#"always([+METRICS_SNAPSHOT_SECRET_LEAKED] true -> (<+PURGE_METRICS_SNAPSHOTS> true | <+REVOKE_METRICS_EXPOSED_CREDENTIALS> true))"#,
+            r#"always([+PURGE_METRICS_SNAPSHOTS] true -> eventually(<+NOTIFY_METRICS_OWNER> true))"#,
             r#"next(<+APPROVE> true)"#,
             r#"next((<+APPROVE> true | [<+REJECT>] true))"#,
             r#"<+WAIT> true until <+APPROVE> true"#,
@@ -5159,6 +5161,18 @@ F2: formula generated_2 {
         ));
     }
 
+    #[test]
+    fn synthesis_list_includes_metrics_snapshot_secret_leak_prompt_examples() {
+        let output = synthesis_list_text();
+
+        assert!(output.contains(
+            "always([+METRICS_SNAPSHOT_SECRET_LEAKED] true -> (<+PURGE_METRICS_SNAPSHOTS> true | <+REVOKE_METRICS_EXPOSED_CREDENTIALS> true))"
+        ));
+        assert!(output.contains(
+            "always([+PURGE_METRICS_SNAPSHOTS] true -> eventually(<+NOTIFY_METRICS_OWNER> true))"
+        ));
+    }
+
     #[test]
     fn synthesis_list_includes_escrow_progression_prompt_examples() {
         let output = synthesis_list_text();
@@ -15278,6 +15292,22 @@ gfp(X, []((X)) & ([<+ARCHIVE>] true))
         verify_synthesized_model(&model, &formulas).unwrap();
     }
 
+    #[test]
+    fn verify_synthesized_model_accepts_metrics_snapshot_secret_leak_prompt_examples() {
+        let formulas = parse_formula_strings(&[
+            "always([+METRICS_SNAPSHOT_SECRET_LEAKED] true -> (<+PURGE_METRICS_SNAPSHOTS> true | <+REVOKE_METRICS_EXPOSED_CREDENTIALS> true))"
+                .to_string(),
+            "always([+PURGE_METRICS_SNAPSHOTS] true -> eventually(<+NOTIFY_METRICS_OWNER> true))"
+                .to_string(),
+        ]);
+        let model = modality_lang::formula_synthesis::synthesize_from_formulas(
+            "MetricsSnapshotSecretLeak",
+            &formulas,
+        );
+
+        verify_synthesized_model(&model, &formulas).unwrap();
+    }
+
     #[test]
     fn verify_synthesized_model_accepts_mixed_alternatives_with_signer_requirement() {
         let formulas = parse_formula_strings(&[