LLZK 2.1.1
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
Public Member Functions | List of all members
llzk::verif::detail::ForbiddenInfluenceAnalyzer Class Reference

Interprocedural verifier-local analysis for forbidden precondition influence. More...

#include <ForbiddenPreconditionInfluence.h>

Public Member Functions

 ForbiddenInfluenceAnalyzer (mlir::ModuleOp owningModule)
 Create a verifier-local analyzer for one LLZK module.
InfluenceInfo analyzeContractValue (verif::ContractOp contract, mlir::Value value)
 Classify the forbidden influence reaching a value inside a contract body.
InfluenceInfo analyzePreconditionOp (verif::ContractOp contract, verif::PreconditionOpInterface preCondOp)
 Classify the forbidden influence reaching a precondition op, including both the condition operand and any enclosing SCF control ancestors.
InfluenceInfo analyzeCallableResult (mlir::CallableOpInterface callableOp, llvm::ArrayRef< InfluenceInfo > argInfluences, unsigned resultNumber)
 Summarize the forbidden influence of one callable result under the given argument influences.
IncludedContractSummary analyzeIncludedContract (verif::ContractOp calleeContract, llvm::ArrayRef< InfluenceInfo > argInfluences, InfluenceInfo inheritedControlInfluence=InfluenceInfo::None())
 Check whether an included contract becomes invalid under caller-provided operand influences, returning every failing callee precondition if so.
IncludedContractSummary analyzeIncludedOp (verif::ContractOp contract, verif::IncludeOp includeOp)
 Check whether an include op becomes invalid under its caller's operand bindings and enclosing SCF control ancestors.

Detailed Description

Interprocedural verifier-local analysis for forbidden precondition influence.

This analysis answers a narrow policy question for verif.require_*: whether an SSA value may depend, through data flow or SCF control flow, on struct members or target-function return values. It computes memoized callable summaries so helper calls can be checked transitively without extending the general-purpose SourceRefAnalysis.

Definition at line 225 of file ForbiddenPreconditionInfluence.h.

Constructor & Destructor Documentation

◆ ForbiddenInfluenceAnalyzer()

llzk::verif::detail::ForbiddenInfluenceAnalyzer::ForbiddenInfluenceAnalyzer ( mlir::ModuleOp owningModule)
inlineexplicit

Create a verifier-local analyzer for one LLZK module.

Definition at line 228 of file ForbiddenPreconditionInfluence.h.

Member Function Documentation

◆ analyzeCallableResult()

InfluenceInfo ForbiddenInfluenceAnalyzer::analyzeCallableResult ( mlir::CallableOpInterface callableOp,
llvm::ArrayRef< InfluenceInfo > argInfluences,
unsigned resultNumber )

Summarize the forbidden influence of one callable result under the given argument influences.

Definition at line 336 of file ForbiddenPreconditionInfluence.cpp.

◆ analyzeContractValue()

InfluenceInfo ForbiddenInfluenceAnalyzer::analyzeContractValue ( verif::ContractOp contract,
mlir::Value value )

Classify the forbidden influence reaching a value inside a contract body.

Definition at line 307 of file ForbiddenPreconditionInfluence.cpp.

◆ analyzeIncludedContract()

IncludedContractSummary ForbiddenInfluenceAnalyzer::analyzeIncludedContract ( verif::ContractOp calleeContract,
llvm::ArrayRef< InfluenceInfo > argInfluences,
InfluenceInfo inheritedControlInfluence = InfluenceInfo::None() )

Check whether an included contract becomes invalid under caller-provided operand influences, returning every failing callee precondition if so.

Definition at line 370 of file ForbiddenPreconditionInfluence.cpp.

◆ analyzeIncludedOp()

IncludedContractSummary ForbiddenInfluenceAnalyzer::analyzeIncludedOp ( verif::ContractOp contract,
verif::IncludeOp includeOp )

Check whether an include op becomes invalid under its caller's operand bindings and enclosing SCF control ancestors.

Definition at line 417 of file ForbiddenPreconditionInfluence.cpp.

◆ analyzePreconditionOp()

InfluenceInfo ForbiddenInfluenceAnalyzer::analyzePreconditionOp ( verif::ContractOp contract,
verif::PreconditionOpInterface preCondOp )

Classify the forbidden influence reaching a precondition op, including both the condition operand and any enclosing SCF control ancestors.

Definition at line 320 of file ForbiddenPreconditionInfluence.cpp.

The documentation for this class was generated from the following files: