Implemented LaunchToken and RentableNFT, with vendored dependencies, ABI exports, adversarial tests, and deployment documentation.

Verified with Solidity 0.8.26:

• forge build passes.
• forge test passes: 42 tests, including fuzzing and 8,192 stateful calls.
• forge fmt --check and ABI consistency checks pass.

Assumptions and operational responsibilities are documented in README.md. Independent review, launch.json, deployment, and the frontend remain assigned to later stages.

Wrote launch.json for the accepted Lease launch and verified it against the schema, the exported ABIs, and a Foundry deployment mirroring the protected floor.

What the manifest contains

• Kind is evm_project. Token is LaunchToken, name Lease, symbol LEAS, 18 decimals, no constructor arguments, matching src/LaunchToken.sol.
• One application contract, RentableNFT, with constructorArgs ["$token"]. Its constructor takes a single address named leas, so the reference fills an address-typed argument and points backward to the token.
• Pool pairs against native ETH with fee 3000, tick spacing 60, initialPrice 79228162514264337593543950336, no hook.
• No $owner argument is used because the accepted RentableNFT has no owner, admin, pause or upgrade role.
• Notes describe the accepted behavior, the ERC-4907 deviation on transfers, and that supply, allocations and chain come from policy.

Verification results

• forge build and forge test: 42 tests passed, 0 failed.
• A scratch Python check validated every schema field, the identifier and price patterns, the reference rules, and cross-checked constructor arity and address types against docs/abi/*.json.
• A scratch Foundry test deployed both contracts from a factory address in manifest order and confirmed the full supply stays with the factory, RentableNFT holds zero LEAS, token() points at the launch token, and the runtime has no DELEGATECALL, CALLCODE or SELFDESTRUCT.
• git status shows launch.json as the only new file. Nothing else in the tree changed. Scratch files live under test/scratch and are not submitted.

No substantiated defects found. Wrote {"findings":[]} to .imd-findings.json. No implementation, test, or configuration files changed.

Attack analysis below assumes owner O, renter R with sufficient approved LEAS, buyer B, token ID 1, and p = 10^18. Each sequence starts independently.

• Rental revocation: O.list(1,p) → R.rent(1,10,p). Before expiry, owner or approved-operator calls setUser(1,0,0) or setUser(1,R,expiry-1) revert with TokenInUse. transferFrom and both safeTransferFrom overloads preserve the user and expiry, including during receiver callbacks. O.unlist(1) → O.list(1,2*p) also leaves the rental unchanged.
• Stale listings: O.list(1,p) → O.transferFrom(O,B,1) → R.rent(1,1,p) reverts with NotListed. Transferring back to O does not restore the deleted listing.
• Price front-running: O.list(1,p) → O.list(1,p+1) → R.rent(1,1,p) reverts with PriceAboveMaximum before payment or user assignment.
• Wrong payment recipient: O.list(1,p) → O.transferFrom(O,B,1) → B.list(1,p) → R.rent(1,2,p) pays exactly 2*p directly to B. Neither the previous owner nor the application receives rent.

launch.json correctly supplies ["$token"] to RentableNFT(address leas); LaunchToken() takes no arguments. Neither constructor assigns an administrative role to the factory or another beneficiary.

Reviewed the existing adversarial, fuzz, and invariant assertions. ABI exports match an in-memory Solidity 0.8.26 compilation; manifest schema constraints and applicable refinements pass.

Implemented the Lease frontend and static export with verified ABIs, runtime deployment manifest, and validation evidence.

• Build, typecheck, and all 15 interaction tests passed.
• Desktop/mobile accessibility checks and live RPC reads passed.
• Candidate Git bundle: 1.99 MB, below 8 MiB.
• No live transactions broadcast.

Validation report · Design documentation

Git staging was blocked because .git is read-only; files remain ready for publisher collection. Design documentation is under docs/ to respect the write scope.