Helper

dsdp_traces_ok

File dumas2017dual/dsdp/dsdp_correctness.v

Section dsdp_computational

Type Lemma

Proof Lines 1

Signature

Lemma dsdp_traces_ok : dsdp_traces = [tuple [bseq d (v3 * u3 + r3 + (v2 * u2 + r2) - r2 - r3 + u1 * v1); e (v3 * u3 + r3 + (v2 * u2 + r2)); e v3; e v2; d r3; d r2; d u3; d u2; d u1; d v1; k dk_a]; [bseq e (v3 * u3 + r3); e (v2 * u2 + r2); d v2; k dk_b]; [bseq e (v3 * u3 + r3 + (v2 * u2 + r2)); d v3; k dk_c]].

Description

Trace structure: each party's trace contains their view of the protocol.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats