Skip to content

Commit ee88272

Browse files
synthesis: add profile dump secret examples
1 parent beac442 commit ee88272

1 file changed

Lines changed: 30 additions & 0 deletions

File tree

rust/modality/src/cmds/synthesize.rs

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -517,6 +517,8 @@ const FORMULA_EXAMPLE_GROUPS: &[FormulaExampleGroup] = &[
517517
r#"always([+PURGE_TRACE_EXPORTS] true -> eventually(<+NOTIFY_TRACING_OWNER> true))"#,
518518
r#"always([+METRICS_SNAPSHOT_SECRET_LEAKED] true -> (<+PURGE_METRICS_SNAPSHOTS> true | <+REVOKE_METRICS_EXPOSED_CREDENTIALS> true))"#,
519519
r#"always([+PURGE_METRICS_SNAPSHOTS] true -> eventually(<+NOTIFY_METRICS_OWNER> true))"#,
520+
r#"always([+PROFILE_DUMP_SECRET_LEAKED] true -> (<+PURGE_PROFILE_DUMPS> true | <+REVOKE_PROFILE_EXPOSED_CREDENTIALS> true))"#,
521+
r#"always([+PURGE_PROFILE_DUMPS] true -> eventually(<+NOTIFY_PROFILING_OWNER> true))"#,
520522
r#"next(<+APPROVE> true)"#,
521523
r#"next((<+APPROVE> true | [<+REJECT>] true))"#,
522524
r#"<+WAIT> true until <+APPROVE> true"#,
@@ -5173,6 +5175,18 @@ F2: formula generated_2 {
51735175
));
51745176
}
51755177

5178+
#[test]
5179+
fn synthesis_list_includes_profile_dump_secret_leak_prompt_examples() {
5180+
let output = synthesis_list_text();
5181+
5182+
assert!(output.contains(
5183+
"always([+PROFILE_DUMP_SECRET_LEAKED] true -> (<+PURGE_PROFILE_DUMPS> true | <+REVOKE_PROFILE_EXPOSED_CREDENTIALS> true))"
5184+
));
5185+
assert!(output.contains(
5186+
"always([+PURGE_PROFILE_DUMPS] true -> eventually(<+NOTIFY_PROFILING_OWNER> true))"
5187+
));
5188+
}
5189+
51765190
#[test]
51775191
fn synthesis_list_includes_escrow_progression_prompt_examples() {
51785192
let output = synthesis_list_text();
@@ -15308,6 +15322,22 @@ gfp(X, []((X)) & ([<+ARCHIVE>] true))
1530815322
verify_synthesized_model(&model, &formulas).unwrap();
1530915323
}
1531015324

15325+
#[test]
15326+
fn verify_synthesized_model_accepts_profile_dump_secret_leak_prompt_examples() {
15327+
let formulas = parse_formula_strings(&[
15328+
"always([+PROFILE_DUMP_SECRET_LEAKED] true -> (<+PURGE_PROFILE_DUMPS> true | <+REVOKE_PROFILE_EXPOSED_CREDENTIALS> true))"
15329+
.to_string(),
15330+
"always([+PURGE_PROFILE_DUMPS] true -> eventually(<+NOTIFY_PROFILING_OWNER> true))"
15331+
.to_string(),
15332+
]);
15333+
let model = modality_lang::formula_synthesis::synthesize_from_formulas(
15334+
"ProfileDumpSecretLeak",
15335+
&formulas,
15336+
);
15337+
15338+
verify_synthesized_model(&model, &formulas).unwrap();
15339+
}
15340+
1531115341
#[test]
1531215342
fn verify_synthesized_model_accepts_mixed_alternatives_with_signer_requirement() {
1531315343
let formulas = parse_formula_strings(&[

0 commit comments

Comments
 (0)