Cleaning flags by yannilefki · Pull Request #49 · charguer/optitrust

yannilefki · 2026-07-23T13:41:12Z

Added new flag policy, and cleaned code along the way.
I did my best to correct any bug I created, but this cleaning is far from bugproof, so I believe it is important to clean incrementally (that is : comment during the first pass, a.k.a this PR, then delete when coming on the code later on, with more experience on the usage of the new flags/the meaning of the past flag policies).

Bastacyclop · 2026-07-24T07:22:29Z

+  (* Yanni : Deprecated flag *)
+  mutable step_typechecking_mode : Flags.typechecking_mode;
+  (* mutable step_flag_check_validity : bool; (* state of flag check_validity at start; must be the same at end *) *)


I assume line 323 is deprecated, not 322 ?

Bastacyclop · 2026-07-24T07:24:49Z

+type typechecking_mode =
+  | Unverified (* equivalent to `resource_typing_enabled = false && check_validity = false` *)
+  | Annotated (* equivalent to `check_validity = false` *)
+  | AnnotatedAndVerified (* equivalent to `check_validity := true && preserve_specs_only = false` *)


I'd suggest describing their semantics independently from the previous flags so that the description stands on its own. Especially since the semantics of the previous flags was unclear, and we will delete them.

For example, Unverified should be closer to resource_typing_enabled = false && check_validity = true in my opinion, in the sense that while the code is not verified and has no annotations, we are in this mode responsible for applying semantics-preserving transformations (not relative to the spec, but relative to the code itself).

Alternative naming option going through my head:

Unverified --> SemanticsPreserving, we do not have specifications and proofs, so no annotations, therefore the code stands as its own specification and we must ensure that we preserve its semantics

AnnotatedAndVerified --> ProofPreserving, we have specifications and proofs in the form of annotations and we are responsible for preserving them so that typechecking can still verify the code against them

Annotated --> ProofRepairing, we have specifications and proofs in the form of annotations and we are in the process of repairing the proof, so typechecking might not be able to verify the code right now, but we promise to go back to ProofPreserving at some point.

The first name matches the standard notion of semantics-preserving transformations.
The second names matches the OptiTrust notion of proof-preserving transformations (not a new notion but had different names in prior work).
The third name matches the standard notion of proof repair where the tool is being guided towards from a broken proof to a fixed proof.

Bastacyclop · 2026-07-24T07:31:23Z

+(* TODO : depreciate transformation *)
 (** [clear_nosimpl tg]: clears all the marks on all the instructions that where
    skipped by the simplifier *)
 let%transfo clear_nosimpl (tg : target) : unit =
  Marks.remove Arith_core.mark_nosimpl [nbMulti; cMark Arith_core.mark_nosimpl]

+(* TODO : depreciate transformation *)
 (** [nosimplf tg]: mark all the instructions targeted by [tg] as "__arith_core_nosimpl" *)
 let%transfo nosimpl (tg : target) : unit =
  Marks.add Arith_core.mark_nosimpl tg


these look like they should still work in all modes, they're just putting marks, so deprecation might not be needed.

Bastacyclop · 2026-07-24T07:37:23Z

+(* TODO : depreciate transformation *)
 let%transfo insert_barrier (tg: target) =
  Sequence_basic.insert ~reparse:false (magic_barrier ()) tg


I wouldn't deprecate this one.

Bastacyclop · 2026-07-24T07:39:51Z

 let%transfo convert_tail_thread_for (loops : int list) (leaf: target) =
  let fission_helper tg =
-    Flags.with_flag Flags.check_validity true (fun () -> Loop.fission tg) in
+    Flags.with_flag (* Flags.check_validity true *) Flags.typechecking_mode Flags.AnnotatedAndVerified (fun () -> Loop.fission tg) in


There's an interested question here : if we set the flag to verified, do we expect the code to be verifiable in the sense that typechecking should succeed, or do we expect the code to be verified in the sense that typechecking did run successfully and that the type information fields are up to date ?

Bastacyclop · 2026-07-24T07:42:45Z

      trm_fail cond "condition is not pure, more advanced checks not yet supported"
-  end;
+  end; *)
  Target.reparse_after ~reparse (Target.apply_at_target_paths (insert_on cond mark mark_then mark_else else_branch)) tg


note that reparse_after should also be deprecated : it is used when the user might insert arbitrary plain text code that requires reparsing into a proper AST ; ideally we don't need this anymore or find a way to do this locally without reparsing the entire program.

