Ghost Code for Rust

.github/workflows/tests.yml

@@ -28,7 +28,7 @@ jobs:
           keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core, key.core.rifl,
           key.core.testgen, keyext.isabelletranslation,  keyext.ui.testgen,  key.ncore.calculus,
           key.util, key.core.example, keyext.caching,
-          keyext.proofmanagement, key.removegenerics ]
+          keyext.proofmanagement, key.removegenerics, keyext.rusty ]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
     env:

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "keyext.rusty/rust-wrapper/rust"]
 	path = keyext.rusty/rust-wrapper/rust
 	url = git@github.com:rust-lang/rust.git
-[submodule "rust-wrapper"]
-	path = rust-wrapper
-	url = https://github.com/Drodt/KeY-rustc-wrapper.git
+[submodule "rml"]
+	path = rml
+	url = https://github.com/yseulp/rml.git

keyext.rusty/example/target/.rustc_info.json

@@ -0,0 +1 @@
+{"rustc_fingerprint":6139828803497917698,"outputs":{"17747080675513052775":{"success":true,"status":"","code":0,"stdout":"rustc 1.88.0 (6b00bc388 2025-06-23)\nbinary: rustc\ncommit-hash: 6b00bc3880198600130e1cf62b8f8a93494488cc\ncommit-date: 2025-06-23\nhost: x86_64-unknown-linux-gnu\nrelease: 1.88.0\nLLVM version: 20.1.5\n","stderr":""},"11857020428658561806":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/yseulp/.rustup/toolchains/stable-x86_64-unknown-linux-gnu\noff\npacked\nunpacked\n___\ndebug_assertions\npanic=\"unwind\"\nproc_macro\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_vendor=\"unknown\"\nunix\n","stderr":""},"7971740275564407648":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/yseulp/.rustup/toolchains/stable-x86_64-unknown-linux-gnu\noff\npacked\nunpacked\n___\ndebug_assertions\npanic=\"unwind\"\nproc_macro\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_vendor=\"unknown\"\nunix\n","stderr":""}},"successes":{}}

keyext.rusty/example/target/CACHEDIR.TAG

@@ -0,0 +1,3 @@
+Signature: 8a477f597d28d172789f06886806bc55
+# This file is a cache directory tag created by cargo.
+# For information about cache directory tags see https://bford.info/cachedir/

keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/invoked.timestamp

@@ -0,0 +1 @@
+This file has an mtime of when this was started.

keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example

@@ -0,0 +1 @@
+94ed5a9cb32ba0b1

keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example.json

@@ -0,0 +1 @@
+{"rustc":11410426090777951712,"features":"[]","declared_features":"[]","target":18343425508367059059,"profile":17672942494452627365,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/example-14b6227221523c01/dep-lib-example","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0}

keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/invoked.timestamp

@@ -0,0 +1 @@
+This file has an mtime of when this was started.

keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example

@@ -0,0 +1 @@
+d855d1ce1ee45f13

keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example.json

@@ -0,0 +1 @@
+{"rustc":11410426090777951712,"features":"[]","declared_features":"[]","target":18343425508367059059,"profile":3316208278650011218,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/example-b6d004a4079f250b/dep-test-lib-example","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0}

keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d

@@ -0,0 +1,5 @@
+/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d: src/lib.rs
+
+/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/libexample-14b6227221523c01.rmeta: src/lib.rs
+
+src/lib.rs:

keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d

@@ -0,0 +1,5 @@
+/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d: src/lib.rs
+
+/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/libexample-b6d004a4079f250b.rmeta: src/lib.rs
+
+src/lib.rs:

keyext.rusty/src/main/antlr/RustySchemaLexer.g4

@@ -27,4 +27,8 @@ PANIC
 
  FN_FRAME: 'fn_frame!';
 
+ GHOST: 'ghost!';
+
+ SNAPSHOT: 'snapshot!';
+
  PANIC_FRAME: 'panic_frame!';

keyext.rusty/src/main/antlr/RustySchemaParser.g4

@@ -48,6 +48,8 @@ expr
    | closureExpr # ClosureExpression_
    | exprWithBlock # ExpressionWithBlock_
    | PANIC LPAREN RPAREN # EmptyPanic
+   | GHOST blockExpr # GhostBlockExpression
+   | SNAPSHOT LPAREN schemaVariable RPAREN # SnapshotExpression
    ;
 
 stmt

keyext.rusty/src/main/java/org/key_project/rusty/RustInfo.java

