candidate onlypasspasssoftplus_logsumexprecommend_protected_loweringno public savings claim

softplus_pair_v0

Small log-sum-exp style expression for EML IR packet-builder intake.

DAG nodes

6

Replay frames

8

Reused nodes

0

Internal DAG delta

0

Obligation cards

3

Domain requirements

1

Checked witnesses

1

Blocked claims

7

Expression

ln(exp(a) + exp(b))

ab

Guard Lens

recommend_protected_loweringlogaddexp-style protected loweringdepth 3

Log-sum-exp/softplus shape should lower to protected runtime code.

matched rules

lower_logaddexp_softplus_v0require_positive_log_domain_guard_v0

blocked claims

general EML superiorityruntime performance

Tree vs DAG Boundary

Public tree SuperBEST baseline

5

Internal DAG SuperBEST candidate

5

Public tree EML baseline

16

Internal DAG EML candidate

16

Generated EML packet is candidate-only. DAG savings are internal evidence, not a public savings claim.

Inputs

Input	Unit	Range
a	dimensionless	-10 .. 10
b	dimensionless	-10 .. 10

Shared DAG Nodes

Node	Kind	Op	Reuse	Source
n0	input	input	1	a
n1	operation	exp	1	exp(n0)
n2	input	input	1	b
n3	operation	exp	1	exp(n2)
n4	operation	add	1	add(n1, n3)
n5	operation	ln	1	ln(n4)

Replay Frames

Tick	State	Kernel	Guard	Reason	Hash
0	INIT	eml_ir_loader	ANNOTATE	program accepted by local parser	sha256:cdf131e35fffc296d0031b13b4ce3f8179637f1df507a1a5778acbb6d038a0b8
1	READY	eml_ir_dag	ANNOTATE	DAG nodes assigned stable ids	sha256:0a764c1cf3b6bfe453f662c6b13b441b0beefef210bbafe90f79597fa384bf62
2	RUNNING	exp	PASS	static expression node	sha256:73ead8ad19ac8c8ec293ae4eed46b76457106eb04b38e2571e1d87522b60e4f7
3	RUNNING	exp	PASS	static expression node	sha256:13948f36b262498f2e58b320600884485254a896ea633e7db9dab9096dd94014
4	RUNNING	add	PASS	static expression node	sha256:f2a23e4b0e318a47d47db64f554556ffc087ff093768fd7baf50646f5c8826cb
5	RUNNING	ln	PASS	static expression node	sha256:6881a09b42daeb8dd792e7f56e3abb454681866f6da22ca4ca942445cea7c4ca
6	END	eml_ir_runtime	ANNOTATE	output node n5 reached	sha256:43779a41ec6e69fe38285a77c05ccbb3d13c5802eb1a752ad051d3a0ecaa3f8e
7	PARKED	eml_ir_runtime	ANNOTATE	explicit replay terminal boundary	sha256:51c1be1e26bd80410f1ebb3f676844d6f3c69198d78fe3fabfd1e675e5592a8b

Domain Safety Lens

Unresolved obligations

2

Checked witnesses

1

Safe rewrite candidates

3

Proved by lens

1

lnchecked_small_witness

argument_positive

log argument may be nonpositive

MachLib.Real.softplus_pair_log_argument_positive

For all a b, exp(a) is positive and exp(b) is positive, so exp(a) + exp(b) is positive.

Introduce log-domain lift, positivity guard, or range proof.

rangedeclared_unverified

a: -10 .. 10

declared range is not runtime, hardware, or proof evidence

Attach runtime guard, sampled replay evidence, or MachLib range proof before promotion.

rangedeclared_unverified

b: -10 .. 10

declared range is not runtime, hardware, or proof evidence

Attach runtime guard, sampled replay evidence, or MachLib range proof before promotion.

Blocked public claims

certified_safety_claimformal_verification_claimhardware_observedproduction_controller_claimpublic_savings_claimrange_safety_proved_claimtheorem_proof_claim

rewrite proposalcandidate_no_compiler_change

Mark this argument_positive guard as proof-backed in review surfaces.

Do not change compiler lowering or public savings claims from this witness alone.

Obligation Cards

domainchecked_small_witnessln

log_argument_positive

Log node requires evidence that its argument is positive over declared inputs/ranges.

softplus_pair_v0:domain:n5:ln-argument-positiveMachLib.Real.softplus_pair_log_argument_positive

For all a b, exp(a) is positive and exp(b) is positive, so exp(a) + exp(b) is positive.

This checked witness discharges one local log-argument positivity obligation; it is not complete EML safety, compiler correctness, or a public savings claim.

range_safetycandidate_onlysafe_range

input_range_respected

Input a declares range [-10.0, 10.0]; downstream runtime or proof work must preserve this boundary.

softplus_pair_v0:range:a:declared-safe-range

This card records a declared range boundary; it is not hardware evidence or a certified safety proof.

range_safetycandidate_onlysafe_range

input_range_respected

Input b declares range [-10.0, 10.0]; downstream runtime or proof work must preserve this boundary.

softplus_pair_v0:range:b:declared-safe-range

This card records a declared range boundary; it is not hardware evidence or a certified safety proof.

Non-Claims

certified_safety_claim

false

compiler_behavior_changed

false

forge_behavior_changed

false

formal_verification_claim

false

hardware_observed

false

live_serial_capture_performed

false

production_controller_claim

false

public_ready

false

public_savings_claim

false

theorem_proof_claim

false