Add ExprCompileCore constructors for bitwise ops, prove sorry #1 (5→4 sorries)

- Add bitAnd/bitOr/bitXor/bitNot constructors to ExprCompileCore inductive
- Add eval_compileExpr helpers for all 4 bitwise ops in FunctionBody.lean
- Add cases to mutual blocks (eval_compileExpr_core_onExpr, evalExpr_lt_evmModulus_core_onExpr,
  compileRequireFailCond, eval_compileRequireFailCond)
- Add cases to GenericInduction.lean match statements
- Tighten SupportedSpec.lean surface checks: sdiv/smod/sgt/slt now return true
  (unsupported), matching that ExprCompileCore has no constructors for them
- Prove exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false by
  structural recursion on Expr, eliminating sorry #1

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: claude

Compiler/Proofs/IRGeneration/ExprCore.lean

@@ -111,6 +111,14 @@ inductive ExprCompileCore : Expr → Prop where
       ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.logicalAnd lhs rhs)
   | logicalOr {lhs rhs : Expr} :
       ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.logicalOr lhs rhs)
+  | bitAnd {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitAnd lhs rhs)
+  | bitOr {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitOr lhs rhs)
+  | bitXor {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitXor lhs rhs)
+  | bitNot {expr : Expr} :
+      ExprCompileCore expr → ExprCompileCore (.bitNot expr)
 
 /-! ## Scope analysis -/