Add interactive WebAssembly formal semantics explorer demo

[Copilot]

Creates a comprehensive educational showcase demonstrating WebAssembly formal verification using the K Framework, making abstract formal methods accessible through interactive visualizations and progressive tutorials.

Structure

Core Infrastructure

• Interactive landing page with responsive design, feature showcase, learning paths
• Complete directory structure: 10 main sections (introduction, tutorials, visualizations, case studies, K deep dive, playground, narratives, advanced topics, comparisons, community)
• Build system with targets for serving, testing, verification examples
• Automated tests validating demo structure (31 tests)

Educational Content

• Introduction guides: formal semantics primer, K Framework overview, WebAssembly architecture, verification rationale
• Progressive tutorials from beginner (⭐) to research-level (⭐⭐⭐⭐⭐)
• Hello WebAssembly tutorial with step-by-step execution trace
• Community resources: contribution guide, build instructions

Interactive Components

• 4 JavaScript visualizers: execution tracer with stack animation, K semantics rule browser, state inspector with tabbed views, proof tree builder with export
• 3 CSS stylesheets: K Framework theming with dark mode, WebAssembly syntax highlighting, animation framework
• SVG diagrams: K Framework logo, stack machine architecture, verification workflow

WebAssembly Examples

• Basic: hello world (i32.const), arithmetic operations, control flow
• Intermediate: function definitions, recursion, Fibonacci

Usage

cd demos/formal_semantics_explorer
make serve  # Launch at http://localhost:8000
python3 test_demo.py  # Validate structure
make verify-example EXAMPLE=memory_safety/bounds_overflow

Demo Features

• Visual execution traces with animated stack operations
• Interactive K rule browser with search and filtering
• Proof tree visualization with LaTeX/GraphViz export
• State inspector showing stack, memory, locals, globals
• Progressive difficulty from basic constants to full verification workflows

Transforms ~500 K semantic rules and formal proofs into an accessible learning experience bridging theory and practice.

Original prompt

🎯 Objective
Create an interactive, visual demonstration of WebAssembly formal semantics using the K Framework, making formal verification accessible through beautiful visualizations, interactive examples, and educational narratives.

📋 Complete Prompt for GitHub Agent
Copy and paste this entire prompt to GitHub Copilot coding agent:

Code
Create a comprehensive exploratory showcase demo for AYUSHMIT/wasm-semantics (forked from runtimeverification/wasm-semantics).

Overview

Build an interactive demonstration of WebAssembly formal semantics in the K Framework, transforming abstract formal verification concepts into accessible, visual, and engaging educational content. This showcase will bridge the gap between formal methods and practical WebAssembly understanding.

Directory Structure

Create: demos/formal_semantics_explorer/ with the following structure:

demos/formal_semantics_explorer/ ├── README.md # Main showcase landing page ├── index.html # Interactive web-based explorer ├── assets/ │ ├── styles/ │ │ ├── formal_methods.css # K Framework themed styling │ │ ├── wasm_syntax_highlight.css # WebAssembly syntax highlighting │ │ └── interactive. css # Animation & transitions │ ├── js/ │ │ ├── wasm_visualizer.js # Visual execution tracer │ │ ├── k_semantics_renderer.js # K rules visualization │ │ ├── proof_tree_builder.js # Derivation tree display │ │ └── state_inspector.js # Configuration state viewer │ ├── images/ │ │ ├── k_framework_logo.svg # K Framework branding │ │ ├── wasm_architecture.svg # WebAssembly stack machine diagram │ │ └── semantics_workflow.svg # Formal verification workflow │ └── wasm_examples/ │ ├── basic/ # Simple examples (. wasm, .wat files) │ ├── intermediate/ # Moderate complexity │ └── advanced/ # Complex verification targets │ ├── 01_introduction/ │ ├── 00_what_is_formal_semantics.md # Gentle introduction │ ├── 01_k_framework_primer.md # K Framework basics │ ├── 02_webassembly_overview.md # WebAssembly architecture │ └── 03_why_verify_wasm.md # Motivation & use cases │ ├── 02_interactive_tutorials/ │ ├── hello_wasm_semantics/ │ │ ├── tutorial. md # Step-by-step guide │ │ ├── example. wat # WebAssembly text format │ │ ├── semantics_trace.html # Interactive execution trace │ │ └── verification_proof.txt # Formal proof output │ ├── arithmetic_operations/ │ │ ├── add_subtract.wat # Basic arithmetic │ │ ├── overflow_detection.wat # Edge case handling │ │ ├── semantics_rules.k # Relevant K rules excerpt │ │ └── interactive_stepper.html # Step-by-step executor │ ├── control_flow/ │ │ ├── if_else.wat # Conditional execution │ │ ├── loops.wat # Loop constructs │ │ ├── blocks_br.wat # Block scoping & branching │ │ └── cfg_visualization.html # Control flow graph viewer │ ├── function_calls/ │ │ ├── simple_call.wat # Function invocation │ │ ├── recursion.wat # Recursive functions │ │ ├── stack_visualization.html # Call stack visualizer │ │ └── frame_semantics.md # Activation frame explanation │ ├── memory_operations/ │ │ ├── load_store.wat # Memory access │ │ ├── bounds_checking.wat # Memory safety verification │ │ ├── memory_viewer.html # Interactive memory inspector │ │ └── safety_proofs.md # Formal safety guarantees │ └── tables_and_references/ │ ├── indirect_calls.wat # Function pointers │ ├── table_operations.wat # Table manipulation │ └── reference_semantics.md # Reference type handling │ ├── 03_visualization_gallery/ │ ├── execution_traces/ │ │ ├── trace_visualizer.html # Animated execution steps │ │ ├── state_transitions.json # Configuration evolution data │ │ └── timeline_viewer.html # Temporal execution view │ ├── semantic_rules/ │ │ ├── rule_browser.html # Browse all K rules │ │ ├── rule_dependencies.html # Rule relationship graph │ │ └── rule_search.js # Search & filter rules │ ├── proof_trees/ │ │ ├── derivation_viewer.html # Interactive proof tree │ │ ├── tree_layout_engine.js # D3.js tree rendering │ │ └── proof_examples/ # Pre-computed proofs │ ├── memory_models/ │ │ ├── heap_visualizer.html # 3D memory visualization │ │ ├── stack_animator.html # Stack evolution animation │ │ └── linear_memory.html # WebAssembly linear memory │ └── type_system/ │ ├── type_checker_viz.html # Type checking visualizer │ ├── validation_flow.html # Module validation steps │ └── type_safety_proof.html # Soundness visualization │ ├── 04_verification_case_studies/ │ ├── memory_safety/ │ │ ├── bounds_overflow.wat # Buffer overflow example │ │ ├── verification_spec.k # Formal specification │ │ ├── proof_script.py # Automated verification │ │ └── results_dashboard.html # Verification results │ ├── type_soundness/ │ │ ├── ill_typed_module.wat # Type error examples │ │ ├── type_preservation.md # Subject reduction theorem │ │ └── progress_proof.md # Progress theorem │ ├── determinism/ │ │ ├── deterministic_execution.wat # Determinism examples │ │ ├── trace_comparison.html # Compare execution traces │ │ └── proof_determinism.txt # Formal determinism proof │ ├── security_properties/ │ │ ├── sandboxin...

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[gitnotebooks]

Review these changes at https://app.gitnotebooks.com/AYUSHMIT/wasm-semantics/pull/1