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 ?

That is correct, I just deleted the comment in the end.

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.

I am not sure I agree with the meaning of the Unverified flag.
For me, any transformation in this mode should be allowed to do pretty much anything. Because such transformations are suppposed to be used as intermediate steps, not high level modification.
In particular, I would expect to be able to have very powerful transformations, such as code deletion, or code addition with no restruction.
Also, is there a way to verify that the semantics are preserved? Or is it in the sense that, "We guarantee, as developers of Optitrust, that this transformation is preserving"?

Then we might need 4 regimes with both Unverified (previously called "TrustMe") and SemanticsPreserving. Here are simple transformations that preserve semantics and do not require separation logic typechecking : deleting an empty sequence, deleting an empty loop whose range expression is effect-free (can be a syntactic check).

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.

You are right, I removed the comments.

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 ?

Now that we mention it, I can't really visualize an example where it is relevant to wrap a function with stricter flags (in this example, going from ProofRepairing to ProofPreserving for the fission). Especially in this case since I believe the actual fission code does not have a different behavior w.r.t the flags.

the fission code needs typechecking metadata that needs to be up-to-date, that's not possible to have during proof repair unless we define what that means

In that case does it make sense to call it in a context where the policy is "ProofRepairing", which is the case in this case study.

do we actually run this code in ProofRepairing ? maybe it should just be ProofPreserving throughout. I can't remember the details there.

Ok I checked, I probably confused it with something else, this function is always called in ProofPreserving context.

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.

I removed every occurence of reparse_after that I could, but I could not remove the one in rewrite.ml. Do you think I can remove it/could you explain to me what the function actually does?

it will print out the entire AST to text and reparse it freshly

it's fine to deal with this after this PR though, if removal is non trivial

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".

Changed this flag, and added a condition inside the loop_minimize function, with a warning in case the flag is not ProofPreserving. We'll see in the future if this needs some strengthening/relaxing.

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

  into:

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


Probably a missclick on my part. Reverted the change.

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

I simply weakened the flag to ProofRepairing. I'll slowly do it to the other tests with time

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.

Importing models on the cpp file appears to work, so I removed the deprecated comment.

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.

I noticed in at least one example (loop_reorder_at_models.ml) that it recomputation is necessary even with the ProofPreserving flag.
This is because some linear resource is not normalized, and can not be found in a context where it is (think 'n + 0' not found in a context where there is 'n').
I did not find an easy fix, so I removed the condition altogether, and keep it as future work to handle local renormalization of resources, instead of a full ast recomputation.

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.

…re expected for a global reparse to remove "trm_arbitrary" arguments. (wip : solve this issue by either implementing local parsing, or meta-programmation tools for arguments)

…dentify how to add them back)

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

Bastacyclop and others added 5 commits July 24, 2026 14:05

Merge branch 'main' into cleaning_flags

d2cbc9b

renaiming flags, and slowly answering comments

e05915b

cleaning reparsing. Resolving issues created

abee804

reverted parts of the changes of reparse : several transformations we…

adde56c

…re expected for a global reparse to remove "trm_arbitrary" arguments. (wip : solve this issue by either implementing local parsing, or meta-programmation tools for arguments)

moved unimportant tests from the workflow. (Wip : go one by one and i…

0aa5fe5

…dentify how to add them back)

		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!

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!

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

Bastacyclop Jul 24, 2026 •

edited

Loading

Bastacyclop Jul 24, 2026 •

edited

Loading