Bastacyclop · 2026-07-24T07:46:22Z

    let loop_mark = next_mark () in
    Loop_basic.move_out ~loop_mark [cPath seq_path; Constr_depth (DepthAt 0); tSpan [tFirst] [cMarkSpanStop mark_moved]];
-    if !Flags.check_validity then Resources.loop_minimize [cMark loop_mark];
+    if (* !Flags.check_validity *) Flags.annotated () then Resources.loop_minimize [cMark loop_mark];


I'm not sure loop minimization makes any sense if the types are not up to date, I remember it to be driven by the typing fields that need to be up-to-date. Some of these might need strengthening to "verified".

Bastacyclop · 2026-07-24T07:51:30Z

  into:

-    // stars_j R(j) * V
+    // stars_j


Bastacyclop · 2026-07-24T07:59:02Z

 open Prelude

-let _ = Flags.check_validity := true
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified


Note that the specifications in this test don't mention values. When setting annotated and verified, specifications should probably mention values, otherwise the program is under-specified and many transformations will succeed while they probably shouldn't.

alternative: accept weakening the test to the weaker specification

Bastacyclop · 2026-07-24T07:59:56Z

-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.use_resources_with_models := true


I believe this flag should also be deprecated.

Bastacyclop · 2026-07-24T08:01:21Z


-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified


this test was probably not designed for full functional verification.

Bastacyclop · 2026-07-24T08:02:52Z

@@ -1,7 +1,8 @@
+(* Deprecated *)


this one should work ?

Bastacyclop · 2026-07-24T08:09:14Z

@@ -1,7 +1,8 @@
+(* Deprecated *)


I think this test should work with validity checks but without using resource annotations ?

this is also used in the unverified cleanup transformation

Bastacyclop · 2026-07-24T08:14:44Z

Since we have a _models variant, we probably want to promote loop_reorder_at_models.ml into loop_reorder_at.ml. Then either we override this file, effectively removing one test, or we demote this file into something like loop_reorder_at_novalues.ml : we can still typecheck the transformation but against under-specified semantics where changing the computed values is not considered wrong (this can still be useful if you only want to check the absence of race conditions in Rust-style for example, some people actually asked me about that usage scenario at events).

Bastacyclop · 2026-07-24T08:20:08Z

@@ -1,8 +1,9 @@
+(* Deprecated *)


we use this in the unverified cleanup, so should probably be re-enabled before merging.

Bastacyclop · 2026-07-24T08:22:14Z

@@ -1,7 +1,8 @@
+(* Deprecated *)


used in unverified cleanup

Bastacyclop · 2026-07-24T08:31:50Z


-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
 let _ = Flags.use_resources_with_models := true


this flag should not be set anymore ?

Bastacyclop · 2026-07-24T08:32:42Z

 let _ = Flags.use_resources_with_models := true
-let _ = Flags.preserve_specs_only := true
+(* let _ = Flags.preserve_specs_only := true *)
+let _ = Flags.typechecking_mode := Flags.Annotated


AndVerified ?

Bastacyclop · 2026-07-24T08:34:03Z

  !! Ghost.flatten_expr_rewrites (sum_tg @ [dRHS]);
  !! replace_with_tree_reduce (trm_int log_tpb) sum_tg;
-  !! Flags.with_flag Flags.check_validity false (fun () -> Function.inline_def [cFunDef "tree_reduce"]);
+  !! Flags.with_flag (* Flags.check_validity false *) Flags.typechecking_mode Flags.Unverified (fun () -> Function.inline_def [cFunDef "tree_reduce"]);


should this not still be Annotated mode ?

Bastacyclop · 2026-07-24T08:37:12Z

