Implement std::intrinsics::raw_eq support in KMIR (#665)

Goal for this PR is not a complete implementation for `raw_eq`, but a
very basic startup to continue the p-token verification. More see:
#666

## Summary
Implements support for the `std::intrinsics::raw_eq` intrinsic function
in KMIR, enabling byte-by-byte equality comparison of referenced values.

## Key Changes

### 1. Intrinsic Architecture Refactoring
- **Modified intrinsic execution pattern**: Changed from
`#execIntrinsic(INTRINSIC_NAME, ARGS, DEST)` to `#readOperands(ARGS) ~>
#execIntrinsic(INTRINSIC_NAME, DEST)`
- **Benefits**: Uniform operand evaluation using freeze/heat pattern,
simplified intrinsic implementations

### 2. Raw Eq Implementation
- **K Semantics (`kmir.md`)**: 
  - Added execution rules for `raw_eq` intrinsic
- Properly dereferences References using `projectionElemDeref` to access
underlying values
  - Uses dedicated `#execRawEq` function to avoid recursion issues
  - Compares values with K's built-in equality operator (`==K`)

### 3. Black Box Updates
- **Adapted to new architecture**: Updated `black_box` intrinsic to work
with the new signature
- **Maintains identity function behavior**: Simply passes argument to
destination

### 4. Documentation
- **Added comprehensive documentation** for `raw_eq` intrinsic
including:
  - Function description and use cases
  - Current implementation limitations
  - Future enhancement requirements

### 5. Test Integration
- **New test case**: `raw_eq_simple` - compares two references to equal
integers
- **Test files**:
  - `raw_eq_simple.rs`: Rust source with assertion
  - `raw_eq_simple.smir.json`: Generated SMIR representation
- `raw_eq_simple.state`: Expected execution state showing
`BoolVal(true)` result

## Implementation Details

The implementation follows an elegant pattern:
1. `#setUpCalleeData` for intrinsics triggers `#readOperands(ARGS)`
first
2. All operands are evaluated to values and placed on the K cell
3. `#execIntrinsic(symbol("raw_eq"), DEST)` matches Reference values
4. Creates dereferenced operands and calls `#readOperands` again
5. `#execRawEq` compares the dereferenced values and sets result

## Test Results
- ✅ `raw_eq_simple` test passes in both LLVM and Haskell backends
- ✅ Correct `BoolVal(true)` result for equal integer values (42 == 42)
- ✅ Execution completes successfully with proper control flow

## Limitations & Future Work
Current implementation only handles References to same-type values. See
issue #666 for enhancement tracking:
- Different types with same memory representation
- Composite types (structs, arrays, enums)
- Memory layout considerations (alignment, padding)

## Files Changed
- `kmir/src/kmir/kdist/mir-semantics/kmir.md` - Core implementation and
documentation
- `kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.rs`
- Test source
-
`kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.smir.json`
- SMIR data
-
`kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state`
- Expected state
- `kmir/src/tests/integration/test_integration.py` - Test configuration

🤖 Generated with [Claude Code](https://claude.ai/code)

---------

Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>

Author: 3 people

CLAUDE.md

@@ -97,10 +97,12 @@ The Python layer (`kmir.py`) bridges between SMIR JSON and K semantics:
 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:
+Intrinsic functions (like `black_box`, `raw_eq`) 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`
 
+**See `docs/dev/adding-intrinsics.md` for detailed implementation guide.**
+
 ## Testing Patterns
 
 ### prove-rs Tests
@@ -118,9 +120,14 @@ Tests in `kmir/src/tests/integration/data/prove-rs/` follow this pattern:
 ## 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
+1. **Always read relevant documentation first**:
+   - Check `docs/` directory for guides on specific topics
+   - Review existing implementations of similar features
+   - Study test patterns in `kmir/src/tests/`
+2. **Understand existing patterns**:
+   - Look at recent PRs for implementation examples
+   - Check how similar features are implemented
+   - Follow established conventions in the codebase
 
 ### Modifying K Semantics
 1. Edit `.md` files in `kmir/src/kmir/kdist/mir-semantics/`
@@ -133,10 +140,7 @@ Tests in `kmir/src/tests/integration/data/prove-rs/` follow this pattern:
 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
+See `docs/dev/adding-intrinsics.md` for complete guide with examples.
 
 ## Debugging Tips
 

docs/dev/adding-intrinsics.md

@@ -1,73 +1,195 @@
 # Adding Intrinsics
 
+## Overview
+
+This guide explains how to add support for new intrinsic functions in KMIR. Intrinsics are compiler built-in functions that don't have regular MIR bodies and require special semantic rules.
+
+## Architecture
+
+Intrinsics use optimized execution:
+1. **Direct Execution**: `#execIntrinsic(IntrinsicFunction(symbol("name")), ARGS, DEST)` bypasses regular function call setup
+2. **Pattern Matching**: Rules match on specific operand patterns for each intrinsic
+3. **Operand Evaluation**: Each intrinsic rule handles its own operand evaluation as needed
+
+See implementation in [kmir.md](../../kmir/src/kmir/kdist/mir-semantics/kmir.md)
+
 ## 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);
-}
+Create a Rust test file in `kmir/src/tests/integration/data/exec-smir/intrinsic/` that uses your intrinsic and verifies its behavior with assertions.
+
+### Step 2: Add Test to Integration Suite
+
+Add entry to `EXEC_DATA` in [test_integration.py](../../kmir/src/tests/integration/test_integration.py):
+
+```python
+(
+    'your_intrinsic',
+    EXEC_DATA_DIR / 'intrinsic' / 'your_intrinsic.smir.json',
+    EXEC_DATA_DIR / 'intrinsic' / 'your_intrinsic.state',
+    65,  # Start with small depth, increase if needed
+),
 ```
 
-### Step 2: Generate SMIR and Verify Intrinsic Detection
+### Step 3: Generate Initial State (Will Show Stuck Point)
+
 ```bash
-# Generate SMIR JSON
-make generate-tests-smir
+# Generate initial state showing where execution gets stuck
+make test-integration TEST_ARGS="-k 'exec_smir and your_intrinsic' --update-expected-output"
+
+# This will create your_intrinsic.state showing execution stuck at:
+# #execIntrinsic(IntrinsicFunction(symbol("your_intrinsic")), ARGS, DEST)
 
-# Update expected outputs and verify intrinsic is detected
-make test-unit TEST_ARGS="--update-expected-output"
+# Save this for comparison
+cp kmir/src/tests/integration/data/exec-smir/intrinsic/your_intrinsic.state \
+   your_intrinsic.state.initial
 ```
 
-Check `tests/expected/unit/test_smir/test_function_symbols/your_intrinsic.expected.json` to confirm the intrinsic appears as `IntrinsicSym`.
+### Step 4: Implement K Semantics Rule
 
-### Step 3: Run Initial Integration Test
+Add rules to [kmir.md](../../kmir/src/kmir/kdist/mir-semantics/kmir.md). 
+
+To find implementation patterns for your intrinsic:
 ```bash
-# Run test and update expected output (will show stuck at intrinsic call)
-make test-integration TEST_ARGS="-k your_intrinsic --update-expected-output"
+# Search for existing intrinsic implementations
+grep -A10 "#execIntrinsic(IntrinsicFunction" kmir/src/kmir/kdist/mir-semantics/kmir.md
 
-# 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
+# Look for helper functions and evaluation patterns
+grep -B2 -A5 "seqstrict" kmir/src/kmir/kdist/mir-semantics/kmir.md
 ```
 
-### Step 4: Implement K Rule
-Edit `kmir/src/kmir/kdist/mir-semantics/kmir.md`:
+Study existing intrinsics like `black_box` (simple value operation) and `raw_eq` (reference dereferencing with helper functions) as reference implementations.
 
-```k
-rule <k> #execIntrinsic(mirString("your_intrinsic"), ARGS, DEST) => 
-      /* your implementation */
-     ... </k>
-```
+### Step 5: Add Documentation
+
+Document your intrinsic in the K semantics file with its implementation.
+
+### Step 6: Rebuild and Test
 
-### 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"
+# Run test again and update the state with working implementation
+make test-integration TEST_ARGS="-k 'exec_smir and 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
+# Compare to see the progress
+diff your_intrinsic.state.initial \
+     kmir/src/tests/integration/data/exec-smir/intrinsic/your_intrinsic.state
 ```
 
-The diff should show progress past the intrinsic call if implementation is correct.
+### Step 7: Verify Both Backends
 
-### Step 6: Verify Results
-Ensure the test completes successfully and the intrinsic behaves as expected.
-
-## Example: black_box
+```bash
+# Test with both LLVM and Haskell backends
+make test-integration TEST_ARGS="-k 'exec_smir and your_intrinsic'"
 
-Initial state (before rule):
+# Both should pass with consistent results
+# If not, you may need backend-specific state files
 ```
-#setUpCalleeData ( IntrinsicFunction ( mirString ( "black_box" ) ) , ...)
+
+## Examples
+
+For implementation examples, see existing intrinsics in [kmir.md](../../kmir/src/kmir/kdist/mir-semantics/kmir.md).
+
+## Common Patterns
+
+### Pattern 1: Direct Operand Evaluation
+Use when the intrinsic needs to evaluate its operands directly.
+
+### Pattern 2: Reference Dereferencing with #withDeref
+Use the `#withDeref` helper function to add dereferencing to operands.
+
+### Pattern 3: seqstrict for Automatic Evaluation
+Use `[seqstrict(2,3)]` attribute to automatically evaluate operand arguments.
+
+### Pattern 4: Pattern Matching on Operands
+Match specific operand patterns directly in the `#execIntrinsic` rule.
+
+## Testing Best Practices
+
+1. **Start Simple**: Test with primitive types first
+2. **Save Initial State**: Keep the stuck state for comparison
+3. **Use Correct Test Filter**: Always use `exec_smir and your_intrinsic` to ensure correct test runs
+4. **Check Both Backends**: Ensure LLVM and Haskell produce same results  
+5. **Document Limitations**: Note what cases aren't handled yet
+6. **Create Issue for Future Work**: Track enhancements needed (like #666 for `raw_eq`)
+
+## Debugging Tips
+
+### Check Execution State
+```bash
+# See where execution is stuck with verbose output
+make test-integration TEST_ARGS="-k 'exec_smir and your_intrinsic' -vv"
+
+# Look for the K cell content to see what values are present
 ```
 
-After implementing rule:
+### Understanding the State File
+The state file shows the complete execution state. Key sections to check:
+- `<k>`: Shows current execution point
+- `<locals>`: Shows local variable values
+- `<functions>`: Should contain `IntrinsicFunction(symbol("your_intrinsic"))`
+
+### Verify Intrinsic Recognition
+```bash
+# Check SMIR JSON to confirm intrinsic is recognized
+cat kmir/src/tests/integration/data/exec-smir/intrinsic/your_intrinsic.smir.json | grep -A5 your_intrinsic
 ```
-Program continues execution with value 11 passed through
-```
+
+## Common Issues
+
+### Issue: Wrong test runs
+**Solution**: Use `-k 'exec_smir and your_intrinsic'` to ensure `test_exec_smir` runs, not other tests.
+
+### Issue: "Function not found"
+**Solution**: The intrinsic should be automatically recognized if it appears in SMIR. Check the SMIR JSON to confirm.
+
+### Issue: Execution stuck at `#execIntrinsic`
+**Solution**: Your rule pattern doesn't match. Check:
+- The exact intrinsic name in the symbol
+- Value types on K cell (use `ListItem(VAL:Value)` to match any value)
+- Number of arguments expected
+
+### Issue: Recursion/infinite loop
+**Solution**: Use helper functions to separate evaluation stages, avoid calling `#execIntrinsic` within itself.
+
+### Issue: Different backend results
+**Solution**: 
+- Increase execution depth if needed
+- Check for backend-specific evaluation order issues
+- May need backend-specific expected files (`.llvm.state`, `.haskell.state`)
+
+### Issue: Test timeout
+**Solution**: 
+- Start with smaller depth (e.g., 65 instead of 1000)
+- Optimize your rule to avoid unnecessary computation
+- Check for infinite loops in your implementation
+
+## Important Notes
+
+### Direct Operand Passing
+The current architecture passes operands directly to intrinsic rules:
+- **Direct Access**: Rules receive operands directly in `#execIntrinsic`
+- **Custom Evaluation**: Each intrinsic controls its own operand evaluation
+- **Better Indexing**: K can better index rules with explicit operand patterns
+
+### When to Use Helper Functions
+Always use a helper function when:
+- You need automatic operand evaluation (with `seqstrict`)
+- The logic is complex enough to benefit from separation
+- You want to transform operands before evaluation (like with `#withDeref`)
+
+### Testing Strategy
+1. Write the test with expected behavior first
+2. Generate initial state to see where it gets stuck
+3. Implement the minimal rule needed
+4. Update state to verify progress
+5. Iterate to handle edge cases
+6. Document limitations for future work
+
+## References
+
+- Recent intrinsic PRs in repository history
+- [Rust Intrinsics Documentation](https://doc.rust-lang.org/std/intrinsics/)