Skip to content

TESTS_OUTSOURCE.md

Latest commit

 

History

History
1540 lines (1292 loc) · 58.8 KB

TESTS_OUTSOURCE.md

File metadata and controls

1540 lines (1292 loc) · 58.8 KB
Raw

Test Specifications: TrustHash v4.0.1

Generated: 2026-03-12T00:00:00Z Project: /Users/manuelpuebla/Documents/claudio/TrustHash Toolchain: leanprover/lean4:v4.16.0 Mathlib: no

Este archivo es leido por otra sesion de Claude Code que escribe los archivos .lean de test. NO contiene codigo compilable.

Instrucciones para la sesion de testing

  1. Leer este archivo completo
  2. Para cada nodo, leer el codigo fuente real (scout.py + Read)
  3. Escribir Tests/Properties/{NodeName}.lean con las propiedades especificadas
  4. Escribir Tests/Integration/{NodeName}.lean con los integration tests
  5. Compilar cada archivo con lake env lean Tests/.../*.lean hasta que pase
  6. Usar /ask-lean o /ask-dojo si faltan tacticas o instancias

Convenciones obligatorias

Properties (Tests/Properties/{Name}.lean):

  • NO Mathlib -- NO SlimCheck available. Use #eval with Bool-returning functions instead
  • Each property as def prop_name : Bool := ... then #eval prop_name expecting true
  • Comment with priority: -- P0, INVARIANT: descripcion

Integration (Tests/Integration/{Name}.lean):

  • Each test prints [PASS] nombre or [FAIL] nombre
  • Function main : IO UInt32 that returns 0 if all pass, 1 if failures
  • Pattern: def T1_name : IO Bool := do ...

Ejecucion (la hace la sesion implementadora)

python3 ~/.claude/skills/plan-project/scripts/close_block.py \
  --project PATH --block "Bloque N" --nodes '{...}'

Especificaciones por nodo

N42.1 -- HashOp type + NodeOps instance

  • Tipo: FUNDACIONAL
  • Archivos fuente: TrustHash/HashOp.lean
  • Target properties: Tests/Properties/HashOp.lean
  • Target integration: Tests/Integration/HashOp.lean
  • Properties: 6 (3 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 INVARIANT: children length equals arity for all constructors Sketch: def prop_children_arity_sbox : Bool := (HashOp.sboxApply 0 3).children.length == (HashOp.sboxApply 0 3).arity (repeat for constOp, varOp, addRoundKey, compose, roundFunc, keccakChi [0,1,2], keccakTheta [0,1], keccakRhoPi, keccakIota) def prop_children_eq_arity : Bool := (HashOp.constOp 42).children.length == (HashOp.constOp 42).arity && (HashOp.varOp 0).children.length == (HashOp.varOp 0).arity && (HashOp.sboxApply 0 3).children.length == (HashOp.sboxApply 0 3).arity && (HashOp.addRoundKey 0 1).children.length == (HashOp.addRoundKey 0 1).arity && (HashOp.compose 0 1).children.length == (HashOp.compose 0 1).arity && (HashOp.roundFunc 0 5).children.length == (HashOp.roundFunc 0 5).arity && (HashOp.keccakRhoPi 0 1).children.length == (HashOp.keccakRhoPi 0 1).arity && (HashOp.keccakIota 0 7).children.length == (HashOp.keccakIota 0 7).arity SampleableExt: no Risk: arity/children inconsistency would break reconstruction

  • [P2] P0 INVARIANT: leaf constructors have zero children Sketch: def prop_leaves_no_children : Bool := (HashOp.constOp 0).children.length == 0 && (HashOp.constOp 99).children.length == 0 && (HashOp.varOp 0).children.length == 0 && (HashOp.varOp 42).children.length == 0 SampleableExt: no Risk: non-empty children on leaves would corrupt e-graph extraction

  • [P3] P0 INVARIANT: role classification is exhaustive and correct Sketch: def prop_role_classification : Bool := (HashOp.sboxApply 0 3).role == .nonlinear && (HashOp.keccakChi [0,1]).role == .nonlinear && (HashOp.mdsMix [0] 4).role == .linear && (HashOp.keccakTheta [0,1]).role == .linear && (HashOp.keccakRhoPi 0 1).role == .linear && (HashOp.addRoundKey 0 1).role == .keyAdd && (HashOp.keccakIota 0 7).role == .keyAdd && (HashOp.compose 0 1).role == .structural && (HashOp.roundFunc 0 5).role == .structural && (HashOp.constOp 0).role == .leaf && (HashOp.varOp 0).role == .leaf SampleableExt: no Risk: misclassified role could corrupt degree tracking and security analysis

  • [P4] P1 EVAL: evalHashOp preserves semantics on concrete values Sketch: def prop_eval_concrete : Bool := evalHashOp (.sboxApply 0 3) [2] (fun _ => 0) == 8 && evalHashOp (.addRoundKey 0 1) [3, 5] (fun _ => 0) == 8 && evalHashOp (.compose 0 1) [4, 7] (fun _ => 0) == 28 && evalHashOp (.constOp 42) [] (fun _ => 0) == 42 && evalHashOp (.varOp 0) [] (fun i => i + 10) == 10 && evalHashOp (.keccakRhoPi 0 5) [7] (fun _ => 0) == 7 && evalHashOp (.keccakIota 0 3) [10] (fun _ => 0) == 13 SampleableExt: no Risk: evaluation bug silently propagates through soundness chain

  • [P5] P1 DEGREE: algDegree matches expected values for all constructors Sketch: def prop_algDegree : Bool := (HashOp.sboxApply 0 7).algDegree == 7 && (HashOp.sboxApply 0 3).algDegree == 3 && (HashOp.keccakChi [0]).algDegree == 2 && (HashOp.mdsMix [0] 1).algDegree == 1 && (HashOp.keccakTheta [0]).algDegree == 1 && (HashOp.addRoundKey 0 1).algDegree == 1 && (HashOp.constOp 0).algDegree == 0 && (HashOp.varOp 0).algDegree == 1 && (HashOp.roundFunc 0 10).algDegree == 10 SampleableExt: no Risk: incorrect degree would corrupt algebraic security analysis

  • [P6] P2 RECONSTRUCT: reconstruction from correct children succeeds Sketch: def prop_reconstruct_success : Bool := (reconstructHashExpr (.sboxApply 0 3) [.leaf 1]).isSome && (reconstructHashExpr (.addRoundKey 0 1) [.leaf 1, .leaf 2]).isSome && (reconstructHashExpr (.compose 0 1) [.var 0, .var 1]).isSome && (reconstructHashExpr (.constOp 42) []).isSome && (reconstructHashExpr (.varOp 0) []).isSome && (reconstructHashExpr (.keccakRhoPi 0 5) [.var 0]).isSome && (reconstructHashExpr (.keccakIota 0 3) [.var 0]).isSome && (reconstructHashExpr (.keccakChi [0,1]) [.var 0, .var 1]).isSome SampleableExt: no Risk: reconstruction failure blocks extraction pipeline

INTEGRATION:

  • [T1] BASIC: children extraction for all 11 HashOp constructors Setup: construct one instance of each constructor with concrete ClassRef values Check: children lists match expected values (compare List Nat equality)

  • [T2] BASIC: eval round-trip: evalHashOp with known inputs gives expected outputs Setup: sboxApply with input=2, degree=3; addRoundKey with 10,20; compose with 3,4 Check: results are 8, 30, 12 respectively

  • [T3] MEDIUM: reconstruction + eval consistency: reconstruct then eval matches evalHashOp Setup: for sboxApply 0 3 with child [.leaf 5], reconstruct then eval with id env Check: reconstructed expr eval == evalHashOp (.sboxApply 0 3) [5] id

  • [T4] MEDIUM: toAlgExpr round-trip: HashExprF.toAlgExpr produces correct AlgExpr evaluation Setup: build .sbox (.leaf 2) 3, evaluate toAlgExpr and HashExprF.eval Check: both produce same Nat value (8)

  • [T5] EDGE: wrong arity reconstruction fails: sbox with 0 or 2 children gives none Setup: reconstructHashExpr (.sboxApply 0 3) [] and (.sboxApply 0 3) [.leaf 1, .leaf 2] Check: both return none

BRIDGE:

  • [B1] CHECK: #check @evalHashOp
  • [B2] CHECK: #check @reconstructHashExpr
  • [B3] CHECK: #check @HashOp.role
  • [B4] CHECK: #check @HashOp.algDegree
  • [B5] WITNESS: children_constOp -- rfl proof, verify constOp 42 children = []

N42.2 -- HashExpr + Extractable + EvalExpr + ExtractableSound

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/HashExpr.lean
  • Target properties: Tests/Properties/HashExpr.lean
  • Target integration: Tests/Integration/HashExpr.lean
  • Properties: 5 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 INVARIANT: depth of leaf/var is zero, sbox/comp increases by 1 Sketch: def prop_depth_structure : Bool := HashExprF.depth (.leaf 0) == 0 && HashExprF.depth (.var 0) == 0 && HashExprF.depth (.sbox (.leaf 0) 3) == 1 && HashExprF.depth (.comp (.leaf 0) (.leaf 1)) == 1 && HashExprF.depth (.sbox (.sbox (.leaf 0) 3) 7) == 2 && HashExprF.depth (.ark (.sbox (.leaf 0) 3) (.leaf 1)) == 2 SampleableExt: no Risk: depth miscalculation would corrupt saturation depth-reduction claims

  • [P2] P0 INVARIANT: size is always >= 1 for any expression Sketch: def prop_size_pos : Bool := HashExprF.size (.leaf 0) >= 1 && HashExprF.size (.var 0) >= 1 && HashExprF.size (.sbox (.leaf 0) 3) >= 1 && HashExprF.size (.ark (.leaf 0) (.leaf 1)) >= 1 && HashExprF.size (.comp (.sbox (.var 0) 3) (.leaf 1)) >= 1 SampleableExt: no Risk: zero-size expression could break termination arguments

  • [P3] P1 EVAL: HashExprF.eval matches expected values Sketch: def prop_eval_correct : Bool := let env := fun i => i + 1 (.leaf 42 : HashExprF).eval env == 42 && (.var 0 : HashExprF).eval env == 1 && (.var 5 : HashExprF).eval env == 6 && (.sbox (.leaf 2) 3 : HashExprF).eval env == 8 && (.ark (.leaf 3) (.leaf 5) : HashExprF).eval env == 8 && (.comp (.leaf 3) (.leaf 4) : HashExprF).eval env == 12 && (.rhoPi (.leaf 7) 99 : HashExprF).eval env == 7 && (.iota (.leaf 10) 3 : HashExprF).eval env == 13 SampleableExt: no Risk: evaluation semantics bug propagates through soundness

  • [P4] P1 EXTRACT: extractF succeeds on leaf/var with fuel 1 Sketch: def prop_extractF_leaf : Bool := let classes := fun i => if i == 0 then some { bestOp := some (.constOp 42), childClasses := [] : EGraphClass } else none (extractF classes 0 1) == some (.leaf 42) def prop_extractF_var : Bool := let classes := fun i => if i == 0 then some { bestOp := some (.varOp 5), childClasses := [] : EGraphClass } else none (extractF classes 0 1) == some (.var 5) SampleableExt: no Risk: extraction failure blocks entire pipeline

  • [P5] P2 EXTRACT: extractF with zero fuel always returns none Sketch: def prop_extractF_zero_fuel : Bool := let classes := fun _ => some { bestOp := some (.constOp 0), childClasses := [] : EGraphClass } (extractF classes 0 0).isNone && (extractF classes 1 0).isNone && (extractF classes 99 0).isNone SampleableExt: no Risk: non-none at zero fuel would violate fuel semantics

INTEGRATION:

  • [T1] BASIC: depth computation on nested expressions Setup: build .sbox (.sbox (.ark (.var 0) (.var 1)) 3) 1 (depth should be 3) Check: depth == 3

  • [T2] BASIC: size computation on known tree Setup: .ark (.leaf 0) (.leaf 1) has 3 nodes Check: size == 3

  • [T3] MEDIUM: Extractable instance works: reconstruct via typeclass Setup: Extractable.reconstruct (.constOp 42) ([] : List HashExprF) Check: result == some (.leaf 42)

  • [T4] MEDIUM: EvalExpr instance works: evalExpr via typeclass Setup: EvalExpr.evalExpr (.leaf 42) (fun _ => 0) Check: result == 42

BRIDGE:

  • [B1] CHECK: #check @Extractable.reconstruct HashOp HashExprF
  • [B2] CHECK: #check @EvalExpr.evalExpr HashExprF Nat
  • [B3] CHECK: #check @extractF
  • [B4] WITNESS: extractF_constOp -- extraction succeeds for constOp leaf

N42.3 -- SboxCertifiedParams

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/Sbox/SboxCertifiedParams.lean
  • Target properties: Tests/Properties/SboxCertifiedParams.lean
  • Target integration: Tests/Integration/SboxCertifiedParams.lean
  • Properties: 5 (3 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 INVARIANT: AES certified params have correct values Sketch: def prop_aes_params : Bool := aesCertParams.inputBits == 8 && aesCertParams.nonlinearity == 112 && aesCertParams.delta == 4 && aesCertParams.degree == 7 SampleableExt: no Risk: wrong AES params invalidate entire AES analysis chain

  • [P2] P0 INVARIANT: PRESENT certified params have correct values Sketch: def prop_present_params : Bool := presentCertParams.inputBits == 4 && presentCertParams.nonlinearity == 4 && presentCertParams.delta == 4 && presentCertParams.degree == 3 SampleableExt: no Risk: wrong PRESENT params invalidate PRESENT pipeline

  • [P3] P0 INVARIANT: degree <= inputBits for both S-boxes (structure invariant) Sketch: def prop_degree_bounded : Bool := aesCertParams.degree <= aesCertParams.inputBits && presentCertParams.degree <= presentCertParams.inputBits SampleableExt: no Risk: invariant violation means SboxCertifiedParams structure is broken

  • [P4] P1 COMPARISON: AES has higher degree and NL than PRESENT Sketch: def prop_aes_stronger : Bool := aesCertParams.degree > presentCertParams.degree && aesCertParams.nonlinearity > presentCertParams.nonlinearity && aesCertParams.inputBits > presentCertParams.inputBits && aesCertParams.delta == presentCertParams.delta -- same delta SampleableExt: no Risk: reversed comparison would invert security ordering

  • [P5] P1 CONVERSION: toHashOp produces correct HashOp with matching degree Sketch: def prop_toHashOp : Bool := aesCertParams.toHashOp 0 == HashOp.sboxApply 0 7 && presentCertParams.toHashOp 0 == HashOp.sboxApply 0 3 && (aesCertParams.toHashOp 0).algDegree == 7 && (presentCertParams.toHashOp 0).algDegree == 3 SampleableExt: no Risk: toHashOp mismatch breaks S-box -> circuit bridge

INTEGRATION:

  • [T1] BASIC: AES params match published cryptographic values Setup: access aesCertParams fields Check: bits=8, nl=112, delta=4, degree=7

  • [T2] BASIC: PRESENT params match published values Setup: access presentCertParams fields Check: bits=4, nl=4, delta=4, degree=3

  • [T3] MEDIUM: minRoundsEstimate produces reasonable values Setup: call aesCertParams.minRoundsEstimate and presentCertParams.minRoundsEstimate Check: both > 0 (non-trivial estimate)

  • [T4] MEDIUM: toHashOp role is nonlinear, toSboxDegree matches degree Setup: aesCertParams.toHashOp 0 and aesCertParams.toSboxDegree Check: role == .nonlinear, toSboxDegree == 7

BRIDGE:

  • [B1] CHECK: #check @SboxCertifiedParams.mk
  • [B2] CHECK: #check @SboxCertifiedParams.toHashOp
  • [B3] WITNESS: aes_degree -- aesCertParams.degree = 7
  • [B4] WITNESS: both_maximal_degree -- both are n-1 maximal

N43.1 -- HashSoundRules: 10+ SoundRewriteRule instances

  • Tipo: CRITICO
  • Archivos fuente: TrustHash/HashSoundRules.lean
  • Target properties: Tests/Properties/HashSoundRules.lean
  • Target integration: Tests/Integration/HashSoundRules.lean
  • Properties: 6 (3 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 INVARIANT: allRules has exactly 12 rules Sketch: def prop_rule_count : Bool := allRules.length == 12 SampleableExt: no Risk: missing rule means incomplete saturation

  • [P2] P0 SOUNDNESS: each rule preserves eval on its trigger pattern Sketch: def prop_sbox_compose_sound : Bool := let e := HashExprF.sbox (.sbox (.var 0) 3) 7 let env := fun i => i + 2 match sboxComposeApply e with | some e' => e.eval env == e'.eval env | none => false def prop_ark_zero_sound : Bool := let e := HashExprF.ark (.var 0) (.leaf 0) let env := fun i => i + 5 match arkZeroRightApply e with | some e' => e.eval env == e'.eval env | none => false def prop_const_fold_sound : Bool := let e := HashExprF.ark (.leaf 3) (.leaf 5) let env := fun _ => 0 match constFoldArkApply e with | some e' => e.eval env == e'.eval env | none => false (combine all into one Bool checking all 12 rules on their trigger patterns) SampleableExt: no Risk: unsound rule would silently corrupt all downstream proofs

  • [P3] P0 SOUNDNESS: saturate preserves eval for multiple fuel levels Sketch: def prop_saturate_sound : Bool := let e := HashExprF.sbox (.sbox (.var 0) 3) 7 let env := fun i => i + 2 (saturate allRules e 0).eval env == e.eval env && (saturate allRules e 1).eval env == e.eval env && (saturate allRules e 5).eval env == e.eval env && (saturate allRules e 100).eval env == e.eval env SampleableExt: no Risk: saturate losing eval equivalence invalidates all pipeline demos

  • [P4] P1 RULES: each rule fires on its designed pattern Sketch: def prop_all_rules_fire : Bool := (sboxComposeApply (.sbox (.sbox (.var 0) 3) 7)).isSome && (roundsComposeApply (.sbox (.rounds (.var 0) 2) 3)).isSome && (arkZeroRightApply (.ark (.var 0) (.leaf 0))).isSome && (arkZeroLeftApply (.ark (.leaf 0) (.var 0))).isSome && (compOneRightApply (.comp (.var 0) (.leaf 1))).isSome && (compOneLeftApply (.comp (.leaf 1) (.var 0))).isSome && (sboxOneApply (.sbox (.var 0) 1)).isSome && (roundsOneApply (.rounds (.var 0) 1)).isSome && (rhoPiElimApply (.rhoPi (.var 0) 42)).isSome && (iotaZeroApply (.iota (.var 0) 0)).isSome && (constFoldArkApply (.ark (.leaf 3) (.leaf 5))).isSome && (constFoldCompApply (.comp (.leaf 3) (.leaf 5))).isSome SampleableExt: no Risk: non-firing rule means dead code in saturation

  • [P5] P1 RULES: rules produce expected simplified forms Sketch: def prop_rule_results : Bool := sboxComposeApply (.sbox (.sbox (.var 0) 3) 7) == some (.sbox (.var 0) 21) && arkZeroRightApply (.ark (.var 0) (.leaf 0)) == some (.var 0) && compOneRightApply (.comp (.var 0) (.leaf 1)) == some (.var 0) && sboxOneApply (.sbox (.var 0) 1) == some (.var 0) && constFoldArkApply (.ark (.leaf 3) (.leaf 5)) == some (.leaf 8) && constFoldCompApply (.comp (.leaf 3) (.leaf 5)) == some (.leaf 15) SampleableExt: no Risk: wrong simplification result corrupts degree analysis

  • [P6] P2 NEGATIVE: rules do not fire on non-matching patterns Sketch: def prop_no_false_fire : Bool := (sboxComposeApply (.var 0)).isNone && (sboxComposeApply (.leaf 5)).isNone && (arkZeroRightApply (.leaf 0)).isNone && (arkZeroRightApply (.ark (.var 0) (.leaf 1))).isNone && -- leaf 1, not 0 (compOneRightApply (.comp (.var 0) (.leaf 0))).isNone && -- leaf 0, not 1 (sboxOneApply (.sbox (.var 0) 2)).isNone -- degree 2, not 1 SampleableExt: no Risk: false positive rule firing would corrupt expressions

INTEGRATION:

  • [T1] BASIC: applyFirst finds the correct rule among all 12 Setup: pass .sbox (.sbox (.var 0) 3) 7 to applyFirst allRules Check: result == some (.sbox (.var 0) 21)

  • [T2] BASIC: saturate with fuel 1 applies one step on nested sbox Setup: saturate allRules (.sbox (.sbox (.var 0) 3) 7) 1 Check: result == .sbox (.var 0) 21

  • [T3] MEDIUM: saturate chain -- multiple steps on identity-wrapped expression Setup: saturate allRules (.sbox (.var 0) 1) 1 Check: result == .var 0

  • [T4] MEDIUM: saturate reaches fixpoint (no further rewrites) Setup: saturate allRules (.var 0) 10 Check: result == .var 0 (unchanged, no rules apply)

  • [T5] EDGE: saturate with fuel 0 returns input unchanged Setup: saturate allRules (.sbox (.sbox (.var 0) 3) 7) 0 Check: result == .sbox (.sbox (.var 0) 3) 7

BRIDGE:

  • [B1] CHECK: #check @HashSoundRule.mk
  • [B2] CHECK: #check @applyFirst
  • [B3] CHECK: #check @saturate
  • [B4] CHECK: #check @allRules_saturate_sound
  • [B5] WITNESS: demo_sbox_compose -- sboxComposeApply fires correctly

N43.2 -- RealSaturate: wire rules + partial-saturation soundness

  • Tipo: CRITICO
  • Archivos fuente: TrustHash/EGraph/RealSaturate.lean
  • Target properties: Tests/Properties/RealSaturate.lean
  • Target integration: Tests/Integration/RealSaturate.lean
  • Properties: 5 (2 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 SOUNDNESS: realSaturate preserves eval for concrete expressions Sketch: def prop_realSaturate_sound : Bool := let env := fun i => i + 2 let e1 := HashExprF.sbox (.sbox (.var 0) 3) 7 let e2 := HashExprF.ark (.var 0) (.leaf 0) let e3 := HashExprF.sbox (.var 0) 1 (realSaturate e1).result.eval env == e1.eval env && (realSaturate e2).result.eval env == e2.eval env && (realSaturate e3).result.eval env == e3.eval env SampleableExt: no Risk: unsound realSaturate would invalidate the entire pipeline

  • [P2] P0 SOUNDNESS: selectRules [] returns allRules (12 rules) Sketch: def prop_selectRules_default : Bool := (selectRules []).length == 12 SampleableExt: no Risk: wrong default rule selection breaks all default saturation

  • [P3] P1 PROGRESS: all 12 rules fire on designed patterns via realSaturate Sketch: def prop_twelve_fires : Bool := (realSaturate (.sbox (.sbox (.var 0) 3) 7)).stepsApplied >= 1 && (realSaturate (.ark (.var 0) (.leaf 0))).stepsApplied >= 1 && (realSaturate (.sbox (.var 0) 1)).stepsApplied >= 1 && (realSaturate (.rhoPi (.var 0) 42)).stepsApplied >= 1 && (realSaturate (.iota (.var 0) 0)).stepsApplied >= 1 && (realSaturate (.ark (.leaf 3) (.leaf 5))).stepsApplied >= 1 && (realSaturate (.comp (.leaf 3) (.leaf 5))).stepsApplied >= 1 && (realSaturate (.comp (.var 0) (.leaf 1))).stepsApplied >= 1 SampleableExt: no Risk: non-firing rules indicate dead code or broken wiring

  • [P4] P1 FIXPOINT: var/leaf expressions reach fixpoint with zero steps Sketch: def prop_fixpoint_leaf : Bool := (realSaturate (.var 0)).reachedFixpoint == true && (realSaturate (.var 0)).stepsApplied == 0 && (realSaturate (.leaf 42)).reachedFixpoint == true && (realSaturate (.leaf 42)).stepsApplied == 0 SampleableExt: no Risk: non-terminating on irreducible expressions

  • [P5] P2 STRUCTURE: RealSatResult fields are consistent Sketch: def prop_result_consistent : Bool := let r := realSaturate (.sbox (.sbox (.var 0) 3) 7) r.stepsApplied >= 1 && r.reachedFixpoint == true && r.result == .sbox (.var 0) 21 SampleableExt: no Risk: inconsistent result fields mislead pipeline analysis

INTEGRATION:

  • [T1] BASIC: realSaturate on nested sbox produces correct result Setup: realSaturate (.sbox (.sbox (.var 0) 3) 7) Check: result == .sbox (.var 0) 21, stepsApplied >= 1

  • [T2] BASIC: realSaturate on identity ark eliminates zero Setup: realSaturate (.ark (.var 0) (.leaf 0)) Check: result == .var 0

  • [T3] MEDIUM: zero_fuel_zero_steps via config maxSteps=0 Setup: realSaturate (.sbox (.sbox (.var 0) 3) 7) { maxSteps := 0 } Check: result == original expression, stepsApplied == 0

  • [T4] MEDIUM: selectRules filters correctly Setup: selectRules ["sbox_compose"] Check: length >= 1

  • [T5] EDGE: countApplicable returns correct count Setup: countApplicable allRules (.sbox (.sbox (.var 0) 3) 7) Check: count >= 1 (at least sbox_compose fires)

BRIDGE:

  • [B1] CHECK: #check @realSaturate
  • [B2] CHECK: #check @realSaturate_sound
  • [B3] CHECK: #check @allRules_realSaturate_sound
  • [B4] WITNESS: nested_sbox_fires -- at least 1 step on nested sbox
  • [B5] WITNESS: twelve_rules_fire -- all 12 rules fire

N43.3 -- RealPipelineDemo: PRESENT 1-round depth reduction

  • Tipo: HOJA
  • Archivos fuente: TrustHash/EGraph/RealPipelineDemo.lean
  • Target properties: Tests/Properties/RealPipelineDemo.lean
  • Target integration: Tests/Integration/RealPipelineDemo.lean
  • Properties: 4 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 REGRESSION: redundant, nested identity, and compose simplify to expected forms Sketch: def prop_simplification_forms : Bool := (realSaturate presentRedundant).result == .sbox (.ark (.var 0) (.var 1)) 3 && (realSaturate presentNestedIdentity).result == .sbox (.ark (.var 0) (.var 1)) 3 && (realSaturate present2Compose).result == .sbox (.var 0) 9 SampleableExt: no Risk: regression in simplification forms would break thesis claims

  • [P2] P0 REGRESSION: depth reduction happens for all demo expressions Sketch: def prop_depth_reduced : Bool := presentRedundant.depth > (realSaturate presentRedundant).result.depth && presentNestedIdentity.depth > (realSaturate presentNestedIdentity).result.depth && present2Compose.depth > (realSaturate present2Compose).result.depth SampleableExt: no Risk: no depth reduction means the e-graph optimization claim is vacuous

  • [P3] P1 VALUES: concrete depth values match expected Sketch: def prop_depth_values : Bool := presentRedundant.depth == 3 && (realSaturate presentRedundant).result.depth == 2 && presentNestedIdentity.depth == 3 && (realSaturate presentNestedIdentity).result.depth == 2 && present2Compose.depth == 2 && (realSaturate present2Compose).result.depth == 1 SampleableExt: no Risk: depth value mismatch indicates structural change in expressions

  • [P4] P1 CERTIFIED: certified PRESENT round uses degree 3 and composes to 9 Sketch: def prop_certified : Bool := presentCertifiedRound == .sbox (.ark (.var 0) (.var 1)) 3 && (realSaturate presentCertified2Compose).result == .sbox (.ark (.var 0) (.var 1)) 9 && presentCertParams.degree * presentCertParams.degree == 9 SampleableExt: no Risk: certified parameter not propagating through pipeline

INTEGRATION:

  • [T1] BASIC: presentRound definition has expected structure Setup: inspect presentRound Check: presentRound == .sbox (.ark (.var 0) (.var 1)) 3

  • [T2] BASIC: all three demos reach fixpoint Setup: check reachedFixpoint for redundant, nested_identity, compose Check: all three are true

  • [T3] MEDIUM: all three demos fire at least 1 rule Setup: check stepsApplied for each Check: all >= 1

  • [T4] MEDIUM: soundness check: saturated expressions eval same as originals Setup: evaluate with env = fun i => i + 3 Check: for each pair (original, saturated), eval values match

BRIDGE:

  • [B1] CHECK: #check @presentRedundant
  • [B2] CHECK: #check @redundant_sound
  • [B3] CHECK: #check @redundant_depth_reduced
  • [B4] WITNESS: certified_degree_used -- presentCertifiedRound = .sbox (.ark (.var 0) (.var 1)) 3

N44.1 -- ConstraintGraphCompute

  • Tipo: CRITICO
  • Archivos fuente: TrustHash/ConstraintGraphCompute.lean
  • Target properties: Tests/Properties/ConstraintGraphCompute.lean
  • Target integration: Tests/Integration/ConstraintGraphCompute.lean
  • Properties: 5 (2 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 INVARIANT: circuit numOps matches expected values for all 3 circuits Sketch: def prop_circuit_sizes : Bool := present1RoundCircuit.numOps == 5 && aes1RoundCircuit.numOps == 6 && keccakChiCircuit.numOps == 10 SampleableExt: no Risk: wrong circuit size means wrong constraint graph

  • [P2] P0 INVARIANT: constraint graphs have correct vertex counts Sketch: def prop_graph_vertices : Bool := present1Graph.numVertices == 5 && aes1Graph.numVertices == 6 && keccakChiGraph.numVertices == 10 SampleableExt: no Risk: vertex mismatch means buildFromCircuit is broken

  • [P3] P1 STRUCTURE: PRESENT graph has expected edges (ark depends on inputs) Sketch: def prop_present_edges : Bool := hasEdge present1Graph 2 0 == true && -- ark depends on input hasEdge present1Graph 3 2 == true && -- sbox depends on ark numEdges present1Graph >= 1 SampleableExt: no Risk: missing edges means incorrect constraint graph

  • [P4] P1 TREEWIDTH: treewidths bounded correctly Sketch: def prop_treewidths : Bool := present1TD.width <= 3 && aes1TD.width <= 3 && keccakChiTD.width <= 5 SampleableExt: no Risk: wrong treewidth bound invalidates DP complexity claims

  • [P5] P2 EDGE_CASES: empty and single-node circuits produce trivial graphs Sketch: def prop_edge_cases : Bool := let emptyC : HashCircuit := { nodes := [] } (buildFromCircuit emptyC).numVertices == 0 && let singleC : HashCircuit := { nodes := [{ op := .constOp 0, deps := [] }] } (buildFromCircuit singleC).numVertices == 1 SampleableExt: no Risk: crash on edge case inputs

INTEGRATION:

  • [T1] BASIC: PRESENT 1-round circuit has 5 nodes and edges Setup: build present1Graph Check: numVertices == 5, numEdges >= 1

  • [T2] BASIC: AES 1-round circuit has 6 nodes Setup: build aes1Graph Check: numVertices == 6

  • [T3] MEDIUM: Keccak chi circuit has 10 nodes and highest treewidth Setup: build keccakChiGraph Check: numVertices == 10, keccakChiTD.width >= present1TD.width

  • [T4] MEDIUM: linear chain circuit has small treewidth Setup: build a 4-node linear chain circuit (each depends on previous) Check: treewidth <= 2

  • [T5] EDGE: no_deps_no_edges: circuit with no dependencies has no edges Setup: 3-node circuit with all deps = [] Check: numEdges == 0

BRIDGE:

  • [B1] CHECK: #check @buildFromCircuit
  • [B2] CHECK: #check @present1RoundCircuit
  • [B3] CHECK: #check @present1_treewidth
  • [B4] WITNESS: present1_vertices -- present1Graph.numVertices = 5
  • [B5] WITNESS: aes1_treewidth -- aes1TD.width <= 3

N44.2 -- TreeDecompCertificate

  • Tipo: CRITICO
  • Archivos fuente: TrustHash/TreeDecompCertificate.lean
  • Target properties: Tests/Properties/TreeDecompCertificate.lean
  • Target integration: Tests/Integration/TreeDecompCertificate.lean
  • Properties: 5 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 INVARIANT: all three certificates have positive width and bags Sketch: def prop_certs_valid : Bool := presentCert.certWidth >= 0 && aesCert.certWidth >= 0 && keccakChiCert.certWidth >= 0 && presentCert.td.size >= 1 && aesCert.td.size >= 1 SampleableExt: no Risk: zero-width or empty certificate is vacuous

  • [P2] P0 INVARIANT: certificate width bounds match expected values Sketch: def prop_cert_widths : Bool := presentCert.certWidth <= 3 && aesCert.certWidth <= 3 && keccakChiCert.certWidth <= 4 SampleableExt: no Risk: wrong width bound invalidates DP cost claims

  • [P3] P1 ORDERING: PRESENT <= Keccak treewidth, AES close to PRESENT Sketch: def prop_width_ordering : Bool := presentCert.certWidth <= keccakChiCert.certWidth && aesCert.certWidth <= presentCert.certWidth + 1 SampleableExt: no Risk: cipher ordering violated would invalidate cross-cipher comparisons

  • [P4] P1 DP_BOUND: dpComplexityBound produces bounded values Sketch: def prop_dp_bounds : Bool := dpComplexityBound presentCert <= 80 && dpComplexityBound aesCert <= 96 && dpComplexityBound keccakChiCert <= 320 SampleableExt: no Risk: DP complexity bound too loose or wrong

  • [P5] P1 ORDERING: Keccak has strictly higher DP cost than PRESENT Sketch: def prop_dp_ordering : Bool := dpComplexityBound presentCert < dpComplexityBound keccakChiCert SampleableExt: no Risk: DP ordering violated

INTEGRATION:

  • [T1] BASIC: presentCert width matches TD width Setup: check presentCert.certWidth == presentCert.td.width Check: equality holds (from width_eq)

  • [T2] BASIC: aesCert width matches TD width Setup: check aesCert.certWidth == aesCert.td.width Check: equality holds

  • [T3] MEDIUM: dpComplexityBound formula: 2^(tw+1) * numVertices Setup: compute manually for PRESENT: 2^(present1TD.width+1) * 5 Check: matches dpComplexityBound presentCert

  • [T4] MEDIUM: cross-certificate comparison Setup: compare all three certificates Check: PRESENT < Keccak in DP cost, AES in between or similar

BRIDGE:

  • [B1] CHECK: #check @TDCertificate.mk
  • [B2] CHECK: #check @TDCertificate.verify
  • [B3] CHECK: #check @dpComplexityBound
  • [B4] WITNESS: presentCert_width -- presentCert.certWidth <= 3
  • [B5] WITNESS: keccak_higher_dp_cost -- DP(present) < DP(keccak)

N44.3 -- CryptoDPInstance

  • Tipo: CRITICO
  • Archivos fuente: TrustHash/DP/CryptoDPInstance.lean
  • Target properties: Tests/Properties/CryptoDPInstance.lean
  • Target integration: Tests/Integration/CryptoDPInstance.lean
  • Properties: 5 (2 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 INVARIANT: all DP values are positive Sketch: def prop_dp_positive : Bool := presentDiffDP >= 1 && presentAlgDP >= 1 && presentSecDP >= 1 && aesSecDP >= 1 && keccakChiAlgDP >= 1 SampleableExt: no Risk: zero DP would mean trivially breakable cipher (false negative)

  • [P2] P0 INVARIANT: presentSecDP = min(presentDiffDP, presentAlgDP) Sketch: def prop_secDP_min : Bool := presentSecDP == min presentDiffDP presentAlgDP SampleableExt: no Risk: secDP not being min would violate two-layer model

  • [P3] P1 CERTIFIED: DP uses certified S-box parameters Sketch: def prop_cert_params_used : Bool := presentDiffDP == differentialDP 4 present1NiceTree && presentAlgDP == algebraicDP 3 present1NiceTree && aesDiffDP == differentialDP 4 aes1NiceTree && aesAlgDP == algebraicDP 7 aes1NiceTree && keccakChiAlgDP == algebraicDP 2 keccakChiNiceTree SampleableExt: no Risk: DP not using certified params breaks certification chain

  • [P4] P1 ORDERING: PRESENT <= AES in security DP Sketch: def prop_ordering : Bool := presentSecDP <= aesSecDP && presentAlgDP < aesAlgDP SampleableExt: no Risk: reversed ordering would invalidate security conclusions

  • [P5] P1 STRUCTURE: nice trees have positive size Sketch: def prop_nice_trees_pos : Bool := present1NiceTree.size >= 1 && aes1NiceTree.size >= 1 && keccakChiNiceTree.size >= 1 SampleableExt: no Risk: empty nice tree means no DP computation

INTEGRATION:

  • [T1] BASIC: PRESENT DP uses delta=4 and degree=3 Setup: check presentDiffDP definition matches Check: uses differentialDP 4 and algebraicDP 3

  • [T2] BASIC: AES DP uses delta=4 and degree=7 Setup: check aesDiffDP and aesAlgDP definitions Check: uses differentialDP 4 and algebraicDP 7

  • [T3] MEDIUM: Keccak chi DP with d=2 is positive Setup: compute keccakChiAlgDP Check: >= 1

  • [T4] MEDIUM: cross-circuit DP comparison Setup: compare presentSecDP, aesSecDP, keccakChiAlgDP Check: PRESENT <= AES, Keccak has larger nice tree

  • [T5] EDGE: consistency with TDCertificate bounds Setup: check present_dp_cert_consistent, aes_dp_cert_consistent Check: dpComplexityBound >= 1 for all

BRIDGE:

  • [B1] CHECK: #check @circuitToNiceTree
  • [B2] CHECK: #check @presentDiffDP
  • [B3] CHECK: #check @presentSecDP_eq
  • [B4] WITNESS: presentSecDP_pos -- presentSecDP >= 1
  • [B5] WITNESS: present_dp_cert_consistent -- dpComplexityBound presentCert >= 1

N45.1 -- AES8BitCertified

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/Sbox/AES8BitCertified.lean
  • Target properties: Tests/Properties/AES8BitCertified.lean
  • Target integration: Tests/Integration/AES8BitCertified.lean
  • Properties: 5 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 REGRESSION: AES certified params consistency with DDT Sketch: def prop_cert_consistent : Bool := aesDDTCert.maxDelta == aesCertParams.delta && aesCertParams.degree == 7 && aesCertParams.nonlinearity == 112 SampleableExt: no Risk: DDT/params inconsistency breaks the certification chain

  • [P2] P0 REGRESSION: AES 8-bit fully certified master theorem values Sketch: def prop_fully_certified : Bool := aesCertParams.delta == 4 && aesCertParams.degree == 7 && aesCertParams.nonlinearity == 112 && aesCertParams.inputBits == 8 && aes1TD.width <= 3 SampleableExt: no Risk: any field wrong invalidates aes_8bit_fully_certified

  • [P3] P1 QUALITY: AES NL near optimal, delta minimal for 8-bit Sketch: def prop_quality : Bool := aesCertParams.nonlinearity >= 112 && aesCertParams.delta == 4 && aesCertParams.degree == aesCertParams.inputBits - 1 && aesCertParams.nonlinearity > 2 ^ (aesCertParams.inputBits - 1) / 2 SampleableExt: no Risk: quality metric wrong would mischaracterize AES

  • [P4] P1 COMPARISON: AES vs PRESENT certified comparison Sketch: def prop_aes_vs_present : Bool := aesCertParams.delta == presentCertParams.delta && aesCertParams.degree > presentCertParams.degree && aesCertParams.nonlinearity > presentCertParams.nonlinearity && aesCertParams.inputBits > presentCertParams.inputBits SampleableExt: no Risk: comparison wrong invalidates cipher ordering

  • [P5] P1 BRIDGE: aesHashOp matches expected HashOp Sketch: def prop_hashop_bridge : Bool := aesHashOp == HashOp.sboxApply 0 7 && aesHashOp.role == .nonlinear && aesHashOp.algDegree == 7 SampleableExt: no Risk: HashOp bridge broken means circuit analysis uses wrong degree

INTEGRATION:

  • [T1] BASIC: AES DDT delta matches certified params Setup: check aesDDTCert.maxDelta Check: equals aesCertParams.delta (= 4)

  • [T2] BASIC: AES circuit treewidth and DP complexity Setup: check aes1TD.width and dpComplexityBound aesCert Check: width <= 3, DP <= 96

  • [T3] MEDIUM: AES diff strength vs PRESENT diff strength Setup: compute aesDiffStrength and presentDiffStrength Check: aesDiffStrength > presentDiffStrength (64 > 4)

  • [T4] MEDIUM: AES algebraic immunity: inputBits - degree = 1 Setup: compute aesCertParams.inputBits - aesCertParams.degree Check: result == 1

BRIDGE:

  • [B1] CHECK: #check @aes_cert_delta_consistent
  • [B2] CHECK: #check @aesHashOp
  • [B3] CHECK: #check @aes_8bit_fully_certified
  • [B4] WITNESS: aes_certified_degree_7 -- aesCertParams.degree = 7
  • [B5] WITNESS: aes_circuit_tractable -- numOps <= 10

N45.2 -- KeccakSecurityAnalysis

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/Keccak/KeccakSecurityAnalysis.lean
  • Target properties: Tests/Properties/KeccakSecurityAnalysis.lean
  • Target integration: Tests/Integration/KeccakSecurityAnalysis.lean
  • Properties: 5 (2 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 REGRESSION: SHA-3-256 collision = 128, preimage = 256 Sketch: def prop_sha3_256_bounds : Bool := spongeCollisionSecurity 256 sha3_256_params == 128 && spongePreimageSecurity 256 sha3_256_params == 256 SampleableExt: no Risk: wrong sponge bounds invalidate SHA-3-256 security claims

  • [P2] P0 REGRESSION: chi degree = 2, treewidth = 4 Sketch: def prop_chi_structure : Bool := chiDegree == 2 && keccak_chi_decomp.width == 4 SampleableExt: no Risk: wrong chi parameters invalidate all Keccak structural analysis

  • [P3] P1 DEGREE: degree grows exponentially with rounds Sketch: def prop_degree_growth : Bool := maxAlgDegree 1 == 2 && maxAlgDegree 6 == 64 && maxAlgDegree 24 == 16777216 && maxAlgDegree 6 == laneWidth SampleableExt: no Risk: degree growth wrong would mischaracterize algebraic immunity

  • [P4] P1 STRUCTURAL: cost grows monotonically and exceeds thresholds Sketch: def prop_structural_cost : Bool := keccakStructuralCost 1 == 16 && keccakStructuralCost 6 > 2 ^ 20 && keccakStructuralCost 12 > 2 ^ 40 && keccakStructuralCost 3 > 128 SampleableExt: no Risk: structural cost underestimate could lead to false security claim

  • [P5] P1 TWO_LAYER: sha3_256_twoLayer = 128 (sponge binds) Sketch: def prop_two_layer : Bool := sha3_256_twoLayer == 128 && keccakStructuralCost sha3_256_params.rounds > spongeCollisionSecurity 256 sha3_256_params SampleableExt: no Risk: two-layer computation wrong means incorrect security verdict

INTEGRATION:

  • [T1] BASIC: SHA-3-256 and SHA-3-512 collision/preimage security Setup: compute all four bounds Check: 256-collision=128, 256-preimage=256, 512-collision=256, 512-preimage=512

  • [T2] BASIC: chi degree and treewidth Setup: chiDegree and keccak_chi_decomp.width Check: degree=2, treewidth=4

  • [T3] MEDIUM: structural cost at key round counts Setup: keccakStructuralCost at rounds 1, 3, 6, 12, 24 Check: monotonically increasing, specific threshold values

  • [T4] MEDIUM: SHA-3-256 two-layer security Setup: compute sha3_256_twoLayer Check: == 128 (sponge capacity is binding)

  • [T5] EDGE: Keccak vs DES cross-cipher comparison Setup: keccakStructuralCost 12 vs feistelStructuralCost desParams Check: Keccak 12 rounds > DES structural cost

BRIDGE:

  • [B1] CHECK: #check @spongeCollisionSecurity
  • [B2] CHECK: #check @keccakStructuralCost
  • [B3] CHECK: #check @sha3_256_twoLayer
  • [B4] WITNESS: sha3_256_collision_128 -- collision security = 128
  • [B5] WITNESS: structural_monotone -- cost monotone in rounds

N45.3 -- AES128Analysis

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/AES128Analysis.lean
  • Target properties: Tests/Properties/AES128Analysis.lean
  • Target integration: Tests/Integration/AES128Analysis.lean
  • Properties: 5 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 REGRESSION: aes128Analysis fields match certified values Sketch: def prop_analysis_fields : Bool := aes128Analysis.sboxDelta == 4 && aes128Analysis.sboxDegree == 7 && aes128Analysis.sboxNonlinearity == 112 && aes128Analysis.genericFloor == 64 SampleableExt: no Risk: wrong field values propagate to incorrect verdict

  • [P2] P0 REGRESSION: AES-128 overall security = 62 Sketch: def prop_verdict : Bool := aes128Analysis.overallSecurity == 62 && aes128Analysis.dpSecurityCost == 62 && aes128Analysis.overallSecurity <= aes128Analysis.genericFloor SampleableExt: no Risk: wrong verdict is the central AES-128 claim

  • [P3] P1 CERT_CHAIN: certified params flow through correctly Sketch: def prop_cert_chain : Bool := aes128Analysis.sboxDelta == aesCertParams.delta && aes128Analysis.sboxDegree == aesCertParams.degree && aes128Analysis.sboxNonlinearity == aesCertParams.nonlinearity SampleableExt: no Risk: certification chain broken means unverified values in analysis

  • [P4] P1 NEAR_OPTIMAL: gap between generic and overall is small Sketch: def prop_near_optimal : Bool := aes128Analysis.genericFloor - aes128Analysis.overallSecurity <= 2 SampleableExt: no Risk: large gap would indicate AES circuit structure too weak

  • [P5] P1 CROSS_VALIDATE: existing pipeline verdict matches Sketch: def prop_cross_validate : Bool := pipelineVerdictTag aes128 == "OPTIMAL" && computeVerdict aes128 == 64 && aes128Analysis.genericFloor == computeGenericFloor aes128 SampleableExt: no Risk: inconsistency between old and new pipelines

INTEGRATION:

  • [T1] BASIC: aes128Analysis complete profile Setup: check all fields of aes128Analysis Check: delta=4, degree=7, nl=112, genericFloor=64, overall=62

  • [T2] BASIC: AES-128 DP cost breakdown Setup: check dpDiffCost, dpAlgCost, dpSecurityCost Check: dpSecurityCost = 62, dpDiffCost <= dpAlgCost (diff is bottleneck)

  • [T3] MEDIUM: AES-128 certification chain intact Setup: verify DDT cert -> certified params -> analysis flow Check: aes128_ddt_to_dp holds, circuit_dp_cert holds

  • [T4] MEDIUM: AES-128 complete master theorem values Setup: check all 6 conjuncts of aes128_complete Check: all hold (delta=4, degree=7, nl=112, floor=64, dp>=1, overall=62)

BRIDGE:

  • [B1] CHECK: #check @aes128Analysis
  • [B2] CHECK: #check @aes128_complete
  • [B3] CHECK: #check @aes128_cert_chain
  • [B4] WITNESS: aes128_delta -- aes128Analysis.sboxDelta = 4
  • [B5] WITNESS: aes128_overall_val -- aes128Analysis.overallSecurity = 62

N45.4 -- Keccak256Analysis

  • Tipo: PARALELO
  • Archivos fuente: TrustHash/Keccak/Keccak256Analysis.lean
  • Target properties: Tests/Properties/Keccak256Analysis.lean
  • Target integration: Tests/Integration/Keccak256Analysis.lean
  • Properties: 5 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 REGRESSION: keccak256Analysis fields match expected values Sketch: def prop_analysis_fields : Bool := keccak256Analysis.sboxDegree == 2 && keccak256Analysis.genericFloor == 128 && keccak256Analysis.overallSecurity == 128 && keccak256Analysis.sboxDelta == 0 && keccak256Analysis.sboxNonlinearity == 0 SampleableExt: no Risk: wrong analysis fields invalidate SHA-3-256 claims

  • [P2] P0 REGRESSION: keccak256 verdict = 128 (optimal) Sketch: def prop_verdict : Bool := keccak256Analysis.overallSecurity == 128 && keccak256Analysis.overallSecurity == keccak256Analysis.genericFloor SampleableExt: no Risk: wrong verdict is the central SHA-3-256 claim

  • [P3] P1 SPONGE: sponge parameters correct Sketch: def prop_sponge_params : Bool := sha3_256_params.capacity == 512 && sha3_256_params.rate == 1088 && spongeCollisionSecurity 256 sha3_256_params == 128 && spongePreimageSecurity 256 sha3_256_params == 256 SampleableExt: no Risk: wrong sponge params means wrong security bounds

  • [P4] P1 COMPARISON: Keccak-256 has higher collision security than AES-128 Sketch: def prop_vs_aes : Bool := spongeCollisionSecurity 256 sha3_256_params > computeGenericFloor aes128 SampleableExt: no Risk: reversed comparison invalidates cipher ordering

  • [P5] P1 MARGIN: 3 rounds suffice for structural security Sketch: def prop_margin : Bool := keccakStructuralCost 3 > spongeCollisionSecurity 256 sha3_256_params && sha3_256_params.rounds - 3 == 21 && keccakStructuralCost 3 > 128 SampleableExt: no Risk: margin wrong means incorrect round-reduction claim

INTEGRATION:

  • [T1] BASIC: keccak256Analysis complete profile Setup: check all key fields Check: degree=2, floor=128, overall=128, capacity=512

  • [T2] BASIC: keccak256_complete master theorem values Setup: check 5 conjuncts Check: degree=2, floor=128, overall=128, chi_tw=4, capacity=512

  • [T3] MEDIUM: sponge stronger than simplified model Setup: compare keccak256Analysis.overallSecurity vs computeVerdict keccak256Model Check: sponge analysis gives higher bound (128 > 81)

  • [T4] MEDIUM: structural dominates -- structural cost >> sponge security Setup: keccakStructuralCost 24 vs spongeCollisionSecurity 256 sha3_256_params Check: structural cost > sponge security by large margin

BRIDGE:

  • [B1] CHECK: #check @keccak256Analysis
  • [B2] CHECK: #check @keccak256_complete
  • [B3] CHECK: #check @keccak256_sponge_stronger
  • [B4] WITNESS: keccak256_verdict_128 -- overall = 128
  • [B5] WITNESS: keccak256_degree -- sboxDegree = 2

N46.1 -- PresentEndToEnd

  • Tipo: FUNDACIONAL
  • Archivos fuente: TrustHash/PresentEndToEnd.lean
  • Target properties: Tests/Properties/PresentEndToEnd.lean
  • Target integration: Tests/Integration/PresentEndToEnd.lean
  • Properties: 6 (3 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 INVARIANT: all 7 pipeline stages produce correct values Sketch: def prop_pipeline_stages : Bool := -- Stage 1: certified params presentCertParams.delta == 4 && presentCertParams.degree == 3 && -- Stage 2: expression depth present3Round.depth == 4 && -- Stage 3: depth reduction present3Optimized.depth < present3Round.depth && -- Stage 4: circuit ops present1RoundCircuit.numOps == 5 && -- Stage 5: treewidth present1TD.width <= 3 && -- Stage 6: DP positive presentSecDP >= 1 && -- Stage 7: verdict bounded presentAnalysis.overallSecurity <= presentAnalysis.genericFloor SampleableExt: no Risk: any stage failure breaks the central end-to-end theorem

  • [P2] P0 INVARIANT: present_full_chain master theorem values Sketch: Same as P1 (this tests the theorem statement is non-vacuous) SampleableExt: no Risk: vacuous master theorem

  • [P3] P0 INVARIANT: presentAnalysis uses certified parameters Sketch: def prop_analysis_certified : Bool := presentAnalysis.sboxDelta == 4 && presentAnalysis.sboxDegree == 3 && presentAnalysis.sboxNonlinearity == 4 SampleableExt: no Risk: analysis not using certified params breaks certification

  • [P4] P1 SATURATION: E-graph rules fire and reach fixpoint on present3Round Sketch: def prop_egraph_active : Bool := (realSaturate present3Round).stepsApplied >= 1 && (realSaturate present3Round).reachedFixpoint == true SampleableExt: no Risk: e-graph not firing means no optimization happens

  • [P5] P1 CROSS_CIPHER: PRESENT <= AES in security DP Sketch: def prop_cross_cipher : Bool := presentSecDP <= aesSecDP && present1RoundCircuit.numOps < keccakChiCircuit.numOps SampleableExt: no Risk: cipher ordering reversed

  • [P6] P1 ALL_SECURE: all three ciphers produce positive DP Sketch: def prop_all_secure : Bool := presentSecDP >= 1 && aesSecDP >= 1 && TrustHash.DP.CryptoDPInstance.keccakChiAlgDP >= 1 SampleableExt: no Risk: any cipher with zero DP means broken analysis

INTEGRATION:

  • [T1] BASIC: present3Round definition and depth Setup: check present3Round structure and depth Check: depth == 4, uses certified degree 3

  • [T2] BASIC: present3Optimized is a valid simplification Setup: check depth reduced and eval preserved Check: depth < 4, eval with any env matches present3Round

  • [T3] MEDIUM: full pipeline stages 1-7 sequential validation Setup: trace through all 7 stages with concrete checks Check: each stage output matches expected

  • [T4] MEDIUM: cross-cipher comparison with AES and Keccak Setup: compare presentSecDP, aesSecDP, keccakChiAlgDP Check: PRESENT <= AES, circuit size ordering correct

  • [T5] EDGE: pipeline activity metrics Setup: check pipeline_egraph_active and pipeline_dp_active Check: all >= 1 steps applied, all DP >= 1

BRIDGE:

  • [B1] CHECK: #check @present3Round
  • [B2] CHECK: #check @present_full_chain
  • [B3] CHECK: #check @presentAnalysis
  • [B4] CHECK: #check @all_ciphers_secure
  • [B5] WITNESS: stage3_sound -- optimization is sound
  • [B6] WITNESS: present_vs_aes -- PRESENT <= AES

N46.2 -- ThesisDemonstration

  • Tipo: HOJA
  • Archivos fuente: TrustHash/ThesisDemonstration.lean
  • Target properties: Tests/Properties/ThesisDemonstration.lean
  • Target integration: Tests/Integration/ThesisDemonstration.lean
  • Properties: 4 (2 P0)
  • Integration tests: 4

PROPERTIES:

  • [P1] P0 REGRESSION: thesis_verified master theorem values Sketch: def prop_thesis_master : Bool := (realSaturate present3Round).stepsApplied >= 1 && presentSecDP >= 1 && aesSecDP >= 1 && aes128Analysis.overallSecurity == 62 && keccak256Analysis.overallSecurity == 128 SampleableExt: no Risk: master theorem regression breaks thesis

  • [P2] P0 REGRESSION: all 12 sub-claims hold Sketch: def prop_all_subclaims : Bool := -- Claim 1: depth reduction (4 subclaims) presentRedundant.depth > (realSaturate presentRedundant).result.depth && present2Compose.depth > (realSaturate present2Compose).result.depth && (realSaturate present3Round).stepsApplied >= 1 && (realSaturate present3Round).reachedFixpoint == true && -- Claim 2: DP circuits (4 subclaims) presentSecDP >= 1 && aesSecDP >= 1 && present1TD.width <= 3 && aes1TD.width <= 3 && -- Claim 3: verdicts (4 subclaims check) aes128Analysis.overallSecurity == 62 && keccak256Analysis.overallSecurity == 128 && presentSecDP <= aesSecDP SampleableExt: no Risk: any subclaim failing means incomplete thesis

  • [P3] P1 CLAIMS: Claim 1 rules_count -- all 12 rules fire Sketch: def prop_claim1_rules : Bool := (sboxComposeApply (.sbox (.sbox (.var 0) 3) 7)).isSome && (roundsComposeApply (.sbox (.rounds (.var 0) 2) 3)).isSome && (arkZeroRightApply (.ark (.var 0) (.leaf 0))).isSome && (arkZeroLeftApply (.ark (.leaf 0) (.var 0))).isSome && (compOneRightApply (.comp (.var 0) (.leaf 1))).isSome && (compOneLeftApply (.comp (.leaf 1) (.var 0))).isSome && (sboxOneApply (.sbox (.var 0) 1)).isSome && (roundsOneApply (.rounds (.var 0) 1)).isSome && (rhoPiElimApply (.rhoPi (.var 0) 42)).isSome && (iotaZeroApply (.iota (.var 0) 0)).isSome && (constFoldArkApply (.ark (.leaf 3) (.leaf 5))).isSome && (constFoldCompApply (.comp (.leaf 3) (.leaf 5))).isSome SampleableExt: no Risk: missing rule means Claim 1c fails

  • [P4] P1 CLAIMS: certified flow -- params propagate correctly Sketch: def prop_certified_flow : Bool := presentAnalysis.sboxDelta == presentCertParams.delta && presentAnalysis.sboxDegree == presentCertParams.degree && aes128Analysis.sboxDelta == aesCertParams.delta && aes128Analysis.sboxDegree == aesCertParams.degree && keccak256Analysis.sboxDegree == chiDegree SampleableExt: no Risk: certification flow broken means unverified analysis

INTEGRATION:

  • [T1] BASIC: thesis_verified master theorem 5 conjuncts Setup: check all 5 conjuncts Check: steps>=1, presentDP>=1, aesDP>=1, aesOverall=62, keccakOverall=128

  • [T2] BASIC: claim1 depth reduction on all 4 expressions Setup: check depth before > depth after for each Check: all 4 reduce

  • [T3] MEDIUM: claim2 three circuits with positive DP Setup: check presentSecDP, aesSecDP, keccakChiAlgDP Check: all >= 1

  • [T4] MEDIUM: claim3 cipher ordering and verdicts Setup: check PRESENT <= AES ordering, Keccak floor > AES floor Check: ordering holds

BRIDGE:

  • [B1] CHECK: #check @thesis_verified
  • [B2] CHECK: #check @claim1_depth_reduction
  • [B3] CHECK: #check @claim2_three_circuits
  • [B4] CHECK: #check @claim3_three_verdicts
  • [B5] WITNESS: claim3_cipher_ordering -- PRESENT <= AES, Keccak floor > AES floor

N46.3 -- ValidationV30

  • Tipo: HOJA
  • Archivos fuente: TrustHash/Validation/ValidationV30.lean
  • Target properties: Tests/Properties/ValidationV30.lean
  • Target integration: Tests/Integration/ValidationV30.lean
  • Properties: 4 (2 P0)
  • Integration tests: 5

PROPERTIES:

  • [P1] P0 REGRESSION: v30_all_gaps_closed master theorem values Sketch: def prop_all_gaps : Bool := (realSaturate present3Round).stepsApplied >= 1 && presentSecDP >= 1 && aesSecDP >= 1 && aes128Analysis.overallSecurity == 62 && keccak256Analysis.overallSecurity == 128 && present3Optimized.depth < present3Round.depth SampleableExt: no Risk: regression in gap closure means v3.0 validation fails

  • [P2] P0 REGRESSION: v30_thesis AES=62 and Keccak=128 Sketch: def prop_v30_thesis : Bool := aes128Analysis.overallSecurity == 62 && keccak256Analysis.overallSecurity == 128 SampleableExt: no Risk: central thesis values wrong

  • [P3] P1 METRICS: project metrics met Sketch: def prop_metrics : Bool := -- >= 2 real hash instances presentSecDP >= 1 && aesSecDP >= 1 && -- >= 1 E-graph rules fired (realSaturate present3Round).stepsApplied >= 1 && -- >= 1 DP on real circuit presentSecDP >= 1 && keccakChiAlgDP >= 1 SampleableExt: no Risk: metrics not met means project targets not achieved

  • [P4] P1 REGRESSION: v28 regression -- 23 conditional rules still present Sketch: def prop_v28_regression : Bool := TrustHash.ConditionalRewriteRule.mixedRuleCount TrustHash.CryptoSoundRules.extendedRules TrustHash.ExtendedAttackRules.allConditionalRules == 23 SampleableExt: no Risk: v28 rules lost means backward compatibility broken

INTEGRATION:

  • [T1] BASIC: Gap 1 -- E-graph rules fire Setup: check gap1_egraph_closed values Check: sboxCompose fires, saturation steps >= 1

  • [T2] BASIC: Gap 2 -- DP on 3 real circuits Setup: check gap2_dp_real_circuits values Check: PRESENT=5 nodes, AES=6, Keccak=10, all DP >= 1

  • [T3] BASIC: Gap 3 -- AES analyzed Setup: check gap3_aes_analyzed values Check: delta=4, degree=7, nl=112, overall=62

  • [T4] BASIC: Gap 4 -- Keccak connected Setup: check gap4_keccak_connected values Check: floor=128, degree=2, overall=128

  • [T5] MEDIUM: Gap 5 -- end-to-end pipeline Setup: check gap5_end_to_end values Check: all 6 conjuncts hold (certified params -> depth -> reduction -> DP -> verdict)

BRIDGE:

  • [B1] CHECK: #check @v30_all_gaps_closed
  • [B2] CHECK: #check @v30_thesis
  • [B3] CHECK: #check @regression_v28_rules
  • [B4] WITNESS: gap1_egraph_closed -- E-graph fires
  • [B5] WITNESS: gap5_end_to_end -- full pipeline

Resumen

Nodo Tipo Properties P0 Integration Bridge
N42.1 FUNDACIONAL 6 3 5 5
N42.2 PARALELO 5 2 4 4
N42.3 PARALELO 5 3 4 4
N43.1 CRITICO 6 3 5 5
N43.2 CRITICO 5 2 5 5
N43.3 HOJA 4 2 4 4
N44.1 CRITICO 5 2 5 5
N44.2 CRITICO 5 2 4 5
N44.3 CRITICO 5 2 5 5
N45.1 PARALELO 5 2 4 5
N45.2 PARALELO 5 2 5 5
N45.3 PARALELO 5 2 4 5
N45.4 PARALELO 5 2 4 5
N46.1 FUNDACIONAL 6 3 5 6
N46.2 HOJA 4 2 4 5
N46.3 HOJA 4 2 5 5
TOTAL 80 36 72 78

Formal Bridge Requirements

#check statements (type verification)

-- N42.1
#check @evalHashOp
#check @reconstructHashExpr
#check @HashOp.role
#check @HashOp.algDegree

-- N42.2
#check @TrustHash.HashExpr.Extractable.reconstruct HashOp HashExprF
#check @TrustHash.HashExpr.EvalExpr.evalExpr HashExprF Nat
#check @TrustHash.HashExpr.extractF

-- N42.3
#check @TrustHash.SboxCertifiedParams.SboxCertifiedParams.mk
#check @TrustHash.SboxCertifiedParams.SboxCertifiedParams.toHashOp

-- N43.1
#check @TrustHash.HashSoundRules.HashSoundRule.mk
#check @TrustHash.HashSoundRules.applyFirst
#check @TrustHash.HashSoundRules.saturate
#check @TrustHash.HashSoundRules.allRules_saturate_sound

-- N43.2
#check @TrustHash.EGraph.RealSaturate.realSaturate
#check @TrustHash.EGraph.RealSaturate.realSaturate_sound
#check @TrustHash.EGraph.RealSaturate.allRules_realSaturate_sound

-- N43.3
#check @TrustHash.EGraph.RealPipelineDemo.presentRedundant
#check @TrustHash.EGraph.RealPipelineDemo.redundant_sound
#check @TrustHash.EGraph.RealPipelineDemo.redundant_depth_reduced

-- N44.1
#check @TrustHash.ConstraintGraphCompute.buildFromCircuit
#check @TrustHash.ConstraintGraphCompute.present1RoundCircuit
#check @TrustHash.ConstraintGraphCompute.present1_treewidth

-- N44.2
#check @TrustHash.TreeDecompCertificate.TDCertificate.mk
#check @TrustHash.TreeDecompCertificate.TDCertificate.verify
#check @TrustHash.TreeDecompCertificate.dpComplexityBound

-- N44.3
#check @TrustHash.DP.CryptoDPInstance.circuitToNiceTree
#check @TrustHash.DP.CryptoDPInstance.presentDiffDP
#check @TrustHash.DP.CryptoDPInstance.presentSecDP_eq

-- N45.1
#check @TrustHash.AES8BitCertified.aes_cert_delta_consistent
#check @TrustHash.AES8BitCertified.aesHashOp
#check @TrustHash.AES8BitCertified.aes_8bit_fully_certified

-- N45.2
#check @TrustHash.Keccak.spongeCollisionSecurity
#check @TrustHash.Keccak.keccakStructuralCost
#check @TrustHash.Keccak.KeccakSecurityAnalysis.sha3_256_twoLayer

-- N45.3
#check @TrustHash.AES128Analysis.aes128Analysis
#check @TrustHash.AES128Analysis.aes128_complete
#check @TrustHash.AES128Analysis.aes128_cert_chain

-- N45.4
#check @TrustHash.Keccak.Keccak256Analysis.keccak256Analysis
#check @TrustHash.Keccak.Keccak256Analysis.keccak256_complete
#check @TrustHash.Keccak.Keccak256Analysis.keccak256_sponge_stronger

-- N46.1
#check @TrustHash.PresentEndToEnd.present3Round
#check @TrustHash.PresentEndToEnd.present_full_chain
#check @TrustHash.PresentEndToEnd.presentAnalysis
#check @TrustHash.PresentEndToEnd.all_ciphers_secure

-- N46.2
#check @TrustHash.ThesisDemonstration.thesis_verified
#check @TrustHash.ThesisDemonstration.claim1_depth_reduction
#check @TrustHash.ThesisDemonstration.claim2_three_circuits
#check @TrustHash.ThesisDemonstration.claim3_three_verdicts

-- N46.3
#check @TrustHash.ValidationV30.v30_all_gaps_closed
#check @TrustHash.ValidationV30.v30_thesis
#check @TrustHash.ValidationV30.regression_v28_rules

Witness requirements (non-vacuity concrete instantiation)

-- N42.1: children_constOp, children_varOp, sbox_is_nonlinear, const_is_leaf
-- N42.2: extractF_constOp, extractF_varOp, depth_leaf, size_pos
-- N42.3: aes_degree, present_degree, both_maximal_degree, toHashOp_degree
-- N43.1: demo_sbox_compose, demo_ark_zero, demo_const_fold, allRules_length
-- N43.2: nested_sbox_fires, twelve_rules_fire, fixpoint_on_var, zero_fuel_zero_steps
-- N43.3: certified_degree_used, rules_fired_count, all_reach_fixpoint
-- N44.1: present1_vertices, present1_treewidth, aes1_treewidth, no_deps_no_edges
-- N44.2: presentCert_width, aesCert_width, keccakChiCert_width, keccak_higher_dp_cost
-- N44.3: presentSecDP_pos, aesSecDP_pos, keccakChiAlgDP_pos, present_dp_cert_consistent
-- N45.1: aes_certified_degree_7, aes_certified_nl_112, aes_circuit_tractable, aes_stronger_diff
-- N45.2: sha3_256_collision_128, chi_is_quadratic, structural_cost_1, keccak_sha3_256_complete
-- N45.3: aes128_delta, aes128_overall_val, aes128_cert_chain, aes128_existing_optimal
-- N45.4: keccak256_verdict_128, keccak256_degree, keccak256_sponge_stronger, keccak256_complete
-- N46.1: present_full_chain, stage3_sound, present_vs_aes, all_ciphers_secure
-- N46.2: thesis_verified, claim1_depth_reduction, claim3_cipher_ordering
-- N46.3: v30_all_gaps_closed, v30_thesis, gap5_end_to_end