Add and enforce specification invariant CommittableIndicesAreKnownSignaturesInv

[eddyashton]

Changes to the spec in #5749 are failing because we store non-signatures in committableIndices.

This adds a new invariant, stating that each node's committableIndices are within that node's log, and signatures, and updates the NoConflictAppendEntriesRequest action so that this invariant holds. Previously the action was appending all new log entries to committableIndices, now it only appends the signatures.

[achamayou]

I'd be tempted to s/KnownSignatures/Signatures/ because it lightly implies the existence of unknown signatures?

Anyway, this is a good fix!

[eddyashton]

I'd be tempted to s/KnownSignatures/Signatures/ because it lightly implies the existence of unknown signatures?

Anyway, this is a good fix!

I use "Known" here for "in my log", where "unknown signatures" would be unknown as signatures by "me". Trying to make the invariant name precise, describing the 2 properties that are checked.

[achamayou]

@eddyashton that does make sense!

[ghost]

add_committable_indices_are_sigs_tla_invariant@77685 aka 20231024.17 vs main ewma over 20 builds from 77015 to 77665

Click to see table

main

build_id	build_number	pi_basic_mt_virtual_cft^	Commit latency factor	tpcc_sgx_cft^	tpcc_sgx_cft_mem	ls_sgx_cft^	ls_sgx_cft_mem	pi_ls_sgx_cft^	pi_ls_sgx_cft_mem	pi_basic_sgx_cft^	pi_basic_sgx_cft_mem	pi_basic_mt_sgx_cft^	pi_basic_mt_sgx_cft_mem	pi_basic_js_sgx_cft^	pi_basic_js_sgx_cft_mem	tpcc_virtual_cft^	ls_jwt_sgx_cft^	ls_jwt_sgx_cft_mem	pi_ls_jwt_sgx_cft^	pi_ls_jwt_sgx_cft_mem	ls_virtual_cft^	pi_ls_virtual_cft^	ls_js_sgx_cft^	ls_js_sgx_cft_mem	pi_basic_virtual_cft^	pi_basic_js_virtual_cft^	ls_full_js_sgx_cft^	ls_full_js_sgx_cft_mem	ls_jwt_virtual_cft^	pi_ls_jwt_virtual_cft^	ls_js_jwt_sgx_cft^	ls_js_jwt_sgx_cft_mem	ls_js_virtual_cft^	ls_full_js_virtual_cft^	ls_js_jwt_virtual_cft^	hist_sgx_cft^	RB put (/s)^	CHAMP put (/s)^	RB get (/s)^	CHAMP get (/s)^
77015	20231010.4	62049.7	0.83228	5592.78	8.59996e+07	14023.3	1.88908e+07	14107	1.05021e+07	15597.5	1.25993e+07	27777.8	2.30851e+07	1436	1.25993e+07	17372.9	6898.77	1.88908e+07	7117.8	6.30784e+06	45785.1	48171.9	5804.14	1.67936e+07	53651.8	4441.2	5786.43	1.67936e+07	17407.2	19739.4	4016.78	1.67936e+07	17105.5	16857.9	9954.93	41221.6	825345	1.18742e+06	8.12844e+06	3.06711e+07
77052	20231010.17	87071.8	0.805827	5614.03	8.59996e+07	14004.1	1.88908e+07	14072.2	1.05021e+07	15532.7	1.25993e+07	27851.7	2.51822e+07	1434.8	1.25993e+07	17123.9	6879.16	1.88908e+07	6931.4	6.30784e+06	45707.2	48521.1	5811.67	1.67936e+07	53548.8	4435.4	5725.25	1.88908e+07	17238.9	19725.4	3978.87	1.67936e+07	17064.9	16932.1	9900.42	39661.9	835356	1.17508e+06	8.12795e+06	3.02453e+07
77065	20231010.21	76791.9	0.805254	5593.79	8.59996e+07	13984.2	1.88908e+07	14076.6	1.05021e+07	15457.8	1.46964e+07	27866.2	2.51822e+07	1431.7	1.25993e+07	17453.5	6839.77	1.67936e+07	6882.8	6.30784e+06	45981.3	47639.7	5802.59	1.67936e+07	53782.5	4471.3	5713.9	1.67936e+07	17159.7	19727	3982.91	1.67936e+07	17221.9	16835.2	9888.21	47354.4	831464	1.17023e+06	8.14609e+06	3.06028e+07
77080	20231011.6	77100.4	0.805739	5614.98	8.59996e+07	14016.4	1.67936e+07	14058.7	1.05021e+07	15607.1	1.25993e+07	28231.3	2.30851e+07	1435.6	1.25993e+07	17356.8	6865.39	1.88908e+07	6917	6.30784e+06	45541.3	47443.3	5768.86	1.67936e+07	53459.3	4480.6	5749.11	1.67936e+07	17192.9	19626.7	3974.5	1.67936e+07	16932.3	16704.5	9841.59	44338.6	839572	1.1863e+06	8.14557e+06	3.07489e+07
77087	20231011.8	83135	0.821071	5620.28	8.59996e+07	14043.4	1.88908e+07	14129.4	1.05021e+07	15619	1.46964e+07	27891.2	2.51822e+07	1427.7	1.25993e+07	17648.9	6872.29	1.67936e+07	7079.7	6.30784e+06	45716.6	48214.1	5780.82	1.67936e+07	53475.5	4431.6	5765.08	1.67936e+07	17316.9	19004.2	3974.44	1.67936e+07	17758.2	16880.7	9849.81	40652.5	827510	1.16961e+06	8.14036e+06	3.30899e+07
77124	20231011.20	81677.3	0.810686	5576.3	8.59996e+07	13934.9	1.88908e+07	14029.2	1.05021e+07	15421.8	1.25993e+07	27859.9	2.51822e+07	1419.9	1.25993e+07	17272.2	6782.48	1.67936e+07	7028.9	6.30784e+06	45763.1	48479	5759.88	1.67936e+07	54961.6	4431	5495.58	1.88908e+07	17497.2	19917.1	3980.45	1.67936e+07	17216.9	16806.9	9875.23	42920	829281	1.17704e+06	8.02253e+06	3.09324e+07
77138	20231011.24	79701.7	0.817166	5505.15	8.59996e+07	13944.3	1.88908e+07	14007.9	1.05021e+07	15414.3	1.46964e+07	27788.7	2.51822e+07	1420.9	1.25993e+07	17450.2	6826.31	1.88908e+07	6933.7	6.30784e+06	43714.5	47439	5805.03	1.67936e+07	54645.3	4386.8	5491.25	1.67936e+07	16999.7	19561.8	3992.65	1.67936e+07	17388.6	14746.3	9915	39122	838714	1.18152e+06	8.09934e+06	3.09754e+07
77148	20231012.2	88890.3	0.806977	5622.22	8.59996e+07	14012.7	1.88908e+07	14136.8	1.05021e+07	15607.9	1.25993e+07	28066.3	2.51822e+07	1437.4	1.25993e+07	17218.1	6885.22	1.88908e+07	6981.9	6.30784e+06	46048.4	48655.6	5813.57	1.67936e+07	55217	4449.2	5723.57	1.88908e+07	17077.4	19720.8	4000.45	1.67936e+07	17064.5	15135.1	9799.03	45326.3	828634	1.17897e+06	8.14758e+06	3.07383e+07
77236	20231016.5	59377	0.79596	5620.83	8.59996e+07	13995.4	1.88908e+07	14108.1	1.05021e+07	15609.7	1.46964e+07	27858.7	2.51822e+07	1442	1.25993e+07	17148.6	6827.74	1.67936e+07	7065.1	6.30784e+06	45783.9	48719.4	5817.83	1.67936e+07	54902.8	4441	5743.02	1.67936e+07	17077.1	18804.1	4006.32	1.67936e+07	17198.3	15291.6	9993.77	44154.4	838342	1.17813e+06	8.15154e+06	3.18804e+07
77284	20231016.20	76928.2	0.800376	5523.42	8.59996e+07	13858.5	1.88908e+07	14093.4	1.05021e+07	15419	1.46964e+07	27801.1	2.30851e+07	1423.4	1.05021e+07	17222.7	6815.4	1.88908e+07	6872.8	6.30784e+06	45566.9	48808.1	5802.5	1.67936e+07	54701.8	4442.5	5472.72	1.67936e+07	17018.1	19157.5	3973.37	1.67936e+07	17650.8	14639.8	9852.83	43502.1	833609	1.17767e+06	8.15537e+06	3.06513e+07
77294	20231016.23	84572	0.822085	5504.43	8.59996e+07	14028.1	1.88908e+07	14087.6	1.05021e+07	15527	1.46964e+07	27413.6	2.51822e+07	1420.2	1.05021e+07	17297.3	6819.85	1.88908e+07	6931.4	6.30784e+06	45995.1	48594.2	5754.38	1.67936e+07	53897	4439.9	5710.32	1.67936e+07	17262.3	19125.2	3992.44	1.67936e+07	17406.6	14896.4	9812.12	41300	823461	1.17985e+06	8.1493e+06	3.05375e+07
77306	20231017.4	60982.9	0.806546	5649.91	8.59996e+07	13997.7	1.88908e+07	14120.3	1.05021e+07	15513.7	1.46964e+07	27907.4	2.30851e+07	1427.4	1.25993e+07	17275.1	6895.99	1.67936e+07	6972.2	6.30784e+06	46102.1	47686.9	5811.89	1.67936e+07	53983.1	4424.7	5778.4	1.67936e+07	17066.2	19713	4010.44	1.67936e+07	14599.9	14833.6	9890.99	45776.1	832093	1.181e+06	8.15615e+06	3.10764e+07
77410	20231019.5	89839.8	0.79845	5633.52	8.59996e+07	14034.4	1.88908e+07	14172.6	1.05021e+07	15641.4	1.25993e+07	27911.2	2.30851e+07	1439.9	1.25993e+07	17335.1	6838.11	1.67936e+07	7046.5	6.30784e+06	43709	47970.1	5772.37	1.67936e+07	54598	4449.7	5751.39	1.67936e+07	17103.2	19628.2	4007.97	1.67936e+07	14821.2	14920.8	9802.6	42755.2	840034	1.18128e+06	8.17441e+06	3.06839e+07
77459	20231020.5	83682.7	0.806882	5609.6	8.59996e+07	14027.3	1.88908e+07	14086.4	1.05021e+07	15436.7	1.46964e+07	27942.3	2.51822e+07	1431.9	1.25993e+07	17271.7	6873.38	1.88908e+07	6974.5	6.30784e+06	45556.9	48282.6	5805.89	1.67936e+07	53165.7	4426.2	5491.04	1.67936e+07	17066.3	17662.5	3972.9	1.67936e+07	16990.3	14844.7	9889.88	42113.3	830635	1.18094e+06	8.16668e+06	3.0923e+07
77461	20231020.6	86522.6	0.797578	5645.01	8.59996e+07	13956.1	1.88908e+07	14152	1.05021e+07	15499.4	1.46964e+07	27968.8	2.30851e+07	1437.7	1.25993e+07	17246.7	7235.96	1.67936e+07	7078.7	6.30784e+06	45887.8	48453.6	5801.29	1.67936e+07	54176.2	4426.2	5742.38	1.67936e+07	17079.1	19435.2	3995.17	1.67936e+07	15003.7	14699.8	9770.09	43030.2	825201	1.1798e+06	8.16489e+06	3.14443e+07
77485	20231020.14	67488.2	0.827982	5614.45	8.59996e+07	14042.3	1.67936e+07	14155.3	1.05021e+07	15587	1.46964e+07	27955.5	2.51822e+07	1441.5	1.25993e+07	17203.3	7220.81	1.67936e+07	6925.4	6.30784e+06	45720.2	47505.9	5824.33	1.67936e+07	52771.4	4441	5745.31	1.67936e+07	17168.5	19652.2	3980.22	1.67936e+07	16950.7	14720	9771.33	46913.9	831368	1.1798e+06	8.12782e+06	3.08955e+07
77532	20231020.31	60943.5	0.835073	5614.22	8.59996e+07	14001.1	1.88908e+07	14174.9	1.05021e+07	15520.9	1.46964e+07	27967.5	2.51822e+07	1429.6	1.25993e+07	17092.6	7252.76	1.67936e+07	7086.5	6.30784e+06	43713.6	47796.6	5806.4	1.67936e+07	52609.1	4332.3	5491.29	1.67936e+07	17195.4	19336.7	4001.82	1.67936e+07	17022.6	14750.8	10188.5	40351.5	833120	1.18235e+06	8.17343e+06	3.12829e+07
77555	20231023.5	74767.3	0.816011	5639.66	8.59996e+07	14029.3	1.88908e+07	14118.1	1.05021e+07	15640.2	1.46964e+07	28238.2	2.51822e+07	1432.7	1.25993e+07	17264.2	7273.33	1.67936e+07	6953.5	6.30784e+06	45924.9	47674	5781.01	1.67936e+07	53843.3	4365.2	5742.5	1.67936e+07	17152.3	19152.3	3995.51	1.67936e+07	17286.3	14910.6	10169.6	43068.6	829052	1.18151e+06	8.148e+06	3.09408e+07
77584	20231023.15	63643	0.839543	5525.06	8.59996e+07	13936	1.88908e+07	13990.4	1.05021e+07	15424.6	1.46964e+07	27775.2	2.51822e+07	1427	1.25993e+07	17237.3	6853.5	1.88908e+07	6881.2	6.30784e+06	43785.4	47940.2	5758.93	1.67936e+07	54114.3	4430	5762.09	1.67936e+07	17010.7	19396.4	3983.52	1.67936e+07	17307.2	14810.6	9823.55	42679.4	825381	1.18095e+06	8.16893e+06	3.13159e+07
77665	20231024.10	71956.1	0.782853	5565	8.59996e+07	13918.6	1.88908e+07	14015.8	1.05021e+07	15439.4	1.46964e+07	28077.5	2.30851e+07	1417.5	1.25993e+07	17332.4	6827.52	1.88908e+07	6933.8	6.30784e+06	43627.5	47460.4	5759.87	1.67936e+07	55764.1	4480.7	5778.73	1.67936e+07	16984.5	19600.5	3994.77	1.67936e+07	17210.4	15032.4	9934.79	42277.7	837727	1.17659e+06	8.1335e+06	3.08424e+07

