Skip to content

Commit 74f64ca

Browse files
lisandrasilvalisandrasilva
committed
Implemented traceTransaction
1 parent 337c1cc commit 74f64ca

5 files changed

Lines changed: 121 additions & 72 deletions

File tree

‎pyproject.toml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@ readme = "README.md"
1010
requires-python = "~=3.10"
1111
dependencies = [
1212
"stellar-sdk>=13.2.1",
13-
"komet@git+https://github.com/runtimeverification/komet.git@v0.1.77",
13+
"komet@git+https://github.com/runtimeverification/komet.git@v0.1.79",
14+
"kframework>=7.1.318,<7.1.321",
1415
]
1516

1617
[[project.authors]]

‎src/komet_node/interpreter.py‎

Lines changed: 56 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@
2222
from pyk.konvert import kast_to_kore, kore_to_kast
2323
from pyk.kore.parser import KoreParser
2424
from pyk.kore.prelude import str_dv
25+
from pyk.kore.syntax import App, Pattern
2526
from pyk.ktool.krun import KRunOutput, _krun
2627
from pykwasm.wasm2kast import wasm2kast
2728
from stellar_sdk import Network, StrKey, xdr
@@ -67,19 +68,18 @@ def __init__(self, network_passphrase: str = Network.TESTNET_NETWORK_PASSPHRASE,
6768
self.trace = trace
6869

6970
def _trace_config_vars(self) -> tuple[dict[str, str], dict[str, str]]:
70-
return {'TRACE': str_dv(_TRACE_FILE).text}, {'TRACE': 'cat'}
71+
trace_path = _TRACE_FILE if self.trace else ''
72+
return {'TRACE': str_dv(trace_path).text}, {'TRACE': 'cat'}
7173

7274
def empty_config(self) -> str:
7375
"""Return the initial idle K configuration, with tracing enabled if requested."""
74-
kwargs: dict = {'output': KRunOutput.KORE}
75-
if self.trace:
76-
cmap, pmap = self._trace_config_vars()
77-
kwargs['cmap'] = cmap
78-
kwargs['pmap'] = pmap
76+
cmap, pmap = self._trace_config_vars()
7977
res = self.definition.krun_with_kast(
8078
pgm=steps_of([set_exit_code(0)]),
8179
sort=KSort('Steps'),
82-
**kwargs,
80+
output=KRunOutput.KORE,
81+
cmap=cmap,
82+
pmap=pmap,
8383
)
8484
res.check_returncode()
8585
return res.stdout
@@ -357,6 +357,46 @@ def run_request_file(self, input_file: Path, request_str: str) -> InterpreterRes
357357

358358
return InterpreterResponse(final_kore=res.stdout, trace=trace)
359359

360+
def run_transaction_with_trace(
361+
self, input_file: Path, transaction: Transaction, ledger_seq: int = 0
362+
) -> InterpreterResponse:
363+
"""Like run_transaction but always produces a trace, regardless of self.trace."""
364+
if self.trace:
365+
return self.run_transaction(input_file, transaction, ledger_seq)
366+
367+
request_str = self.encode_transaction_to_json(transaction, ledger_seq)
368+
if request_str is not None:
369+
return self._run_request_file_force_trace(input_file, request_str)
370+
371+
# KORE round-trip (wasm upload) — tracing not supported for this path
372+
return self.run_transaction(input_file, transaction, ledger_seq)
373+
374+
def _run_request_file_force_trace(self, input_file: Path, request_str: str) -> InterpreterResponse:
375+
"""Run request.json with tracing forced on by patching <ioDir> in state.kore."""
376+
state_kore = KoreParser(input_file.read_text()).pattern()
377+
patched_kore = _set_io_dir(state_kore, _TRACE_FILE)
378+
379+
with temp_working_directory() as root:
380+
(root / REQUEST_FILE).write_text(request_str)
381+
patched_state = root / 'state_traced.kore'
382+
patched_state.write_text(patched_kore.text)
383+
384+
res = _krun(
385+
input_file=patched_state,
386+
definition_dir=self.definition.path,
387+
parser='cat',
388+
term=True,
389+
output=KRunOutput.KORE,
390+
check=False,
391+
)
392+
393+
if res.returncode:
394+
raise NodeInterpreterError(f'krun failed for traced request: {request_str}', res)
395+
396+
trace_file = root / _TRACE_FILE
397+
trace = trace_file.read_text() if trace_file.exists() else None
398+
return InterpreterResponse(final_kore=res.stdout, trace=trace)
399+
360400
def run_steps(self, input_file: Path, steps: Iterable[KInner]) -> InterpreterResponse:
361401
input_state_kore = KoreParser(input_file.read_text()).pattern()
362402
input_state_kast = kore_to_kast(self.definition.kdefinition, input_state_kore)
@@ -432,5 +472,14 @@ def _encode_scval(scval: xdr.SCVal) -> dict:
432472
raise NotImplementedError(f'Unsupported SCVal type for JSON encoding: {scval.type}')
433473

434474

475+
def _set_io_dir(pattern: Pattern, path: str) -> Pattern:
476+
"""Walk a KORE pattern and set the <ioDir> cell value to `path`."""
477+
if isinstance(pattern, App):
478+
if pattern.symbol == "Lbl'-LT-'ioDir'-GT-'":
479+
return App(pattern.symbol, pattern.sorts, (str_dv(path),))
480+
return App(pattern.symbol, pattern.sorts, tuple(_set_io_dir(a, path) for a in pattern.args))
481+
return pattern
482+
483+
435484
class NodeInterpreterError(RuntimeError):
436485
pass

‎src/komet_node/kdist/fs.md‎

Lines changed: 10 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,63 +1,19 @@
11

22
```k
3+
requires "soroban-semantics/fs.md"
4+
35
module FILE-OPERATIONS
46
imports BOOL
5-
imports INT
6-
imports K-EQUAL
77
imports K-IO
8-
imports STRING
9-
10-
syntax Int ::= "MAX_READ" [alias]
11-
// ------------------------------
12-
13-
rule MAX_READ => 104857600 // 100mb
14-
15-
syntax IOString ::= #readFile( String ) [function, impure, symbol(readFile)]
16-
// -----------------------------------------------------------------------------------
17-
18-
syntax K ::= #writeFile( String, String ) [function, impure, symbol(writeFile)]
19-
| #appendFile( String, String) [function, impure, symbol(appendFile)]
20-
| #appendFileToFile( String, String ) [function, impure, symbol(appendFileToFile)]
21-
// --------------------------------------------------------------------------------------------------
22-
23-
rule #readFile( FILE )
24-
=> #let HANDLE:IOInt = #open( FILE, "r" ) #in
25-
#let RESULT = #read({HANDLE}:>Int, MAX_READ) #in
26-
#let _ = #close({HANDLE}:>Int) #in
27-
RESULT
28-
29-
rule #writeFile( FILE, CONTENTS )
30-
=> #let HANDLE:IOInt = #open( FILE, "w") #in
31-
#let RESULT = #write({HANDLE}:>Int, CONTENTS) #in
32-
#let _ = #close({HANDLE}:>Int) #in
33-
RESULT
34-
35-
rule #appendFile( FILE, CONTENTS )
36-
=> #let HANDLE:IOInt = #open( FILE, "a" ) #in
37-
#let RESULT = #write({HANDLE}:>Int, CONTENTS) #in
38-
#let _ = #close({HANDLE}:>Int) #in
39-
RESULT
40-
41-
rule #appendFileToFile( DEST, SOURCE )
42-
=> #system( "dd if=" +String SOURCE +String " of=" +String DEST +String " bs=1M oflag=append conv=notrunc" )
8+
imports FILE-SYSTEM
439
44-
rule #systemResult( _, _, _ ) => .K [owise]
45-
46-
syntax Bool ::= #fileExists( String ) [function, impure]
47-
// ----------------------------------------------------------
48-
rule #fileExists( FILE ) => #let HANDLE:IOInt = #open( FILE, "r" ) #in
49-
#if isError(HANDLE)
50-
#then
51-
false
52-
#else
53-
#let _ = #close({HANDLE}:>Int) #in
54-
true
55-
#fi
10+
syntax Bool ::= #fileExists( String ) [function, impure]
11+
| #fileExistsResult( IOInt ) [function, impure]
12+
// -----------------------------------------------------------------
13+
rule #fileExists( FILE ) => #fileExistsResult(#open(FILE, "r"))
5614
57-
syntax Bool ::= isError(KItem) [function, total]
58-
// ----------------------------------------------------
59-
rule isError(_:IOError) => true
60-
rule isError(_) => false [owise]
15+
rule #fileExistsResult(HANDLE:Int) => #let _ = #close(HANDLE) #in true
16+
rule #fileExistsResult(_:IOError) => false
6117
6218
endmodule
63-
```
19+
```

‎src/komet_node/server.py‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ def _register_stellar_methods(self) -> None:
4747
'getLatestLedger': self.exec_get_latest_ledger,
4848
'sendTransaction': self.exec_send_transaction,
4949
'getTransaction': self.exec_get_transaction,
50+
'traceTransaction': self.exec_trace_transaction,
5051
}.items():
5152
self.register_method(name, fn)
5253

@@ -103,6 +104,46 @@ def exec_send_transaction(self, transaction: str) -> dict[str, Any]:
103104
'latestLedgerCloseTime': now,
104105
}
105106

107+
def exec_trace_transaction(self, transaction: str) -> dict[str, Any]:
108+
now = str(int(time.time()))
109+
envelope = TransactionEnvelope.from_xdr(transaction, self.interpreter.network_passphrase)
110+
tx_hash = envelope.hash_hex()
111+
112+
try:
113+
result = self.interpreter.run_transaction_with_trace(
114+
self.state_file, envelope.transaction, self.ledger_seq
115+
)
116+
self.state_file.write_text(result.final_kore)
117+
self.ledger_seq += 1
118+
self._transactions[tx_hash] = {
119+
'status': 'SUCCESS',
120+
'ledger': str(self.ledger_seq),
121+
'createdAt': now,
122+
'envelopeXdr': transaction,
123+
'resultXdr': '',
124+
'resultMetaXdr': '',
125+
'trace': result.trace,
126+
}
127+
except NodeInterpreterError:
128+
self._transactions[tx_hash] = {
129+
'status': 'FAILED',
130+
'ledger': str(self.ledger_seq),
131+
'createdAt': now,
132+
'envelopeXdr': transaction,
133+
'resultXdr': '',
134+
'resultMetaXdr': '',
135+
'trace': None,
136+
}
137+
138+
return {
139+
'hash': tx_hash,
140+
'status': self._transactions[tx_hash]['status'],
141+
'ledger': self._transactions[tx_hash]['ledger'],
142+
'trace': self._transactions[tx_hash]['trace'],
143+
'latestLedger': str(self.ledger_seq),
144+
'latestLedgerCloseTime': now,
145+
}
146+
106147
def exec_get_transaction(self, hash: str) -> dict[str, Any]:
107148
now = str(int(time.time()))
108149
result = self._transactions.get(hash)

‎uv.lock‎

Lines changed: 12 additions & 10 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)