diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs
index 640d0b02db..b40650701e 100644
--- a/Source/DafnyCore/AST/Grammar/Printer.cs
+++ b/Source/DafnyCore/AST/Grammar/Printer.cs
@@ -583,7 +583,12 @@ public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition
       }
       wr.Write("{0} ", module.Name);
       if (module.Implements != null) {
-        wr.Write("refines {0} ", module.Implements.Target);
+        var kindString = module.Implements.Kind switch {
+          ImplementationKind.Refinement => "refines",
+          ImplementationKind.Replacement => "replaces",
+          _ => throw new ArgumentOutOfRangeException()
+        };
+        wr.Write($"{kindString} {module.Implements.Target} ");
       }
       if (!module.TopLevelDecls.Any()) {
         wr.WriteLine("{ }");
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
index d5ef3edcaa..289bb46308 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
index 3f73a8610c..b0c70f3574 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
index ac45478e52..45727f4816 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
index beab34ae3b..8510c9484f 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
index 27523da94c..b904a93dfe 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ
diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
index 78945df6ba..4b61fef781 100644
Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ
diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java
index 33d38947d7..81fd9e48d1 100644
--- a/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java
+++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java
@@ -7,11 +7,13 @@ public class AtomicBox<T> {
     private volatile T val;
 
     public AtomicBox(T t) {
-        val = t;
     }
 
-    public AtomicBox(dafny.TypeDescriptor td, T t) {
-        this(t);
+    public AtomicBox(dafny.TypeDescriptor td) {
+    }
+    
+    public void __ctor(T t) {
+        val = t;
     }
 
     public void Put(T t) {
diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs
index becbb8d78c..19444a5c1a 100644
--- a/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs
+++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs
@@ -10,6 +10,8 @@ public MutableMap() {
             map = new ConcurrentDictionary<K, V>();
         }
 
+        public void __ctor() { }
+
         public Dafny.ISet<K> Keys() {
             return Dafny.Set<K>.FromCollection(map.Keys);
         }
@@ -58,11 +60,14 @@ public class AtomicBox<T> {
         private T val;
         private Lock l;
 
-        public AtomicBox(T t) {
-            val = t;
+        public AtomicBox() {
             l = new Lock();
         }
 
+        public void __ctor(T t) {
+          val = t;
+        }
+
         public void Put(T t) {
             l.__Lock();
             val = t;
@@ -81,6 +86,9 @@ public class Lock {
 
         private static System.Threading.Mutex mut = new System.Threading.Mutex();
 
+        public void __ctor() {
+        }
+
         public void __Lock() {
             mut.WaitOne();
         }
diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java
index a07168500c..7b35aa7b14 100644
--- a/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java
+++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java
@@ -6,6 +6,8 @@ public class Lock {
 
     private final ReentrantLock lock = new ReentrantLock();
 
+    public void __ctor() {}
+
     public void __Lock() {
         lock.lock();
     }
diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java
index 1fc171ec63..27b718ab42 100644
--- a/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java
+++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java
@@ -19,6 +19,8 @@ public MutableMap(dafny.TypeDescriptor<K> td_K, dafny.TypeDescriptor<V> td_V) {
         this.td_V = td_V;
         map = new ConcurrentHashMap<K, V>();
     }
+    
+    public void __ctor() { }
 
     public dafny.DafnySet<K> Keys() {
         return new dafny.DafnySet<K>(Collections.list(map.keys()));
diff --git a/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js
index b327d81031..188e5e0f70 100644
--- a/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js
+++ b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js
@@ -3,9 +3,9 @@
 *  SPDX-License-Identifier: MIT
 *******************************************************************************/
 
-var Std_ConcurrentInterface = Std_ConcurrentInterface || {};
-var FileIOInternalExterns = FileIOInternalExterns || {};
-FileIOInternalExterns.__default = (function() {
+var Std_Concurrent = Std_Concurrent || {};
+var Std_FileIOInternalExterns = Std_FileIOInternalExterns || {};
+Std_FileIOInternalExterns.__default = (function() {
   const buffer = require("buffer");
   const fs = require("fs");
   const nodePath = require("path");
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy
index 0296e711b5..4370198604 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy
@@ -6,7 +6,6 @@ Std.GoConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -34,8 +33,6 @@ Std.GoConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy
index 5e7f5c6f1a..b5b2f17e75 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy
@@ -3,7 +3,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent {
   class {:extern "AtomicBox"} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy
index ca0355b00d..08d7ddbc9c 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy
@@ -4,7 +4,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -32,8 +31,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy
index 1079d09ffe..ac29b7f360 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy
@@ -3,7 +3,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy
similarity index 93%
rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy
rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy
index c7f69bd07d..332adb69ce 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy
@@ -47,6 +47,10 @@ replaceable module Std.Concurrent {
     // Invariant on values this box may hold
     ghost const inv: T -> bool
 
+    constructor (ghost inv: T -> bool, t: T)
+      requires inv(t)
+      ensures this.inv == inv
+
     method Get() returns (t: T)
       reads {}
       ensures inv(t)
@@ -68,6 +72,9 @@ replaceable module Std.Concurrent {
     // Invariant on key-value pairs this map may hold
     ghost const inv: (K, V) -> bool
 
+    constructor (ghost inv: (K, V) -> bool)
+      ensures this.inv == inv
+
     method Keys() returns (keys: set<K>)
       reads {}
       ensures forall k <- keys :: exists v :: inv(k, v)
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy
index 3b61ab9195..4843b72d50 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy
@@ -3,7 +3,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 
diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy
index 7f87ee27fe..77680d67aa 100644
--- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy
+++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy
@@ -13,7 +13,7 @@ module
   // But it makes debugging the translated output a little clearer.
   {:compile false}
 {:extern}
-{:dummyImportMember "Dummy_", true}
+{:dummyImportMember "Dummy__", true}
 Std.GoFileIOInternalExterns replaces FileIOInternalExterns {
   method
     {:extern}
diff --git a/Source/DafnyStandardLibraries/src/Std_Concurrent.py b/Source/DafnyStandardLibraries/src/Std_Concurrent.py
index 2da109f619..9983f12281 100644
--- a/Source/DafnyStandardLibraries/src/Std_Concurrent.py
+++ b/Source/DafnyStandardLibraries/src/Std_Concurrent.py
@@ -10,6 +10,9 @@
 
 
 class MutableMap:
+    def ctor__(self):
+        pass
+        
     def __init__(self) -> None:
         self.map = dict()
         self.lock = Lock()
@@ -66,8 +69,12 @@ def Size(self):
 
 
 class AtomicBox:
-    def __init__(self, t) -> None:
+    def __init__(self) -> None:
+        pass
+        
+    def ctor__(self, t):
         self.boxed = t
+        pass
 
     def Get(self):
         return self.boxed
@@ -76,6 +83,9 @@ def Put(self, t):
         self.boxed = t
 
 class Lock:
+    def ctor__(self):
+        pass
+        
     def __init__(self) -> None:
         self.lock = threading.Lock()
 
diff --git a/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go b/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go
index 7bea051e2d..4fe317dba8 100644
--- a/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go
+++ b/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go
@@ -1,4 +1,4 @@
-package DafnyStdLibs_Concurrent
+package Std_Concurrent
 
 import (
   _dafny "dafny"
@@ -56,7 +56,7 @@ func (_this *MutableMap) ParentTraits_() []*_dafny.TraitID {
 }
 var _ _dafny.TraitOffspring = &MutableMap{}
 
-func (_this *MutableMap) Ctor__(inv func (interface{}, interface{}) bool) {
+func (_this *MutableMap) Ctor__() {
   {
   }
 }
@@ -188,7 +188,7 @@ func (_this *AtomicBox) ParentTraits_() []*_dafny.TraitID {
 }
 var _ _dafny.TraitOffspring = &AtomicBox{}
 
-func (_this *AtomicBox) Ctor__(inv func (interface{}) bool, t interface{}) {
+func (_this *AtomicBox) Ctor__(t interface{}) {
   {
     _this.mu.Lock()
     _this.Boxed = t
diff --git a/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go b/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go
index a5c1e88b9e..83ec9a86b5 100644
--- a/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go
+++ b/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go
@@ -1,4 +1,4 @@
-package DafnyStdLibs_FileIOInternalExterns
+package Std_FileIOInternalExterns
 
 import (
 	_dafny "dafny"
@@ -8,7 +8,12 @@ import (
 
 type Dummy__ struct{}
 
-func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
+type CompanionStruct_Default___ struct {
+}
+var Companion_Default___ = CompanionStruct_Default___ {
+}
+
+func (_static *CompanionStruct_Default___) INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
 	p := _dafny.SequenceVerbatimString(path, false)
 	dat, err := os.ReadFile(p)
 	if err != nil {
@@ -19,7 +24,7 @@ func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead
 	return false, datAsSequence, _dafny.EmptySeq
 }
 
-func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
+func (_static *CompanionStruct_Default___) INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
 	p := _dafny.SequenceVerbatimString(path, false)
 
 	// Create directories
@@ -32,4 +37,4 @@ func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (is
 		return true, errAsSequence
 	}
 	return false, _dafny.EmptySeq
-}
+}
\ No newline at end of file