fix: wary substitution + concrete subst parsing + de Bruijn shadowing

keyext.rusty/src/main/java/org/key_project/rusty/logic/WaryClashFreeSubst.java

@@ -0,0 +1,75 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.rusty.logic;
+
+import org.key_project.logic.Term;
+import org.key_project.logic.op.Operator;
+import org.key_project.logic.op.QuantifiableVariable;
+import org.key_project.rusty.logic.op.LogicVariable;
+import org.key_project.rusty.logic.op.RModality;
+import org.key_project.rusty.logic.op.TermTransformer;
+import org.key_project.rusty.logic.op.UpdateApplication;
+import org.key_project.util.collection.ImmutableArray;
+
+/// De Bruijn substitution that does **not** push the replacement into "state-dependent" positions
+/// — the post-formula of a modality, the target of an update application, or an operand of a
+/// transformer. Occurrences in such positions are kept (and [#wasBlocked] is set), so the caller
+/// can wrap the result in a residual substitution; occurrences elsewhere are substituted normally.
+///
+/// Used by [org.key_project.rusty.logic.op.WarySubstOp] for non-rigid replacements. The
+/// replacement is assumed ground (no free logic variables, e.g. a program variable), so no de
+/// Bruijn shifting of the replacement is needed.
+public class WaryClashFreeSubst {
+    private final Term s;
+    private final TermBuilder tb;
+    private boolean blocked = false;
+
+    public WaryClashFreeSubst(Term s, TermBuilder tb) {
+        this.s = s;
+        this.tb = tb;
+    }
+
+    /// Whether at least one occurrence was left unsubstituted because it sat below a protected
+    /// operator.
+    public boolean wasBlocked() {
+        return blocked;
+    }
+
+    public Term apply(Term body) {
+        return apply1(body, 1, false);
+    }
+
+    private Term apply1(Term t, int index, boolean below) {
+        if (t.op() instanceof LogicVariable lv && lv.getIndex() == index) {
+            if (below) {
+                // keep the variable below a modality/update/transformer; the caller re-wraps the
+                // substitution as a residual
+                blocked = true;
+                return t;
+            }
+            return s;
+        }
+        final int arity = t.arity();
+        final Term[] newSubterms = new Term[arity];
+        for (int i = 0; i < arity; i++) {
+            int subIndex = index;
+            if (t.op().bindVarsAt(i)) {
+                subIndex += t.varsBoundHere(i).size();
+            }
+            newSubterms[i] = apply1(t.sub(i), subIndex, below || isProtected(t.op()));
+        }
+        return tb.tf().createTerm(t.op(), newSubterms,
+            (ImmutableArray<QuantifiableVariable>) t.boundVars());
+    }
+
+    /// Whether the subterms of an `op`-rooted term are state dependent: a modality, an update
+    /// application, or a transformer. This is conservative for updates — the replacement is not
+    /// pushed into an update application at all (neither into the update nor behind it); the
+    /// update-simplification taclets take care of propagating into the update where sound.
+    static boolean isProtected(Operator op) {
+        return op instanceof RModality
+                || op == UpdateApplication.UPDATE_APPLICATION
+                || op instanceof TermTransformer;
+    }
+}

keyext.rusty/src/main/java/org/key_project/rusty/logic/op/WarySubstOp.java