+(* Yanni : might change this flag to [Flags.Annotated] instead *)
 (** [without_substep_validity_checks f] executes [f] with
    the flag [check_validity] temporarily set to false.
    Only for internal use; user scripts should use the [trustme] function. *)
 let without_substep_validity_checks (f: unit -> 'a): 'a =
-  Flags.with_flag Flags.check_validity false f
+  Flags.with_flag (* Flags.check_validity false *) Flags.typechecking_mode Flags.Unverified f


I'd suggest renaming this function and checking all call sites for the intended semantics (multiple call sites may disagree on what they want).

Bastacyclop · 2026-07-24T08:39:24Z

  (* Check that [Flags.check_validity] is like at the start of the step *)
-  if not on_error && (!Flags.check_validity && (not !Flags.use_resources_with_models)) <> infos.step_flag_check_validity
+  if not on_error && (!Flags.typechecking_mode <> infos.step_typechecking_mode) (* (!Flags.check_validity && (not !Flags.use_resources_with_models)) <> infos.step_flag_check_validity *)
    then raise (TraceFailure "At finalize_step, Flags.check_validity is not same as when step was opened.");


need to update the failure message

how does that work with transformations like unverified cleanup that transition from one mode to another ?

Bastacyclop · 2026-07-24T08:40:35Z

 let resource_error_expected (f: unit -> unit): unit =
  failure_expected (function
  | Resource_computation.ResourceError _ -> true
  | _ -> false) (fun () -> f (); recompute_resources ())


I think we have Resources.ensure_computed () which is potentially cheaper (avoid duplicated triggers).

Bastacyclop · 2026-07-24T08:41:32Z

 let dump_ast_details : bool ref = ref false

-(* TODO : deprecate once optilambda surface display works *)
+(* TODO Yanni : deprecate once optilambda surface display works *)


we can deprecate right now and incrementally improve the optilambda display to fit our needs

Bastacyclop · 2026-07-24T09:08:50Z

 let justif_correct (why : string) : unit =
-  if !Flags.check_validity then begin
-    ensure_computed ();
-    Trace.justif (sprintf "resources are correct: %s" why)
-  end
+  (* if !Flags.check_validity then begin *)
+  if Flags.annotated () then ensure_computed ();
+  Trace.justif (sprintf "resources are correct: %s" why)


I'd say this is only useful in Unverified/SemanticsPreserving mode, where there is no self-certifying proof. Calling it in another mode should trigger a warning.

Bastacyclop · 2026-07-24T09:15:48Z

+    let (unfolds, folds) = if (* !Flags.check_validity *) Flags.annotated () then begin
      let (res_start, res_stop) = Resources.around_instrs span_instrs in


Ideally, reading any kind of computed resource information should not be allowed if they are not up-to-date. This means that this code should fail if not in AnnotatedAndVerified/ProofPreserving.

Bastacyclop

Looks like nice progress. Some thoughts:

We have too many deprecated tests, we should take the time to add models mentioning values for a bunch of them, we may also alternatively try running the verified mode on weaker models that don't constrain values : it is a weaker test than semantic preservation but still better than nothing.
We have many deprecated transformations, but a lot of them would probably be worth updating to the new modes. We should make it clear that this wave of deprecation does not mean "you shouldn't use this transformation anymore", but rather "you should reimplement this transformation before using it, or truly deprecate it if you have a better API".
In terms of short-term priority to counter-act all of this deprecation, I think we need to enforce the following before merging and going forward: every non-deprecated transformation should have a working non-deprecated unit test (including a trivial _doc test), ideally proof-preserving models mentioning values, possibly proof-preserving weaker models not mentioning values, possibly semantics-preserving without annotations/proof.

yannilefki added 9 commits July 20, 2026 15:23

[WIP] cleaning flags

2209c46

deprecating non-model tests

cdc15ac

more cleaning

d725fd3

done cleaning "check_validity" . [WIP] Deprecating non-model flags

971246f

wip cleaning flags

06f0f65

solved one unit test

ec6c3db

corrected weird comments coloring

21c43f7

corrected loop reorder_at_models test.

39e0016

moving deprecated tests to ignored.tests

63f8dad

Bastacyclop reviewed Jul 24, 2026

View reviewed changes

Comment thread lib/transfo/loop_swap.ml

into:

// stars_j R(j) * V

// stars_j

Bastacyclop Jul 24, 2026

Copy link
Copy Markdown

Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

?

Bastacyclop reviewed Jul 24, 2026

View reviewed changes

Merge branch 'main' into cleaning_flags

d2cbc9b

		let (unfolds, folds) = if (* !Flags.check_validity *) Flags.annotated () then begin
		let (res_start, res_stop) = Resources.around_instrs span_instrs in

Conversation

yannilefki commented Jul 23, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Bastacyclop Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Bastacyclop Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Bastacyclop left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Bastacyclop Jul 24, 2026 •

edited

Loading

Bastacyclop Jul 24, 2026 •

edited

Loading

Bastacyclop left a comment •

edited

Loading