Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generate rewrite relation #4745

Merged
merged 16 commits into from
Jan 27, 2025
Merged

Conversation

tothtamas28
Copy link
Contributor

Closes #4728

Generates an inductive type Rewrites : GeneratedTopCell -> GeneratedTopCell -> Prop where each constructor (except for the first one which expresses transitivity) encodes a K rewrite rule.

Each constructor has the following signature:

  • An implicit binder for each free variable.
  • An explicit binder for each function application which expresses definedness of the function over the arguments.
  • An explicit binder for the requires clause.
  • The type Rewrites <lhs> <rhs>.

@rv-jenkins rv-jenkins changed the base branch from master to develop January 22, 2025 16:19
@tothtamas28 tothtamas28 force-pushed the rewrite-relation branch 3 times, most recently from b2c798c to ea1e82e Compare January 24, 2025 10:51
@tothtamas28 tothtamas28 changed the base branch from develop to update-deps January 24, 2025 10:51
@tothtamas28 tothtamas28 changed the base branch from update-deps to develop January 24, 2025 10:51
@tothtamas28
Copy link
Contributor Author

The Rewrites type definition generated for evm-semantics.llvm compiles in about 20 mins (after imports, patching ite and setting set_option maxHeartbeats 10000000).

Rewrite.txt

@tothtamas28 tothtamas28 self-assigned this Jan 24, 2025
@tothtamas28 tothtamas28 requested a review from JuanCoRo January 24, 2025 11:35
@tothtamas28 tothtamas28 marked this pull request as ready for review January 24, 2025 11:35
@JuanCoRo
Copy link
Member

Where do the names of rewrite rules such as _43a65b8 come from?

@JuanCoRo
Copy link
Member

Where do the names of rewrite rules such as _43a65b8 come from?

I guess from unnamed rules. But maybe it's better to have something like ruleN where N is the counter of how many rules there are. Otherwise proving things with this can get more convoluted.

A related question: Even if we named all rules in K definitions, will there be generated rules by the compiler that we cannot name?

@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Jan 24, 2025

Where do the names of rewrite rules such as _43a65b8 come from?

It's a prefix of the UNIQUE-ID generated by the frontend for each rule.

But maybe it's better to have something like ruleN where N is the counter of how many rules there are.

I can make that change, but that'll make it significantly harder to manually trace back and forth between K and Lean source. Right now you can look up the source and UNIQUE-ID attributes from compiled.txt or definition.kore, which provides the mapping. And it's easier to search for a unique string in those files then to navigate to the n-th match of a regex identifying rule axioms.

A related question: Even if we named all rules in K definitions, will there be generated rules by the compiler that we cannot name?

The only frontend-generated rules I can think of are heating-cooling rules, but they seem to have a label. Still, it's possible there are unlabeled generated rules.

@JuanCoRo
Copy link
Member

It's a prefix of the UNIQUE-ID generated by the frontend for each rule.

Is it correct that the frontend will generate such UNIQUE-ID if the rule is unnamed? If so, perhaps we should name all rules for a better Lean 4 user experience.

that'll make it significantly harder to manually trace back and forth between K and Lean source

Makes sense! Let's leave it like this then.

@tothtamas28
Copy link
Contributor Author

Is it correct that the frontend will generate such UNIQUE-ID if the rule is unnamed?

Yes, the UNIQUE-ID is generated for all rules.

perhaps we should name all rules for a better Lean 4 user experience.

That would be ideal, I agree. Similarly, all symbol productions should have the symbol attribute to avoid KORE symbol names like

_________EVM_InternalOp_CallOp_Int_Int_Int_Int_Int_Int_Int

@JuanCoRo
Copy link
Member

Would it require much work to indent the parameters of the rules? Currently they are written in a single line, which makes it hard to parse. A candidate style for indenting the parameters of a rule could be the following, although it would generate a lot more lines:

