Implement std::hint::black_box intrinsic support in KMIR

CLAUDE.md

@@ -0,0 +1,161 @@
+# CLAUDE.md
+
+This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
+
+## Repository Overview
+
+MIR Semantics provides a K Framework-based formal semantics for Rust's Stable MIR (Mid-level Intermediate Representation), enabling symbolic execution and formal verification of Rust programs.
+
+## Essential Commands
+
+### Build and Setup
+```bash
+# Initial setup - install stable-mir-json tool for SMIR generation
+make stable-mir-json
+
+# Build K semantics definitions (required after any K file changes)
+make build
+
+# Full build and check
+make check build
+```
+
+### Testing
+```bash
+# Run all tests
+make test
+
+# Run unit tests only
+make test-unit
+
+# Run integration tests (requires stable-mir-json and build)
+make test-integration
+
+# Run a single test
+uv --directory kmir run pytest kmir/src/tests/integration/test_prove.py::test_prove_rs -k "test_name"
+
+# Generate and parse SMIR for test files
+make smir-parse-tests
+```
+
+### Code Quality
+```bash
+# Format code
+make format
+
+# Check code quality (linting, type checking, formatting)
+make check
+
+# Individual checks
+make check-flake8
+make check-mypy
+make check-black
+```
+
+### Working with KMIR Tool
+```bash
+# Activate environment for interactive use
+source kmir/.venv/bin/activate
+
+# Or run commands directly
+uv --directory kmir run kmir <command>
+
+# Prove Rust code directly (recommended)
+uv --directory kmir run kmir prove-rs path/to/file.rs --verbose
+
+# Generate SMIR JSON from Rust
+./scripts/generate-smir-json.sh file.rs output_dir
+
+# View proof results
+uv --directory kmir run kmir show proof_id --proof-dir ./proof_dir
+```
+
+## Architecture Overview
+
+### Directory Structure
+- `kmir/` - Python frontend tool and K semantics
+  - `src/kmir/` - Python implementation
+    - `kmir.py` - Main KMIR class handling K semantics interaction
+    - `smir.py` - SMIR JSON parsing and info extraction
+    - `kdist/mir-semantics/` - K semantics definitions
+  - `src/tests/` - Test suites
+    - `integration/data/prove-rs/` - Rust test programs for prove-rs
+    - `integration/data/exec-smir/` - Rust programs for execution tests
+
+### Key K Semantics Files
+- `kmir.md` - Main execution semantics and control flow
+- `mono.md` - Monomorphized item definitions  
+- `body.md` - Function body and basic block semantics
+- `rt/configuration.md` - Runtime configuration cells
+- `rt/data.md` - Runtime data structures
+- `ty.md` - Type system definitions
+
+### Python-K Integration
+The Python layer (`kmir.py`) bridges between SMIR JSON and K semantics:
+1. Parses SMIR JSON via `SMIRInfo` class
+2. Transforms to K terms using `_make_function_map`, `_make_type_and_adt_maps`
+3. Executes via K framework's `KProve`/`KRun` interfaces
+
+### Intrinsic Functions
+Intrinsic functions (like `black_box`) don't have regular function bodies. They're handled by:
+1. Python: `_make_function_map` adds `IntrinsicFunction` entries to function map
+2. K: Special rules in `kmir.md` execute intrinsics via `#execIntrinsic`
+
+## Testing Patterns
+
+### prove-rs Tests
+Tests in `kmir/src/tests/integration/data/prove-rs/` follow this pattern:
+- Simple Rust programs with assertions
+- File naming: `test-name.rs` (passes), `test-name-fail.rs` (expected to fail)
+- Tests run via `kmir prove-rs` command
+- Generate SMIR automatically during test execution
+
+### Adding New Tests
+1. Add Rust file to `prove-rs/` directory
+2. Use assertions to verify behavior
+3. Run with: `uv --directory kmir run kmir prove-rs your-test.rs`
+
+## Development Workflow
+
+### Before Starting Any Task
+1. Read README and documentation in docs/ directory first
+2. Study existing development patterns and conventions
+3. Understand the codebase structure before making changes
+
+### Modifying K Semantics
+1. Edit `.md` files in `kmir/src/kmir/kdist/mir-semantics/`
+2. Run `make build` to compile changes
+3. Test with `make test-integration`
+
+### Modifying Python Code
+1. Edit files in `kmir/src/kmir/`
+2. Run `make format && make check` to verify code quality and formatting
+3. Test with `make test-unit`
+
+### Adding Intrinsic Support
+1. Update `_make_function_map` in `kmir.py` to recognize intrinsic
+2. Add `IntrinsicFunction` constructor in `mono.md`
+3. Add execution rules in `kmir.md` under `#execIntrinsic`
+4. Add test in `prove-rs/` directory
+
+## Debugging Tips
+
+### Viewing Proof Execution
+```bash
+# Show specific nodes in proof
+uv --directory kmir run kmir show proof_id --nodes "1,2,3" --proof-dir ./proof_dir
+
+# Show transitions between nodes
+uv --directory kmir run kmir show proof_id --node-deltas "1:2,2:3" --proof-dir ./proof_dir
+
+# Show rules applied
+uv --directory kmir run kmir show proof_id --rules "1:2" --proof-dir ./proof_dir
+
+# Full details with static info
+uv --directory kmir run kmir show proof_id --full-printer --no-omit-static-info --proof-dir ./proof_dir
+```
+
+### Common Issues
+- `Function not found` errors: Check if function is in `FUNCTIONS_CELL` (may be intrinsic)
+- K compilation errors: Rules must be properly formatted, check syntax
+- SMIR generation fails: Ensure using correct Rust nightly version (2024-11-29)

docs/dev/adding-intrinsics.md

@@ -0,0 +1,73 @@
+# Adding Intrinsics
+
+## Development Workflow
+
+### Step 1: Create Test File
+Create `tests/rust/intrinsic/your_intrinsic.rs`:
+
+```rust
+fn main() {
+    let result = your_intrinsic(args);
+    assert_eq!(result, expected);
+}
+```
+
+### Step 2: Generate SMIR and Verify Intrinsic Detection
+```bash
+# Generate SMIR JSON
+make generate-tests-smir
+
+# Update expected outputs and verify intrinsic is detected
+make test-unit TEST_ARGS="--update-expected-output"
+```
+
+Check `tests/expected/unit/test_smir/test_function_symbols/your_intrinsic.expected.json` to confirm the intrinsic appears as `IntrinsicSym`.
+
+### Step 3: Run Initial Integration Test
+```bash
+# Run test and update expected output (will show stuck at intrinsic call)
+make test-integration TEST_ARGS="-k your_intrinsic --update-expected-output"
+
+# Backup the initial state for comparison
+cp tests/expected/integration/test_exec_smir/intrinsic_your_intrinsic.state \
+   tests/expected/integration/test_exec_smir/intrinsic_your_intrinsic.state.backup
+```
+
+### Step 4: Implement K Rule
+Edit `kmir/src/kmir/kdist/mir-semantics/kmir.md`:
+
+```k
+rule <k> #execIntrinsic(mirString("your_intrinsic"), ARGS, DEST) => 
+      /* your implementation */
+     ... </k>
+```
+
+### Step 5: Rebuild and Test
+```bash
+# Rebuild K semantics
+make build
+
+# Run test again
+make test-integration TEST_ARGS="-k your_intrinsic --update-expected-output"
+
+# Compare results
+diff tests/expected/integration/test_exec_smir/intrinsic_your_intrinsic.state.backup \
+     tests/expected/integration/test_exec_smir/intrinsic_your_intrinsic.state
+```
+
+The diff should show progress past the intrinsic call if implementation is correct.
+
+### Step 6: Verify Results
+Ensure the test completes successfully and the intrinsic behaves as expected.
+
+## Example: black_box
+
+Initial state (before rule):
+```
+#setUpCalleeData ( IntrinsicFunction ( mirString ( "black_box" ) ) , ...)
+```
+
+After implementing rule:
+```
+Program continues execution with value 11 passed through
+```

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -418,6 +418,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
   // other item kinds are not expected or supported
   rule #getBlocksAux(monoItemStatic(_, _, _)) => .List // should not occur in calls
   rule #getBlocksAux(monoItemGlobalAsm(_)) => .List // not supported
+  rule #getBlocksAux(IntrinsicFunction(_)) => .List // intrinsics have no body
 ```
 
 When a `terminatorKindReturn` is executed but the optional target is empty
@@ -511,9 +512,20 @@ An operand may be a `Reference` (the only way a function could access another fu
          ...
        </currentFrame>
   // TODO: Haven't handled "noBody" case
+
+  // Handle intrinsic functions - execute directly without setting up local stack frame
+  rule <k> #setUpCalleeData(IntrinsicFunction(INTRINSIC_NAME), ARGS) 
+        => #execIntrinsic(INTRINSIC_NAME, ARGS, DEST) ~> #execBlockIdx(RETURN_TARGET)
+       </k>
+       <currentFrame>
+         <dest> DEST </dest>
+         <target> someBasicBlockIdx(RETURN_TARGET) </target>
+         ...
+       </currentFrame>
 
   syntax KItem ::= #setArgsFromStack ( Int, Operands)
                  | #setArgFromStack ( Int, Operand)
+                 | #execIntrinsic ( Symbol, Operands, Place )
 
   // once all arguments have been retrieved, execute
   rule <k> #setArgsFromStack(_, .Operands) ~> CONT => CONT </k>
@@ -602,6 +614,23 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre
        </k>
 ```
 
