|
| 1 | +{ |
| 2 | + "schema_version": 1, |
| 3 | + "description": "Authoritative ownership and proof-boundary status for major Verity feature surfaces. Use this to distinguish source syntax, compiler lowering, proof coverage, trust reporting, and compatibility shims.", |
| 4 | + "status_values": [ |
| 5 | + "supported", |
| 6 | + "partial", |
| 7 | + "unsupported", |
| 8 | + "not_applicable" |
| 9 | + ], |
| 10 | + "surfaces": [ |
| 11 | + { |
| 12 | + "id": "source_internal_helpers", |
| 13 | + "name": "Source-level internal helper functions", |
| 14 | + "owner": "Verity.Macro / Compiler.CompilationModel / Compiler.Proofs.SourceSemantics", |
| 15 | + "source_supported": "supported", |
| 16 | + "compile_supported": "supported", |
| 17 | + "proof_modeled": "partial", |
| 18 | + "trust_reported": "not_applicable", |
| 19 | + "deprecated": false, |
| 20 | + "canonical_entrypoints": [ |
| 21 | + "Verity/Macro/Translate.lean", |
| 22 | + "Compiler/CompilationModel.lean", |
| 23 | + "Compiler/Proofs/SourceSemantics.lean" |
| 24 | + ], |
| 25 | + "notes": "Internal helpers stay out of ABI dispatch. Helper-summary reuse is available in source-semantics lemmas but is not yet fully consumed through the generic body/IR theorem path." |
| 26 | + }, |
| 27 | + { |
| 28 | + "id": "typed_external_interface_calls", |
| 29 | + "name": "Typed external interface calls", |
| 30 | + "owner": "Verity.Macro / Compiler.Modules.Calls", |
| 31 | + "source_supported": "supported", |
| 32 | + "compile_supported": "supported", |
| 33 | + "proof_modeled": "unsupported", |
| 34 | + "trust_reported": "supported", |
| 35 | + "deprecated": false, |
| 36 | + "canonical_entrypoints": [ |
| 37 | + "Verity/Macro/Translate.lean", |
| 38 | + "Compiler/Modules/Calls.lean", |
| 39 | + "docs/EXTERNAL_CALL_MODULES.md" |
| 40 | + ], |
| 41 | + "notes": "Interface dot calls lower through the standard ABI-call ECM surface and remain explicit trust-report entries." |
| 42 | + }, |
| 43 | + { |
| 44 | + "id": "low_level_call_returndata", |
| 45 | + "name": "Low-level calls and returndata mechanics", |
| 46 | + "owner": "Compiler.CompilationModel / Compiler.Modules.Calls", |
| 47 | + "source_supported": "partial", |
| 48 | + "compile_supported": "supported", |
| 49 | + "proof_modeled": "unsupported", |
| 50 | + "trust_reported": "supported", |
| 51 | + "deprecated": false, |
| 52 | + "canonical_entrypoints": [ |
| 53 | + "Compiler/CompilationModel.lean", |
| 54 | + "Compiler/CompilationModel/Compile.lean", |
| 55 | + "Compiler/Modules/Calls.lean", |
| 56 | + "docs/INTERPRETER_FEATURE_MATRIX.md" |
| 57 | + ], |
| 58 | + "notes": "call/staticcall/delegatecall and returndata plumbing are compiler-supported and tested, but outside proof interpreters." |
| 59 | + }, |
| 60 | + { |
| 61 | + "id": "constructors_fallback_receive", |
| 62 | + "name": "Constructors, fallback, and receive", |
| 63 | + "owner": "Verity.Macro / Compiler.CompilationModel", |
| 64 | + "source_supported": "partial", |
| 65 | + "compile_supported": "partial", |
| 66 | + "proof_modeled": "partial", |
| 67 | + "trust_reported": "supported", |
| 68 | + "deprecated": false, |
| 69 | + "canonical_entrypoints": [ |
| 70 | + "Verity/Macro/Translate.lean", |
| 71 | + "Compiler/CompilationModel.lean", |
| 72 | + "docs/VERIFICATION_STATUS.md" |
| 73 | + ], |
| 74 | + "notes": "Constructor and special-entrypoint syntax exists, but the generic proof fragment only covers selected initialization and entrypoint shapes." |
| 75 | + }, |
| 76 | + { |
| 77 | + "id": "events_logs_typed_errors", |
| 78 | + "name": "Events, logs, and typed errors", |
| 79 | + "owner": "Verity.Macro / Compiler.CompilationModel", |
| 80 | + "source_supported": "supported", |
| 81 | + "compile_supported": "supported", |
| 82 | + "proof_modeled": "partial", |
| 83 | + "trust_reported": "supported", |
| 84 | + "deprecated": false, |
| 85 | + "canonical_entrypoints": [ |
| 86 | + "Verity/Macro/Translate.lean", |
| 87 | + "Compiler/CompilationModel/Compile.lean", |
| 88 | + "docs/EXTERNAL_CALL_MODULES.md" |
| 89 | + ], |
| 90 | + "notes": "User-facing forms compile, while raw logs and richer ABI payload mechanics remain proof-boundary surfaces." |
| 91 | + }, |
| 92 | + { |
| 93 | + "id": "rich_storage_layout", |
| 94 | + "name": "Rich storage layout features", |
| 95 | + "owner": "Verity.Macro / Compiler.CompilationModel", |
| 96 | + "source_supported": "partial", |
| 97 | + "compile_supported": "partial", |
| 98 | + "proof_modeled": "partial", |
| 99 | + "trust_reported": "supported", |
| 100 | + "deprecated": false, |
| 101 | + "canonical_entrypoints": [ |
| 102 | + "Verity/Macro/Translate.lean", |
| 103 | + "Compiler/CompilationModel/StorageLayout.lean", |
| 104 | + "docs/SOLIDITY_PARITY_PROFILE.md" |
| 105 | + ], |
| 106 | + "notes": "Many scalar, mapping, struct, packed-word, and ERC-7201 forms are present, but compatibility layout features are not all inside the generic proof fragment." |
| 107 | + }, |
| 108 | + { |
| 109 | + "id": "foreach_positive_nonempty", |
| 110 | + "name": "Positive non-empty forEach bodies", |
| 111 | + "owner": "Compiler.Proofs.IRGeneration", |
| 112 | + "source_supported": "supported", |
| 113 | + "compile_supported": "supported", |
| 114 | + "proof_modeled": "partial", |
| 115 | + "trust_reported": "not_applicable", |
| 116 | + "deprecated": false, |
| 117 | + "canonical_entrypoints": [ |
| 118 | + "Compiler/Proofs/IRGeneration/GenericInduction.lean", |
| 119 | + "artifacts/layer2_boundary_catalog.json", |
| 120 | + "docs/VERIFICATION_STATUS.md" |
| 121 | + ], |
| 122 | + "notes": "Zero-bound supported bodies and literal-bound empty bodies are covered. Positive non-empty loop bodies remain outside the current generic theorem." |
| 123 | + }, |
| 124 | + { |
| 125 | + "id": "legacy_spec_aliases", |
| 126 | + "name": "Legacy CompilationModel spec aliases", |
| 127 | + "owner": "Contracts.Legacy", |
| 128 | + "source_supported": "not_applicable", |
| 129 | + "compile_supported": "supported", |
| 130 | + "proof_modeled": "not_applicable", |
| 131 | + "trust_reported": "not_applicable", |
| 132 | + "deprecated": true, |
| 133 | + "canonical_entrypoints": [ |
| 134 | + "Contracts/Legacy/SpecAliases.lean", |
| 135 | + "Contracts/SpecAliases.lean" |
| 136 | + ], |
| 137 | + "notes": "Historical names remain available through a compatibility namespace. New code should import the canonical contract module and use Contracts.<Name>.spec directly." |
| 138 | + }, |
| 139 | + { |
| 140 | + "id": "patched_compiler_entrypoint", |
| 141 | + "name": "Patch-enabled compiler binary", |
| 142 | + "owner": "Compiler.MainPatched", |
| 143 | + "source_supported": "not_applicable", |
| 144 | + "compile_supported": "supported", |
| 145 | + "proof_modeled": "not_applicable", |
| 146 | + "trust_reported": "supported", |
| 147 | + "deprecated": false, |
| 148 | + "canonical_entrypoints": [ |
| 149 | + "Compiler/Main.lean", |
| 150 | + "Compiler/MainPatched.lean", |
| 151 | + "lakefile.lean", |
| 152 | + "packages/verity-compiler/lakefile.lean" |
| 153 | + ], |
| 154 | + "notes": "The canonical compiler binary is Compiler.Main / verity-compiler. MainPatched remains as the intentionally separate parity and patch-enabled binary." |
| 155 | + }, |
| 156 | + { |
| 157 | + "id": "external_call_with_return_ecm_name", |
| 158 | + "name": "externalCallWithReturn ECM module name", |
| 159 | + "owner": "Compiler.Modules.Calls", |
| 160 | + "source_supported": "not_applicable", |
| 161 | + "compile_supported": "supported", |
| 162 | + "proof_modeled": "unsupported", |
| 163 | + "trust_reported": "supported", |
| 164 | + "deprecated": true, |
| 165 | + "canonical_entrypoints": [ |
| 166 | + "Compiler/Modules/Calls.lean", |
| 167 | + "docs/EXTERNAL_CALL_MODULES.md" |
| 168 | + ], |
| 169 | + "notes": "The public API is Calls.withReturn / Calls.withReturnModule. The old module name remains in emitted metadata for compatibility and should be migrated in a future focused PR." |
| 170 | + } |
| 171 | + ] |
| 172 | +} |
0 commit comments