# Linking External Libraries

For cryptographic primitives (Poseidon, Groth16, etc.) that are impractical to implement in Lean, or for reusing audited Yul libraries. Your proofs verify contract logic against a placeholder; the real implementation is injected at compile time.

## How it works

1. **Yul library**, plain function definitions, no `object` wrapper.
2. **Lean placeholder**, used only by proofs; never appears in compiled Yul.
3. **`externals` declaration on the `CompilationModel`**, the linker only injects into contracts that declare what they need.
4. **`--link` flag**, pass `.yul` library files at compile time.

## Walkthrough

**Yul library** (`examples/external-libs/MyHash.yul`):

```yul
function myHash(a, b) -> result {
    result := add(xor(a, b), 0x42)
}
```

**Lean placeholder** (used for proofs, ignored at compile time):

```verity
def myHash (a b : Uint256) : Contract Uint256 := return add a b
```

**`CompilationModel`** (`Compiler/Specs.lean`):

```verity
def myCompilationModel : CompilationModel := {
  name := "MyContract"
  fields := [...]
  externals := [
    { name := "myHash"
      params := [ParamType.uint256, ParamType.uint256]
      returnType := some ParamType.uint256
      proofStatus := .assumed
      axiomNames := [] }
  ]
  functions := [
    { name := "storeHash"
      params := [...]
      returnType := none
      body := [
        Stmt.letVar "h" (Expr.externalCall "myHash" [Expr.param "a", Expr.param "b"]),
        ...
      ]
    }
  ]
}
```

> **The `externals` field is required.** Without it, the linker silently skips this contract even if `--link` is passed. `Expr.param "a"` must match the parameter `name` declared in `params`.

**Compile**:

```bash
lake exe verity-compiler --link examples/external-libs/MyHash.yul -o artifacts/yul
```

The linker parses each `.yul`, validates (no duplicate names, no shadowing of Yul builtins or `mappingSlot`, all references resolved, correct arity), and injects functions into the runtime `code {}` block. Unresolved references fail closed:

```
Unresolved external references: myHash
```

## Reference example: CryptoHash

The repo includes a working setup in [`Contracts/CryptoHash/Contract.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/CryptoHash/Contract.lean) with libraries in [`examples/external-libs/`](https://github.com/lfglabs-dev/verity/tree/main/examples/external-libs). Look at `cryptoHashSpec` in `Compiler/Specs.lean` for a complete `externals` declaration.

## Trust model

External libraries are **outside the formal verification boundary**. The linker validates *structure* (no shadowing, resolved references, correct arity); it does not verify *behavior*. Your proofs establish: *if the library functions behave like the placeholders, then the contract is correct*.

In practice: a contract using `PoseidonT3_hash` via the linker has formally verified logic (storage, access control, arithmetic) but an *unverified* cryptographic core. The proof guarantees the contract correctly *uses* the hash; it does not guarantee the hash *is* Poseidon. Auditing the `.yul` library is the developer's responsibility.

To increase confidence: use audited implementations, add Foundry tests that exercise the linked contract end-to-end, compare library output against a reference, and document the assumption in [`TRUST_ASSUMPTIONS.md`](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md).

## CLI

```
lake exe verity-compiler [options]

--link <path>           Link external Yul library (repeatable)
-o, --output <dir>      Output directory (default: artifacts/yul)
--abi-output <dir>      Output ABI JSON artifacts
--backend-profile <p>   semantic (default) | solidity-parity-ordering
--mapping-slot-scratch-base <n>   Scratch memory base for mappingSlot
-v, --verbose
--help
```

Patch-enabled generation lives in `verity-compiler-patched`:

```bash
lake exe verity-compiler-patched --backend-profile solidity-parity
lake exe verity-compiler-patched --enable-patches --patch-report artifacts/patch-report.tsv
```

## Common errors

- `Unresolved external references: <name>`, missing `--link`, or the name doesn't match between `CompilationModel` and the `.yul` file (case-sensitive).
- `Arity mismatch: <name>: called with N args but library defines M params`, return values don't count as parameters.
- Contract works with the placeholder but reverts at runtime, usually gas, or the library returns an unexpected shape. Run Foundry tests against the linked Yul.