Merge remote-tracking branch 'origin/develop'

flake.nix

@@ -54,7 +54,7 @@
 
             k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-6rGuU8NFSp3lQVxxPj5WREpNVPneMqPH45DFEmLiH6I=";
+                mvnHash = "sha256-HkAwMZq2vvrnEgT1Ksoxb5YnQ8+CMQdB2Sd/nR0OttU=";
                 manualMvnArtifacts = [
                   "org.scala-lang:scala-compiler:2.13.13"
                   "ant-contrib:ant-contrib:1.0b3"

k-frontend/pom.xml

@@ -24,11 +24,6 @@
       <artifactId>org.eclipse.lsp4j</artifactId>
       <version>0.19.0</version>
     </dependency>
-    <dependency>
-      <groupId>org.bouncycastle</groupId>
-      <artifactId>bcprov-jdk15on</artifactId>
-      <version>1.69</version>
-    </dependency>
     <dependency>
       <groupId>com.google.inject</groupId>
       <artifactId>guice</artifactId>

k-frontend/src/main/java/org/kframework/compile/NumberSentences.java

@@ -1,13 +1,15 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 package org.kframework.compile;
 
+import java.security.MessageDigest;
+import java.security.NoSuchAlgorithmException;
 import java.util.Arrays;
+import java.util.HexFormat;
 import java.util.List;
-import org.bouncycastle.jcajce.provider.digest.SHA3;
-import org.bouncycastle.util.encoders.Hex;
 import org.kframework.attributes.Att;
 import org.kframework.definition.RuleOrClaim;
 import org.kframework.definition.Sentence;
+import org.kframework.utils.errorsystem.KEMException;
 
 public class NumberSentences {
 
@@ -31,17 +33,23 @@ public static Sentence number(Sentence s) {
         preservedAtts.stream()
             .filter(att -> s.att().contains(att))
             .map(att -> Att.empty().add(att, s.att().get(att)))
-            .reduce(Att.empty(), (acc, elem) -> acc.addAll(elem));
+            .reduce(Att.empty(), Att::addAll);
 
     String id = ruleHash(s.withAtt(a));
     return s.withAtt(s.att().add(Att.UNIQUE_ID(), id));
   }
 
   private static String ruleHash(Sentence s) {
-    String text = new NormalizeVariables().normalize(s).toString();
-    SHA3.Digest256 sha3engine = new SHA3.Digest256();
-    byte[] digest = sha3engine.digest(text.getBytes());
-    String digestString = Hex.toHexString(digest);
-    return digestString;
+    try {
+      String text = new NormalizeVariables().normalize(s).toString();
+      byte[] digest = MessageDigest.getInstance("SHA3-256").digest(text.getBytes());
+      return HexFormat.of().formatHex(digest);
+    } catch (NoSuchAlgorithmException e) {
+      // This exception should never actually be thrown in practice; it's just a limitation of the
+      // Java cryptography APIs that we need to request algorithms by constant string keys and cope
+      // with them potentially not existing. SHA3-256 is part of the Java standard library from JDK
+      // 17 onwards.
+      throw KEMException.criticalError("Error computing rule digest (SHA3-256 unavailable)", e);
+    }
   }
 }