tama.toml & tama.lock

`tama.toml`

tama.toml has four roles:

mark the project as a Tama project;
pin the intended Verity framework version;
define Verity/Tama-side paths;
define Yul compilation and audit policy.

Full example:

[project]
name = "my_protocol"
verity = "0.5.0"

[paths]
src = "verity/src"
spec = "verity/spec"
proof = "verity/proof"
mirror_test = "test/verity"
generated_solidity = "src/generated/verity"
out = "artifacts"

[yul]
solc = "0.8.33"
evm_version = "cancun"
optimizer = true
optimizer_runs = 200
yul_optimizer = true
metadata_bytecode_hash = "none"

[trust.allow_axioms]
"Classical.choice" = "accepted Lean classical reasoning"
"Quot.sound"       = "accepted Lean quotient axiom"

`[project]`

Key	Required	Description
`name`	yes	Project name (matches `lakefile.toml`).
`verity`	yes	Verity framework tag or commit. Pinned in lock.

`[paths]`

Optional. Omitted fields fall back to the defaults shown above.

Every path must be a non-empty relative path inside the project. Absolute paths, .. components, and root-collapsing values like . are rejected before Tama writes or removes anything.

When Tama also consumes Foundry paths (src, test, out, cache_path in foundry.toml) for audit and clean behavior, the same project-relative rule applies.

`[yul]`

Key	Default	Description
`solc`	required	`solc` version Tama uses for generated Yul.
`evm_version`	`cancun`	EVM target.
`optimizer`	`true`	Enable the Yul optimizer.
`optimizer_runs`	`200`	Optimizer run count.
`yul_optimizer`	`true`	Enable the standalone Yul optimizer step.
`metadata_bytecode_hash`	`"none"`	Reproducible bytecode by default.

metadata_bytecode_hash = "none" is intentional: it removes the non-deterministic Solidity metadata trailer from the generated bytecode, so the manifest’s recorded hash is reproducible across machines.

`[trust.allow_axioms]`

A map of axiom-name -> reason. Each reason must be a non-empty string.

sorryAx cannot be allowlisted. tama audit trust-boundary denies it unconditionally.

Strict parsing

tama.toml is strict: unknown Tama-owned table names or keys are errors, not warnings. This prevents misspelled compiler or path settings from silently changing build behavior. Foundry-specific settings remain in foundry.toml and are parsed by Foundry.

`tama.lock`

Resolved state for reproducible builds. Tama writes it on init, refreshes it after a successful build, validates it under --locked, and reports drift via doctor.

version = 1

[resolved]
verity_version = "0.5.0"
verity_git     = "https://github.com/lfglabs-dev/verity"
verity_rev     = "3a6f..."
lean_toolchain = "leanprover/lean4:v4.22.0"
solc           = "0.8.33"
solc_sha256    = "..."

[inputs]
tama_toml_sha256      = "..."
lakefile_toml_sha256  = "..."
lake_manifest_sha256  = "..."
foundry_toml_sha256   = "..."

[yul]
evm_version            = "cancun"
optimizer              = true
optimizer_runs         = 200
yul_optimizer          = true
metadata_bytecode_hash = "none"

[resolved.lake]
"verity"        = { rev = "3a6f...", url = "https://github.com/lfglabs-dev/verity" }
"verity-erc20"  = { rev = "1c2d...", url = "https://github.com/lfglabs-dev/verity-erc20" }

Rules

tama init writes the initial lockfile.
tama build refreshes the lockfile after a successful build.
tama build --locked (and CI) fails if the lockfile or any tracked input is stale.
tama update recomputes the lockfile after refreshing dependencies.
tama doctor reports drift; tama doctor --fix may apply narrow, formatting-preserving repairs.

`[resolved.lake]`

Direct git packages from lake-manifest.json are recorded here so the lock captures Lake’s actual resolved commit, not just the requested branch or tag in lakefile.toml.

Relationship to other configs

File	Owned by	Purpose
`tama.toml`	You	Verity pin, paths, Yul, audit policy
`tama.lock`	Tama	Resolved versions and input hashes
`foundry.toml`	You	Solidity compiler, fuzz, profiles, RPC, etc.
`lakefile.toml`	You (after `tama init`)	Lake build targets and Lean dependencies
`lake-manifest.json`	Lake	Resolved Lake dependency graph
`lean-toolchain`	You	Pinned Lean toolchain

Tama does not read foundry.toml to configure Yul. Foundry does not read tama.toml. The two share the project on disk, not in memory.