Spaces:
Sleeping
Sleeping
| import streamlit as st | |
| import subprocess | |
| import os | |
| import tempfile | |
| import shutil | |
| from verifier import analyze_contract, run_formal_verification, generate_specification | |
| def compile_solidity_to_bytecode(solidity_code): | |
| if os.path.exists("out"): | |
| shutil.rmtree("out") | |
| with tempfile.NamedTemporaryFile(suffix=".sol", delete=False) as f: | |
| f.write(solidity_code.encode("utf-8")) | |
| solidity_file = f.name | |
| try: | |
| try: | |
| solc_path = subprocess.check_output(["which", "solc"]).decode().strip() | |
| st.info(f"Using solc from: {solc_path}") | |
| except: | |
| st.error("solc is not available in the container.") | |
| return None | |
| result = subprocess.run( | |
| ["solc", "--bin", "--ast-compact-json", "--optimize", "--overwrite", solidity_file, "-o", "out"], | |
| capture_output=True, | |
| text=True, | |
| timeout=30 | |
| ) | |
| if result.returncode != 0: | |
| st.error("Error compiling Solidity code.") | |
| st.text(result.stderr) | |
| return None | |
| bytecode_file = os.path.join("out", os.path.basename(solidity_file).replace(".sol", ".bin")) | |
| if os.path.exists(bytecode_file): | |
| with open(bytecode_file, "r") as f: | |
| bytecode = f.read().strip() | |
| return bytecode | |
| else: | |
| st.error("Bytecode file not found.") | |
| return None | |
| finally: | |
| os.remove(solidity_file) | |
| def run_kevm(bytecode): | |
| return f"Simulated KEVM Spec for Bytecode:{bytecode[:60]}..." | |
| st.title("Smart Contract Verifier") | |
| st.markdown("Upload a smart contract for analysis and get formal specification.") | |
| uploaded_file = st.file_uploader("Upload contract file", type=["sol"]) | |
| language = st.selectbox("Language", ["Solidity", "Vyper"]) | |
| tool = st.selectbox("Tool", ["slither", "mythril"]) | |
| verify_formally = st.checkbox("Formal Verification") | |
| spec_lang = st.selectbox("Spec Language", ["KEVM", "TLA+", "Z Notation"]) | |
| if uploaded_file: | |
| code = uploaded_file.read().decode("utf-8") | |
| st.code(code, language="solidity") | |
| if st.button("Analyze Contract"): | |
| try: | |
| summary, report = analyze_contract(code, language, tool, verify_formally) | |
| except Exception as e: | |
| summary, report = "Analysis failed.", str(e) | |
| st.subheader("Summary") | |
| st.write(summary) | |
| st.subheader("Report") | |
| st.text(report) | |
| st.download_button("Download Report", report, file_name="report.txt") | |
| if verify_formally: | |
| fv_summary, fv_report = run_formal_verification(code) | |
| st.subheader("Formal Verification") | |
| st.text(fv_report) | |
| if spec_lang == "KEVM": | |
| bytecode = compile_solidity_to_bytecode(code) | |
| if bytecode: | |
| spec = run_kevm(bytecode) | |
| st.subheader("KEVM Spec") | |
| st.text(spec) | |
| st.download_button("Download Spec", spec, file_name="kevm_spec.txt") | |
| else: | |
| spec = generate_specification(code, spec_lang) | |
| st.subheader(f"{spec_lang} Specification") | |
| st.text(spec) | |
| st.download_button("Download Spec", spec, file_name=f"{spec_lang.lower()}_spec.txt") | |