add_committable_indices_are_sigs_tla_invariant

build_id	build_number	Commit latency factor	pi_basic_mt_virtual_cft^	tpcc_sgx_cft^	tpcc_sgx_cft_mem	tpcc_virtual_cft^	ls_sgx_cft^	ls_sgx_cft_mem	ls_virtual_cft^	pi_ls_sgx_cft^	pi_ls_sgx_cft_mem	pi_ls_virtual_cft^	pi_basic_sgx_cft^	pi_basic_sgx_cft_mem	pi_basic_virtual_cft^	pi_basic_mt_sgx_cft^	pi_basic_mt_sgx_cft_mem	pi_basic_js_virtual_cft^	ls_jwt_virtual_cft^	pi_ls_jwt_virtual_cft^	ls_js_virtual_cft^	pi_basic_js_sgx_cft^	pi_basic_js_sgx_cft_mem	ls_full_js_virtual_cft^	ls_jwt_sgx_cft^	ls_jwt_sgx_cft_mem	ls_js_jwt_virtual_cft^	pi_ls_jwt_sgx_cft^	pi_ls_jwt_sgx_cft_mem	ls_js_sgx_cft^	ls_js_sgx_cft_mem	ls_full_js_sgx_cft^	ls_full_js_sgx_cft_mem	hist_sgx_cft^	ls_js_jwt_sgx_cft^	ls_js_jwt_sgx_cft_mem	RB put (/s)^	CHAMP put (/s)^	RB get (/s)^	CHAMP get (/s)^
77659	20231024.7	0.779613	73770.9	5627.56	8.59996e+07	17244.3	14051.1	1.88908e+07	43654.3	14102.4	1.05021e+07	47340.2	15644.5	1.46964e+07	56207.6	27937.8	2.51822e+07	4483.9	17045.9	19146.5	16939.2	1443.2	1.25993e+07	14582.6	6878.37	1.88908e+07	9926.41	6921	6.30784e+06	5810.37	1.67936e+07	5779.8	1.67936e+07	43499.7	3996.14	1.67936e+07	824747	1.17917e+06	8.13399e+06	3.1012e+07
77685	20231024.17	0.782702	71956.4	5591.3	8.59996e+07	17122.2	13971.1	1.88908e+07	43549.1	14084	1.05021e+07	46892.7	15588.1	1.46964e+07	55003.9	27999.7	2.30851e+07	4372	16933.2	19437.1	17593.4	1438.6	1.25993e+07	14885.8	6822.59	1.67936e+07	9948.84	6930.5	6.30784e+06	5802.77	1.67936e+07	5446.62	1.67936e+07	42634.3	3963.73	1.67936e+07	836416	1.18258e+06	8.17177e+06	3.07152e+07