link

doc/ADR/ADR_001.md

@@ -48,7 +48,7 @@ The types we actually have to deal with boil down to primitives, arrays (Vectors
 
 Thus, _State_ is inherently JSON-like, since we already know, from the design of Apalache's ITF, how to represent maps and arrays/vectors (representing structs/enums should be straightforward as well). 
 
-In contrast, _Interface_ is simply an unordered collection of the public methods admitted by a contract, and can be thought of a simple set or array.
+In contrast, _Interface_ is simply an unordered collection of the public method names admitted by a contract (which suffices, since Rust, and consequently Soroboan, disallow overloading), and can be thought of as a simple set or array.
 
 It is important to emphasize, that we do not need to capture function behavior in any way; the Transition Extractor observes a history of transactions that have already happened, and the effects of functions are observed as changes to the state of a contract, from one block to another.
 
@@ -72,6 +72,8 @@ We envision the following methods, as part of the Transition Extractor interface
 fn readState(contractId: ContractId) -> State
 ```
 
+where `contractId` is the hash of the uploaded contract code itself, as defined[here][gLE].
+
 ### Monitor Executor
 
 The role of this component is to interact with Apalache.