Optimized ADD rule definition
inductive Rewrites : SortGeneratedTopCell → SortGeneratedTopCell → Prop where
  | tran
      {s1 s2 s3 : SortGeneratedTopCell}
      (t1 : Rewrites s1 s2)
      (t2 : Rewrites s2 s3)
      : Rewrites s1 s3
  | EVM_OPTIMIZATIONS_optimized_add
      {GAVAIL _Val11 : SortGas}
      {PCOUNT W0 W1 _Val7 _Val8 : SortInt}
      {SCHED : SortSchedule}
      {USEGAS _Val5 : SortBool}
      {WS : SortWordStack}
      {_DotVar0 : SortGeneratedCounterCell}
      {_DotVar2 : SortK}
      {_DotVar3 : SortNetworkCell}
      {_Gen0 : SortProgramCell}
      {_Gen1 : SortJumpDestsCell}
      {_Gen10 : SortCallDepthCell}
      {_Gen11 : SortOutputCell}
      {_Gen12 : SortStatusCodeCell}
      {_Gen13 : SortCallStackCell}
      {_Gen14 : SortInterimStatesCell}
      {_Gen15 : SortTouchedAccountsCell}
      {_Gen16 : SortSubstateCell}
      {_Gen17 : SortGasPriceCell}
      {_Gen18 : SortOriginCell}
      {_Gen19 : SortBlockhashesCell}
      {_Gen2 : SortIdCell}
      {_Gen20 : SortBlockCell}
      {_Gen21 : SortExitCodeCell}
      {_Gen22 : SortModeCell}
      {_Gen3 : SortCallerCell}
      {_Gen4 : SortCallDataCell}
      {_Gen5 : SortCallValueCell}
      {_Gen6 : SortLocalMemCell}
      {_Gen7 : SortMemoryUsedCell}
      {_Gen8 : SortCallGasCell}
      {_Gen9 : SortStaticCell}
      (defn_Val0 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» (SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst) SCHED = some _Val0)
      (defn_Val1 : «_<=Gas__GAS-SYNTAX_Bool_Gas_Gas» ((@inj SortInt SortGas) _Val0) GAVAIL = some _Val1)
      (defn_Val2 : kite USEGAS _Val1 true = some _Val2)
      (defn_Val3 : «#sizeWordStack» WS = some _Val3)
      (defn_Val4 : «_<=Int_» _Val3 1023 = some _Val4)
      (defn_Val5 : _andBool_ _Val2 _Val4 = some _Val5)
      (defn_Val6 : «_+Int_» W0 W1 = some _Val6)
      (defn_Val7 : chop _Val6 = some _Val7)
      (defn_Val8 : «_+Int_» PCOUNT 1 = some _Val8)
      (defn_Val9 : «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» (SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst) SCHED = some _Val9)
      (defn_Val10 : «_-Gas__GAS-SYNTAX_Gas_Gas_Gas» GAVAIL ((@inj SortInt SortGas) _Val9) = some _Val10)
      (defn_Val11 : kite USEGAS _Val10 GAVAIL = some _Val11) (req : _Val5 = true) : Rewrites
      { kevm := {
          k := { val := SortK.kseq ((@inj SortInternalOp SortKItem) (SortInternalOp.«#next[_]_EVM_InternalOp_MaybeOpCode» ((@inj SortBinStackOp SortMaybeOpCode) (SortBinStackOp.ADD_EVM_BinStackOp)))) _DotVar2 },
          exitCode := _Gen21,
          mode := _Gen22,
          schedule := { val := SCHED },
          useGas := { val := USEGAS },
          ethereum := {
            evm := {
              output := _Gen11,
              statusCode := _Gen12,
              callStack := _Gen13,
              interimStates := _Gen14,
              touchedAccounts := _Gen15,
              callState := { program := _Gen0,
                             jumpDests := _Gen1,
                             id := _Gen2,
                             caller := _Gen3,
                             callData := _Gen4,
                             callValue := _Gen5,
                             wordStack := { val := SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» W0 (SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» W1 WS) },
                             localMem := _Gen6,
                             pc := { val := PCOUNT },
                             gas := { val := GAVAIL },
                             memoryUsed := _Gen7,
                             callGas := _Gen8,
                             static := _Gen9,
                             callDepth := _Gen10 },
                substate := _Gen16,
                gasPrice := _Gen17,
                origin := _Gen18,
                blockhashes := _Gen19,
                block := _Gen20 },
              network := _DotVar3 } },
          generatedCounter := _DotVar0 }
      { kevm := {
        k := { val := _DotVar2 },
        exitCode := _Gen21,
        mode := _Gen22,
        schedule := { val := SCHED },
        useGas := { val := USEGAS },
        ethereum := {
          evm := {
            output := _Gen11,
            statusCode := _Gen12,
            callStack := _Gen13,
            interimStates := _Gen14,
            touchedAccounts := _Gen15,
            callState := { program := _Gen0,
                           jumpDests := _Gen1,
                           id := _Gen2,
                           caller := _Gen3,
                           callData := _Gen4,
                           callValue := _Gen5,
                           wordStack := { val := SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Val7 WS },
                           localMem := _Gen6,
                           pc := { val := _Val8 },
                           gas := { val := _Val11 },
                           memoryUsed := _Gen7,
                           callGas := _Gen8,
                           static := _Gen9,
                           callDepth := _Gen10 },
                           substate := _Gen16,
                           gasPrice := _Gen17,
                           origin := _Gen18,
                           blockhashes := _Gen19,
                           block := _Gen20 },
          network := _DotVar3 } },
        generatedCounter := _DotVar0 }

@tothtamas28
Copy link
Contributor Author

Would it require much work to indent the parameters of the rules? Currently they are written in a single line, which makes it hard to parse.

Let's open an issue for this. My hope is we don't need to address this in the generator, but can pipe the generated output through some existing code formatter for Lean.

@JuanCoRo
Copy link
Member

JuanCoRo commented Jan 24, 2025

Opened #4747

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit e85cda0 into develop Jan 27, 2025
18 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the rewrite-relation branch January 27, 2025 12:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Generate rewrite rules
2 participants