@@ -0,0 +1,50 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.rusty.logic.op;
+
+import org.key_project.logic.Name;
+import org.key_project.logic.Term;
+import org.key_project.rusty.logic.Subst;
+import org.key_project.rusty.logic.TermBuilder;
+import org.key_project.rusty.logic.WaryClashFreeSubst;
+
+/// Wary first-order substitution operator (de Bruijn). Like [SubstOp] it replaces the bound
+/// variable by the substituted term, but it does **not** push a *non-rigid* term across a modality,
+/// behind an update, or into a transformer — doing so would be unsound, because the value of a
+/// non-rigid term (e.g. a program variable) depends on the state.
+///
+/// This mirrors KeY-Java's `WarySubstOp` / `WaryClashFreeSubst`, adapted to de Bruijn indices.
+/// Capture avoidance is automatic under de Bruijn, so the only "wary" concern left is state
+/// dependence: when the substituted term is non-rigid and the variable occurs below a protected
+/// operator, the substitution is left unreduced (a residual `{\subst …}` term). The `subst_to_eq`
+/// rule can then introduce a fresh rigid Skolem constant capturing the term's current value, after
+/// which the (now rigid) substitution is pushed through soundly.
+public final class WarySubstOp extends SubstOp {
+
+    /// the wary substitution operator; the one actually used by the parser
+    public static final SubstOp SUBST = new WarySubstOp(new Name("subst"));
+
+    private WarySubstOp(Name name) {
+        super(name);
+    }
+
+    @Override
+    public Term apply(Term term, TermBuilder tb) {
+        final Term substTerm = term.sub(0);
+        final Term origTerm = term.sub(1);
+        if (substTerm.isRigid()) {
+            // a rigid term may be pushed anywhere
+            return new Subst(substTerm, tb).apply(origTerm);
+        }
+        // a non-rigid term is pushed into ordinary (state-independent) positions, e.g. the update
+        // of an update application, but NOT across a modality / behind an update / into a
+        // transformer; occurrences there are kept and wrapped in a residual substitution
+        final WaryClashFreeSubst cfs = new WaryClashFreeSubst(substTerm, tb);
+        final Term res = cfs.apply(origTerm);
+        if (cfs.wasBlocked()) {
+            return tb.subst(this, term.varsBoundHere(1).get(0), substTerm, res);
+        }
+        return res;
+    }
+}

keyext.rusty/src/main/java/org/key_project/rusty/parser/builder/ExpressionBuilder.java

@@ -741,27 +741,38 @@ public Term visitQuantifierterm(KeYRustyParser.QuantifiertermContext ctx) {
 
     @Override
     public Object visitSubstitution_term(KeYRustyParser.Substitution_termContext ctx) {
-        SubstOp op = SubstOp.SUBST;
+        SubstOp op = WarySubstOp.SUBST;
         Namespace<QuantifiableVariable> orig = variables();
         AbstractSortedOperator v = accept(ctx.bv);
         unbindVars(orig);
-        if (v instanceof LogicVariable) {
-            // bindVar((LogicVariable) v);
-            throw new RuntimeException("TODO @ DD");
+        // the substitution binds its own variable; declare it so that occurrences in the body
+        // resolve to it (de Bruijn index 1)
+        BoundVariable declared = null;
+        if (v instanceof BoundVariable bv) {
+            // a sort was given: visitOne_bound_variable already registered the bound variable
+            declared = bv;
+            bindVar();
+        } else if (v instanceof LogicVariable lv) {
+            // no sort given and the name resolved to an enclosing variable: declare the
+            // substitution's own (shadowing) bound variable of the same sort
+            declared = bindVar(ctx.bv.id.getText(), lv.sort());
+            v = declared;
         } else {
+            // schema variable (taclets)
             bindVar();
         }
 
         Term a1 = accept(ctx.replacement);
         Term a2 = oneOf(ctx.atom_prefix(), ctx.unary_formula());
         try {
-            Term result =
-                getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2);
-            return result;
+            return getServices().getTermBuilder().subst(op, (QuantifiableVariable) v, a1, a2);
         } catch (Exception e) {
             throw new BuildingException(ctx, e);
         } finally {
             unbindVars(orig);
+            if (declared != null) {
+                unbindVars(List.of(declared));
+            }
         }
     }
 
@@ -943,9 +954,11 @@ private Term toNum(String number) {
     @Override
     protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName,
             KeYRustyParser.Formal_sort_argsContext genericArgsCtxt) {
-        // Might be quantified variable
+        // Might be quantified variable. Search from the innermost binder outwards so that, when
+        // several bound variables share a name, an occurrence binds to the innermost one
+        // (de Bruijn shadowing).
         var idx = -1;
-        for (int i = 0; i < boundVars.size(); ++i) {
+        for (int i = boundVars.size() - 1; i >= 0; --i) {
             if (varfuncName.equals(boundVars.get(i).name().toString())) {
                 idx = i;
                 break;

keyext.rusty/src/main/java/org/key_project/rusty/pp/NotationInfo.java

@@ -92,7 +92,7 @@ private HashMap<Object, Notation> createDefaultNotation() {
             new Notation.ModalSVNotation(PRIORITY_MODALITY, PRIORITY_POST_MODALITY));
         tbl.put(IfThenElse.IF_THEN_ELSE, new Notation.IfThenElse(PRIORITY_ATOM, "\\if"));
         // tbl.put(IfExThenElse.IF_EX_THEN_ELSE, new Notation.IfThenElse(PRIORITY_ATOM, "\\ifEx"));
-        tbl.put(SubstOp.SUBST, new Notation.Subst());
+        tbl.put(WarySubstOp.SUBST, new Notation.Subst());
         tbl.put(UpdateApplication.UPDATE_APPLICATION, new Notation.UpdateApplicationNotation());
         tbl.put(UpdateJunctor.PARALLEL_UPDATE, new Notation.ParallelUpdateNotation());
 

keyext.rusty/src/test/java/org/key_project/rusty/parser/WarySubstAndShadowingTest.java

@@ -0,0 +1,81 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.rusty.parser;
+
+import org.key_project.logic.Name;
+import org.key_project.logic.Term;
+import org.key_project.logic.sort.Sort;
+import org.key_project.rusty.ast.expr.BlockExpression;
+import org.key_project.rusty.logic.RustyBlock;
+import org.key_project.rusty.logic.op.BoundVariable;
+import org.key_project.rusty.logic.op.LogicVariable;
+import org.key_project.rusty.logic.op.ProgramVariable;
+import org.key_project.rusty.logic.op.SubstOp;
+import org.key_project.rusty.logic.op.WarySubstOp;
+import org.key_project.rusty.util.TacletForTests;
+import org.key_project.util.collection.ImmutableSLList;
+
+import org.junit.jupiter.api.BeforeAll;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
+
+/// Parser tests for de Bruijn substitution: concrete `{\subst …}` parsing, innermost binding of
+/// shadowed quantified variables, and the wariness of the substitution operator (a non-rigid
+/// replacement is not pushed across a modality). Uses the `testrules.key` signature (sort `s`,
+/// predicate `p(s)`, constant `cnst -> s`, program variable `i: u32`).
+public class WarySubstAndShadowingTest {
+
+    @BeforeAll
+    static void setUp() {
+        TacletForTests.parse();
+    }
+
+    @Test
+    void shadowedQuantifiedVariableBindsInnermost() {
+        // the x in p(x) binds to the inner \forall (de Bruijn index 1), not the outer one
+        Term t = TacletForTests.parseTerm("\\forall s x;\\forall s x; p(x)");
+        Term body = t.sub(0).sub(0); // p(x)
+        assertEquals(1, ((LogicVariable) body.sub(0).op()).getIndex());
+    }
+
+    @Test
+    void parseConcreteSubstitution() {
+        Term t = TacletForTests.parseTerm("{\\subst s x; cnst} p(x)");
+        assertInstanceOf(SubstOp.class, t.op());
+        Term body = t.sub(1);
+        assertEquals(1, ((LogicVariable) body.sub(0).op()).getIndex());
+
+        // cnst is rigid, so it is substituted: p(cnst)
+        var tb = TacletForTests.services().getTermBuilder();
+        Term applied = WarySubstOp.SUBST.apply(t, tb);
+        Term expected = TacletForTests.parseTerm("p(cnst)");
+        assertEquals(expected, applied);
+    }
+
+    @Test
+    void nonRigidReplacementIsNotPushedAcrossModality() {
+        // {\subst u32 x; i}\<{}\>(x = i): i is a (non-rigid) program variable, so it is not pushed
+        // into the modality — the substitution is left as a residual. Built programmatically to
+        // avoid the empty-modality concrete syntax.
+        var services = TacletForTests.services();
+        var tb = services.getTermBuilder();
+        ProgramVariable i =
+            (ProgramVariable) services.getNamespaces().programVariables().lookup(new Name("i"));
+        Sort u32 = i.sort();
+
+        BoundVariable x = new BoundVariable(new Name("x"), u32);
+        Term lvX = tb.var(LogicVariable.create(1, u32));
+        Term iTerm = tb.var(i);
+        RustyBlock emptyBlock =
+            new RustyBlock(new BlockExpression(ImmutableSLList.nil(), null));
+        Term body = tb.dia(emptyBlock, tb.equals(lvX, iTerm)); // \<{}\>(x = i)
+        Term substTerm = tb.subst(WarySubstOp.SUBST, x, iTerm, body);
+
+        Term applied = WarySubstOp.SUBST.apply(substTerm, tb);
+        assertEquals(substTerm, applied,
+            "a non-rigid replacement must not be pushed across a modality");
+    }
+}