Generated artifacts

On-disk layout

After a successful tama build, the project contains:

artifacts/
├── lean/                              # Lake build directory
├── yul/
│   └── <Contract>.yul                 # Verity-emitted Yul
├── bytecode/
│   ├── <Contract>.bin                 # creation bytecode (hex)
│   └── <Contract>.runtime.bin         # runtime bytecode (hex)
├── solc-json/
│   ├── <Contract>.input.json          # solc standard-json input
│   └── <Contract>.output.json         # solc standard-json output
├── manifest/
│   └── <Contract>.json                # tama.contract-manifest.v1
├── trust-probe/
│   └── axioms.json                    # tama.trust-probe.v1
├── trust-report.json                  # Verity compiler trust surface
└── assumption-report.json             # undischarged compiler assumptions

src/generated/verity/
├── <Contract>Iface.sol                # ABI-level interface
└── <Contract>Deployer.sol             # library, embeds creation bytecode

Producer / consumer table

Path	Produced by	Consumed by
`artifacts/lean/`	`lake`	`lake`
`artifacts/yul/<C>.yul`	Verity compiler	`solc`, `tama inspect yul`
`artifacts/solc-json/<C>.input.json`	Tama	`solc`
`artifacts/solc-json/<C>.output.json`	`solc`	Tama (bytecode + layout extraction)
`artifacts/bytecode/<C>.bin`	Tama	Bridge generator, `tama inspect bytecode`, audit
`artifacts/bytecode/<C>.runtime.bin`	Tama	`tama inspect runtime-bytecode`
`artifacts/manifest/<C>.json`	Tama	Bridge generator, `tama inspect`, every audit
`artifacts/trust-probe/axioms.json`	Lean (via Tama)	`tama audit trust-boundary`
`artifacts/trust-report.json`	Verity compiler	`tama audit trust-boundary`
`artifacts/assumption-report.json`	Verity compiler	`tama audit trust-boundary`
`src/generated/verity/<C>Iface.sol`	Tama	User Solidity, `forge build`, `tama audit selectors`
`src/generated/verity/<C>Deployer.sol`	Tama	Mirror tests, `forge build`, `tama audit structure`

Generated Solidity headers

Every generated Solidity file starts with exactly:

// GENERATED by tama; do not edit.

Tama refuses to overwrite a file whose first line has been altered. This is a safety net so accidental hand edits aren’t silently lost — not a guarantee that hand edits will survive. The next clean regeneration will overwrite an unaltered file.

If you need to change a generated bridge, change the source (verity/src/<Contract>.lean) or move the change into a user-owned Solidity file that imports the generated interface.

`bytecode_hash`

The bytecode_hash field in each manifest is the SHA-256 of the creation bytecode file contents. It is the anchor that ties:

the Verity source (which produced the Yul),
the Yul (which produced the bytecode via solc),
the manifest (which records the hash),
the deployer (which embeds the bytes),
the on-chain deployment (which runs them).

tama audit structure rejects any of these going out of sync.

Trust artifacts

Two complementary inputs feed tama audit trust-boundary:

artifacts/trust-probe/axioms.json (schema tama.trust-probe.v1) — the closure of axioms, unsafe declarations, and unresolved names reachable from each @[tama.obligation] theorem, computed via Lean’s collectAxioms.
artifacts/trust-report.json and artifacts/assumption-report.json — Verity compiler outputs that localize unsupported or partially modeled mechanics, unsafe blocks, and unchecked dependency buckets.

Both are required for a release-grade audit, and both must be present before tama audit trust-boundary can succeed.

What `tama clean` removes

artifacts/yul/                src/generated/verity/
artifacts/bytecode/           out/
artifacts/solc-json/          cache/
artifacts/manifest/
artifacts/lean/

Foundry’s out and cache_path honor foundry.toml overrides.

tama clean --deep additionally removes Lake dependency state under .lake/packages.