@@ -79,6 +79,10 @@ public KeYRustyType getKeYRustyType(Type type) {
             var krt = new KeYRustyType(f);
             type2KRTCache.put(type, krt);
             return krt;
+        } else if (type instanceof GhostType g) {
+            var krt = new KeYRustyType(g, g.getSort(services));
+            type2KRTCache.put(type, krt);
+            return krt;
         } else {
             throw new IllegalArgumentException("Unsupported type: " + type);
         }

keyext.rusty/src/main/java/org/key_project/rusty/ast/ConstDef.java

@@ -0,0 +1,33 @@
+/* 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.ast;
+
+import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.op.Function;
+import org.key_project.rusty.ast.expr.Expr;
+import org.key_project.rusty.ast.ty.RustType;
+import org.key_project.rusty.ast.visitor.Visitor;
+
+import org.jspecify.annotations.NonNull;
+
+public record ConstDef(String name, RustType rustType, Expr expr, Function fn) implements Item {
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnConstDef(this);
+    }
+
+    @Override
+    public @NonNull SyntaxElement getChild(int n) {
+        if (n == 0)
+            return rustType;
+        if (n == 1)
+            return expr;
+        throw new IndexOutOfBoundsException();
+    }
+
+    @Override
+    public int getChildCount() {
+        return 2;
+    }
+}

keyext.rusty/src/main/java/org/key_project/rusty/ast/EnumDef.java

@@ -0,0 +1,26 @@
+/* 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.ast;
+
+import org.key_project.logic.SyntaxElement;
+import org.key_project.rusty.ast.visitor.Visitor;
+
+import org.jspecify.annotations.NonNull;
+
+public record EnumDef() implements Item {
+    @Override
+    public void visit(Visitor v) {
+        v.performActionOnEnumDef(this);
+    }
+
+    @Override
+    public @NonNull SyntaxElement getChild(int n) {
+        throw new IndexOutOfBoundsException("No children");
+    }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+}

keyext.rusty/src/main/java/org/key_project/rusty/ast/HirConverter.java

@@ -25,6 +25,7 @@
 import org.key_project.rusty.ast.stmt.LetStatement;
 import org.key_project.rusty.ast.stmt.Statement;
 import org.key_project.rusty.ast.ty.*;
+import org.key_project.rusty.logic.op.IProgramVariable;
 import org.key_project.rusty.logic.op.ParametricFunctionDecl;
 import org.key_project.rusty.logic.op.ProgramFunction;
 import org.key_project.rusty.logic.op.ProgramVariable;
@@ -48,8 +49,6 @@
 import org.key_project.rusty.speclang.FnSpecConverter;
 import org.key_project.rusty.speclang.LoopSpecConverter;
 import org.key_project.rusty.speclang.spec.FnSpec;
-import org.key_project.rusty.speclang.spec.LoopSpec;
-import org.key_project.rusty.speclang.spec.SpecMap;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -59,30 +58,15 @@
 public class HirConverter {
     private final Services services;
 
-    private final @Nullable Map<DefId, FnSpec> fnSpecs;
-    private final @Nullable Map<HirId, LoopSpec> loopSpecs;
     private final Map<DefId, Adt> adts = new HashMap<>();
     private final FnSpecConverter fnSpecConverter;
     private final LoopSpecConverter loopSpecConverter;
     private @Nullable GenericParam[] currentParams = null;
 
-    public HirConverter(Services services, @Nullable SpecMap specs) {
+    public HirConverter(Services services) {
         this.services = services;
         fnSpecConverter = new FnSpecConverter(services);
         loopSpecConverter = new LoopSpecConverter(services);
-        if (specs != null) {
-            fnSpecs = new HashMap<>(specs.fnSpecs().length);
-            loopSpecs = new HashMap<>(specs.loopSpecs().length);
-            for (var e : specs.fnSpecs()) {
-                fnSpecs.put(e.id(), e.value());
-            }
-            for (var e : specs.loopSpecs()) {
-                loopSpecs.put(e.id(), e.value());
-            }
-        } else {
-            fnSpecs = null;
-            loopSpecs = null;
-        }
     }
 
     public Services getServices() {
@@ -132,8 +116,8 @@ public Crate convertCrate(org.key_project.rusty.parser.hir.Crate crate) {
         Crate crate1 = new Crate(convertMod(crate.topMod()));
         for (var fn : fnsToComplete.keySet()) {
             currentFn = fn;
-            var spec = fn2Spec.get(fn);
             var hirFn = fnsToComplete.get(fn);
+            var specCases = hirFn.specCases();
             convertGenerics(hirFn.tyGenerics());
             if (hirFn.generics() != null) {
                 org.key_project.rusty.parser.hir.GenericParam[] params = hirFn.generics().params();
@@ -165,11 +149,10 @@ public Crate convertCrate(org.key_project.rusty.parser.hir.Crate crate) {
             fn.setParams(new ImmutableArray<>(params));
             fn.setBody((BlockExpression) convertExpr(hirFn.body().value()));
             services.getRustInfo().registerFunction(fn);
-            if (spec != null) {
+            if (specCases.length > 0) {
                 var contracts =
-                    fnSpecConverter.convert(spec,
-                        Objects.requireNonNull(services.getRustInfo().getFunction(fn),
-                            "Could not get function for " + fn));
+                    fnSpecConverter.convert(specCases,
+                        Objects.requireNonNull(services.getRustInfo().getFunction(fn)));
                 for (var contract : contracts) {
                     services.getSpecificationRepository().addContract(contract);
                 }
@@ -199,19 +182,35 @@ private Mod convertMod(org.key_project.rusty.parser.hir.Mod mod) {
                                                                        // above
             case org.key_project.rusty.parser.hir.item.Struct s -> null; // Handled by ADT
                                                                          // conversion above
+            case org.key_project.rusty.parser.hir.item.Const c -> convertConstDef(c);
             default -> throw new IllegalArgumentException("Unknown item: " + item);
         };
     }
 
+    private Item convertConstDef(org.key_project.rusty.parser.hir.item.Const c) {
+        var rustTy = convertHirTy(c.ty());
+        assert c.body().params().length == 0;
+        org.key_project.rusty.parser.hir.expr.Expr value = c.body().value();
+        var expr = convertExpr(value);
+        // TODO: Get type in second step
+        var ty = convertTy(rawTypes.get(value.hirId()));
+        String name = c.ident().name();
+        var fn = new RFunction(new Name(name), ty.getSort(services));
+        return new ConstDef(name, rustTy, expr, fn);
+    }
+
     private Item convertUse(org.key_project.rusty.parser.hir.item.Use use) {
         var path = convertPath(use.path(), rs -> {
             var lst = Arrays.stream(rs).map(this::convertRes).toList();
             return new ImmutableArray<>(lst);
         });
         var kind = switch (use.useKind()) {
-            case org.key_project.rusty.parser.hir.item.Use.UseKind.Single -> Use.UseKind.Single;
-            case org.key_project.rusty.parser.hir.item.Use.UseKind.Glob -> Use.UseKind.Glob;
-            case org.key_project.rusty.parser.hir.item.Use.UseKind.ListStem -> Use.UseKind.ListStem;
+            case org.key_project.rusty.parser.hir.item.Use.UseKind.Single ignored ->
+                Use.UseKind.Single;
+            case org.key_project.rusty.parser.hir.item.Use.UseKind.Glob ignored -> Use.UseKind.Glob;
+            case org.key_project.rusty.parser.hir.item.Use.UseKind.ListStem ignored ->
+                Use.UseKind.ListStem;
+            default -> throw new IllegalArgumentException("Unknown use kind: " + use);
         };
         return new Use(path, kind);
     }
@@ -223,11 +222,6 @@ private Function convertFn(Fn fn, LocalDefId id) {
         @SuppressWarnings("argument.type.incompatible")
         Function function = new Function(name, Function.ImplicitSelfKind.None,
             null, retTy, null);
-        if (fnSpecs != null) {
-            var spec = fnSpecs.get(new DefId(id.localDefIndex(), 0));
-            if (spec != null)
-                fn2Spec.put(function, Objects.requireNonNull(spec, name.toString()));
-        }
         localFns.put(id, function);
         fnsToComplete.put(function, fn);
         return function;
@@ -281,10 +275,18 @@ private Expr convertExpr(org.key_project.rusty.parser.hir.expr.Expr expr) {
             case ExprKind.Struct e -> convertStructExpr(e);
             case ExprKind.Repeat e -> convertRepeat(e, ty);
             // case ExprKind.Yield e -> convertYieldExpr(e);
+            case ExprKind.GhostBlockExpr e -> convertGhostBlockExpr(e);
+            case ExprKind.Snapshot e -> convertSnapshotExpr(e);
             default -> throw new IllegalArgumentException("Unknown expression: " + expr);
         };
     }
 
+    private SnapshotExpression convertSnapshotExpr(ExprKind.Snapshot e) {
+        var body = e.expr();
+        IProgramVariable pv = (IProgramVariable) convertExpr(body);
+        return new SnapshotExpression(pv);
+    }
+
     private ConstBlockExpression convertConstBlockExpr(ExprKind.ConstBlock e) {
         var body = (BlockExpression) convertExpr(e.block().body().value());
         return new ConstBlockExpression(body);
@@ -409,6 +411,12 @@ private BlockExpression convertBlockExpr(ExprKind.BlockExpr expr) {
         return new BlockExpression(ImmutableList.fromList(stmts), value);
     }
 
+    private GhostBlockExpression convertGhostBlockExpr(ExprKind.GhostBlockExpr expr) {
+        var stmts = Arrays.stream(expr.block().stmts()).map(this::convertStmt).toList();
+        var value = expr.block().expr() == null ? null : convertExpr(expr.block().expr());
+        return new GhostBlockExpression(ImmutableList.fromList(stmts), value);
+    }
+
     private LiteralExpression convertLitExpr(Lit expr, Type type) {
         return switch (expr.node()) {
             case LitKind.Bool(var v) -> new BooleanLiteralExpression(v);
@@ -453,9 +461,8 @@ private LoopExpression convertLoopExpr(ExprKind.Loop l, HirId id, Type type) {
         var body = convertBlockExpr(new ExprKind.BlockExpr(l.block()));
         var le = new InfiniteLoopExpression(null, body);
 
-        if (loopSpecs != null && loopSpecs.containsKey(id)) {
-            var ls = loopSpecConverter.convert(loopSpecs.get(id),
-                Objects.requireNonNull(currentFn, "Missing local fn"),
+        if (l.spec() != null) {
+            var ls = loopSpecConverter.convert(l.spec(), Objects.requireNonNull(currentFn),
                 le, pvs);
             services.getSpecificationRepository().addLoopSpec(ls);
         }
@@ -882,6 +889,9 @@ private Adt getAdt(AdtDef def) {
         Adt adt = switch (def.kind()) {
             case Struct -> {
                 assert def.variants().size() == 1;
+                if (def.pathStr().equals("rml_contracts::Ghost")) {
+                    yield new GenericGhostType(generics, services);
+                }
                 if (generics.isEmpty()) {
                     var fields = convertFields(def.pathStr(), def.variants().get(0).fields());
                     yield new Struct(name, fields, null, null);
@@ -990,6 +1000,7 @@ private Type convertAdtTy(AdtDef def, GenericTyArgKind[] args) {
             case Enum e -> e;
             case GenericStruct g -> g.instantiate(convertGenericArgs(args), services);
             case Struct s -> s;
+            case GenericGhostType g -> g.instantiate(convertGenericArgs(args), services);
             default -> throw new IllegalArgumentException("Unknown adt: " + adt);
         };
 

keyext.rusty/src/main/java/org/key_project/rusty/ast/HirRustyReader.java

@@ -91,8 +91,8 @@ public RustyBlock readBlock(String block, Context context) {
 
                 var wrapperOutput = getWrapperOutput(tmpDir);
                 var beforeConversion = System.nanoTime();
-                var converter = new HirConverter(services, null);
-                var converted = converter.convertCrate(wrapperOutput.crate());
+                var converter = new HirConverter(services);
+                var converted = converter.convertCrate(wrapperOutput);
                 LOGGER.debug("HIR conversion took {}",
                     PerfScope.formatTime(System.nanoTime() - beforeConversion));
                 BlockExpression body = converted.getVerificationTarget().body();
@@ -144,19 +144,19 @@ public RustyBlock readBlock(String block, Context context) {
         }
     }
 
-    public static Crate.WrapperOutput getWrapperOutput(Path path) throws IOException {
+    public static Crate getWrapperOutput(Path path) throws IOException {
         return getWrapperOutput(path, false);
     }
 
-    public static Crate.WrapperOutput getWrapperOutput(Path path, boolean clean)
+    public static Crate getWrapperOutput(Path path, boolean clean)
             throws IOException {
         var startTime = System.nanoTime();
         long rustCEnd;
         try {
             Process cleanCmd =
                 Runtime.getRuntime().exec(new String[] { "cargo", "clean" }, null, path.toFile());
             cleanCmd.waitFor();
-            var command = new String[] { "cargo", "key", "-o", "hir.json" };
+            var command = new String[] { "cargo", "rml", "-o", "hir.json" };
             Process cmd = Runtime.getRuntime().exec(command, null, path.toFile());
             var stdErr = cmd.getErrorStream();
             var errReader = new BufferedReader(new InputStreamReader(stdErr));
@@ -176,7 +176,7 @@ public static Crate.WrapperOutput getWrapperOutput(Path path, boolean clean)
             LOGGER.debug("rustc took {}", PerfScope.formatTime(rustCEnd - startTime));
         }
         var hir = Files.readString(path.resolve("hir.json"), Charset.defaultCharset());
-        Crate.WrapperOutput output = Crate.parseJSON(hir);
+        Crate output = Crate.parseJSON(hir);
         LOGGER.debug("JSON parsing took {}", PerfScope.formatTime(System.nanoTime() - rustCEnd));
         return output;
     }