Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pyk scripts #10

Merged
merged 13 commits into from
Aug 23, 2024
Prev Previous commit
Next Next commit
Adding the capabilities to load data into the K cell
ACassimiro committed Aug 21, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 9c4c353de3676ab3d2634a53829433db0084a2ec
11 changes: 8 additions & 3 deletions rust-lite/src/rust_lite/__main__.py
Original file line number Diff line number Diff line change
@@ -23,11 +23,16 @@


def main() -> None:
print("Instantiating module manager")
print("Instantiating module manager;")

module_manager = RustLiteManager()

print("Module manager initiated")
print("Module manager initiated; Trying to load program into K cell;")

pass
module_manager.load_program("Test")

print("Program loaded; Trying to fetch the content of the K cell.")

module_manager.fetch_k_cell_content()


32 changes: 20 additions & 12 deletions rust-lite/src/rust_lite/manager.py
Original file line number Diff line number Diff line change
@@ -4,20 +4,25 @@
import json
import logging
import sys
import pprint
from collections.abc import Iterable
from typing import TYPE_CHECKING
from pathlib import Path

from pathos.pools import ProcessPool # type: ignore
from pyk.cli.pyk import parse_toml_args
from pyk.kast.inner import KApply, KSequence, KSort, KToken, Subst
from pyk.kast.manip import set_cell
from pyk.cterm import CTerm
from pyk.ktool.krun import KRun
from pyk.prelude.k import GENERATED_TOP_CELL
from pyk.kdist import kdist
from pyk.kore.prelude import top_cell_initializer
from pyk.kore.tools import kore_print
from pyk.utils import FrozenDict
from pyk.prelude.string import stringToken

_PPRINT = pprint.PrettyPrinter(width=41, compact=True)

class RustLiteManager():
krun: KRun
@@ -30,16 +35,19 @@ def __init__(self) -> None:

def _init_cterm(self) -> None:
self.krun.definition.empty_config(GENERATED_TOP_CELL)
init_config = self.krun.definition.init_config(GENERATED_TOP_CELL)
self.cterm = CTerm.from_kast(init_config)

def load_program(self, program: str) -> None:
# self.cterm = CTerm.from_kast(set_cell(self.cterm.config, 'K_CELL', KApply(program, [])))
self.cterm = CTerm.from_kast(set_cell(self.cterm.config, 'K_CELL', stringToken(program)))
pattern = self.krun.kast_to_kore(self.cterm.config, sort=GENERATED_TOP_CELL)
output_kore = self.krun.run_pattern(pattern, pipe_stderr=True)
self.cterm = CTerm.from_kast(self.krun.kore_to_kast(output_kore))

# init_subst = {
# '$PGM': KSequence([KEVM.sharp_execute()]),
# '$MODE': KApply('NORMAL'),
# '$SCHEDULE': KApply('SHANGHAI_EVM'),
# '$USEGAS': TRUE,
# '$CHAINID': intToken(0),
# }

# init_config = set_cell(init_config, 'ACCOUNTS_CELL', KEVM.accounts(init_accounts_list))

# init_term = Subst(init_subst)(init_config)
# self.cterm = CTerm.from_kast(init_term)

def fetch_k_cell_content(self):
cell = self.cterm.cell('K_CELL')
# assert type(cell) is KToken
_PPRINT.pprint(cell)
return cell