+### Intrinsic Functions
+
+Intrinsic functions are built-in functions provided by the compiler that don't have regular MIR bodies.
+They are handled specially in the execution semantics through the `#execIntrinsic` mechanism.
+When an intrinsic function is called, the execution bypasses the normal function call setup and directly
+executes the intrinsic-specific logic.
+
+#### Black Box (`std::hint::black_box`)
+
+The `black_box` intrinsic serves as an optimization barrier, preventing the compiler from making assumptions
+about the value passed through it. In the semantics, it acts as an identity function that simply passes
+its argument to the destination without modification.
+
+```k
+  // Black box intrinsic implementation - identity function  
+  rule <k> #execIntrinsic(symbol("black_box"), ARG .Operands, DEST) => #setLocalValue(DEST, ARG) ... </k>
+```
 
 ### Stopping on Program Errors
 

kmir/src/kmir/kdist/mir-semantics/mono.md

@@ -34,6 +34,7 @@ syntax MonoItemKind ::= monoItemFn(name: Symbol, id: DefId, body: MaybeBody)
                           [ group(mir-enum)
                           , symbol(MonoItemKind::MonoItemGlobalAsm)
                           ]
+                      | IntrinsicFunction(Symbol) [ symbol(IntrinsicFunction) ]
 syntax MonoItem ::= monoItem(symbolName: Symbol, monoItemKind: MonoItemKind)
                       [symbol(monoItemWrapper), group(mir---symbol-name--mono-item-kind)]
 syntax MonoItems ::= List {MonoItem, ""}

kmir/src/kmir/kmir.py

@@ -68,9 +68,11 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
-    def _make_function_map(self, smir_info: SMIRInfo) -> KInner:
+    def functions(self, smir_info: SMIRInfo) -> dict[int, KInner]:
         parser = Parser(self.definition)
-        parsed_items: dict[KInner, KInner] = {}
+        functions: dict[int, KInner] = {}
+
+        # Parse regular functions
         for item_name, item in smir_info.items.items():
             if not item_name in smir_info.function_symbols_reverse:
                 _LOGGER.warning(f'Item not found in SMIR: {item_name}')
@@ -82,9 +84,23 @@ def _make_function_map(self, smir_info: SMIRInfo) -> KInner:
             assert isinstance(parsed_item_kinner, KApply) and parsed_item_kinner.label.name == 'monoItemWrapper'
             # each item can have several entries in the function table for linked SMIR JSON
             for ty in smir_info.function_symbols_reverse[item_name]:
-                item_ty = KApply('ty', [token(ty)])
-                parsed_items[item_ty] = parsed_item_kinner.args[1]
-        return map_of(parsed_items)
+                functions[ty] = parsed_item_kinner.args[1]
+
+        # Add intrinsic functions
+        for ty, sym in smir_info.function_symbols.items():
+            if 'IntrinsicSym' in sym and ty not in functions:
+                functions[ty] = KApply(
+                    'IntrinsicFunction',
+                    [KApply('symbol(_)_LIB_Symbol_String', [token(sym['IntrinsicSym'])])],
+                )
+
+        return functions
+
+    def _make_function_map(self, smir_info: SMIRInfo) -> KInner:
+        parsed_terms: dict[KInner, KInner] = {}
+        for ty, body in self.functions(smir_info).items():
+            parsed_terms[KApply('ty', [token(ty)])] = body
+        return map_of(parsed_terms)
 
     def _make_type_and_adt_maps(self, smir_info: SMIRInfo) -> tuple[KInner, KInner]:
         parser = Parser(self.definition)

kmir/src/kmir/smir.py

@@ -116,8 +116,10 @@ def function_symbols_reverse(self) -> dict[str, list[int]]:
         tys_for_name: dict[str, list[int]] = {}
         for ty, sym in self.function_symbols.items():
             if 'NormalSym' in sym:
-                tys_for_name.setdefault(sym['NormalSym'], [])
-                tys_for_name[sym['NormalSym']].append(ty)
+                tys_for_name.setdefault(sym['NormalSym'], []).append(ty)
+            elif 'IntrinsicSym' in sym:
+                tys_for_name.setdefault(sym['IntrinsicSym'], []).append(ty)
+            # Skip other symbol types like NoOpSym for now
         return tys_for_name
 
     @cached_property